c launch: /data/cnf/sc2014/app/MD5-32-5.cnf.bz2
c host: atom11
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 Fri May  8 15:09:13 CEST 2015
c compiled Fri May  8 15:09:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c Linux cluster2 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/MD5-32-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-32-5.cnf.bz2
c no embedded options
c found 'p cnf 9534 73676' header
c read 9534 variables, 73676 clauses, 288490 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=2
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 9523 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] VMTF (--score=2)
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    9523    73411         0       0      0     0    0     0    4   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 3 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 123 out of 123 constraints (100%) meet size limits
c [card-1] found 3 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 32 variables
c [simpleprobe-1] all 9502 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 12 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 12 variables, found 340 hbrs, 4 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 64 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 9490 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 2731 variables 29% in round 1 in 9805920 steps
c [elim-1-1] backward subsumption/strengthening limit 9805900
c [elim-1-1-1] backward checking 6647 touched variables 70%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 15 and strengthened 18 clauses in 1344721 steps
c [elim-1-1] rescheduled 42 variables 0% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 118354 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2731 = 29% variables out of 9490 scheduled
c [phase-count-1] 71910 negative 99.1% of 72539 except 629 0.9%
c [phase-count-1] 69826 positive 96.3% of 72539 except 2713 3.7%
c [phase-count-1] less non-negative clauses 629 than limit 7200 (10.0%)
c [phase-count-1] non-pos/non-neg = 2713/629 = 4.31 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6759 negative 100%
c [sort-queue-1] sorted 6759 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6759 (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 2764 variables 29.0% (6759 remain 71%)
c [simplification-1] removed 872 irredundant clauses 1.2% (72539 remain 99%)
c [simplification-1] maximum reduction of 29% = max (29%, 1%)
c [simplification-1] large reduction 29% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] all 6759 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1942 variables remain 29% (4817 retained 71%)
c [simpleprobe-2] removed 0 variables, found 28 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12313 literals 91%
c [treelook-1] scheduling used 300050 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300041 steps
c [treelook-1] 9413 literals remain 70%
c [treelook-1] 5465 variables remain to probed next time 81%
c [treelook-1] removed 0 variables, found 66 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 757 sched 11%, 0 failed, 0 lifted, 31 hbrs
c [basicprobe-1-1] 766 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 31 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6759 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 0 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 45 clauses out of 856 (5%) of length 6
c [cce-1-1] eliminated 9160 clauses out of 29049 (32%) of length 5
c [cce-1-1] eliminated 314 clauses out of 24771 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 9519 large clauses in 12718666 steps
c [cce-1-1] allowing another 6359333 steps for small clauses
c [cce-1-1] scheduling 15760 clauses = 619 binary + 15141 ternary
c [cce-1-1] tried to eliminate 15760 small clauses 100%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 245 ternary clauses 2%
c [cce-1-1] eliminated 248 small clauses 2%
c [cce-1-1] eliminated 248 small clauses in 8655021 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 9767 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 5735033 steps for small clauses
c [cce-1-2] scheduling 15512 clauses = 616 binary + 14896 ternary
c [cce-1-2] tried to eliminate 15512 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 9767 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6759 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 40 variables 1% in round 1 in 16786696 steps
c [elim-2-1] backward subsumption/strengthening limit 3213304
c [elim-2-1-1] backward checking 201 touched variables 3%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 6 clauses in 78374 steps
c [elim-2-1] rescheduled 13 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 11207 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 40 = 1% variables out of 6759 scheduled
c [elim-2] 40 < 1/100 * 6759 = 67 considered unsuccessful
c [bca-1] limit of 10000000 steps and 125980 added (scaled 2)
c [bca-1] 11626 out of 13440 literals actually usable 87%
c [bca-1] added 0 blocked clauses in 50194 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2494 pos 37.1% + 4225 neg 62.9% = 6719 sched 100.0% ret 0
c [sweep-1-1] 1000484 steps 858 queries 566.48 avg class size
c [sweep-1-1] 8127 decisions 862 SAT calls 16.69 avg env size
c [sweep-1-1] 1510 variables remain 22% (5209 retained 78%)
c [decomp-7] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 857 queries)
c [sort-queue-2] sorted 6718 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 3071 (46%), zero 3647 (54%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 41 variables 0.6% (6718 remain 71%)
c [simplification-2] removed 9799 irredundant clauses 13.5% (62740 remain 85%)
c [simplification-2] maximum reduction of 14% = max (1%, 14%)
c [simplification-2] large reduction 14% >= 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 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 25221 quaternary clauses 52% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 306 single-self-subsuming ternary resolvents
c [quatres-1-2] added 488 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 6718 free variables schedulable
c [ternres-1] 3988 ternary resolvents (18 bin, 3970 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] found 8 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 10 out of 10 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 10331 xors of average arity 3.4
c [gauss-1] connected 34832 occurrences of 2983 variables (average 11.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 9549 occurrences of 2983 variables (average 3.2)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 80 tauts, 0 hbrs, 84 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 13 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 812 (0%) of length 6
c [cce-2-1] eliminated 10 clauses out of 19894 (0%) of length 5
c [cce-2-1] eliminated 26 clauses out of 24592 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 37 large clauses in 10854568 steps
c [cce-2-1] allowing another 5427284 steps for small clauses
c [cce-2-1] scheduling 15305 clauses = 641 binary + 14664 ternary
c [cce-2-1] tried to eliminate 15305 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 0%
c [cce-2-1] eliminated 5 ternary clauses 0%
c [cce-2-1] eliminated 7 small clauses 0%
c [cce-2-1] eliminated 7 small clauses in 7695842 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 44 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 5425048 steps for small clauses
c [cce-2-2] scheduling 15298 clauses = 639 binary + 14659 ternary
c [cce-2-2] tried to eliminate 15298 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 44 covered clauses in TOTAL during 2 rounds
c [cce-2] 44 < 1/100 * 62738 = 627 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 557 pos 36.9% + 953 neg 63.1% = 1510 sched 22.5% ret 5208
c [sweep-2-1] 253291 steps 625 queries 156.09 avg class size
c [sweep-2-1] 5304 decisions 624 SAT calls 14.69 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 2649 pos 39.4% + 4069 neg 60.6% = 6718 sched 100.0% ret 0
c [sweep-2-2] 746881 steps 546 queries 663.73 avg class size
c [sweep-2-2] 6153 decisions 545 SAT calls 19.35 avg env size
c [sweep-2-2] 3202 variables remain 48% (3516 retained 52%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 1169 queries)
c [sort-queue-3] sorted 6718 enqueued variables after 3000 conflicts
c [score-dist-3] active 0 (0%), one 4398 (65%), zero 2320 (35%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 0 variables 0.0% (6718 remain 71%)
c [simplification-3] removed 46 irredundant clauses 0.1% (62694 remain 85%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 33000 (soft 23000 + delta 10000)
c [simplification-3] new conflict limit 23000 (hard 33000)
c 
c [simplification-4] limit of 1720 ternary hit after 1720 ternaries
c [quatres-2] found 26918 quaternary clauses 51% in total
c [quatres-2-1] added 5 double-self-subsuming ternary resolvents
c [quatres-2-2] added 593 single-self-subsuming ternary resolvents
c [quatres-2-2] added 901 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 6718 free variables schedulable
c [ternres-2] 981 ternary resolvents (5 bin, 976 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 4996 literals 37%
c [treelook-2] scheduling used 150014 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150049 steps
c [treelook-2] 3614 literals remain 27%
c [treelook-2] 2993 variables remain to probed next time 45%
c [treelook-2] removed 0 variables, found 21 hbrs
c [transred-2] limit 408739 with penalty 0 = 0 + 0
c [transred-2] removed 10 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 6718 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6718 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 950 not tried 14% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 8 = 0% variables out of 6718 scheduled
c [elim-3] 8 < 1/100 * 6718 = 67 considered unsuccessful
c [bca-2] limit of 10000000 steps and 125796 added (scaled 2)
c [bca-2] 5249 out of 13422 literals actually usable 39%
c [bca-2] added 0 blocked clauses in 32137 steps
c [sort-queue-4] sorted 6710 enqueued variables after 12527 conflicts
c [score-dist-4] active 0 (0%), one 5340 (80%), zero 1370 (20%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 8 variables 0.1% (6710 remain 70%)
c [simplification-4] removed 46 irredundant clauses 0.1% (62648 remain 85%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] forced so keeping old conflict interval 20000
c [simplification-4] conflict limit remains at 23000 (hard 33000)
c [simplification-4] new ternary interval 10000
c 
c [simplification-5] limit 23000 conflicts (hard 33000) hit after 23001 conflicts
c [quatres-3] found 28597 quaternary clauses 50% in total
c [quatres-3-1] added 9 double-self-subsuming ternary resolvents
c [quatres-3-2] added 509 single-self-subsuming ternary resolvents
c [quatres-3-2] added 892 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 6710 free variables schedulable
c [ternres-3] 786 ternary resolvents (10 bin, 776 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4452 xors of average arity 3.0
c [gauss-2] connected 13356 occurrences of 1545 variables (average 8.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 909739 with penalty 0 = 0 + 0
c [transred-3] removed 5 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 43 clauses out of 19773 (0%) of length 5
c [cce-3-1] eliminated 161 clauses out of 24605 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 204 large clauses in 12928026 steps
c [cce-3-1] allowing another 6464013 steps for small clauses
c [cce-3-1] scheduling 914 clauses = 633 binary + 281 ternary
c [cce-3-1] tried to eliminate 914 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 5 ternary clauses 2%
c [cce-3-1] eliminated 6 small clauses 1%
c [cce-3-1] eliminated 6 small clauses in 6575957 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 210 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 4212024 steps for small clauses
c [cce-3-2] scheduling 908 clauses = 632 binary + 276 ternary
c [cce-3-2] tried to eliminate 908 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 210 covered clauses in TOTAL during 2 rounds
c [cce-3] 210 < 1/100 * 62648 = 626 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 1402 pos 43.8% + 1798 neg 56.2% = 3200 sched 47.7% ret 3510
c [sweep-3-1] 500637 steps 333 queries 286.02 avg class size
c [sweep-3-1] 7069 decisions 333 SAT calls 32.52 avg env size
c [sweep-3-1] 1325 variables remain 20% (5385 retained 80%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 332 queries)
c [sort-queue-5] sorted 6710 enqueued variables after 23001 conflicts
c [score-dist-5] active 0 (0%), one 5610 (84%), zero 1100 (16%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-5] removed 210 irredundant clauses 0.3% (62438 remain 85%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 40000
c [simplification-5] penalized conflict interval 40000 = 1 * 40000
c [simplification-5] hard conflict limit 83001 (soft 63001 + delta 20000)
c [simplification-5] new conflict limit 63001 (hard 83001)
c 
c [simplification-6] limit 63001 conflicts (hard 83001) hit after 63001 conflicts
c [quatres-4] found 32125 quaternary clauses 45% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 17 double-self-subsuming ternary resolvents
c [quatres-4-2] added 736 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1027 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6710 free variables schedulable
c [ternres-4] 1152 ternary resolvents (21 bin, 1131 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 5 at-most-one constraints of average size 3.0
c [card-3] found 12 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 17 out of 17 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 8690856 penalty 1 = 1 + 0
c [basicprobe-2-0] 1153 sched 17%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-2-1] 1158 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 21 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [unhide-3] limit 173817 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 6 tauts, 0 hbrs, 1310 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 14 transitive binary clauses
c [sort-queue-6] sorted 6710 enqueued variables after 63001 conflicts
c [score-dist-6] active 0 (0%), one 5919 (88%), zero 791 (12%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-6] removed 1 irredundant clauses 0.0% (62437 remain 85%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 40000
c [simplification-6] new conflict interval 80000
c [simplification-6] penalized conflict interval 80000 = 1 * 80000
c [simplification-6] hard conflict limit 183001 (soft 143001 + delta 40000)
c [simplification-6] new conflict limit 143001 (hard 183001)
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 -   24.7    6710    62437     89927   35207  14938   602    9   380   11   2%    760  112    9    6  151%
c 
c [simplification-7] limit 143001 conflicts (hard 183001) hit after 143001 conflicts
c [quatres-5] found 36378 quaternary clauses 40% in total
c [quatres-5-1] added 13 double-self-subsuming ternary resolvents
c [quatres-5-2] added 627 single-self-subsuming ternary resolvents
c [quatres-5-2] added 991 quaternary resolvents
c [ternres-5] limit 10192063 with penalty 0 = 0 + 0
c [ternres-5] all 6710 free variables schedulable
c [ternres-5] 505 ternary resolvents (9 bin, 496 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 10 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 6710 variables 100%
c [block-3] limit of 25480158 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-4] 950 variables 14% will be scheduled this time
c [elim-4] scheduled 950 variables 14%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1019206325 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 6630032 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 950 scheduled
c [bca-3] limit of 10000000 steps and 125212 added (scaled 2)
c [bca-3] 2573 out of 13422 literals actually usable 19%
c [bca-3] added 0 blocked clauses in 97856 steps
c [sort-queue-7] sorted 6710 enqueued variables after 143001 conflicts
c [score-dist-7] active 0 (0%), one 5997 (89%), zero 713 (11%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-7] removed 81 irredundant clauses 0.1% (62356 remain 85%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 80000
c [simplification-7] new conflict interval 160000
c [simplification-7] penalized conflict interval 160000 = 1 * 160000
c [simplification-7] hard conflict limit 383001 (soft 303001 + delta 80000)
c [simplification-7] new conflict limit 303001 (hard 383001)
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 -   44.0    6710    62356    155605   50007  17158   624   10   385   12   3%    927   44   10    8  130%
c -   61.7    6710    62356    221507   66642  17998   643   11   415   13   3%    989   33   11   10  115%
c -   77.1    6710    62356    281447   77673  18416   647   12   425   14   3%   1010   18   13   11  115%
c 
c [simplification-8] limit 303001 conflicts (hard 383001) hit after 303002 conflicts
c [quatres-6] found 41630 quaternary clauses 34% in total
c [quatres-6-1] removed 6 duplicate quaternary clauses
c [quatres-6-1] added 12 double-self-subsuming ternary resolvents
c [quatres-6-2] added 530 single-self-subsuming ternary resolvents
c [quatres-6-2] added 828 quaternary resolvents
c [ternres-6] limit 22407657 with penalty 0 = 0 + 0
c [ternres-6] all 6710 free variables schedulable
c [ternres-6] 375 ternary resolvents (6 bin, 369 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1120382 penalty 2 = 2 + 0
c [gauss-3] extracted 3158 xors of average arity 3.0
c [gauss-3] connected 9474 occurrences of 1545 variables (average 6.1)
c [gauss-3] limit 1120382 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1926 schedulable variables 29%
c [simpleprobe-3] limit 44815315 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 73 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 52 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 280095722 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 45 clauses out of 19523 (0%) of length 5
c [cce-4-1] eliminated 300 clauses out of 24422 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 345 large clauses in 10575174 steps
c [cce-4-1] allowing another 5287587 steps for small clauses
c [cce-4-1] scheduling 980 clauses = 635 binary + 345 ternary
c [cce-4-1] tried to eliminate 980 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 1 small clauses 0%
c [cce-4-1] eliminated 1 small clauses in 5397118 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 346 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 5220382 steps for small clauses
c [cce-4-2] scheduling 979 clauses = 634 binary + 345 ternary
c [cce-4-2] tried to eliminate 979 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 346 covered clauses in TOTAL during 2 rounds
c [cce-4] 346 < 1/100 * 62356 = 623 considered unsuccessful
c [sweep-4] limit 1680574 penalty 2 = 2 + 0
c [sweep-4-1] 618 pos 46.6% + 707 neg 53.4% = 1325 sched 19.7% ret 5385
c [sweep-4-1] 899122 steps 377 queries 73.87 avg class size
c [sweep-4-1] 11472 decisions 376 SAT calls 54.27 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 3249 pos 48.4% + 3461 neg 51.6% = 6710 sched 100.0% ret 0
c [sweep-4-2] 784609 steps 108 queries 642.52 avg class size
c [sweep-4-2] 7052 decisions 107 SAT calls 145.84 avg env size
c [sweep-4-2] 3490 variables remain 52% (3220 retained 48%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 483 queries)
c [sort-queue-8] sorted 6710 enqueued variables after 303002 conflicts
c [score-dist-8] active 0 (0%), one 6127 (91%), zero 583 (9%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-8] removed 346 irredundant clauses 0.6% (62010 remain 84%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 80000 = 160000 / 2
c [simplification-8] new conflict interval 240000
c [simplification-8] penalized conflict interval 240000 = 1 * 240000
c [simplification-8] hard conflict limit 663002 (soft 543002 + delta 120000)
c [simplification-8] new conflict limit 543002 (hard 663002)
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 -   92.0    6710    62010    341156   87286  19623   681   14   430   15   3%   1018    9   14   12  116%
c -  105.4    6710    62010    401294   96929  19831   683   15   453   16   3%   1022   21   16   13  121%
c -  118.0    6710    62010    461378  105536  20048   687   15   464   16   3%   1023   19   17   14  117%
c -  130.2    6710    62010    521827  113609  20248   695   16   462   17   3%   1024   14   18   15  117%
c 
c [simplification-9] limit 543002 conflicts (hard 663002) hit after 543004 conflicts
c [quatres-7] found 45727 quaternary clauses 29% in total
c [quatres-7-1] removed 23 duplicate quaternary clauses
c [quatres-7-1] added 5 double-self-subsuming ternary resolvents
c [quatres-7-2] added 344 single-self-subsuming ternary resolvents
c [quatres-7-2] added 705 quaternary resolvents
c [ternres-7] limit 37196231 with penalty 0 = 0 + 0
c [ternres-7] all 6710 free variables schedulable
c [ternres-7] 281 ternary resolvents (8 bin, 273 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 18 transitive binary clauses
c [sort-queue-9] sorted 6710 enqueued variables after 543004 conflicts
c [score-dist-9] active 0 (0%), one 6187 (92%), zero 523 (8%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-9] removed 0 irredundant clauses 0.0% (62010 remain 84%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 240000
c [simplification-9] new conflict interval 480000
c [simplification-9] penalized conflict interval 480000 = 1 * 480000
c [simplification-9] hard conflict limit 1263004 (soft 1023004 + delta 240000)
c [simplification-9] new conflict limit 1023004 (hard 1263004)
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 -  142.6    6710    62010    582765  121709  20991   686   17   461   18   4%   1024    6   18   16  114%
c -  155.2    6710    62010    644136  129798  21116   687   18   452   18   4%   1024   -5   20   17  119%
c -  167.8    6710    62010    705715  137907  21235   694   19   468   19   4%   1024   11   21   18  123%
c -  180.2    6710    62010    766991  146355  21347   701   19   468   20   4%   1024    8   22   18  121%
c -  192.5    6710    62010    827493  153202  21452   703   19   469   20   4%   1024    2   20   18  107%
c -  205.2    6710    62010    888619  159984  21552   707   19   470   21   4%   1024    3   16   19   86%
c -  218.6    6710    62010    950234  166927  21633   709   19   469   21   4%   1024    1   20   19  105%
c -  232.4    6710    62010   1011921  173366  21697   710   20   465   22   4%   1024   -2   23   19  119%
c 
c [simplification-10] limit 1023004 conflicts (hard 1263004) hit after 1027419 conflicts
c [quatres-8] found 50831 quaternary clauses 24% in total
c [quatres-8-1] removed 20 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 300 single-self-subsuming ternary resolvents
c [quatres-8-2] added 860 quaternary resolvents
c [ternres-8] limit 67774323 with penalty 0 = 0 + 0
c [ternres-8] all 6710 free variables schedulable
c [ternres-8] 191 ternary resolvents (5 bin, 186 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4235895 penalty 3 = 3 + 0
c [card-4] found 6 at-most-one constraints of average size 3.0
c [card-4] found 21 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4235895 for elimination
c [card-4] 26 out of 27 constraints (96%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1694358 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 1079 tauts, 0 hbrs, 10178 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 12 transitive binary clauses
c [sort-queue-10] sorted 6710 enqueued variables after 1027419 conflicts
c [score-dist-10] active 0 (0%), one 6454 (96%), zero 256 (4%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (6710 remain 70%)
c [simplification-10] removed 0 irredundant clauses 0.0% (62010 remain 84%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 480000
c [simplification-10] new conflict interval 960000
c [simplification-10] penalized conflict interval 960000 = 1 * 960000
c [simplification-10] hard conflict limit 2467419 (soft 1987419 + delta 480000)
c [simplification-10] new conflict limit 1987419 (hard 2467419)
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 -  247.3    6710    62010   1074387  180288  21379   705   19   476   22   4%   1024   10   14   19   72%
c -  261.8    6710    62010   1137351  186923  21456   706   20   481   23   4%   1024   15   17   20   87%
c -  276.6    6710    62010   1200675  193354  21537   707   21   470   23   4%   1024    1   24   20  120%
c -  291.8    6710    62010   1264400  199433  21615   708   20   470   24   4%   1024   -5   19   20   94%
c -  307.3    6710    62010   1328683  205705  21664   709   22   480   25   4%   1024    8   25   21  120%
c -  323.4    6710    62010   1393123  210820  21712   710   21   456   25   5%   1024  -19   25   21  119%
c -  339.5    6710    62010   1459510  218048  21786   710   21   481   25   4%   1024    5   23   21  110%
c -  355.9    6710    62010   1525742  224071  21870   711   20   489   26   4%   1024   14   20   21   97%
c -  373.2    6710    62010   1592704  229975  21941   713   22   457   27   5%   1024  -14   21   21   97%
c -  391.5    6710    62010   1660617  235708  22029   716   22   467   27   5%   1024   -5   21   21   98%
c -  409.6    6710    62010   1729660  242677  22104   718   21   447   27   5%   1024  -25   22   22  103%
c -  429.0    6710    62010   1798225  248325  22183   719   23   475   28   5%   1024    1   23   22  104%
c -  447.7    6710    62010   1868019  254528  22274   720   21   482   28   4%   1024    7   26   22  120%
c -  467.8    6710    62010   1938506  260389  22367   722   23   472   29   5%   1024   -3   25   22  116%
c 
c [simplification-11] limit 1987419 conflicts (hard 2467419) hit after 1989136 conflicts
c [quatres-9] found 57170 quaternary clauses 19% in total
c [quatres-9-1] removed 47 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 516 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1044 quaternary resolvents
c [ternres-9] limit 142290244 with penalty 0 = 0 + 0
c [ternres-9] all 6710 free variables schedulable
c [ternres-9] 364 ternary resolvents (3 bin, 361 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 3557256 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 6386 literals 48%
c [treelook-3] scheduling used 1117100 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3557256 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 741254 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 4 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 6 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6710 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 6710 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 4 variables 0% in round 1 in 16235308 steps
c [elim-5-1] backward subsumption/strengthening limit 16235300
c [elim-5-1-1] backward checking 27 touched variables 0%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 3 and strengthened 2 clauses in 51714 steps
c [elim-5-1] rescheduled 11 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 10524 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 4 = 0% variables out of 6710 scheduled
c [elim-5] 4 < 1/100 * 6710 = 67 considered unsuccessful
c [bca-4] limit of 10000000 steps and 124332 added (scaled 2)
c [bca-4] 569 out of 13414 literals actually usable 4%
c [bca-4] added 0 blocked clauses in 313104 steps
c [sort-queue-11] sorted 6706 enqueued variables after 1989136 conflicts
c [score-dist-11] active 0 (0%), one 6651 (99%), zero 55 (1%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 4 variables 0.1% (6706 remain 70%)
c [simplification-11] removed 94 irredundant clauses 0.2% (61916 remain 84%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 960000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3489136 (soft 2989136 + delta 500000)
c [simplification-11] new conflict limit 2989136 (hard 3489136)
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 -  490.0    6706    61916   2010378  266957  23242   715   22   463   29   5%   1024  -12   27   22  125%
c -  511.4    6706    61916   2082167  272279  23281   716   22   476   30   5%   1024    2   23   22  106%
c -  533.1    6706    61916   2155355  278278  23328   717   23   492   31   5%   1024   17   22   22   98%
c -  555.1    6706    61916   2229354  284353  23395   718   22   472   31   5%   1024   -5   22   22   99%
c -  577.7    6706    61916   2304419  290983  23492   720   22   467   32   5%   1024   -6   26   22  116%
c -  601.0    6706    61916   2379567  296841  23554   721   22   461   32   5%   1024  -12   24   22  107%
c -  625.5    6706    61916   2455782  302457  23630   721   23   481   33   5%   1024    6   22   22  101%
c -  650.0    6706    61916   2533586  309541  23728   724   22   458   33   5%   1024  -18   19   22   84%
c -  674.5    6706    61916   2611314  316106  23848   725   23   480   34   5%   1024    7   22   22   99%
c -  700.3    6706    61916   2689150  322066  23943   727   21   493   34   4%   1024   18   18   23   80%
c -  726.6    6706    61916   2768689  328342  24043   730   23   476   35   5%   1024    1   21   23   91%
c -  753.9    6706    61916   2849237  334520  24190   733   24   471   35   5%   1024   -1   20   23   88%
c -  781.6    6706    61916   2930212  340095  24243   734   20   474   36   4%   1024   -1   19   23   85%
c 
c [simplification-12] limit 2989136 conflicts (hard 3489136) hit after 2990658 conflicts
c [quatres-10] found 62742 quaternary clauses 17% in total
c [quatres-10-1] removed 47 duplicate quaternary clauses
c [quatres-10-1] added 14 double-self-subsuming ternary resolvents
c [quatres-10-2] added 497 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1051 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 6706 free variables schedulable
c [ternres-10] 341 ternary resolvents (8 bin, 333 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5930117 penalty 3 = 3 + 0
c [gauss-4] extracted 23028 xors of average arity 3.7
c [gauss-4] connected 85692 occurrences of 6580 variables (average 13.0)
c [gauss-4] limit 5930117 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 5 transitive binary clauses
c [cce-5] limit of 148252936 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 37 clauses out of 19280 (0%) of length 5
c [cce-5-1] eliminated 264 clauses out of 24142 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 301 large clauses in 12363752 steps
c [cce-5-1] allowing another 6181876 steps for small clauses
c [cce-5-1] scheduling 15416 clauses = 633 binary + 14783 ternary
c [cce-5-1] tried to eliminate 15416 small clauses 100%
c [cce-5-1] eliminated 2 binary clauses 0%
c [cce-5-1] eliminated 3 ternary clauses 0%
c [cce-5-1] eliminated 5 small clauses 0%
c [cce-5-1] eliminated 5 small clauses in 8763504 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 306 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 6120396 steps for small clauses
c [cce-5-2] scheduling 15411 clauses = 631 binary + 14780 ternary
c [cce-5-2] tried to eliminate 15411 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 306 covered clauses in TOTAL during 2 rounds
c [cce-5] 306 < 1/100 * 61916 = 619 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 88951761 penalty 3 = 3 + 0
c [sweep-5-1] 1726 pos 49.5% + 1763 neg 50.5% = 3489 sched 52.0% ret 3217
c [sweep-5-1] 4144111 steps 306 queries 79.58 avg class size
c [sweep-5-1] 24067 decisions 308 SAT calls 345.46 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 3332 pos 49.7% + 3374 neg 50.3% = 6706 sched 100.0% ret 0
c [sweep-5-2] 4998105 steps 344 queries 162.66 avg class size
c [sweep-5-2] 28596 decisions 343 SAT calls 436.76 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 3332 pos 49.7% + 3374 neg 50.3% = 6706 sched 100.0% ret 0
c [sweep-5-3] 4899315 steps 347 queries 153.17 avg class size
c [sweep-5-3] 27120 decisions 348 SAT calls 393.16 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 994 queries)
c [sort-queue-12] sorted 6706 enqueued variables after 2990658 conflicts
c [score-dist-12] active 0 (0%), one 6706 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (6706 remain 70%)
c [simplification-12] removed 306 irredundant clauses 0.5% (61610 remain 84%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] hard conflict limit 4490658 (soft 3990658 + delta 500000)
c [simplification-12] new conflict limit 3990658 (hard 4490658)
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 -  814.5    6706    61610   3012626  347842  25230   756   23   467   36   5%   1024   -8   25   23  108%
c -  843.4    6706    61610   3095651  353896  25299   756   22   478   37   5%   1024    3   20   22   89%
c -  874.0    6706    61610   3179821  359667  25362   757   22   462   37   5%   1024  -14   23   22  105%
c -  905.0    6706    61610   3266104  366522  25474   758   23   481   38   5%   1024    3   29   22  134%
c -  937.7    6706    61610   3352685  372459  25540   759   22   475   39   5%   1024   -4   23   22  104%
c -  970.6    6706    61610   3440735  380344  25607   760   23   472   39   5%   1024   -3   21   22   94%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1 basic ate = 1 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 493291 steps
c bkwd: tried 16028 clauses, 32025 lits, 2.00 lits/clause
c bkwd: checked 543479 occs, 33.91 occs/clause, 16.97 occs/lit
c bkwd: subsumed 0 binary, 17 ternary, 1 large
c bkwd: strengthened 0 binary, 15 ternary (100% self), 11 large (0% self)
c blkd: 4 bces, 0 removed, 2312721 resolutions, 4886031 steps
c blkd: 2 blocking literals 0%, 0 pure
c bump: 3499158 bumped seen, 203076859 lits 58.0 on average
c card: 4 count, 3 units, 0 am1, 7927914 steps
c card: 58 rescheduled, 247 eliminated, 37670 resolved, 1799 subsumed
c card: 16 at-most-one constraints found, average size 3.00
c card: 16 at-most-one constraints used 100%, average size 3.00
c card: 161 at-most-two constraints found, average size 4.00
c card: 160 at-most-two constraints used 99%, average size 4.00
c cces: 5 cces, 10673 eliminated, 10671 ate 100%, 2 abce 0%
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: 362166 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 46 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 29 decompositions, 27 equivalent 0%
c deco: 337 decision-only clauses 0%, 40% reduction
c decs: 37022053 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 2783 eliminated 29%, 0 pure 0%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 2783 small 100%, 0 large 0%
c elms: 18642 tried small, 2783 succeeded 15%, 15859 failed 85%
c elms: 338 subsumed, 177 strengthened, 0 blocked
c elms: 1432941 copies, 2635015 resolutions, 1797311 ipos
c elms: 48061 subchks, 48255 strchks
c gaus: 4 extractions, 40969 extracted, 3.5 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 19461382 steps, 9730691 extr 50%, 8399373 elim 43%
c glue: 19.9 orig avg, 19.9 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 623 = 441 simple 71% + 170 trn 27% + 12 lrg 2%, 11 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3499157 clauses, 38.4 length
c lrnd: 134498137 lits = 141824092 orig - 7325955 removed 5%
c lrnd: 1592129 uips 46%, 1457435 flips 42%
c mins: 3215433 mins 92%, 68 bin 0%, 281816 size 8%
c mins: 114864025 poisoned searches, 8432798 hits, 7% hit rate
c mins: 232528089 used twice searches, 43922392 hits, 19% hit rate
c move: moved 310, 9 bin 3%, 301 trn 97%
c otfs: 19357 driving 45%, 23293 restarting 55%
c otfs: str 42650, 42066 red 99%, 584 irr 1%
c otfs: str 42650, 0 bin 0%, 358 trn 1%, 42292 lrg 99%
c otfs: sub 557, 557 red 100%, 0 irr 0%
c otfs: sub 557, 0 bin 0%, 99 trn 18%, 458 lrg 82%
c phas: 1 computed, 6759 set, 0 pos (0%), 6759 neg (100%)
c prbs: 2 basic, 7668 probed, 0 failed, 0 lifted
c prbs: 3 simple, 33717 probed, 4 failed, 24 eqs
c prbs: 3 treelook, 10668 probed, 0 failed, 0 lifted
c prom: 345691 locked 28% out of 1250341 tried
c prps: 656423776 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 8787 quat, 4958 self1, 86 self2, 145 dup
c queu: 12 sorted, 37022053 next (201 steps 0.00)
c queu: 203166970 enq (203166946 steps 1.00), 203076859 deq 100%
c redc: 3727 clauses 1%, 713415 tried 20%, 1 sat 0%
c redc: 3843 lits 0%, 5816269 tried 4%, 1 sat 0%
c redc: 125 times jump level reduced, 12.8 levels on average
c reds: 49 count, 71776.2 conflicts per reduce
c reds: 0 memlim 0%, 49 arith 100%
c reds: 1774479 collected 59%, 1242512 retired 41%
c rmbd: 72 removed, 72 red 100%
c rsts: 36168 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 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: 12 count, 11 confs 92%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 8%
c subl: 3499157 count (3451962 tried 1.0), 15181 sub out of 3488503 (0.4%)
c swps: 5 count, 9 rounds, 3835 queries (426.1/round)
c swps: 3846 sat calls, 12 unsat (0.4% success rate)
c swps: 124960 decisions 32.5, 1482 conflicts 0.4
c swps; 331.7 avg class size, 123.2 avg environment size
c swps: 0 failed, 1 impls, 1 equivs
c swp0: 1274 type 0 queries, 18 unsat (1.4%), 1274 sat (100.0%)
c swp1: 2561 type 1 queries, 92 unsat (3.6%), 2560 sat (100.0%)
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: 81042662 calls to obtain time
c tops: 18 fixed 0%, 0 its, 0.00 confs/it
c trds: 10 transitive reductions, 145 removed, 0 failed
c trds: 133905 nodes, 12330 edges, 19624 steps
c trim: 122692 words, 0.5 MB
c trnr: 10 count, 93 bin, 8871 trn, 47309068 steps
c unhd: 4 count, 5 rounds, 2959828 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1249 tauts, 0 bin 0%, 1040 trn 83%, 192 lrg 15%
c unhd: 1249 tauts, 17 stamp 1%, 1207 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 11636 str, 0 bin 0%, 131 trn 1%, 11505 lrg 99%, 11551 red 99%
c vars: 6706 remaining 70% and 2828 removed 30% out of 9534
c vars: 18 fixed 0%, 2783 eliminated 29%, 27 equivalent 0%
c vsts: 29377613828 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 44.8 search visits per propagation, 8348.2 per conflict
c wchs: 9902644075 pushed, 16316926 enlarged, 1056 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3497290       1774479       1242512     186540680      26961967       1686534
c 
c  0 0        376686  11       551   0         0   0 169818300  91< 22519456  84<  1409606  84<   11.5
c  1 5        266375   8    133997   8    115450   9   8839209   5   1470042   5    101590   6     0.6
c  2 6        707820  20    368306  21    316915  26   4113095   2   1047811   4     66455   4     1.1
c  3 9        676965  19    375137  21    282951  23   1479011   1    658204   2     35354   2     1.3
c  4 14       482440  14<   286414  16<   182330  15<   865763   0    449777   2     24484   1     1.5
c  5 21       326540   9    200231  11    116481   9    520976   0    290302   1     16026   1     1.6
c  6 30       223432   6    139029   8     77404   6    326841   0    187963   1     10577   1     1.7
c  7 41       154940   4     97681   6     52184   4    213387   0    126093   0      7571   0     1.7
c  8 54       106630   3     67661   4     35432   3    141150   0     84174   0      5292   0     1.7
c  9 69        72582   2     45890   3     24251   2     94009   0     55860   0      3707   0     1.6
c 10 86        76222   2     45913   3     27267   2     96336   0     55650   0      4260   0     2.5
c 11 126       25625   1     13279   1     11282   1     31414   0     16109   0      1562   0     1.3
c 12 230        1015   0       381   0       559   0      1169   0       514   0        50   0     0.1
c 13 534          18   0         9   0         6   0        20   0        12   0         0   0     0.0
c 
c avg                  3.5           4.1           3.7           0.2           0.5           0.5
c std                  2.5           2.3           2.2           0.8           1.4           1.4
c 
c   26.024   3% decide
c   16.050   2% bump
c    2.508   0% cce
c 
c    7.453 < 1% rest (below)
c 
c    2.503   0% elim
c    2.498   0% sweep
c    1.845   0% quatres
c    0.845   0% gauss
c    0.802   0% probe
c    0.436   0% block
c    0.344   0% ternres
c    0.259   0% unhide
c    0.240   0% bca
c    0.161   0% card
c    0.023   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.751   0% preprocessing     5%
c   13.134   1% inprocessing     95%
c ==================================
c   13.885   1% simplifying
c  986.155  99% search
c ==================================
c 1000.041 100% all
c 
c       3517033 conflicts,        3516.9 confs/sec
c         10343 ternaries,         340.0 confs/ternary
c            87 binaries,        40425.7 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            49 reductions,          0.0 redus/sec,  71776.2 confs/reduction
c         36168 restarts,           36.2 rests/sec,     97.2 confs/restart
c      37022053 decisions,       37020.5 decis/sec,     10.5 decis/conflict
c     656423776 propagations,   656397.1 props/sec,     17.7 props/decision
c 
c 1000.0 seconds, 95.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
