c launch: /data/cnf/sc2014/app/MD5-28-5.cnf.bz2
c host: atom26
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/MD5-28-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-28-5.cnf.bz2
c no embedded options
c found 'p cnf 8279 62533' header
c read 8279 variables, 62533 clauses, 243687 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 --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 8270 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 
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    8270    62320         0       0      0     0    0     0    3   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 4 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] 124 out of 124 constraints (100%) meet size limits
c [card-1] found 5 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 8247 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 15 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 15 variables, found 331 hbrs, 5 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 8232 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 2590 variables 31% in round 1 in 9105617 steps
c [elim-1-1] backward subsumption/strengthening limit 9105600
c [elim-1-1-1] backward checking 5593 touched variables 68%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 82 and strengthened 155 clauses in 1211943 steps
c [elim-1-1] rescheduled 246 variables 3% by backward subsumption
c [elim-1-2] eliminated 43 variables 1% in round 2 in 590451 steps
c [elim-1-2] backward subsumption/strengthening limit 590400
c [elim-1-2-1] backward checking 236 touched variables 3%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 40 and strengthened 183 clauses in 295271 steps
c [elim-1-2] rescheduled 172 variables 2% by backward subsumption
c [elim-1-3] eliminated 3 variables 0% in round 3 in 499645 steps
c [elim-1-3] backward subsumption/strengthening limit 499600
c [elim-1-3-1] backward checking 93 touched variables 1%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 0 and strengthened 0 clauses in 166277 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2636 = 32% variables out of 8232 scheduled
c [phase-count-1] 57604 negative 99.1% of 58132 except 528 0.9%
c [phase-count-1] 55936 positive 96.2% of 58132 except 2196 3.8%
c [phase-count-1] less non-negative clauses 528 than limit 5800 (10.0%)
c [phase-count-1] non-pos/non-neg = 2196/528 = 4.16 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 5596 negative 100%
c [sort-queue-1] sorted 5596 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5596 (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 2674 variables 32.3% (5596 remain 68%)
c [simplification-1] removed 4188 irredundant clauses 6.7% (58132 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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 [decomp-3] removed 1 variables
c [simpleprobe-2] all 5595 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2445 variables remain 44% (3150 retained 56%)
c [simpleprobe-2] removed 0 variables, found 19 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 11190 literals 100%
c [treelook-1] scheduling used 278373 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300121 steps
c [treelook-1] 8207 literals remain 73%
c [treelook-1] 4663 variables remain to probed next time 83%
c [treelook-1] removed 0 variables, found 54 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 612 sched 11%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-1-1] 622 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 623 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 19 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5595 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 155 blocked clauses
c [block-1] 155 < 1/100 * 58130 = 581 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 118 clauses out of 950 (12%) of length 6
c [cce-1-1] eliminated 7487 clauses out of 22651 (33%) of length 5
c [cce-1-1] eliminated 337 clauses out of 19706 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7942 large clauses in 9394132 steps
c [cce-1-1] allowing another 4697066 steps for small clauses
c [cce-1-1] scheduling 889 clauses = 452 binary + 437 ternary
c [cce-1-1] tried to eliminate 889 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 1%
c [cce-1-1] eliminated 87 ternary clauses 20%
c [cce-1-1] eliminated 91 small clauses 10%
c [cce-1-1] eliminated 91 small clauses in 4796260 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 8033 covered clauses in round 1
c [cce-1-2] eliminated 4 clauses out of 832 (0%) of length 6
c [cce-1-2] eliminated 35 clauses out of 15164 (0%) of length 5
c [cce-1-2] eliminated 44 clauses out of 19369 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 83 large clauses in 8325431 steps
c [cce-1-2] allowing another 4162715 steps for small clauses
c [cce-1-2] scheduling 798 clauses = 448 binary + 350 ternary
c [cce-1-2] tried to eliminate 798 small clauses 100%
c [cce-1-2] eliminated 1 ternary clauses 0%
c [cce-1-2] eliminated 1 small clauses 0%
c [cce-1-2] eliminated 1 small clauses in 4259543 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 84 covered clauses in round 2
c [cce-1-3] eliminated 2 clauses out of 828 (0%) of length 6
c [cce-1-3] eliminated 34 clauses out of 15129 (0%) of length 5
c [cce-1-3] eliminated 28 clauses out of 19325 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 64 large clauses in 9426930 steps
c [cce-1-3] allowing another 4713465 steps for small clauses
c [cce-1-3] scheduling 797 clauses = 448 binary + 349 ternary
c [cce-1-3] tried to eliminate 797 small clauses 100%
c [cce-1-3] eliminated 4 ternary clauses 1%
c [cce-1-3] eliminated 4 small clauses 1%
c [cce-1-3] eliminated 4 small clauses in 4817627 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 68 covered clauses in round 3
c [cce-1] eliminated 8185 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5584 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 221 variables 4% in round 1 in 11918921 steps
c [elim-2-1] backward subsumption/strengthening limit 8081079
c [elim-2-1-1] backward checking 562 touched variables 10%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 38 clauses in 152953 steps
c [elim-2-1] rescheduled 70 variables 1% by backward subsumption
c [elim-2-2] eliminated 1 variables 0% in round 2 in 200673 steps
c [elim-2-2] backward subsumption/strengthening limit 200600
c [elim-2-2-1] backward checking 5 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 50564 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 222 = 4% variables out of 5584 scheduled
c [bca-1] limit of 10000000 steps and 95912 added (scaled 2)
c [bca-1] 9053 out of 10726 literals actually usable 84%
c [bca-1] added 0 blocked clauses in 36177 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1998 pos 37.3% + 3364 neg 62.7% = 5362 sched 100.0% ret 0
c [sweep-1-1] 826198 steps 1068 queries 307.21 avg class size
c [sweep-1-1] 8786 decisions 1070 SAT calls 14.73 avg env size
c [sweep-1-1] fully completed sweeping round
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-1-2] 1998 pos 37.3% + 3364 neg 62.7% = 5362 sched 100.0% ret 0
c [sweep-1-2] 174110 steps 170 queries 1102.34 avg class size
c [sweep-1-2] 1738 decisions 169 SAT calls 18.09 avg env size
c [sweep-1-2] 4621 variables remain 86% (741 retained 14%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 0 vars in TOTAL (2 rounds, 1236 queries)
c [sort-queue-2] sorted 5362 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 2744 (51%), zero 2618 (49%)
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 234 variables 4.2% (5362 remain 65%)
c [simplification-2] removed 10426 irredundant clauses 17.9% (47706 remain 77%)
c [simplification-2] maximum reduction of 18% = max (4%, 18%)
c [simplification-2] large reduction 18% >= 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 19228 quaternary clauses 53% in total
c [quatres-1-2] added 277 single-self-subsuming ternary resolvents
c [quatres-1-2] added 542 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 5362 free variables schedulable
c [ternres-1] 3817 ternary resolvents (70 bin, 3747 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 at-most-one constraints of average size 3.0
c [card-2] found 27 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 26 out of 28 constraints (93%) 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 14412 xors of average arity 3.6
c [gauss-1] connected 51917 occurrences of 4232 variables (average 12.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 167 tauts, 0 hbrs, 147 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 26 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 19 clauses out of 14416 (0%) of length 5
c [cce-2-1] eliminated 62 clauses out of 18600 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 81 large clauses in 7520024 steps
c [cce-2-1] allowing another 3760012 steps for small clauses
c [cce-2-1] scheduling 12586 clauses = 474 binary + 12112 ternary
c [cce-2-1] tried to eliminate 12586 small clauses 100%
c [cce-2-1] eliminated 6 binary clauses 1%
c [cce-2-1] eliminated 198 ternary clauses 2%
c [cce-2-1] eliminated 204 small clauses 2%
c [cce-2-1] eliminated 204 small clauses in 5444383 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 285 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 3749041 steps for small clauses
c [cce-2-2] scheduling 12382 clauses = 468 binary + 11914 ternary
c [cce-2-2] tried to eliminate 12382 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 285 covered clauses in TOTAL during 2 rounds
c [cce-2] 285 < 1/100 * 47701 = 477 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5360 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 188 variables 4% in round 1 in 11434564 steps
c [elim-3-1] backward subsumption/strengthening limit 8565436
c [elim-3-1-1] backward checking 304 touched variables 6%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 3 and strengthened 21 clauses in 90923 steps
c [elim-3-1] rescheduled 40 variables 1% by backward subsumption
c [elim-3-2] eliminated 8 variables 0% in round 2 in 87110 steps
c [elim-3-2] backward subsumption/strengthening limit 87100
c [elim-3-2-1] backward checking 14 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 5 and strengthened 8 clauses in 47974 steps
c [elim-3-2] rescheduled 12 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 27164 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 196 = 4% variables out of 5360 scheduled
c [sort-queue-3] sorted 5164 enqueued variables after 3000 conflicts
c [score-dist-3] active 0 (0%), one 3425 (66%), zero 1739 (34%)
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 198 variables 3.7% (5164 remain 62%)
c [simplification-3] removed 1873 irredundant clauses 3.9% (45833 remain 74%)
c [simplification-3] maximum reduction of 4% = max (4%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 17000 (soft 7000 + delta 10000)
c [simplification-3] new conflict limit 7000 (hard 17000)
c 
c [simplification-4] limit 7000 conflicts (hard 17000) hit after 7001 conflicts
c [quatres-2] found 19645 quaternary clauses 53% in total
c [quatres-2-1] added 5 double-self-subsuming ternary resolvents
c [quatres-2-2] added 365 single-self-subsuming ternary resolvents
c [quatres-2-2] added 739 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5164 free variables schedulable
c [ternres-2] 684 ternary resolvents (8 bin, 676 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5425 literals 53%
c [treelook-2] scheduling used 150011 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150032 steps
c [treelook-2] 3907 literals remain 38%
c [treelook-2] 3262 variables remain to probed next time 63%
c [treelook-2] removed 0 variables, found 26 hbrs
c [transred-2] limit 197750 with penalty 0 = 0 + 0
c [transred-2] removed 23 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5164 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 596 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5074 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 29 variables 1% in round 1 in 11138449 steps
c [elim-4-1] backward subsumption/strengthening limit 11138400
c [elim-4-1-1] backward checking 78 touched variables 2%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 9 clauses in 48988 steps
c [elim-4-1] rescheduled 18 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 25106 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 29 = 1% variables out of 5074 scheduled
c [elim-4] 29 < 1/100 * 5074 = 50 considered unsuccessful
c [bca-2] limit of 10000000 steps and 90368 added (scaled 2)
c [bca-2] 3877 out of 10092 literals actually usable 38%
c [bca-2] added 0 blocked clauses in 20943 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 2017 pos 46.3% + 2344 neg 53.7% = 4361 sched 86.4% ret 684
c [sweep-2-1] 500459 steps 460 queries 333.92 avg class size
c [sweep-2-1] 6419 decisions 459 SAT calls 22.59 avg env size
c [sweep-2-1] 1283 variables remain 25% (3762 retained 75%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 459 queries)
c [sort-queue-4] sorted 5045 enqueued variables after 7001 conflicts
c [score-dist-4] active 0 (0%), one 4086 (81%), zero 959 (19%)
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 119 variables 2.3% (5045 remain 61%)
c [simplification-4] removed 899 irredundant clauses 2.0% (44934 remain 72%)
c [simplification-4] maximum reduction of 2% = max (2%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 10666
c [simplification-4] penalized conflict interval 10666 = 1 * 10666
c [simplification-4] hard conflict limit 27667 (soft 17667 + delta 10000)
c [simplification-4] new conflict limit 17667 (hard 27667)
c 
c [simplification-5] limit 17667 conflicts (hard 27667) hit after 17667 conflicts
c [quatres-3] found 21104 quaternary clauses 51% in total
c [quatres-3-1] added 10 double-self-subsuming ternary resolvents
c [quatres-3-2] added 607 single-self-subsuming ternary resolvents
c [quatres-3-2] added 918 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5045 free variables schedulable
c [ternres-3] 645 ternary resolvents (6 bin, 639 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4784 xors of average arity 3.0
c [gauss-2] connected 14352 occurrences of 1286 variables (average 11.2)
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 613969 with penalty 0 = 0 + 0
c [transred-3] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5045 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 158 blocked clauses
c [block-3] 158 < 1/100 * 44934 = 449 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 48 clauses out of 13680 (0%) of length 5
c [cce-3-1] eliminated 146 clauses out of 17715 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 194 large clauses in 8614513 steps
c [cce-3-1] allowing another 4307256 steps for small clauses
c [cce-3-1] scheduling 11358 clauses = 462 binary + 10896 ternary
c [cce-3-1] tried to eliminate 11358 small clauses 100%
c [cce-3-1] eliminated 3 binary clauses 1%
c [cce-3-1] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 5 small clauses 0%
c [cce-3-1] eliminated 5 small clauses in 6071070 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 199 covered clauses in round 1
c [cce-3-2] eliminated 1 clauses out of 13632 (0%) of length 5
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 1 large clauses in 8543777 steps
c [cce-3-2] allowing another 4271888 steps for small clauses
c [cce-3-2] scheduling 11353 clauses = 459 binary + 10894 ternary
c [cce-3-2] tried to eliminate 11353 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 1 covered clauses in round 2
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] allowing another 1448445 steps for small clauses
c [cce-3-3] scheduling 11353 clauses = 459 binary + 10894 ternary
c [cce-3-3] tried to eliminate 9361 small clauses 82%
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 0 covered clauses in round 3
c [cce-3] eliminated 200 covered clauses in TOTAL during 3 rounds
c [cce-3] 200 < 1/100 * 44776 = 447 considered unsuccessful
c [sort-queue-5] sorted 5023 enqueued variables after 17667 conflicts
c [score-dist-5] active 0 (0%), one 4263 (85%), zero 760 (15%)
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 22 variables 0.4% (5023 remain 61%)
c [simplification-5] removed 358 irredundant clauses 0.8% (44576 remain 72%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 20666
c [simplification-5] penalized conflict interval 20666 = 1 * 20666
c [simplification-5] hard conflict limit 48666 (soft 38333 + delta 10333)
c [simplification-5] new conflict limit 38333 (hard 48666)
c 
c [simplification-6] limit of 2969 ternary hit after 2969 ternaries
c [quatres-4] found 23067 quaternary clauses 49% in total
c [quatres-4-1] added 17 double-self-subsuming ternary resolvents
c [quatres-4-2] added 694 single-self-subsuming ternary resolvents
c [quatres-4-2] added 984 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5023 free variables schedulable
c [ternres-4] 559 ternary resolvents (9 bin, 550 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 17 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 3509686 penalty 1 = 1 + 0
c [basicprobe-2-0] 869 sched 17%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-2-1] 871 sched 17%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-2-2] 871 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 30 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-3] limit 70193 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 15 tauts, 0 hbrs, 444 literals
c [transred-4] limit 1403874 with penalty 0 = 0 + 0
c [transred-4] removed 11 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5023 variables 100%
c [elim-5] limit of 14038745 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1 variables 0% in round 1 in 10928685 steps
c [elim-5-1] backward subsumption/strengthening limit 3110060
c [elim-5-1-1] backward checking 12 touched variables 0%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 34923 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1 = 0% variables out of 5023 scheduled
c [elim-5] 1 < 1/100 * 5023 = 50 considered unsuccessful
c [sort-queue-6] sorted 5022 enqueued variables after 34194 conflicts
c [score-dist-6] active 0 (0%), one 4579 (91%), zero 443 (9%)
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 1 variables 0.0% (5022 remain 61%)
c [simplification-6] removed 57 irredundant clauses 0.1% (44519 remain 71%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 20666
c [simplification-6] conflict limit remains at 38333 (hard 48666)
c [simplification-6] new ternary interval 10000
c 
c [simplification-7] limit 38333 conflicts (hard 48666) hit after 38335 conflicts
c [quatres-5] found 23691 quaternary clauses 48% in total
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 192 single-self-subsuming ternary resolvents
c [quatres-5-2] added 400 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 5022 free variables schedulable
c [ternres-5] 137 ternary resolvents (8 bin, 129 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 1644471 with penalty 0 = 0 + 0
c [transred-5] removed 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5022 variables 100%
c [block-4] limit of 25000000 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps and 89538 added (scaled 2)
c [bca-3] 1398 out of 10046 literals actually usable 14%
c [bca-3] added 0 blocked clauses in 39025 steps
c [sweep-3] limit 250000 penalty 2 = 2 + 0
c [sweep-3-1] 597 pos 47.0% + 672 neg 53.0% = 1269 sched 25.3% ret 3753
c [sweep-3-1] 252247 steps 110 queries 176.64 avg class size
c [sweep-3-1] 3827 decisions 109 SAT calls 54.14 avg env size
c [sweep-3-1] 666 variables remain 13% (4356 retained 87%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 109 queries)
c [sort-queue-7] sorted 5022 enqueued variables after 38335 conflicts
c [score-dist-7] active 0 (0%), one 4587 (91%), zero 435 (9%)
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% (5022 remain 61%)
c [simplification-7] removed 0 irredundant clauses 0.0% (44519 remain 71%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20666
c [simplification-7] new conflict interval 41332
c [simplification-7] penalized conflict interval 41332 = 1 * 41332
c [simplification-7] hard conflict limit 100333 (soft 79667 + delta 20666)
c [simplification-7] new conflict limit 79667 (hard 100333)
c 
c [simplification-8] limit 79667 conflicts (hard 100333) hit after 79668 conflicts
c [quatres-6] found 26785 quaternary clauses 44% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 515 single-self-subsuming ternary resolvents
c [quatres-6-2] added 770 quaternary resolvents
c [ternres-6] limit 4571354 with penalty 0 = 0 + 0
c [ternres-6] all 5022 free variables schedulable
c [ternres-6] 323 ternary resolvents (4 bin, 319 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1658 xors of average arity 3.0
c [gauss-3] connected 4974 occurrences of 1221 variables (average 4.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2196 schedulable variables 44%
c [simpleprobe-3] limit 9142709 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 21 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 19 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 75000000 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 47 clauses out of 13480 (0%) of length 5
c [cce-4-1] eliminated 215 clauses out of 17547 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 262 large clauses in 6975023 steps
c [cce-4-1] allowing another 3487511 steps for small clauses
c [cce-4-1] scheduling 827 clauses = 460 binary + 367 ternary
c [cce-4-1] tried to eliminate 827 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 8 ternary clauses 2%
c [cce-4-1] eliminated 9 small clauses 1%
c [cce-4-1] eliminated 9 small clauses in 3575269 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 271 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 3437830 steps for small clauses
c [cce-4-2] scheduling 818 clauses = 459 binary + 359 ternary
c [cce-4-2] tried to eliminate 818 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 271 covered clauses in TOTAL during 2 rounds
c [cce-4] 271 < 1/100 * 44518 = 445 considered unsuccessful
c [sort-queue-8] sorted 5022 enqueued variables after 79668 conflicts
c [score-dist-8] active 0 (0%), one 4681 (93%), zero 341 (7%)
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% (5022 remain 61%)
c [simplification-8] removed 272 irredundant clauses 0.6% (44247 remain 71%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 20666 = 41332 / 2
c [simplification-8] new conflict interval 61998
c [simplification-8] penalized conflict interval 61998 = 1 * 61998
c [simplification-8] hard conflict limit 172665 (soft 141666 + delta 30999)
c [simplification-8] new conflict limit 141666 (hard 172665)
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.2    5022    44247     88564   32663  13107   477    9   360    9   3%    755  112    9    6  161%
c 
c [simplification-9] limit 141666 conflicts (hard 172665) hit after 141666 conflicts
c [quatres-7] found 29969 quaternary clauses 39% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 12 double-self-subsuming ternary resolvents
c [quatres-7-2] added 486 single-self-subsuming ternary resolvents
c [quatres-7-2] added 708 quaternary resolvents
c [ternres-7] limit 9491058 with penalty 0 = 0 + 0
c [ternres-7] all 5022 free variables schedulable
c [ternres-7] 198 ternary resolvents (10 bin, 188 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 5 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5022 variables 100%
c [elim-6] limit of 47455293 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 10735771 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 5022 scheduled
c [sort-queue-9] sorted 5022 enqueued variables after 141666 conflicts
c [score-dist-9] active 0 (0%), one 4817 (96%), zero 205 (4%)
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% (5022 remain 61%)
c [simplification-9] removed 26 irredundant clauses 0.1% (44221 remain 71%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 61998
c [simplification-9] new conflict interval 123996
c [simplification-9] penalized conflict interval 123996 = 1 * 123996
c [simplification-9] hard conflict limit 327660 (soft 265662 + delta 61998)
c [simplification-9] new conflict limit 265662 (hard 327660)
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 -   43.1    5022    44221    156776   49985  14797   495   10   368   11   3%    929   49   10    8  118%
c -   60.0    5022    44221    221065   65479  15326   507   12   367   20   3%    988   18   11   10  116%
c 
c [simplification-10] limit 265662 conflicts (hard 327660) hit after 265663 conflicts
c [quatres-8] found 34007 quaternary clauses 34% in total
c [quatres-8-1] removed 7 duplicate quaternary clauses
c [quatres-8-1] added 8 double-self-subsuming ternary resolvents
c [quatres-8-2] added 433 single-self-subsuming ternary resolvents
c [quatres-8-2] added 606 quaternary resolvents
c [ternres-8] limit 18865446 with penalty 0 = 0 + 0
c [ternres-8] all 5022 free variables schedulable
c [ternres-8] 251 ternary resolvents (3 bin, 248 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1179090 penalty 3 = 3 + 0
c [card-4] no at-most-one constraint found
c [card-4] found 20 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1179090 for elimination
c [card-4] 19 out of 20 constraints (95%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 471636 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 677 tauts, 0 hbrs, 9482 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 3 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5022 variables 100%
c [block-5] limit of 47163617 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [sort-queue-10] sorted 5022 enqueued variables after 265663 conflicts
c [score-dist-10] active 0 (0%), one 4920 (98%), zero 102 (2%)
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% (5022 remain 61%)
c [simplification-10] removed 0 irredundant clauses 0.0% (44221 remain 71%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 123996
c [simplification-10] new conflict interval 247992
c [simplification-10] penalized conflict interval 247992 = 1 * 247992
c [simplification-10] hard conflict limit 637651 (soft 513655 + delta 123996)
c [simplification-10] new conflict limit 513655 (hard 637651)
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 -   74.8    5022    44221    281093   73749  15837   511   13   379   12   3%   1010   12   13   11  116%
c -   88.0    5022    44221    343672   85542  16094   512   14   391   13   4%   1019   12   15   13  117%
c -  100.2    5022    44221    404619   95351  16323   514   15   393   23   4%   1022    6   16   14  118%
c -  112.1    5022    44221    465022  103881  16541   517   16   403   15   4%   1023    8   16   15  104%
c 
c [simplification-11] limit 513655 conflicts (hard 637651) hit after 513764 conflicts
c [quatres-9] found 38452 quaternary clauses 28% in total
c [quatres-9-1] removed 21 duplicate quaternary clauses
c [quatres-9-1] added 7 double-self-subsuming ternary resolvents
c [quatres-9-2] added 368 single-self-subsuming ternary resolvents
c [quatres-9-2] added 666 quaternary resolvents
c [ternres-9] limit 33620560 with penalty 0 = 0 + 0
c [ternres-9] all 5022 free variables schedulable
c [ternres-9] 314 ternary resolvents (6 bin, 308 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 840514 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 6575 literals 65%
c [treelook-3] scheduling used 706557 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 840514 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 684893 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 14 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 5 transitive binary clauses
c [bca-4] limit of 10000000 steps and 88942 added (scaled 2)
c [bca-4] 270 out of 10046 literals actually usable 3%
c [bca-4] added 0 blocked clauses in 153419 steps
c [sweep-4] limit 1260771 penalty 3 = 3 + 0
c [sweep-4-1] 328 pos 49.2% + 338 neg 50.8% = 666 sched 13.3% ret 4356
c [sweep-4-1] 1049796 steps 157 queries 31.49 avg class size
c [sweep-4-1] 11068 decisions 156 SAT calls 233.76 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] 2441 pos 48.6% + 2581 neg 51.4% = 5022 sched 100.0% ret 0
c [sweep-4-2] 214162 steps 25 queries 1063.56 avg class size
c [sweep-4-2] 2026 decisions 24 SAT calls 356.42 avg env size
c [sweep-4-2] 4589 variables remain 91% (433 retained 9%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 180 queries)
c [sort-queue-11] sorted 5022 enqueued variables after 513764 conflicts
c [score-dist-11] active 0 (0%), one 4991 (99%), zero 31 (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 0 variables 0.0% (5022 remain 61%)
c [simplification-11] removed 0 irredundant clauses 0.0% (44221 remain 71%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 247992
c [simplification-11] new conflict interval 495984
c [simplification-11] penalized conflict interval 495984 = 1 * 495984
c [simplification-11] hard conflict limit 1257740 (soft 1009748 + delta 247992)
c [simplification-11] new conflict limit 1009748 (hard 1257740)
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 -  124.2    5022    44221    525835  113067  17427   535   17   411   15   4%   1024   10   18   16  115%
c -  135.6    5022    44221    586153  121440  17526   538   18   405   16   4%   1024   -1   15   17   86%
c -  146.8    5022    44221    646011  129539  17642   538   18   421   17   4%   1024   10   21   18  117%
c -  157.7    5022    44221    705613  137857  17761   540   19   423   17   4%   1024    8   21   18  114%
c -  169.4    5022    44221    764358  144806  17862   541   19   423   18   5%   1024    8   20   19  108%
c -  181.1    5022    44221    823791  151561  17990   542   19   413   19   5%   1024   -5   17   19   91%
c -  193.0    5022    44221    883417  158543  18072   542   20   423   19   5%   1024    4   21   20  107%
c -  205.1    5022    44221    943020  165461  18179   542   21   417   20   5%   1024   -1   22   20  111%
c -  217.4    5022    44221   1002286  171770  18252   542   22   415   20   5%   1024   -2   24   21  116%
c 
c [simplification-12] limit 1009748 conflicts (hard 1257740) hit after 1009748 conflicts
c [quatres-10] found 43522 quaternary clauses 23% in total
c [quatres-10-1] removed 33 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 306 single-self-subsuming ternary resolvents
c [quatres-10-2] added 771 quaternary resolvents
c [ternres-10] limit 64365252 with penalty 0 = 0 + 0
c [ternres-10] all 5022 free variables schedulable
c [ternres-10] 218 ternary resolvents (8 bin, 210 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1609131 penalty 3 = 3 + 0
c [gauss-4] extracted 4160 xors of average arity 3.0
c [gauss-4] connected 12480 occurrences of 1286 variables (average 9.7)
c [gauss-4] limit 1609131 penalty 3 = 3 + 0
c [gauss-4] fully completed
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 8 transitive binary clauses
c [cce-5] limit of 40228283 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 56 clauses out of 13317 (0%) of length 5
c [cce-5-1] eliminated 214 clauses out of 17304 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 270 large clauses in 8190963 steps
c [cce-5-1] allowing another 4095481 steps for small clauses
c [cce-5-1] scheduling 11457 clauses = 460 binary + 10997 ternary
c [cce-5-1] tried to eliminate 11457 small clauses 100%
c [cce-5-1] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 2 small clauses 0%
c [cce-5-1] eliminated 2 small clauses in 5862183 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 272 covered clauses in round 1
c [cce-5-2] eliminated 2 clauses out of 13261 (0%) of length 5
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 2 large clauses in 8100090 steps
c [cce-5-2] allowing another 4050045 steps for small clauses
c [cce-5-2] scheduling 11455 clauses = 460 binary + 10995 ternary
c [cce-5-2] tried to eliminate 11455 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 2 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 4051066 steps for small clauses
c [cce-5-3] scheduling 11455 clauses = 460 binary + 10995 ternary
c [cce-5-3] tried to eliminate 11455 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 274 covered clauses in TOTAL during 3 rounds
c [cce-5] 274 < 1/100 * 44221 = 442 considered unsuccessful
c [sort-queue-12] sorted 5022 enqueued variables after 1009748 conflicts
c [score-dist-12] active 0 (0%), one 5022 (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% (5022 remain 61%)
c [simplification-12] removed 274 irredundant clauses 0.6% (43947 remain 71%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 247992 = 495984 / 2
c [simplification-12] new conflict interval 743976
c [simplification-12] penalized conflict interval 743976 = 1 * 743976
c [simplification-12] hard conflict limit 2125712 (soft 1753724 + delta 371988)
c [simplification-12] new conflict limit 1753724 (hard 2125712)
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 -  231.2    5022    43947   1061762  178283  18803   542   21   414   21   5%   1024   -4   20   21   93%
c -  244.1    5022    43947   1121487  184708  18857   543   22   424   21   5%   1024    7   20   22   92%
c -  257.1    5022    43947   1181054  190188  18908   543   22   410   22   5%   1024  -10   22   22   98%
c -  270.8    5022    43947   1241300  195713  18958   544   23   419   22   5%   1024   -0   26   22  117%
c -  284.8    5022    43947   1302143  201120  19000   545   24   421   23   6%   1024   -1   25   23  112%
c -  299.0    5022    43947   1363674  206874  19028   545   23   430   23   5%   1024   12   25   23  112%
c -  313.6    5022    43947   1425494  212459  19065   545   24   427   24   6%   1024    5   25   23  109%
c -  328.7    5022    43947   1487588  217657  19093   545   23   422   24   5%   1024    0   24   23  101%
c -  343.7    5022    43947   1550505  223311  19146   546   23   421   24   6%   1024   -3   22   23   93%
c -  359.2    5022    43947   1613623  228328  19177   546   25   399   25   6%   1024  -20   29   23  122%
c -  375.6    5022    43947   1677716  232848  19211   547   23   419   25   6%   1024    1   21   23   91%
c -  392.5    5022    43947   1743107  238175  19238   548   24   434   26   5%   1024   16   25   23  105%
c 
c [simplification-13] limit 1753724 conflicts (hard 2125712) hit after 1753724 conflicts
c [quatres-11] found 47861 quaternary clauses 19% in total
c [quatres-11-1] removed 39 duplicate quaternary clauses
c [quatres-11-1] added 11 double-self-subsuming ternary resolvents
c [quatres-11-2] added 206 single-self-subsuming ternary resolvents
c [quatres-11-2] added 641 quaternary resolvents
c [ternres-11] limit 121644097 with penalty 0 = 0 + 0
c [ternres-11] all 5022 free variables schedulable
c [ternres-11] 105 ternary resolvents (5 bin, 100 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 4 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5022 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 2 variables 0% in round 1 in 10546386 steps
c [elim-7-1] backward subsumption/strengthening limit 10546300
c [elim-7-1-1] backward checking 21 touched variables 0%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 3 clauses in 37846 steps
c [elim-7-1] rescheduled 10 variables 0% by backward subsumption
c [elim-7-2] no variable eliminated in round 2 in 10038 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2 = 0% variables out of 5022 scheduled
c [elim-7] 2 < 1/100 * 5022 = 50 considered unsuccessful
c [sort-queue-13] sorted 5020 enqueued variables after 1753724 conflicts
c [score-dist-13] active 0 (0%), one 5020 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 2 variables 0.0% (5020 remain 61%)
c [simplification-13] removed 26 irredundant clauses 0.1% (43921 remain 70%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 743976
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] hard conflict limit 3253724 (soft 2753724 + delta 500000)
c [simplification-13] new conflict limit 2753724 (hard 3253724)
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 -  410.9    5020    43921   1808916  243327  19546   548   24   414   26   6%   1024   -5   30   24  125%
c -  428.7    5020    43921   1876018  249027  19571   548   23   431   27   5%   1024    8   17   24   73%
c -  447.1    5020    43921   1943142  254321  19590   550   25   412   27   6%   1024  -10   26   24  106%
c -  465.8    5020    43921   2010840  259309  19616   550   25   426   27   6%   1024    5   21   25   86%
c -  484.7    5020    43921   2079438  264278  19637   550   24   435   28   6%   1024   13   24   24  100%
c -  504.1    5020    43921   2148848  270014  19671   551   25   436   29   6%   1024   16   24   25   99%
c -  523.7    5020    43921   2218199  275064  19703   552   25   420   29   6%   1024   -3   23   25   93%
c -  544.0    5020    43921   2288044  279560  19729   552   26   419   29   6%   1024   -3   24   25   95%
c -  564.2    5020    43921   2359078  285066  19755   554   24   424   30   6%   1024    2   30   25  119%
c -  585.3    5020    43921   2430314  289778  19776   554   25   422   30   6%   1024   -1   26   25  104%
c -  606.7    5020    43921   2502695  295294  19803   554   25   427   31   6%   1024    4   24   25   94%
c -  628.5    5020    43921   2575196  299979  19831   554   25   427   31   6%   1024    5   30   26  119%
c -  651.8    5020    43921   2648614  304063  19849   554   26   416   31   6%   1024   -6   24   26   92%
c -  675.0    5020    43921   2723676  309695  19872   554   25   429   32   6%   1024    6   27   26  104%
c 
c [simplification-14] limit 2753724 conflicts (hard 3253724) hit after 2756904 conflicts
c [quatres-12] found 51731 quaternary clauses 16% in total
c [quatres-12-1] removed 54 duplicate quaternary clauses
c [quatres-12-1] added 3 double-self-subsuming ternary resolvents
c [quatres-12-2] added 152 single-self-subsuming ternary resolvents
c [quatres-12-2] added 588 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 5020 free variables schedulable
c [ternres-12] 118 ternary resolvents (7 bin, 111 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-3] limit 100000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 1083 sched 22%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 1084 sched 22%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 5 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5020 variables 100%
c [block-6] limit of 100000000 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [sort-queue-14] sorted 5020 enqueued variables after 2756904 conflicts
c [score-dist-14] active 0 (0%), one 5020 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 0 variables 0.0% (5020 remain 61%)
c [simplification-14] removed 0 irredundant clauses 0.0% (43921 remain 70%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 1000000
c [simplification-14] new conflict interval 2000000
c [simplification-14] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-14] hard conflict limit 5756904 (soft 4756904 + delta 1000000)
c [simplification-14] new conflict limit 4756904 (hard 5756904)
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 -  700.3    5020    43921   2798694  314855  20149   558   27   410   32   7%   1024  -12   28   26  109%
c -  724.5    5020    43921   2874632  320075  20181   559   26   426   33   6%   1024    4   31   26  119%
c -  749.2    5020    43921   2951008  324943  20204   559   26   423   33   6%   1024    4   30   26  115%
c -  774.5    5020    43921   3028122  329988  20224   560   25   431   34   6%   1024    6   31   26  119%
c -  800.7    5020    43921   3105968  334611  20231   561   28   429   34   6%   1024    8   31   26  119%
c -  827.6    5020    43921   3184729  339720  20248   561   27   417   35   7%   1024   -4   25   26   96%
c -  854.4    5020    43921   3264062  345416  20271   561   26   430   35   6%   1024    9   24   27   91%
c -  881.9    5020    43921   3343456  349988  20291   561   27   425   35   6%   1024    0   34   26  128%
c -  909.8    5020    43921   3423892  355115  20314   561   27   425   36   6%   1024    0   25   27   95%
c -  938.9    5020    43921   3504771  360134  20333   562   27   407   36   7%   1024  -14   25   27   94%
c -  968.0    5020    43921   3586184  364415  20353   562   26   428   37   6%   1024    5   32   27  118%
c -  998.7    5020    43921   3668865  368779  20371   562   27   435   37   6%   1024   12   29   27  110%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2 basic ate = 2 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (74 skipped), 249564 steps
c bkwd: tried 19835 clauses, 39314 lits, 1.98 lits/clause
c bkwd: checked 655743 occs, 33.06 occs/clause, 16.68 occs/lit
c bkwd: subsumed 0 binary, 26 ternary, 106 large
c bkwd: strengthened 0 binary, 15 ternary (100% self), 402 large (0% self)
c blkd: 6 bces, 909 removed, 2448293 resolutions, 5214701 steps
c blkd: 296 blocking literals 2%, 123 pure
c bump: 3655981 bumped seen, 246526749 lits 67.4 on average
c card: 4 count, 5 units, 0 am1, 4129127 steps
c card: 60 rescheduled, 250 eliminated, 22822 resolved, 1722 subsumed
c card: 5 at-most-one constraints found, average size 3.00
c card: 5 at-most-one constraints used 100%, average size 3.00
c card: 184 at-most-two constraints found, average size 4.00
c card: 181 at-most-two constraints used 98%, average size 4.00
c cces: 5 cces, 9215 eliminated, 9063 ate 98%, 152 abce 2%
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: 306220 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 55 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 31 decompositions, 31 equivalent 0%
c deco: 2088 decision-only clauses 0%, 42% reduction
c decs: 32311104 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 3209 eliminated 39%, 8 pure 0%
c elms: 17 rounds, 2.4 rounds/bve
c elms: 3078 small 96%, 0 large 0%
c elms: 24436 tried small, 3078 succeeded 13%, 21358 failed 87%
c elms: 940 subsumed, 1013 strengthened, 0 blocked
c elms: 1951062 copies, 3609313 resolutions, 2340104 ipos
c elms: 58156 subchks, 52754 strchks
c gaus: 4 extractions, 25014 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10218670 steps, 5109335 extr 50%, 2903848 elim 28%
c glue: 22.3 orig avg, 22.3 real avg, 3.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 536 = 371 simple 69% + 151 trn 28% + 14 lrg 3%, 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: 3655981 clauses, 45.5 length
c lrnd: 166367630 lits = 175927113 orig - 9559483 removed 5%
c lrnd: 1632296 uips 45%, 1579234 flips 43%
c mins: 3391858 mins 93%, 34 bin 0%, 259287 size 7%
c mins: 152549368 poisoned searches, 11726498 hits, 8% hit rate
c mins: 294492903 used twice searches, 50479928 hits, 17% hit rate
c move: moved 825, 16 bin 2%, 809 trn 98%
c otfs: 17396 driving 43%, 22716 restarting 57%
c otfs: str 40112, 39631 red 99%, 481 irr 1%
c otfs: str 40112, 0 bin 0%, 257 trn 1%, 39855 lrg 99%
c otfs: sub 468, 468 red 100%, 0 irr 0%
c otfs: sub 468, 0 bin 0%, 68 trn 15%, 400 lrg 85%
c phas: 1 computed, 5596 set, 0 pos (0%), 5596 neg (100%)
c prbs: 3 basic, 13270 probed, 0 failed, 0 lifted
c prbs: 3 simple, 30250 probed, 5 failed, 28 eqs
c prbs: 3 treelook, 11076 probed, 0 failed, 0 lifted
c prom: 445430 locked 28% out of 1575780 tried
c prps: 614081306 props, 19 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 8333 quat, 4601 self1, 87 self2, 161 dup
c queu: 14 sorted, 32311104 next (108 steps 0.00)
c queu: 246606412 enq (0 steps 0.00), 246526749 deq 100%
c redc: 3213 clauses 0%, 697354 tried 19%, 1 sat 0%
c redc: 3291 lits 0%, 5768940 tried 3%, 1 sat 0%
c redc: 117 times jump level reduced, 11.4 levels on average
c reds: 54 count, 68012.5 conflicts per reduce
c reds: 0 memlim 0%, 54 arith 100%
c reds: 2034762 collected 62%, 1226046 retired 38%
c rmbd: 58 removed, 58 red 100%
c rsts: 34857 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 14 count, 13 confs 93%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 7%
c subl: 3655981 count (4308585 tried 1.2), 15023 sub out of 3647525 (0.4%)
c swps: 4 count, 6 rounds, 1984 queries (330.7/round)
c swps: 1987 sat calls, 3 unsat (0.4% success rate)
c swps: 33864 decisions 17.0, 700 conflicts 0.4
c swps; 362.9 avg class size, 40.3 avg environment size
c swps: 0 failed, 3 impls, 0 equivs
c swp0: 660 type 0 queries, 3 unsat (0.5%), 660 sat (100.0%)
c swp1: 1324 type 1 queries, 42 unsat (3.2%), 1324 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: 71934445 calls to obtain time
c tops: 19 fixed 0%, 0 its, 0.00 confs/it
c trds: 12 transitive reductions, 113 removed, 0 failed
c trds: 121270 nodes, 11109 edges, 17461 steps
c trim: 122340 words, 0.5 MB
c trnr: 12 count, 144 bin, 7225 trn, 44501918 steps
c unhd: 4 count, 4 rounds, 1374666 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: 943 tauts, 1 bin 0%, 800 trn 85%, 133 lrg 14%
c unhd: 943 tauts, 9 stamp 1%, 899 red 95%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 10137 str, 0 bin 0%, 124 trn 1%, 10013 lrg 99%, 10030 red 99%
c vars: 5020 remaining 61% and 3259 removed 39% out of 8279
c vars: 19 fixed 0%, 3209 eliminated 39%, 31 equivalent 0%
c vsts: 31854375983 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 51.9 search visits per propagation, 8672.5 per conflict
c wchs: 10305634581 pushed, 14238339 enlarged, 1119 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3655858       2034762       1226046     199646276      31970150       1814841
c 
c  0 0        352336  10       688   0         0   0 180286222  90< 26496883  83<  1491666  82    10.9
c  1 5        258901   7    128628   6    112437   9  10548735   5   1934785   6    119896   7<    0.7
c  2 6        707875  19    402808  20    295436  24   4481678   2   1238199   4     72206   4     1.0
c  3 9        684859  19    412292  20    268143  22   1650066   1    762929   2     40050   2     1.2
c  4 14       496444  14<   318020  16<   175501  14<   965540   0    516208   2     27849   2     1.4
c  5 21       349311  10    230610  11    116529  10    586320   0    336396   1     18558   1     1.6
c  6 30       250439   7    168437   8     80407   7    378563   0    226686   1     13083   1     1.8
c  7 41       182578   5    124504   6     56856   5    257342   0    157928   0      9590   1     2.0
c  8 54       132856   4     91063   4     40762   3    180305   0    111810   0      7373   0     2.1
c  9 69        93923   3     64633   3     28505   2    124339   0     77698   0      5306   0     2.0
c 10 86       104600   3     69447   3     34145   3    134823   0     82249   0      6556   0     3.4
c 11 126       37987   1     22189   1     15442   1     47636   0     26141   0      2513   0     2.2
c 12 230        3749   0      1443   0      1883   0      4707   0      2238   0       195   0     0.3
c 
c avg                  3.7           4.3           3.9           0.2           0.5           0.5
c std                  2.6           2.4           2.4           0.8           1.4           1.5
c 
c   22.214   2% decide
c   14.709   1% bump
c    3.140   0% elim
c 
c    4.629 < 1% rest (below)
c 
c    2.308   0% cce
c    1.756   0% quatres
c    0.846   0% probe
c    0.537   0% sweep
c    0.459   0% block
c    0.345   0% gauss
c    0.313   0% ternres
c    0.130   0% bca
c    0.120   0% unhide
c    0.102   0% card
c    0.021   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.682   0% preprocessing     6%
c   10.660   1% inprocessing     94%
c ==================================
c   11.343   1% simplifying
c  988.648  99% search
c ==================================
c  999.990 100% all
c 
c       3672677 conflicts,        3672.7 confs/sec
c          8261 ternaries,         444.6 confs/ternary
c            47 binaries,        78142.1 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            54 reductions,          0.1 redus/sec,  68012.5 confs/reduction
c         34857 restarts,           34.9 rests/sec,    105.4 confs/restart
c      32311104 decisions,       32311.4 decis/sec,      8.8 decis/conflict
c     614081306 propagations,   614087.3 props/sec,     19.0 props/decision
c 
c 1000.0 seconds, 99.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
