c launch: /data/cnf/sc2014/app/q_query_3_L90_coli.sat.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/q_query_3_L90_coli.sat.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/q_query_3_L90_coli.sat.cnf.bz2
c no embedded options
c found 'p cnf 282842 1350458' header
c read 282842 variables, 1350458 clauses, 3903824 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 243248 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  243248  1268704         0       0      0     0    0     0   98   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 2389 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2389 out of 2389 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 99068 variables
c [simpleprobe-1] all 183774 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 17603 variables
c [simpleprobe-1] 141586 variables remain 85% (24585 retained 15%)
c [simpleprobe-1] removed 17603 variables, found 10618 hbrs, 68 units
c [unhide-1] limit 52218 based on 835497 irredundant clauses
c [unhide-1-1] 88 units, 130 failed, 58 tauts, 0 hbrs, 223 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 165810 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 93991 not tried 57% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 71831 = 43% variables out of 165810 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 610926 negative 97.2% of 628528 except 17602 2.8%
c [phase-count-1] 485472 positive 77.2% of 628528 except 143056 22.8%
c [phase-count-1] less non-negative clauses 17602 than limit 62800 (10.0%)
c [phase-count-1] non-pos/non-neg = 143056/17602 = 8.13 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 93979 negative 100%
c [sort-queue-1] sorted 93979 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 93979 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 126206 variables 57.3% (93979 remain 39%)
c [simplification-1] removed 640176 irredundant clauses 50.5% (628528 remain 50%)
c [simplification-1] maximum reduction of 57% = max (57%, 50%)
c [simplification-1] large reduction 57% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.4   93978   628528         1       0      0   133    0     0   51   0%      0    0    0    0    0%
c i    3.4   93643   628528        15      10      2   134    0     1   51   3%      0    1    1    0 24981%
c i    3.4   93642   628528        47      32      5   140    0     2   51   4%      0    2    1    0 22942%
c i    3.4   93641   628528        76      52     11   141    0     2   51   5%      0    2    1    0 21769%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 4629 variables
c [simpleprobe-2] 76377 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 81 variables
c [simpleprobe-2] 76420 variables remain 86% (12849 retained 14%)
c [simpleprobe-2] removed 81 variables, found 4799 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 29718 literals 17%
c [treelook-1] scheduling used 300063 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 307487 steps
c [treelook-1] 29588 literals remain 17%
c [treelook-1] 28592 variables remain to probed next time 32%
c [decomp-5] removed 41 variables
c [treelook-1] removed 45 variables, found 1302 hbrs
c [basicprobe-1] limit 4496168 based on 562021 irredundant clauses
c [basicprobe-1-0] 38751 probes remain 44% after last round
c [basicprobe-1-0] 261 units = 196 failed (75%) + 65 lifted (25%)
c [basicprobe-1-0] removed 661 variables, found 71445 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 13 units, 26 failed, 4440 tauts, 0 hbrs, 394 literals
c [elim-2] 88381 variables 100% will be scheduled this time
c [elim-2] scheduled 88381 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 9407 not tried 11% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 51863 = 59% variables out of 88381 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 350490 negative 98.1% of 357344 except 6854 1.9%
c [phase-count-2] 263745 positive 73.8% of 357344 except 93599 26.2%
c [phase-count-2] less non-negative clauses 6854 than limit 35700 (10.0%)
c [phase-count-2] non-pos/non-neg = 93599/6854 = 13.66 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 10845 negative 100%
c [sort-queue-2] sorted 34572 enqueued variables after 1010 conflicts
c [score-dist-2] active 1946 (5%), one 0 (0%), zero 34572 (95%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 504, avg 504.3
c [simplification-2] removed 57123 variables 61.0% (36518 remain 15%)
c [simplification-2] removed 271184 irredundant clauses 43.1% (357344 remain 28%)
c [simplification-2] maximum reduction of 61% = max (61%, 43%)
c [simplification-2] large reduction 61% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13010 (soft 3010 + delta 10000)
c [simplification-2] new conflict limit 3010 (hard 13010)
c 
c [simplification-3] limit 3010 conflicts (hard 13010) hit after 3010 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2901 at-most-one constraints of average size 3.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 2901 out of 2901 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 102 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 8426 literals 12%
c [treelook-2] scheduling used 300012 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 772769 steps
c [treelook-2] 8412 literals remain 12%
c [treelook-2] 5315 variables remain to probed next time 15%
c [treelook-2] removed 0 variables, found 2963 hbrs
c [unhide-3] limit 105303 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 681 tauts, 0 hbrs, 4889 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 36416 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1793 not tried 5% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 252 = 1% variables out of 36416 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 347003 negative 98.1% of 353771 except 6768 1.9%
c [phase-count-3] 260136 positive 73.5% of 353771 except 93635 26.5%
c [phase-count-3] less non-negative clauses 6768 than limit 35300 (10.0%)
c [phase-count-3] non-pos/non-neg = 93635/6768 = 13.83 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 10661 negative 100%
c [sort-queue-3] sorted 33578 enqueued variables after 3010 conflicts
c [score-dist-3] active 2586 (7%), one 0 (0%), zero 33578 (93%)
c [score-dist-3] max exp 512, different 12 (2%)
c [score-dist-3] median active exp 505, avg 505.2
c [simplification-3] removed 354 variables 1.0% (36164 remain 15%)
c [simplification-3] removed 3571 irredundant clauses 1.0% (353771 remain 28%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23010 (soft 13010 + delta 10000)
c [simplification-3] new conflict limit 13010 (hard 23010)
c 
c [simplification-4] limit 13010 conflicts (hard 23010) hit after 13010 conflicts
c [basicprobe-2] limit 10493016 penalty 0 = 0 + 0
c [basicprobe-2-0] 14483 probes remain 40% after last round
c [basicprobe-2-0] 4 units = 3 failed (75%) + 1 lifted (25%)
c [basicprobe-2-0] removed 4 variables, found 63026 hbrs
c [elim-4] 1793 variables 5% will be scheduled this time
c [elim-4] scheduled 1793 variables 5%
c [elim-4] boosting limit by 20
c [elim-4] limit of 839441280 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 239365245 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 1793 scheduled
c [phase-count-4] 336727 negative 98.0% of 343486 except 6759 2.0%
c [phase-count-4] 249274 positive 72.6% of 343486 except 94212 27.4%
c [phase-count-4] less non-negative clauses 6759 than limit 34300 (10.0%)
c [phase-count-4] non-pos/non-neg = 94212/6759 = 13.94 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 10607 negative 100%
c [sort-queue-4] sorted 33128 enqueued variables after 13010 conflicts
c [score-dist-4] active 3032 (8%), one 0 (0%), zero 33128 (92%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 506, avg 506.5
c [simplification-4] removed 4 variables 0.0% (36160 remain 15%)
c [simplification-4] removed 10273 irredundant clauses 2.9% (343486 remain 27%)
c [simplification-4] maximum reduction of 3% = max (0%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 15000
c [simplification-4] penalized conflict interval 15000 = 1 * 15000
c [simplification-4] hard conflict limit 38010 (soft 28010 + delta 10000)
c [simplification-4] new conflict limit 28010 (hard 38010)
c 
c [simplification-5] limit 28010 conflicts (hard 38010) hit after 28011 conflicts
c [quatres-1] found 12442 quaternary clauses 28% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 63 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3446 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 30264860 with penalty 0 = 0 + 0
c [ternres-1] all 36160 free variables schedulable
c [ternres-1] 4586 ternary resolvents (3 bin, 4583 trn)
c [ternres-1] 15095 variables remain 42% (21065 retained 58%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 41 xors of average arity 3.0
c [gauss-1] connected 122 occurrences of 106 variables (average 1.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2 variables
c [simpleprobe-3] 30399 schedulable variables 84%
c [simpleprobe-3] limit 24211891 penalty 0 = 0 + 0
c [decomp-10] removed 3 variables
c [simpleprobe-3] 18143 variables remain 50% (18012 retained 50%)
c [simpleprobe-3] removed 3 variables, found 5802 hbrs, 2 units
c [unhide-4] limit 605297 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 2 failed, 8363 tauts, 0 hbrs, 24454 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 4055 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 36154 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 605297270 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 14015 blocked clauses
c [cce-1] limit of 30264863 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 12
c [cce-1-1] eliminated 16 clauses out of 119 (13%) of length 11
c [cce-1-1] eliminated 2 clauses out of 8 (25%) of length 10
c [cce-1-1] eliminated 1 clauses out of 173 (1%) of length 9
c [cce-1-1] eliminated 1128 clauses out of 1487 (76%) of length 8
c [cce-1-1] eliminated 427 clauses out of 3614 (12%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1576 large clauses in 30266390 steps
c [cce-1-1] allowing another 15133195 steps for small clauses
c [cce-1-1] scheduling 175850 clauses = 32598 binary + 143252 ternary
c [cce-1-1] tried to eliminate 5823 small clauses 3%
c [cce-1-1] eliminated 318 binary clauses 1%
c [cce-1-1] eliminated 4211 ternary clauses 3%
c [cce-1-1] eliminated 4529 small clauses 3%
c [cce-1-1] eliminated 4529 small clauses in 30264868 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 6105 covered clauses in round 1
c [cce-1] eliminated 6105 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 646278 added (scaled 2)
c [bca-1] 65795 out of 72308 literals actually usable 91%
c [bca-1] added 0 blocked clauses in 169975 steps
c [sweep-1] limit 1815891 penalty 0 = 0 + 0
c [sweep-1-1] 8647 pos 23.9% + 27506 neg 76.1% = 36153 sched 100.0% ret 0
c [sweep-1-1] 1839842 steps 48 queries 7690.65 avg class size
c [sweep-1-1] 1338 decisions 35 SAT calls 216.37 avg env size
c [sweep-1-1] 35891 variables remain 99% (262 retained 1%)
c [decomp-11] removed 16 variables
c [sweep-1-1] removed 16 vars (0 failed, 14 eqs, 23 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 16 vars in TOTAL (1 rounds, 47 queries)
c [phase-count-5] 315875 negative 97.8% of 322874 except 6999 2.2%
c [phase-count-5] 234103 positive 72.5% of 322874 except 88771 27.5%
c [phase-count-5] less non-negative clauses 6999 than limit 32200 (10.0%)
c [phase-count-5] non-pos/non-neg = 88771/6999 = 12.68 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 8655 negative 100%
c [sort-queue-5] sorted 32713 enqueued variables after 28011 conflicts
c [score-dist-5] active 3424 (9%), one 0 (0%), zero 32713 (91%)
c [score-dist-5] max exp 516, different 16 (3%)
c [score-dist-5] median active exp 507, avg 507.0
c [simplification-5] removed 23 variables 0.1% (36137 remain 15%)
c [simplification-5] removed 20612 irredundant clauses 6.0% (322874 remain 25%)
c [simplification-5] maximum reduction of 6% = max (0%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 40011 (soft 30011 + delta 10000)
c [simplification-5] new conflict limit 30011 (hard 40011)
c 
c [simplification-6] limit 30011 conflicts (hard 40011) hit after 30015 conflicts
c [quatres-2] found 15762 quaternary clauses 35% in total
c [quatres-2-1] removed 13 duplicate quaternary clauses
c [quatres-2-1] added 8 double-self-subsuming ternary resolvents
c [quatres-2-2] added 33 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2801 quaternary resolvents
c [ternres-2] limit 6704052 with penalty 0 = 0 + 0
c [ternres-2] 15086 schedulable variables 42%
c [ternres-2] 2115 ternary resolvents (22 bin, 2093 trn)
c [ternres-2] 11998 variables remain 33% (24139 retained 67%)
c [card-3] limit 838006 penalty 2 = 2 + 0
c [card-3] found 274 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 838006 for elimination
c [card-3] 274 out of 274 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-5] limit 1340810 with penalty 0 = 0 + 0
c [unhide-5-6] 0 units, 9 failed, 7043 tauts, 0 hbrs, 21139 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 667 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 36129 variables 100%
c [block-2] limit of 67040527 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 23 blocked clauses
c [block-2] 23 < 1/100 * 319372 = 3193 considered unsuccessful
c [cce-2] limit of 33520263 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 296 clauses out of 3187 (9%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 296 large clauses in 33520267 steps
c [cce-2-1] allowing another 16760133 steps for small clauses
c [cce-2-1] scheduling 170374 clauses = 35115 binary + 135259 ternary
c [cce-2-1] tried to eliminate 3927 small clauses 2%
c [cce-2-1] eliminated 273 binary clauses 1%
c [cce-2-1] eliminated 2303 ternary clauses 2%
c [cce-2-1] eliminated 2576 small clauses 2%
c [cce-2-1] eliminated 2576 small clauses in 33520389 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2872 covered clauses in round 1
c [cce-2] eliminated 2872 covered clauses in TOTAL during 1 rounds
c [cce-2] 2872 < 1/100 * 319335 = 3193 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 36128 variables 100%
c [elim-5] limit of 67040527 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 847 not tried 2% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 264 = 1% variables out of 36128 scheduled
c [elim-5] 264 < 1/100 * 36128 = 361 considered unsuccessful
c [sweep-2] limit 2011215 penalty 0 = 0 + 0
c [sweep-2-1] 9257 pos 26.0% + 26368 neg 74.0% = 35625 sched 99.3% ret 239
c [sweep-2-1] 2028389 steps 31 queries 5160.77 avg class size
c [sweep-2-1] 1084 decisions 30 SAT calls 248.80 avg env size
c [sweep-2-1] 35365 variables remain 99% (496 retained 1%)
c [decomp-13] removed 41 variables
c [sweep-2-1] removed 41 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 41 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-6] 305755 negative 97.8% of 312713 except 6958 2.2%
c [phase-count-6] 223504 positive 71.5% of 312713 except 89209 28.5%
c [phase-count-6] less non-negative clauses 6958 than limit 31200 (10.0%)
c [phase-count-6] non-pos/non-neg = 89209/6958 = 12.82 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 7845 negative 100%
c [sort-queue-6] sorted 31902 enqueued variables after 30015 conflicts
c [score-dist-6] active 3921 (11%), one 0 (0%), zero 31902 (89%)
c [score-dist-6] max exp 516, different 16 (3%)
c [score-dist-6] median active exp 507, avg 507.1
c [simplification-6] removed 314 variables 0.9% (35823 remain 15%)
c [simplification-6] removed 10161 irredundant clauses 3.1% (312713 remain 25%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 20000
c [simplification-6] penalized conflict interval 20000 = 1 * 20000
c [simplification-6] hard conflict limit 60015 (soft 50015 + delta 10000)
c [simplification-6] new conflict limit 50015 (hard 60015)
c 
c [simplification-7] limit 50015 conflicts (hard 60015) hit after 50015 conflicts
c [quatres-3] found 17705 quaternary clauses 37% in total
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 19 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1441 quaternary resolvents
c [ternres-3] limit 12277432 with penalty 0 = 0 + 0
c [ternres-3] 11873 schedulable variables 33%
c [ternres-3] 3385 ternary resolvents (12 bin, 3373 trn)
c [ternres-3] 7730 variables remain 22% (28093 retained 78%)
c [gauss-2] limit 1227743 penalty 1 = 1 + 0
c [gauss-2] extracted 36 xors of average arity 3.0
c [gauss-2] connected 107 occurrences of 92 variables (average 1.2)
c [gauss-2] limit 1227743 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 2 variables
c [treelook-3] limit 613871 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 16263 literals 23%
c [treelook-3] scheduling used 613877 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 613871 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 901405 steps
c [treelook-3] 16129 literals remain 23%
c [treelook-3] 4943 variables remain to probed next time 14%
c [treelook-3] removed 0 variables, found 1463 hbrs
c [unhide-6] limit 2455486 with penalty 0 = 0 + 0
c [unhide-6-8] 0 units, 3 failed, 5982 tauts, 0 hbrs, 102021 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 617 transitive binary clauses
c [bca-2] limit of 10000000 steps and 617868 added (scaled 2)
c [bca-2] 63452 out of 71638 literals actually usable 89%
c [bca-2] added 299 blocked clauses in 182729 steps
c [sweep-3] limit 3683229 penalty 0 = 0 + 0
c [sweep-3-1] 9446 pos 26.7% + 25876 neg 73.3% = 35322 sched 98.6% ret 496
c [sweep-3-1] 3712782 steps 96 queries 6740.01 avg class size
c [sweep-3-1] 1950 decisions 82 SAT calls 114.18 avg env size
c [sweep-3-1] 34463 variables remain 96% (1354 retained 4%)
c [decomp-16] removed 21 variables
c [sweep-3-1] removed 21 vars (0 failed, 15 eqs, 30 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 21 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-7] 301690 negative 97.7% of 308639 except 6949 2.3%
c [phase-count-7] 220195 positive 71.3% of 308639 except 88444 28.7%
c [phase-count-7] less non-negative clauses 6949 than limit 30800 (10.0%)
c [phase-count-7] non-pos/non-neg = 88444/6949 = 12.73 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 6859 negative 100%
c [sort-queue-7] sorted 30618 enqueued variables after 50015 conflicts
c [score-dist-7] active 5179 (14%), one 0 (0%), zero 30618 (86%)
c [score-dist-7] max exp 517, different 17 (3%)
c [score-dist-7] median active exp 508, avg 507.7
c [simplification-7] removed 26 variables 0.1% (35797 remain 15%)
c [simplification-7] removed 4073 irredundant clauses 1.3% (308639 remain 24%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 30000
c [simplification-7] penalized conflict interval 30000 = 1 * 30000
c [simplification-7] hard conflict limit 95015 (soft 80015 + delta 15000)
c [simplification-7] new conflict limit 80015 (hard 95015)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   45.6   35797   308639     67941   34595  21740 52346   15    26   42  60%    655   10   13    8  158%
c 
c [simplification-8] limit 80015 conflicts (hard 95015) hit after 80015 conflicts
c [quatres-4] found 19055 quaternary clauses 39% in total
c [quatres-4-1] removed 62 duplicate quaternary clauses
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 54 single-self-subsuming ternary resolvents
c [quatres-4-2] added 874 quaternary resolvents
c [ternres-4] limit 20323252 with penalty 0 = 0 + 0
c [ternres-4] 7727 schedulable variables 22%
c [ternres-4] 5957 ternary resolvents (25 bin, 5932 trn)
c [ternres-4] 1284 variables remain 4% (34513 retained 96%)
c [basicprobe-3] limit 101616263 penalty 0 = 0 + 0
c [basicprobe-3-0] 5796 probes remain 16% after last round
c [basicprobe-3-0] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 14 variables, found 208501 hbrs
c [bate-1] eliminated 43 asymmetric tautologies during probing
c [unhide-7] limit 4064650 with penalty 0 = 0 + 0
c [unhide-7-11] 0 units, 12 failed, 28570 tauts, 0 hbrs, 82733 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 756 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 35772 variables 100%
c [block-3] limit of 101616263 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 150 blocked clauses
c [block-3] 150 < 1/100 * 306001 = 3060 considered unsuccessful
c [cce-3] limit of 50808131 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 32 clauses out of 37 (86%) of length 12
c [cce-3-1] eliminated 25 clauses out of 118 (21%) of length 11
c [cce-3-1] eliminated 7 clauses out of 97 (7%) of length 10
c [cce-3-1] eliminated 3 clauses out of 201 (1%) of length 9
c [cce-3-1] eliminated 1 clauses out of 197 (1%) of length 8
c [cce-3-1] eliminated 295 clauses out of 3058 (10%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 363 large clauses in 50808132 steps
c [cce-3-1] allowing another 25404066 steps for small clauses
c [cce-3-1] scheduling 138666 clauses = 34365 binary + 104301 ternary
c [cce-3-1] tried to eliminate 5074 small clauses 4%
c [cce-3-1] eliminated 370 binary clauses 1%
c [cce-3-1] eliminated 1370 ternary clauses 1%
c [cce-3-1] eliminated 1740 small clauses 1%
c [cce-3-1] eliminated 1740 small clauses in 50808273 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2103 covered clauses in round 1
c [cce-3] eliminated 2103 covered clauses in TOTAL during 1 rounds
c [cce-3] 2103 < 1/100 * 305851 = 3058 considered unsuccessful
c [bca-3] limit of 10000000 steps and 608145 added (scaled 2)
c [bca-3] 63149 out of 71544 literals actually usable 88%
c [bca-3] added 670 blocked clauses in 180680 steps
c [sweep-4] limit 6096975 penalty 0 = 0 + 0
c [sweep-4-1] 9769 pos 28.4% + 24664 neg 71.6% = 34433 sched 96.3% ret 1338
c [sweep-4-1] 6166055 steps 60 queries 3883.57 avg class size
c [sweep-4-1] 1473 decisions 50 SAT calls 111.26 avg env size
c [sweep-4-1] 33651 variables remain 94% (2119 retained 6%)
c [decomp-18] removed 30 variables
c [sweep-4-1] removed 30 vars (0 failed, 9 eqs, 17 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 30 vars in TOTAL (1 rounds, 59 queries)
c [phase-count-8] 296769 negative 97.7% of 303674 except 6905 2.3%
c [phase-count-8] 216224 positive 71.2% of 303674 except 87450 28.8%
c [phase-count-8] less non-negative clauses 6905 than limit 30300 (10.0%)
c [phase-count-8] non-pos/non-neg = 87450/6905 = 12.66 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 6682 negative 100%
c [sort-queue-8] sorted 29951 enqueued variables after 80015 conflicts
c [score-dist-8] active 5790 (16%), one 0 (0%), zero 29951 (84%)
c [score-dist-8] max exp 517, different 17 (3%)
c [score-dist-8] median active exp 508, avg 508.1
c [simplification-8] removed 56 variables 0.2% (35741 remain 15%)
c [simplification-8] removed 4965 irredundant clauses 1.6% (303674 remain 24%)
c [simplification-8] maximum reduction of 2% = max (0%, 2%)
c [simplification-8] geometric conflict interval increment 10000 = 30000 / 3
c [simplification-8] new conflict interval 40000
c [simplification-8] penalized conflict interval 40000 = 1 * 40000
c [simplification-8] hard conflict limit 140015 (soft 120015 + delta 20000)
c [simplification-8] new conflict limit 120015 (hard 140015)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   70.1   35741   303674    101006   37349  28846 211865   13    17   45  77%    801   -1   12   11  114%
c 
c [simplification-9] limit 120015 conflicts (hard 140015) hit after 127949 conflicts
c [quatres-5] found 19751 quaternary clauses 39% in total
c [quatres-5-1] removed 35 duplicate quaternary clauses
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 62 single-self-subsuming ternary resolvents
c [quatres-5-2] added 572 quaternary resolvents
c [ternres-5] limit 39789107 with penalty 0 = 0 + 0
c [ternres-5] 1280 schedulable variables 4%
c [ternres-5] 7914 ternary resolvents (63 bin, 7851 trn)
c [ternres-5] 121 variables remain 0% (35620 retained 100%)
c [decomp-19] removed 3 variables
c [simpleprobe-4] 17923 schedulable variables 50%
c [simpleprobe-4] limit 159156429 penalty 0 = 0 + 0
c [decomp-20] removed 34 variables
c [simpleprobe-4] 613 variables remain 2% (35091 retained 98%)
c [simpleprobe-4] removed 34 variables, found 38353 hbrs, 7 units
c [unhide-8] limit 7957821 with penalty 0 = 0 + 0
c [unhide-8-15] 0 units, 5 failed, 41612 tauts, 0 hbrs, 71903 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 556 transitive binary clauses
c [elim-6] 844 variables 2% will be scheduled this time
c [elim-6] scheduled 844 variables 2%
c [elim-6] limit of 198945536 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 144278079 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 844 scheduled
c [bca-4] limit of 10000000 steps and 605280 added (scaled 2)
c [bca-4] 63065 out of 71402 literals actually usable 88%
c [bca-4] added 1095 blocked clauses in 192381 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 119367320 penalty 0 = 0 + 0
c [sweep-5-1] 9763 pos 29.1% + 23832 neg 70.9% = 33595 sched 94.1% ret 2105
c [sweep-5-1] 119386902 steps 1360 queries 925.21 avg class size
c [sweep-5-1] 13399 decisions 1098 SAT calls 46.86 avg env size
c [sweep-5-1] 20559 variables remain 58% (15130 retained 42%)
c [decomp-21] removed 333 variables
c [sweep-5-1] removed 333 vars (0 failed, 289 eqs, 556 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 333 vars in TOTAL (1 rounds, 1359 queries)
c [phase-count-9] 294145 negative 97.7% of 300973 except 6828 2.3%
c [phase-count-9] 212831 positive 70.7% of 300973 except 88142 29.3%
c [phase-count-9] less non-negative clauses 6828 than limit 30000 (10.0%)
c [phase-count-9] non-pos/non-neg = 88142/6828 = 12.91 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 3069 negative 100%
c [sort-queue-9] sorted 23804 enqueued variables after 127949 conflicts
c [score-dist-9] active 11563 (33%), one 0 (0%), zero 23804 (67%)
c [score-dist-9] max exp 518, different 18 (3%)
c [score-dist-9] median active exp 504, avg 505.8
c [simplification-9] removed 374 variables 1.0% (35367 remain 15%)
c [simplification-9] removed 2701 irredundant clauses 0.9% (300973 remain 24%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 20000 = 40000 / 2
c [simplification-9] new conflict interval 60000
c [simplification-9] penalized conflict interval 60000 = 1 * 60000
c [simplification-9] hard conflict limit 217949 (soft 187949 + delta 30000)
c [simplification-9] new conflict limit 187949 (hard 217949)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   95.3   35367   300973    136328   39680  33619 243544   15    22   47  71%    894    5   15   11  133%
c -  111.5   35367   300973    172248   39403  33632 243546    9    16   47  58%    949   -2   10   12   80%
c -  127.0   35367   300973    208862   41513  33650 243548   10    14   47  74%    981   -3    8   11   75%
c 
c [simplification-10] limit 187949 conflicts (hard 217949) hit after 217953 conflicts
c [quatres-6] found 20040 quaternary clauses 38% in total
c [quatres-6-1] removed 954 duplicate quaternary clauses
c [quatres-6-2] added 91 single-self-subsuming ternary resolvents
c [quatres-6-2] added 181 quaternary resolvents
c [ternres-6] limit 77760592 with penalty 0 = 0 + 0
c [ternres-6] 116 schedulable variables 0%
c [ternres-6] 5668 ternary resolvents (97 bin, 5571 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 4860037 penalty 3 = 3 + 0
c [card-4] found 489 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 4860037 for elimination
c [card-4] 489 out of 489 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3888029 penalty 2 = 2 + 0
c [gauss-3] extracted 142 xors of average arity 3.0
c [gauss-3] connected 420 occurrences of 175 variables (average 2.4)
c [gauss-3] limit 3888029 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 19 variables
c [unhide-9] limit 15552118 with penalty 0 = 0 + 0
c [unhide-9-24] 25 units, 74 failed, 56030 tauts, 0 hbrs, 142446 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 571 transitive binary clauses
c [bca-5] limit of 10000000 steps and 596674 added (scaled 2)
c [bca-5] 61681 out of 70544 literals actually usable 87%
c [bca-5] added 871 blocked clauses in 176425 steps
c [sweep-6] limit 23328177 penalty 0 = 0 + 0
c [sweep-6-1] 5780 pos 28.2% + 14708 neg 71.8% = 20488 sched 58.1% ret 14783
c [sweep-6-1] 23412210 steps 1267 queries 2225.65 avg class size
c [sweep-6-1] 8229 decisions 864 SAT calls 26.40 avg env size
c [sweep-6-1] 15278 variables remain 43% (19974 retained 57%)
c [decomp-23] removed 500 variables
c [sweep-6-1] removed 500 vars (0 failed, 413 eqs, 809 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 500 vars in TOTAL (1 rounds, 1266 queries)
c [phase-count-10] 290279 negative 97.7% of 297037 except 6758 2.3%
c [phase-count-10] 210024 positive 70.7% of 297037 except 87013 29.3%
c [phase-count-10] less non-negative clauses 6758 than limit 29700 (10.0%)
c [phase-count-10] non-pos/non-neg = 87013/6758 = 12.88 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 1033 negative 100%
c [sort-queue-10] sorted 22027 enqueued variables after 217953 conflicts
c [score-dist-10] active 12744 (37%), one 0 (0%), zero 22027 (63%)
c [score-dist-10] max exp 519, different 19 (4%)
c [score-dist-10] median active exp 504, avg 506.0
c [simplification-10] removed 596 variables 1.7% (34771 remain 14%)
c [simplification-10] removed 3936 irredundant clauses 1.3% (297037 remain 23%)
c [simplification-10] maximum reduction of 2% = max (2%, 1%)
c [simplification-10] geometric conflict interval increment 20000 = 60000 / 3
c [simplification-10] new conflict interval 80000
c [simplification-10] penalized conflict interval 80000 = 1 * 80000
c [simplification-10] hard conflict limit 337953 (soft 297953 + delta 40000)
c [simplification-10] new conflict limit 297953 (hard 337953)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  137.5   34770   297037    217982   48663  35538 190569    9    14   48  66%    987   -2    9   11   79%
c -  150.2   34770   297037    247008   42070  35556 190572    8    11   45  77%  -1221   -4    7   10   70%
c i  155.4   34769   297037    258272   50183  35609 190585    8    10   48  78%   -867   -5    6   10   57%
c -  166.8   34765   297037    283159   44681  35634 190588   13    31   46  41%   -707   12   12   11  106%
c -  181.9   34765   297031    315069   45710  35662 190592   13    32   46  42%    -40    6   13   12  111%
c 
c [simplification-11] limit 297953 conflicts (hard 337953) hit after 317554 conflicts
c [quatres-7] found 18654 quaternary clauses 36% in total
c [quatres-7-1] removed 2364 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 83 single-self-subsuming ternary resolvents
c [quatres-7-2] added 90 quaternary resolvents
c [ternres-7] limit 110950337 with penalty 0 = 0 + 0
c [ternres-7] all 34765 free variables schedulable
c [ternres-7] 4637 ternary resolvents (86 bin, 4551 trn)
c [ternres-7] 38 variables remain 0% (34727 retained 100%)
c [decomp-24] removed 7 variables
c [unhide-10] limit 20000000 with penalty 0 = 0 + 0
c [unhide-10-37] 5 units, 90 failed, 40873 tauts, 0 hbrs, 223091 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 458 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 34688 variables 100%
c [block-4] limit of 200000000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 134 blocked clauses
c [block-4] 134 < 1/100 * 293494 = 2934 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 1386879222 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 2 clauses out of 135 (1%) of length 8
c [cce-4-1] eliminated 370 clauses out of 2082 (18%) of length 7
c [cce-4-1] eliminated 5219 clauses out of 14242 (37%) of length 6
c [cce-4-1] eliminated 745 clauses out of 8526 (9%) of length 5
c [cce-4-1] eliminated 1326 clauses out of 9149 (14%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 7662 large clauses in 199071574 steps
c [cce-4-1] allowing another 99535787 steps for small clauses
c [cce-4-1] scheduling 162361 clauses = 35255 binary + 127106 ternary
c [cce-4-1] tried to eliminate 162361 small clauses 100%
c [cce-4-1] eliminated 6015 binary clauses 17%
c [cce-4-1] eliminated 43659 ternary clauses 34%
c [cce-4-1] eliminated 49674 small clauses 31%
c [cce-4-1] eliminated 49674 small clauses in 634434263 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 57336 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 28861786 steps for small clauses
c [cce-4-2] scheduling 112690 clauses = 29240 binary + 83450 ternary
c [cce-4-2] tried to eliminate 112690 small clauses 100%
c [cce-4-2] eliminated 3 ternary clauses 0%
c [cce-4-2] eliminated 3 small clauses 0%
c [cce-4-2] eliminated 3 small clauses in 244753124 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 3 covered clauses in round 2
c [cce-4-3] completed large round (ATE)
c [cce-4-3] allowing another 28854340 steps for small clauses
c [cce-4-3] scheduling 112689 clauses = 29240 binary + 83449 ternary
c [cce-4-3] tried to eliminate 112689 small clauses 100%
c [cce-4-3] eliminated 1 ternary clauses 0%
c [cce-4-3] eliminated 1 small clauses 0%
c [cce-4-3] eliminated 1 small clauses in 244761523 steps
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 1 covered clauses in round 3
c [cce-4] eliminated 57340 covered clauses in TOTAL during 3 rounds
c [bca-6] limit of 10000000 steps and 473959 added (scaled 2)
c [bca-6] 58183 out of 69366 literals actually usable 84%
c [bca-6] added 806 blocked clauses in 154493 steps
c [sweep-7] limit 33285101 penalty 0 = 0 + 0
c [sweep-7-1] 7516 pos 49.3% + 7739 neg 50.7% = 15255 sched 44.0% ret 19427
c [sweep-7-1] 33372415 steps 578 queries 3953.26 avg class size
c [sweep-7-1] 4978 decisions 442 SAT calls 27.94 avg env size
c [sweep-7-1] 13651 variables remain 39% (21026 retained 61%)
c [decomp-25] removed 196 variables
c [sweep-7-1] removed 196 vars (0 failed, 145 eqs, 284 impls)
c [sweep-7] removed 196 vars in TOTAL (1 rounds, 577 queries)
c [phase-count-11] 229234 negative 97.2% of 235868 except 6634 2.8%
c [phase-count-11] 154099 positive 65.3% of 235868 except 81769 34.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 144 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 18281 enqueued variables after 317554 conflicts
c [score-dist-11] active 16205 (47%), one 0 (0%), zero 18281 (53%)
c [score-dist-11] max exp 519, different 19 (4%)
c [score-dist-11] median active exp 506, avg 506.9
c [simplification-11] removed 279 variables 0.8% (34486 remain 14%)
c [simplification-11] removed 61163 irredundant clauses 20.6% (235868 remain 19%)
c [simplification-11] maximum reduction of 21% = max (1%, 21%)
c [simplification-11] large reduction 21% >= 5% limit
c [simplification-11] next conflict interval 3175 = min (317554/100, 80000)
c [simplification-11] penalized conflict interval 3175 = 1 * 3175
c [simplification-11] hard conflict limit 330729 (soft 320729 + delta 10000)
c [simplification-11] new conflict limit 320729 (hard 330729)
c 
c [simplification-12] limit 320729 conflicts (hard 330729) hit after 320729 conflicts
c [quatres-8] found 14004 quaternary clauses 34% in total
c [quatres-8-1] removed 481 duplicate quaternary clauses
c [quatres-8-2] added 24 single-self-subsuming ternary resolvents
c [quatres-8-2] added 24 quaternary resolvents
c [ternres-8] limit 111452075 with penalty 0 = 0 + 0
c [ternres-8] 35 schedulable variables 0%
c [ternres-8] 1554 ternary resolvents (34 bin, 1520 trn)
c [ternres-8] fully completed ternary resolution
c [treelook-4] limit 2786301 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 24038 literals 35%
c [treelook-4] scheduling used 1237780 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2786301 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 2899381 steps
c [treelook-4] 23754 literals remain 34%
c [treelook-4] 4439 variables remain to probed next time 13%
c [decomp-27] removed 2 variables
c [treelook-4] removed 2 variables, found 169 hbrs
c [unhide-11] limit 20000000 with penalty 0 = 0 + 0
c [unhide-11-52] 5 units, 12 failed, 23116 tauts, 0 hbrs, 62974 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 747 transitive binary clauses
c [bca-7] limit of 10000000 steps and 473078 added (scaled 2)
c [bca-7] 57574 out of 68866 literals actually usable 84%
c [bca-7] added 746 blocked clauses in 155748 steps
c [sweep-8] limit 33435622 penalty 0 = 0 + 0
c [sweep-8-1] 6879 pos 50.4% + 6766 neg 49.6% = 13645 sched 39.6% ret 20787
c [sweep-8-1] 34690763 steps 1401 queries 2920.22 avg class size
c [sweep-8-1] 9550 decisions 1154 SAT calls 18.71 avg env size
c [sweep-8-1] 10483 variables remain 30% (23929 retained 70%)
c [decomp-28] removed 309 variables
c [sweep-8-1] removed 309 vars (0 failed, 264 eqs, 530 impls)
c [sweep-8] removed 309 vars in TOTAL (1 rounds, 1400 queries)
c [phase-count-12] 228498 negative 97.2% of 235162 except 6664 2.8%
c [phase-count-12] 153211 positive 65.2% of 235162 except 81951 34.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 17447 enqueued variables after 320729 conflicts
c [score-dist-12] active 16676 (49%), one 0 (0%), zero 17447 (51%)
c [score-dist-12] max exp 519, different 19 (4%)
c [score-dist-12] median active exp 506, avg 506.8
c [simplification-12] removed 363 variables 1.1% (34123 remain 14%)
c [simplification-12] removed 706 irredundant clauses 0.3% (235162 remain 19%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 40000 = 80000 / 2
c [simplification-12] new conflict interval 120000
c [simplification-12] penalized conflict interval 120000 = 1 * 120000
c [simplification-12] hard conflict limit 500729 (soft 440729 + delta 60000)
c [simplification-12] new conflict limit 440729 (hard 500729)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  227.6   34123   235162    357788   43324  78249 145222   14    25   44  56%    470   -3   12   13   94%
c -  241.8   34123   235162    390025   43888  78264 145229   15    34   44  43%    685    3   16   14  118%
c -  256.0   34123   235162    423297   44534  78275 145229   16    27   44  58%    820   -4   16   14  115%
c -  268.9   34123   235162    457255   44518  78284 145234   15    26   44  58%    903   -4   14   15   94%
c 
c [simplification-13] limit 440729 conflicts (hard 500729) hit after 471692 conflicts
c [quatres-9] found 13446 quaternary clauses 31% in total
c [quatres-9-1] removed 1064 duplicate quaternary clauses
c [quatres-9-2] added 34 single-self-subsuming ternary resolvents
c [quatres-9-2] added 85 quaternary resolvents
c [ternres-9] limit 145675632 with penalty 0 = 0 + 0
c [ternres-9] all 34123 free variables schedulable
c [ternres-9] 3311 ternary resolvents (78 bin, 3233 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 4719 sched 14%, 39 failed, 3 lifted, 14662 hbrs
c [decomp-30] removed 138 variables
c [basicprobe-4-1] 11063 sched 33%, 52 failed, 1 lifted, 2664 hbrs
c [decomp-31] removed 144 variables
c [basicprobe-4-2] 10819 sched 32%, 22 failed, 0 lifted, 358 hbrs
c [decomp-32] removed 161 variables
c [basicprobe-4-3] 10664 sched 32%, 24 failed, 1 lifted, 260 hbrs
c [decomp-33] removed 90 variables
c [basicprobe-4-4] 10554 sched 31%, 7 failed, 0 lifted, 107 hbrs
c [decomp-34] removed 30 variables
c [basicprobe-4-5] 10523 sched 31%, 5 failed, 0 lifted, 47 hbrs
c [decomp-35] removed 29 variables
c [basicprobe-4-6] 10504 sched 31%, 3 failed, 0 lifted, 58 hbrs
c [decomp-36] removed 10 variables
c [basicprobe-4-7] 8996 probes remain 27% after last round
c [basicprobe-4-7] 157 units = 152 failed (97%) + 5 lifted (3%)
c [basicprobe-4-7] removed 602 variables, found 18160 hbrs
c [bate-2] eliminated 203 asymmetric tautologies during probing
c [unhide-12] limit 20000000 with penalty 0 = 0 + 0
c [unhide-12-65] 0 units, 0 failed, 28812 tauts, 0 hbrs, 487015 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 738 transitive binary clauses
c [cce-5] limit of 364189080 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 1703 (0%) of length 7
c [cce-5-1] eliminated 21 clauses out of 8433 (0%) of length 6
c [cce-5-1] eliminated 92 clauses out of 7287 (1%) of length 5
c [cce-5-1] eliminated 88 clauses out of 7008 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 205 large clauses in 76809415 steps
c [cce-5-1] allowing another 38404707 steps for small clauses
c [cce-5-1] scheduling 112744 clauses = 30069 binary + 82675 ternary
c [cce-5-1] tried to eliminate 112744 small clauses 100%
c [cce-5-1] eliminated 1026 binary clauses 3%
c [cce-5-1] eliminated 38221 ternary clauses 46%
c [cce-5-1] eliminated 39247 small clauses 35%
c [cce-5-1] eliminated 39247 small clauses in 289213471 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 39452 covered clauses in round 1
c [cce-5-2] eliminated 10 clauses out of 8412 (0%) of length 6
c [cce-5-2] eliminated 26 clauses out of 7195 (0%) of length 5
c [cce-5-2] eliminated 17 clauses out of 6920 (0%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 53 large clauses in 41163415 steps
c [cce-5-2] allowing another 20581707 steps for small clauses
c [cce-5-2] scheduling 73499 clauses = 29043 binary + 44456 ternary
c [cce-5-2] tried to eliminate 62362 small clauses 85%
c [cce-5-2] eliminated 17 binary clauses 0%
c [cce-5-2] eliminated 17 ternary clauses 0%
c [cce-5-2] eliminated 34 small clauses 0%
c [cce-5-2] eliminated 34 small clauses in 74975622 steps
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 87 covered clauses in round 2
c [cce-5] eliminated 39539 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 33521 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 5868 variables 18% in round 1 in 91860783 steps
c [elim-7-1] backward subsumption/strengthening limit 8139217
c [elim-7-1-1] backward checking 22386 touched variables 67%
c [elim-7-1-1] incomplete backward checking 21604 remain 97%
c [elim-7-1] subsumed 36 and strengthened 25 clauses in 8139370 steps
c [elim-7] incomplete 89 not tried 0% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 5868 = 18% variables out of 33521 scheduled
c [bca-8] limit of 10000000 steps and 364809 added (scaled 2)
c [bca-8] 47664 out of 55308 literals actually usable 86%
c [bca-8] added 460 blocked clauses in 118206 steps
c [sweep-9] limit 43702689 penalty 0 = 0 + 0
c [sweep-9-1] 5320 pos 54.9% + 4372 neg 45.1% = 9692 sched 35.0% ret 17961
c [sweep-9-1] 42164055 steps 4711 queries 1293.94 avg class size
c [sweep-9-1] 36743 decisions 4607 SAT calls 17.00 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-37] removed 117 variables
c [sweep-9-1] removed 117 vars (0 failed, 116 eqs, 235 impls)
c [sweep-9-2] 12575 pos 45.7% + 14961 neg 54.3% = 27536 sched 100.0% ret 0
c [sweep-9-2] 1588601 steps 44 queries 5175.68 avg class size
c [sweep-9-2] 1128 decisions 41 SAT calls 71.93 avg env size
c [sweep-9-2] 26927 variables remain 98% (609 retained 2%)
c [decomp-38] removed 3 variables
c [sweep-9-2] removed 3 vars (0 failed, 3 eqs, 3 impls)
c [sweep-9] removed 120 vars in TOTAL (2 rounds, 4753 queries)
c [phase-count-13] 178544 negative 98.6% of 181013 except 2469 1.4%
c [phase-count-13] 113950 positive 63.0% of 181013 except 67063 37.0%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 13062 enqueued variables after 471692 conflicts
c [score-dist-13] active 14471 (53%), one 0 (0%), zero 13062 (47%)
c [score-dist-13] max exp 520, different 20 (4%)
c [score-dist-13] median active exp 506, avg 507.5
c [simplification-13] removed 6590 variables 19.3% (27533 remain 11%)
c [simplification-13] removed 54149 irredundant clauses 23.0% (181013 remain 14%)
c [simplification-13] maximum reduction of 23% = max (19%, 23%)
c [simplification-13] large reduction 23% >= 5% limit
c [simplification-13] next conflict interval 4716 = min (471692/100, 120000)
c [simplification-13] penalized conflict interval 4716 = 1 * 4716
c [simplification-13] hard conflict limit 486408 (soft 476408 + delta 10000)
c [simplification-13] new conflict limit 476408 (hard 486408)
c 
c [simplification-14] limit 476408 conflicts (hard 486408) hit after 476409 conflicts
c [quatres-10] found 10212 quaternary clauses 25% in total
c [quatres-10-1] removed 496 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 25 single-self-subsuming ternary resolvents
c [quatres-10-2] added 192 quaternary resolvents
c [ternres-10] limit 146378688 with penalty 0 = 0 + 0
c [ternres-10] all 27533 free variables schedulable
c [ternres-10] 5320 ternary resolvents (18 bin, 5302 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3659467 penalty 3 = 3 + 0
c [gauss-4] extracted 239 xors of average arity 3.0
c [gauss-4] connected 717 occurrences of 146 variables (average 4.9)
c [gauss-4] limit 3659467 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] 367 schedulable variables 1%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 69 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 69 variables, found 15896 hbrs, 5 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 3349 transitive binary clauses
c [transred-10] found 4 units
c [cce-6] limit of 731893443 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 9 clauses out of 35 (26%) of length 11
c [cce-6-1] eliminated 16 clauses out of 131 (12%) of length 10
c [cce-6-1] eliminated 39 clauses out of 630 (6%) of length 9
c [cce-6-1] eliminated 3 clauses out of 149 (2%) of length 8
c [cce-6-1] eliminated 4 clauses out of 1577 (0%) of length 7
c [cce-6-1] eliminated 25 clauses out of 13052 (0%) of length 6
c [cce-6-1] eliminated 101 clauses out of 10100 (1%) of length 5
c [cce-6-1] eliminated 437 clauses out of 6011 (7%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 634 large clauses in 81865198 steps
c [cce-6-1] allowing another 40932599 steps for small clauses
c [cce-6-1] scheduling 61765 clauses = 17465 binary + 44300 ternary
c [cce-6-1] tried to eliminate 61765 small clauses 100%
c [cce-6-1] eliminated 190 binary clauses 1%
c [cce-6-1] eliminated 1072 ternary clauses 2%
c [cce-6-1] eliminated 1262 small clauses 2%
c [cce-6-1] eliminated 1294 small clauses in 75440462 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 1928 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 33352874 steps for small clauses
c [cce-6-2] scheduling 60503 clauses = 17275 binary + 43228 ternary
c [cce-6-2] tried to eliminate 60503 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 1928 covered clauses in TOTAL during 2 rounds
c [bca-9] limit of 10000000 steps and 360117 added (scaled 2)
c [bca-9] 46083 out of 54922 literals actually usable 84%
c [bca-9] added 324 blocked clauses in 120507 steps
c [sweep-10] limit 43913606 penalty 0 = 0 + 0
c [sweep-10-1] 12759 pos 47.5% + 14100 neg 52.5% = 26859 sched 97.8% ret 601
c [sweep-10-1] 43913780 steps 1825 queries 192.36 avg class size
c [sweep-10-1] 19585 decisions 1794 SAT calls 29.24 avg env size
c [sweep-10-1] 8618 variables remain 31% (18840 retained 69%)
c [decomp-41] removed 62 variables
c [sweep-10-1] removed 62 vars (0 failed, 57 eqs, 112 impls)
c [sweep-10] removed 62 vars in TOTAL (1 rounds, 1824 queries)
c [phase-count-14] 176149 negative 98.7% of 178541 except 2392 1.3%
c [phase-count-14] 111917 positive 62.7% of 178541 except 66624 37.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 12346 enqueued variables after 476409 conflicts
c [score-dist-14] active 15052 (55%), one 0 (0%), zero 12346 (45%)
c [score-dist-14] max exp 520, different 20 (4%)
c [score-dist-14] median active exp 506, avg 507.5
c [simplification-14] removed 135 variables 0.5% (27398 remain 11%)
c [simplification-14] removed 2472 irredundant clauses 1.4% (178541 remain 14%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 60000 = 120000 / 2
c [simplification-14] new conflict interval 180000
c [simplification-14] penalized conflict interval 180000 = 1 * 180000
c [simplification-14] hard conflict limit 746409 (soft 656409 + delta 90000)
c [simplification-14] new conflict limit 656409 (hard 746409)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  320.9   27398   178541    528454   40631  96801 47207   15    29   41  51%    983   -1   16   15  105%
c -  333.6   27398   178541    564139   42192  96810 47208   15    22   40  67%   1000   -5   13   15   85%
c -  344.6   27398   178541    600439   42914  96827 47213   15    23   40  63%   1010   -2   16   15  111%
c -  359.1   27398   178541    637444   43092  96839 47215   15    22   40  67%   1016   -3   12   15   80%
c -  373.4   27398   178541    678004   44025  96842 47222   14    20   40  69%   1020   -3   16   15  106%
c 
c [simplification-15] limit 656409 conflicts (hard 746409) hit after 680134 conflicts
c [quatres-11] found 9495 quaternary clauses 21% in total
c [quatres-11-1] removed 138 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 121 single-self-subsuming ternary resolvents
c [quatres-11-2] added 55 quaternary resolvents
c [ternres-11] limit 185014575 with penalty 0 = 0 + 0
c [ternres-11] all 27398 free variables schedulable
c [ternres-11] 2350 ternary resolvents (86 bin, 2264 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 5781705 penalty 4 = 4 + 0
c [card-5] found 2628 at-most-one constraints of average size 3.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 5781705 for elimination
c [card-5] 2628 out of 2628 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [unhide-13] limit 10000000 with penalty 1 = 1 + 0
c [unhide-13-74] 1 units, 14 failed, 22729 tauts, 0 hbrs, 125785 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1439 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 27390 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 21 blocked clauses
c [block-5] 21 < 1/100 * 178097 = 1780 considered unsuccessful
c [cce-7] limit of 925072876 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 152 (1%) of length 8
c [cce-7-1] eliminated 3 clauses out of 1565 (0%) of length 7
c [cce-7-1] eliminated 21 clauses out of 12416 (0%) of length 6
c [cce-7-1] eliminated 109 clauses out of 10535 (1%) of length 5
c [cce-7-1] eliminated 53 clauses out of 5368 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 187 large clauses in 104478127 steps
c [cce-7-1] allowing another 52239063 steps for small clauses
c [cce-7-1] scheduling 61801 clauses = 18711 binary + 43090 ternary
c [cce-7-1] tried to eliminate 61801 small clauses 100%
c [cce-7-1] eliminated 305 binary clauses 2%
c [cce-7-1] eliminated 5298 ternary clauses 12%
c [cce-7-1] eliminated 5603 small clauses 9%
c [cce-7-1] eliminated 5603 small clauses in 119179048 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 5790 covered clauses in round 1
c [cce-7-2] eliminated 21 clauses out of 12395 (0%) of length 6
c [cce-7-2] eliminated 8 clauses out of 10426 (0%) of length 5
c [cce-7-2] eliminated 7 clauses out of 5315 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 36 large clauses in 74693184 steps
c [cce-7-2] allowing another 37346592 steps for small clauses
c [cce-7-2] scheduling 56198 clauses = 18406 binary + 37792 ternary
c [cce-7-2] tried to eliminate 56198 small clauses 100%
c [cce-7-2] eliminated 12 binary clauses 0%
c [cce-7-2] eliminated 2 ternary clauses 0%
c [cce-7-2] eliminated 14 small clauses 0%
c [cce-7-2] eliminated 14 small clauses in 84051931 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 50 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 37271388 steps for small clauses
c [cce-7-3] scheduling 56184 clauses = 18394 binary + 37790 ternary
c [cce-7-3] tried to eliminate 56184 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 5840 covered clauses in TOTAL during 3 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 27390 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 118 variables 0% in round 1 in 81237081 steps
c [elim-8-1] backward subsumption/strengthening limit 81237000
c [elim-8-1-1] backward checking 838 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 3 clauses in 2839964 steps
c [elim-8-1] rescheduled 10 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 106742 steps
c [elim-8-2] backward subsumption/strengthening limit 106700
c [elim-8-2-1] backward checking 8 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 35330 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 119 = 0% variables out of 27390 scheduled
c [elim-8] 119 < 1/100 * 27390 = 273 considered unsuccessful
c [bca-10] limit of 10000000 steps and 346879 added (scaled 2)
c [bca-10] 43606 out of 54544 literals actually usable 80%
c [bca-10] added 334 blocked clauses in 138060 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 555043720 penalty 0 = 0 + 0
c [sweep-11-1] 4391 pos 51.0% + 4214 neg 49.0% = 8605 sched 31.6% ret 18666
c [sweep-11-1] 45617845 steps 3411 queries 494.44 avg class size
c [sweep-11-1] 29912 decisions 3379 SAT calls 19.38 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-43] removed 77 variables
c [sweep-11-1] removed 77 vars (0 failed, 75 eqs, 168 impls)
c [sweep-11-2] 12587 pos 46.3% + 14607 neg 53.7% = 27194 sched 100.0% ret 0
c [sweep-11-2] 73265106 steps 4157 queries 75.50 avg class size
c [sweep-11-2] 38548 decisions 4219 SAT calls 23.34 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-44] removed 26 variables
c [sweep-11-2] removed 26 vars (0 failed, 20 eqs, 58 impls)
c [sweep-11-3] 12588 pos 46.3% + 14580 neg 53.7% = 27168 sched 100.0% ret 0
c [sweep-11-3] 75492617 steps 3940 queries 74.29 avg class size
c [sweep-11-3] 37420 decisions 3990 SAT calls 22.98 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-45] removed 28 variables
c [sweep-11-3] removed 28 vars (0 failed, 11 eqs, 43 impls)
c [sweep-11] removed 131 vars in TOTAL (3 rounds, 11505 queries)
c [phase-count-15] 169117 negative 98.6% of 171514 except 2397 1.4%
c [phase-count-15] 105289 positive 61.4% of 171514 except 66225 38.6%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 11137 enqueued variables after 680134 conflicts
c [score-dist-15] active 16003 (59%), one 0 (0%), zero 11137 (41%)
c [score-dist-15] max exp 521, different 21 (4%)
c [score-dist-15] median active exp 506, avg 508.0
c [simplification-15] removed 258 variables 0.9% (27140 remain 11%)
c [simplification-15] removed 7027 irredundant clauses 3.9% (171514 remain 14%)
c [simplification-15] maximum reduction of 4% = max (1%, 4%)
c [simplification-15] geometric conflict interval increment 36000 = 180000 / 5
c [simplification-15] new conflict interval 216000
c [simplification-15] penalized conflict interval 216000 = 1 * 216000
c [simplification-15] hard conflict limit 1004134 (soft 896134 + delta 108000)
c [simplification-15] new conflict limit 896134 (hard 1004134)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  404.3   27140   171514    717550   45847 100032 28362   14    23   40  63%   1022   -0   14   15   93%
c -  419.8   27140   171514    761221   47383 100062 28365   14    20   40  72%   1023   -2   14   15   99%
c -  434.5   27140   171514    806583   47965 100074 28370   14    19   40  74%   1023   -0   14   14  104%
c -  451.5   27140   171514    853036   49288 100081 28372   13    16   41  80%   1024   -3   13   14   98%
c i  455.0   27139   171514    862098   56986 100081 28374   11    14   45  79%   1024   -4    9   13   68%
c i  455.2   27138   171514    862935   57720 100082 28374   11    15   45  78%  -4208   -4   14   13  107%
c -  472.4   27138   171514    908922   50270 100094 28375   12    15   40  84%  -3674   -2   12   13   95%
c -  488.2   27138   171508    957926   52269 100209 28384   12    16   40  75%  -1200   -4   13   12  111%
c i  491.5   27137   171508    966853   59551 100210 28385   13    16   44  81%   -917   -4   13   12  106%
c 
c [simplification-16] limit 896134 conflicts (hard 1004134) hit after 1004134 conflicts
c [quatres-12] found 9979 quaternary clauses 20% in total
c [quatres-12-1] removed 259 duplicate quaternary clauses
c [quatres-12-1] added 5 double-self-subsuming ternary resolvents
c [quatres-12-2] added 166 single-self-subsuming ternary resolvents
c [quatres-12-2] added 170 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 27137 free variables schedulable
c [ternres-12] 15847 ternary resolvents (48 bin, 15799 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-46] removed 4 variables
c [treelook-5] limit 12589174 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 16380 literals 30%
c [treelook-5] scheduling used 1021709 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 12589174 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 12641285 steps
c [treelook-5] 14124 literals remain 26%
c [treelook-5] 3456 variables remain to probed next time 13%
c [decomp-47] removed 2 variables
c [treelook-5] removed 5 variables, found 5779 hbrs
c [unhide-14] limit 20000000 with penalty 0 = 0 + 0
c [unhide-14-87] 0 units, 53 failed, 28815 tauts, 0 hbrs, 248898 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 621 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 12589174090 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 10 clauses out of 129 (8%) of length 10
c [cce-8-1] eliminated 5 clauses out of 1551 (0%) of length 7
c [cce-8-1] eliminated 25 clauses out of 11876 (0%) of length 6
c [cce-8-1] eliminated 98 clauses out of 10601 (1%) of length 5
c [cce-8-1] eliminated 46 clauses out of 5272 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 184 large clauses in 89040019 steps
c [cce-8-1] allowing another 44520009 steps for small clauses
c [cce-8-1] scheduling 102324 clauses = 19307 binary + 83017 ternary
c [cce-8-1] tried to eliminate 102324 small clauses 100%
c [cce-8-1] eliminated 250 binary clauses 1%
c [cce-8-1] eliminated 12558 ternary clauses 15%
c [cce-8-1] eliminated 12808 small clauses 13%
c [cce-8-1] eliminated 12808 small clauses in 162600615 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 12992 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 32636282 steps for small clauses
c [cce-8-2] scheduling 89516 clauses = 19057 binary + 70459 ternary
c [cce-8-2] tried to eliminate 89516 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 12992 covered clauses in TOTAL during 2 rounds
c [bca-11] limit of 10000000 steps and 317598 added (scaled 2)
c [bca-11] 40507 out of 54226 literals actually usable 75%
c [bca-11] added 184 blocked clauses in 156857 steps
c [sweep-12] limit 75535044 penalty 0 = 0 + 0
c [sweep-12-1] 12999 pos 47.9% + 14113 neg 52.1% = 27112 sched 100.0% ret 0
c [sweep-12-1] 77640386 steps 1910 queries 221.63 avg class size
c [sweep-12-1] 24121 decisions 1920 SAT calls 32.39 avg env size
c [sweep-12-1] 5874 variables remain 22% (21237 retained 78%)
c [decomp-48] removed 13 variables
c [sweep-12-1] removed 13 vars (0 failed, 12 eqs, 33 impls)
c [sweep-12] 13 < 1/1000 * 27112 = 27 considered unsuccessful
c [sweep-12] removed 13 vars in TOTAL (1 rounds, 1909 queries)
c [phase-count-16] 154741 negative 98.5% of 157127 except 2386 1.5%
c [phase-count-16] 91987 positive 58.5% of 157127 except 65140 41.5%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 10532 enqueued variables after 1004134 conflicts
c [score-dist-16] active 16567 (61%), one 0 (0%), zero 10532 (39%)
c [score-dist-16] max exp 521, different 21 (4%)
c [score-dist-16] median active exp 508, avg 508.6
c [simplification-16] removed 38 variables 0.1% (27099 remain 11%)
c [simplification-16] removed 14381 irredundant clauses 8.4% (157127 remain 12%)
c [simplification-16] maximum reduction of 8% = max (0%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 10041 = min (1004134/100, 216000)
c [simplification-16] penalized conflict interval 10041 = 1 * 10041
c [simplification-16] hard conflict limit 1024175 (soft 1014175 + delta 10000)
c [simplification-16] new conflict limit 1014175 (hard 1024175)
c 
c [simplification-17] limit 1014175 conflicts (hard 1024175) hit after 1024175 conflicts
c [quatres-13] found 9854 quaternary clauses 20% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-1] added 8 double-self-subsuming ternary resolvents
c [quatres-13-2] added 60 single-self-subsuming ternary resolvents
c [quatres-13-2] added 77 quaternary resolvents
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 27099 free variables schedulable
c [ternres-13] 19918 ternary resolvents (13 bin, 19905 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 9992 sched 38%, 236 failed, 0 lifted, 3267 hbrs
c [decomp-50] removed 1050 variables
c [basicprobe-5-1] 10397 sched 40%, 15 failed, 0 lifted, 1181 hbrs
c [decomp-51] removed 18 variables
c [basicprobe-5-2] 10373 sched 40%, 1 failed, 0 lifted, 58 hbrs
c [decomp-52] removed 1 variables
c [basicprobe-5-3] 10372 sched 40%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-4] 10372 sched 40%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-4] fully completed probing
c [basicprobe-5-4] 252 units = 252 failed (100%) + 0 lifted (0%)
c [basicprobe-5-4] removed 1069 variables, found 4514 hbrs
c [bate-3] eliminated 196 asymmetric tautologies during probing
c [unhide-15] limit 20000000 with penalty 0 = 0 + 0
c [unhide-15-100] 0 units, 0 failed, 21906 tauts, 0 hbrs, 85387 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 410 transitive binary clauses
c [cce-9] limit of 1283952498 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 1530 (0%) of length 7
c [cce-9-1] eliminated 19 clauses out of 9741 (0%) of length 6
c [cce-9-1] eliminated 95 clauses out of 11330 (1%) of length 5
c [cce-9-1] eliminated 40 clauses out of 4188 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 155 large clauses in 83435245 steps
c [cce-9-1] allowing another 41717622 steps for small clauses
c [cce-9-1] scheduling 85463 clauses = 18865 binary + 66598 ternary
c [cce-9-1] tried to eliminate 85463 small clauses 100%
c [cce-9-1] eliminated 770 binary clauses 4%
c [cce-9-1] eliminated 2049 ternary clauses 3%
c [cce-9-1] eliminated 2819 small clauses 3%
c [cce-9-1] eliminated 2819 small clauses in 171225936 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 2974 covered clauses in round 1
c [cce-9-2] eliminated 12 clauses out of 9722 (0%) of length 6
c [cce-9-2] eliminated 18 clauses out of 11235 (0%) of length 5
c [cce-9-2] eliminated 7 clauses out of 4148 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 37 large clauses in 79931703 steps
c [cce-9-2] allowing another 39965851 steps for small clauses
c [cce-9-2] scheduling 82644 clauses = 18095 binary + 64549 ternary
c [cce-9-2] tried to eliminate 82644 small clauses 100%
c [cce-9-2] eliminated 191 binary clauses 1%
c [cce-9-2] eliminated 38 ternary clauses 0%
c [cce-9-2] eliminated 229 small clauses 0%
c [cce-9-2] eliminated 229 small clauses in 157257837 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 266 covered clauses in round 2
c [cce-9-3] eliminated 2 clauses out of 9710 (0%) of length 6
c [cce-9-3] eliminated 1 clauses out of 11217 (0%) of length 5
c [cce-9-3] eliminated 1 clauses out of 4141 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 4 large clauses in 79627995 steps
c [cce-9-3] allowing another 39813997 steps for small clauses
c [cce-9-3] scheduling 82415 clauses = 17904 binary + 64511 ternary
c [cce-9-3] tried to eliminate 82415 small clauses 100%
c [cce-9-3] eliminated 7 ternary clauses 0%
c [cce-9-3] eliminated 7 small clauses 0%
c [cce-9-3] eliminated 7 small clauses in 156673601 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 11 covered clauses in round 3
c [cce-9] eliminated 3251 covered clauses in TOTAL during 3 rounds
c [bca-12] limit of 10000000 steps and 294284 added (scaled 2)
c [bca-12] 39705 out of 52062 literals actually usable 76%
c [bca-12] added 131 blocked clauses in 153280 steps
c [phase-count-17] 143220 negative 98.5% of 145445 except 2225 1.5%
c [phase-count-17] 82542 positive 56.8% of 145445 except 62903 43.2%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 10503 enqueued variables after 1024175 conflicts
c [score-dist-17] active 15527 (60%), one 0 (0%), zero 10503 (40%)
c [score-dist-17] max exp 521, different 21 (4%)
c [score-dist-17] median active exp 508, avg 508.7
c [simplification-17] removed 1069 variables 3.9% (26030 remain 11%)
c [simplification-17] removed 11682 irredundant clauses 7.4% (145445 remain 11%)
c [simplification-17] maximum reduction of 7% = max (4%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 10241 = min (1024175/100, 216000)
c [simplification-17] penalized conflict interval 10241 = 1 * 10241
c [simplification-17] hard conflict limit 1044416 (soft 1034416 + delta 10000)
c [simplification-17] new conflict limit 1034416 (hard 1044416)
c 
c [simplification-18] limit 1034416 conflicts (hard 1044416) hit after 1044416 conflicts
c [quatres-14] found 7817 quaternary clauses 17% in total
c [quatres-14-1] removed 9 duplicate quaternary clauses
c [quatres-14-1] added 3 double-self-subsuming ternary resolvents
c [quatres-14-2] added 35 single-self-subsuming ternary resolvents
c [quatres-14-2] added 37 quaternary resolvents
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] all 26030 free variables schedulable
c [ternres-14] 2478 ternary resolvents (8 bin, 2470 trn)
c [ternres-14] 7 variables remain 0% (26023 retained 100%)
c [decomp-54] removed 1 variables
c [simpleprobe-6] all 26029 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-55] removed 139 variables
c [simpleprobe-6] 289 variables remain 1% (25601 retained 99%)
c [simpleprobe-6] removed 139 variables, found 9393 hbrs, 3 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1232 transitive binary clauses
c [cce-10] limit of 1307079550 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 3 clauses out of 119 (3%) of length 7
c [cce-10-1] eliminated 200 clauses out of 10132 (2%) of length 6
c [cce-10-1] eliminated 21 clauses out of 11289 (0%) of length 5
c [cce-10-1] eliminated 3 clauses out of 4063 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 227 large clauses in 50918553 steps
c [cce-10-1] allowing another 25459276 steps for small clauses
c [cce-10-1] scheduling 81016 clauses = 18204 binary + 62812 ternary
c [cce-10-1] tried to eliminate 81016 small clauses 100%
c [cce-10-1] eliminated 179 binary clauses 1%
c [cce-10-1] eliminated 21 ternary clauses 0%
c [cce-10-1] eliminated 200 small clauses 0%
c [cce-10-1] eliminated 200 small clauses in 109124786 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 427 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 25336517 steps for small clauses
c [cce-10-2] scheduling 80816 clauses = 18025 binary + 62791 ternary
c [cce-10-2] tried to eliminate 80816 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 427 covered clauses in TOTAL during 2 rounds
c [cce-10] 427 < 1/100 * 142846 = 1428 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 25890 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1201 variables 5% in round 1 in 53476603 steps
c [elim-9-1] backward subsumption/strengthening limit 46523397
c [elim-9-1-1] backward checking 6575 touched variables 25%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 6 and strengthened 1 clauses in 8125077 steps
c [elim-9-1] rescheduled 21 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 677908 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1201 = 5% variables out of 25890 scheduled
c [bca-13] limit of 10000000 steps and 284290 added (scaled 2)
c [bca-13] 38372 out of 49380 literals actually usable 78%
c [bca-13] added 10 blocked clauses in 146814 steps
c [sweep-13] limit 39212386 penalty 1 = 1 + 0
c [sweep-13-1] 3718 pos 65.4% + 1966 neg 34.6% = 5684 sched 23.0% ret 19005
c [sweep-13-1] 39083188 steps 2622 queries 522.14 avg class size
c [sweep-13-1] 23122 decisions 2631 SAT calls 18.53 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-56] removed 16 variables
c [sweep-13-1] removed 16 vars (0 failed, 7 eqs, 15 impls)
c [sweep-13-2] 12299 pos 49.8% + 12374 neg 50.2% = 24673 sched 100.0% ret 0
c [sweep-13-2] 213997 steps 5 queries 8894.80 avg class size
c [sweep-13-2] 253 decisions 4 SAT calls 116.00 avg env size
c [sweep-13-2] 24668 variables remain 100% (5 retained 0%)
c [sweep-13-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] 16 < 1/1000 * 24689 = 24 considered unsuccessful
c [sweep-13] removed 16 vars in TOTAL (2 rounds, 2625 queries)
c [phase-count-18] 138345 negative 98.6% of 140292 except 1947 1.4%
c [phase-count-18] 78948 positive 56.3% of 140292 except 61344 43.7%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 10348 enqueued variables after 1044416 conflicts
c [score-dist-18] active 14325 (58%), one 0 (0%), zero 10348 (42%)
c [score-dist-18] max exp 521, different 21 (4%)
c [score-dist-18] median active exp 508, avg 508.8
c [simplification-18] removed 1357 variables 5.2% (24673 remain 10%)
c [simplification-18] removed 5153 irredundant clauses 3.5% (140292 remain 11%)
c [simplification-18] maximum reduction of 5% = max (5%, 4%)
c [simplification-18] large reduction 5% >= 5% limit
c [simplification-18] next conflict interval 10444 = min (1044416/100, 216000)
c [simplification-18] penalized conflict interval 10444 = 1 * 10444
c [simplification-18] hard conflict limit 1064860 (soft 1054860 + delta 10000)
c [simplification-18] new conflict limit 1054860 (hard 1064860)
c 
c [simplification-19] limit 1054860 conflicts (hard 1064860) hit after 1064860 conflicts
c [quatres-15] found 9492 quaternary clauses 21% in total
c [quatres-15-1] removed 4 duplicate quaternary clauses
c [quatres-15-1] added 9 double-self-subsuming ternary resolvents
c [quatres-15-2] added 55 single-self-subsuming ternary resolvents
c [quatres-15-2] added 211 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] 6 schedulable variables 0%
c [ternres-15] 1949 ternary resolvents (6 bin, 1943 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] extracted 337 xors of average arity 3.0
c [gauss-5] connected 1011 occurrences of 273 variables (average 3.7)
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 26644524 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 14310 literals 29%
c [treelook-6] scheduling used 940421 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 26644524 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 15737499 steps
c [treelook-6] fully completed tree based probing
c [treelook-6] removed 1 variables, found 3922 hbrs
c [unhide-16] limit 10000000 with penalty 1 = 1 + 0
c [unhide-16-108] 0 units, 0 failed, 45603 tauts, 0 hbrs, 79912 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 493 transitive binary clauses
c [bca-14] limit of 10000000 steps and 283909 added (scaled 2)
c [bca-14] 37956 out of 49346 literals actually usable 77%
c [bca-14] added 16 blocked clauses in 126868 steps
c [phase-count-19] 138274 negative 98.6% of 140222 except 1948 1.4%
c [phase-count-19] 78847 positive 56.2% of 140222 except 61375 43.8%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 10342 enqueued variables after 1064860 conflicts
c [score-dist-19] active 14330 (58%), one 0 (0%), zero 10342 (42%)
c [score-dist-19] max exp 521, different 21 (4%)
c [score-dist-19] median active exp 508, avg 508.8
c [simplification-19] removed 1 variables 0.0% (24672 remain 10%)
c [simplification-19] removed 62 irredundant clauses 0.0% (140222 remain 11%)
c [simplification-19] maximum reduction of 0% = max (0%, 0%)
c [simplification-19] full geometric conflict interval increment 216000
c [simplification-19] new conflict interval 432000
c [simplification-19] penalized conflict interval 432000 = 1 * 432000
c [simplification-19] hard conflict limit 1712860 (soft 1496860 + delta 216000)
c [simplification-19] new conflict limit 1496860 (hard 1712860)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  589.5   24671   140214   1093547   69411 132958 14129    8    10   46  85%    505   -5    6   11   52%
c -  597.4   24572   140213   1118780   51347 132990 14139   14    17   40  78%   -698    2   13   11  114%
c i  601.3   24571   140211   1130584   60159 133002 14143   12    15   44  80%   -414   -0   11   12   99%
c i  606.1   24570   140211   1145121   71561 133013 14153   11    13   45  84%   -599   -2   13   11  116%
c i  608.1   24569   140210   1151263   75997 133032 14158   11    14   48  79%   -663   -1   10   11   92%
c i  608.2   24568   140210   1151538   76183 133032 14158   11    14   48  79%   -679   -1   12   11  102%
c i  614.5   24567   140210   1170206   90228 133039 14173   10    12   48  87%   -316   -3    8   11   68%
c -  615.7   24567   140210   1173413   53507 133043 14176   10    13   40  82%   -522   -2   11   11  101%
c i  618.2   24566   140210   1181536   59064 133052 14178   10    12   43  84%   -353   -2    9   11   82%
c i  619.9   24565   140210   1186783   62055 133068 14182    9    10   43  88%   -412   -4    7   11   60%
c -  632.9   24565   140208   1225851   54999 133077 14186   12    14   40  86%    186   -1   11   12   91%
c i  640.3   24564   140208   1249422   72865 133100 14188   10    11   45  88%    439   -3    7   12   60%
c i  646.2   24563   140208   1266609   85291 133117 14194   10    11   48  90%   -191   -4    9   11   76%
c -  650.9   22788   140207   1278879   53230 133122 14196   14    18   40  76%   -209    3   10   12   87%
c i  656.1   22787   140207   1296222   66297 133153 14208    9    12   44  78%     77   -3    7   12   56%
c i  659.6   22786   140207   1306491   73865 133164 14212   11    14   47  81%   -187   -1    7   12   59%
c i  659.6   22774   140207   1306512   73868 133170 14215   11    14   47  81%   -190   -1    7   12   57%
c i  659.6   22768   140207   1306513   73868 133170 14215   11    14   47  81%   -190   -1    7   12   57%
c i  660.4   22762   140207   1308854   75490 133173 14218   10    13   47  80%   -286   -2    7   12   59%
c i  660.4   22706   140207   1308857   75492 133173 14218   10    13   47  80%   -286   -2    7   12   58%
c i  660.4   22703   140207   1308858   75492 133173 14218   10    13   47  80%   -286   -2    7   12   58%
c i  660.6   22697   140207   1309577   75889 133182 14224   10    13   47  79%   -298   -2    6   12   51%
c i  660.6   22065   140207   1309585   75890 133182 14226   10    12   47  79%   -298   -2    6   12   50%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  660.6   21757   140207   1309586   75890 133182 14226   10    12   47  79%   -298   -2    6   12   50%
c i  660.6   21669   140207   1309587   75890 133182 14226   10    12   47  79%   -298   -2    6   12   50%
c 0  660.6   21653   140207   1309587   75890 133182 14226   10    12   47  79%   -298   -2    6   12   50%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 442 basic ate = 406 trn 92% + 36 lrg 8% in 3 updates
c bcas: 14 count, 5946 added (7017 skipped), 2173023 steps
c bkwd: tried 167562 clauses, 335064 lits, 2.00 lits/clause
c bkwd: checked 14907713 occs, 88.97 occs/clause, 44.49 occs/lit
c bkwd: subsumed 0 binary, 32 ternary, 10 large
c bkwd: strengthened 0 binary, 8 ternary (100% self), 21 large (0% self)
c blkd: 5 bces, 14343 removed, 5373832 resolutions, 15327830 steps
c blkd: 25682 blocking literals 5%, 9 pure
c bump: 1318031 bumped seen, 166997619 lits 126.7 on average
c card: 5 count, 0 units, 0 am1, 75828412 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 44335 subsumed
c card: 8681 at-most-one constraints found, average size 3.69
c card: 8681 at-most-one constraints used 100%, average size 3.69
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 10 cces, 132365 eliminated, 102935 ate 78%, 29430 abce 22%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 5254282 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 157 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 60317 equivalent 21%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2680258 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 126224 eliminated 45%, 565 pure 0%
c elms: 13 rounds, 1.4 rounds/bve
c elms: 124061 small 98%, 1589 large 1%
c elms: 185598 tried small, 124061 succeeded 67%, 61537 failed 33%
c elms: 7519 subsumed, 25624 strengthened, 110 blocked
c elms: 5964440 copies, 6301539 resolutions, 3395718 ipos
c elms: 13569694 subchks, 4397445 strchks
c gaus: 5 extractions, 795 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 27814502 steps, 13907251 extr 50%, 23424 elim 0%
c glue: 12.8 orig avg, 12.8 real avg, 3.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 554272 = 84861 simple 15% + 468709 trn 85% + 702 lrg 0%, 14869 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1318031 clauses, 38.5 length
c lrnd: 50771350 lits = 96633959 orig - 45862609 removed 47%
c lrnd: 265039 uips 20%, 781762 flips 59%
c mins: 1312775 mins 100%, 301 bin 0%, 4955 size 0%
c mins: 128826025 poisoned searches, 18454719 hits, 14% hit rate
c mins: 205668184 used twice searches, 7049450 hits, 3% hit rate
c move: moved 139501, 18666 bin 13%, 120835 trn 87%
c otfs: 3281 driving 19%, 13958 restarting 81%
c otfs: str 17239, 16746 red 97%, 493 irr 3%
c otfs: str 17239, 0 bin 0%, 487 trn 3%, 16752 lrg 97%
c otfs: sub 496, 426 red 86%, 70 irr 14%
c otfs: sub 496, 0 bin 0%, 24 trn 5%, 472 lrg 95%
c phas: 19 computed, 160379 set, 144 pos (0%), 160235 neg (100%)
c prbs: 5 basic, 266048 probed, 617 failed, 71 lifted
c prbs: 6 simple, 278355 probed, 85 failed, 21038 eqs
c prbs: 6 treelook, 17118 probed, 7 failed, 0 lifted
c prom: 183393 locked 8% out of 2349012 tried
c prps: 1250582216 props, 455 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 15 count, 10256 quat, 925 self1, 53 self2, 8230 dup
c queu: 19 sorted, 2680258 next (208502 steps 0.08)
c queu: 167760731 enq (297421931 steps 1.77), 166997619 deq 100%
c redc: 12418 clauses 12%, 101043 tried 8%, 16 sat 0%
c redc: 17488 lits 1%, 1335132 tried 1%, 16 sat 0%
c redc: 277 times jump level reduced, 3.8 levels on average
c reds: 27 count, 48503.2 conflicts per reduce
c reds: 0 memlim 0%, 27 arith 100%
c reds: 850534 collected 93%, 64012 retired 7%
c rmbd: 89113 removed, 87661 red 98%
c rsts: 23197 restarts 99%, 207 skipped 1%
c rsts: 207 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 19 count, 19 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1318031 count (1172602 tried 0.9), 183560 sub out of 1314196 (14.0%)
c swps: 13 count, 17 rounds, 27449 queries (1614.6/round)
c swps: 26340 sat calls, 375 unsat (0.4% success rate)
c swps: 252833 decisions 9.6, 11725 conflicts 0.4
c swps; 825.8 avg class size, 24.3 avg environment size
c swps: 0 failed, 2917 impls, 1450 equivs
c swp0: 9144 type 0 queries, 336 unsat (3.7%), 9073 sat (99.2%)
c swp1: 18305 type 1 queries, 3952 unsat (21.6%), 16926 sat (92.5%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 7996985 calls to obtain time
c tops: 74648 fixed 26%, 30 its, 43652.90 confs/it
c trds: 15 transitive reductions, 16709 removed, 4 failed
c trds: 307344 nodes, 228237 edges, 29478210 steps
c trim: 1064618 words, 4.1 MB
c trnr: 15 count, 599 bin, 86390 trn, 1456879316 steps
c unhd: 16 count, 108 rounds, 167950261 steps
c unhd: 3140 non-trivial sccs of average size 2.9
c unhd: 137 units, 134 bin, 3 trn, 0 lrg
c unhd: 430 failed, 378 stamp, 0 lits, 2 bin, 27 trn, 0 lrg
c unhd: 364633 tauts, 2912 bin 1%, 23949 trn 7%, 62708 lrg 17%
c unhd: 364633 tauts, 275064 stamp 75%, 349965 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1763264 str, 134 bin 0%, 16795 trn 1%, 1746335 lrg 99%, 1744393 red 99%
c vars: 21653 remaining 8% and 261189 removed 92% out of 282842
c vars: 74648 fixed 26%, 126224 eliminated 45%, 60317 equivalent 21%
c vsts: 32943816538 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 26.2 search visits per propagation, 24403.1 per conflict
c wchs: 1946346430 pushed, 35192583 enlarged, 235 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1324452        850534         64012      40520440      16488040        711799
c 
c  0 0         50800   4      5153   1         0   0  25589393  63   7562959  46    148962  21     0.8
c  1 5         31166   2     11019   1      5459   9   3627783   9<  1496574   9<    57565   8     0.4
c  2 6        171119  13     85754  10     15744  25   5231902  13   2962861  18    174584  25<    2.1
c  3 9        493425  37<   305801  36<    23521  37<  4309376  11   3108672  19    236210  33     5.4
c  4 14       505963  38    385061  45     16844  26   1617533   4   1254983   8     88764  12     7.8
c  5 21        71105   5     57132   7      2365   4    142563   0    100985   1      5648   1     2.4
c  6 30          854   0       601   0        78   0      1844   0       966   0        65   0     0.1
c  7 41           20   0        13   0         1   0        46   0        40   0         1   0     0.0
c 
c avg                  3.2           3.4           2.9           0.8           1.4           2.1
c std                  1.1           0.9           1.0           1.3           1.4           1.3
c 
c   49.447   7% cce
c   31.608   5% unhide
c   26.610   4% bump
c   25.118   4% sweep
c   24.840   4% probe
c   13.876   2% ternres
c   11.852   2% elim
c    3.235   0% transred
c 
c    6.627 < 1% rest (below)
c 
c    1.587   0% bca
c    1.468   0% decide
c    1.302   0% block
c    1.086   0% quatres
c    0.705   0% gauss
c    0.479   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.344   1% preprocessing     2%
c  168.503  26% inprocessing     98%
c ==================================
c  171.847  26% simplifying
c  488.745  74% search
c ==================================
c  660.596 100% all
c 
c       1309587 conflicts,        1982.4 confs/sec
c          1243 ternaries,        1053.6 confs/ternary
c           200 binaries,         6547.9 confs/binary
c            30 iterations,      43652.9 confs/iteration
c 
c            27 reductions,          0.0 redus/sec,  48503.2 confs/reduction
c         23197 restarts,           35.1 rests/sec,     56.5 confs/restart
c       2680258 decisions,        4057.3 decis/sec,      2.0 decis/conflict
c    1250582216 propagations,  1893111.9 props/sec,    466.6 props/decision
c 
c 660.6 seconds, 128.6 MB
c launch: done
