c launch: /data/cnf/sc2014/app/003-23-80.cnf.bz2
c host: atom05
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/003-23-80.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/003-23-80.cnf.bz2
c no embedded options
c found 'p cnf 4288 132592' header
c read 4288 variables, 132592 clauses, 873647 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 3829 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    3829    76353         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 7 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 10 constraints (90%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 602 variables
c [simpleprobe-1] all 3686 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 138 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 138 variables, found 10 hbrs, 61 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 662 tauts, 0 hbrs, 22 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3548 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 124 variables 3% in round 1 in 2047727 steps
c [elim-1-1] backward subsumption/strengthening limit 2047700
c [elim-1-1-1] backward checking 1179 touched variables 33%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 32 and strengthened 86 clauses in 745507 steps
c [elim-1-1] rescheduled 158 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 121400 steps
c [elim-1-2] backward subsumption/strengthening limit 121400
c [elim-1-2-1] backward checking 39 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 2 and strengthened 0 clauses in 103050 steps
c [elim-1-2] rescheduled 5 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 3260 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 127 = 4% variables out of 3548 scheduled
c [phase-count-1] 67777 negative 99.2% of 68317 except 540 0.8%
c [phase-count-1] 67500 positive 98.8% of 68317 except 817 1.2%
c [phase-1] phase bias: 1481 positive 43%, 1940 negative 57%
c [sort-queue-1] sorted 3421 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3421 (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 393 variables 10.3% (3421 remain 89%)
c [simplification-1] removed 8036 irredundant clauses 10.5% (68317 remain 89%)
c [simplification-1] maximum reduction of 11% = max (10%, 11%)
c [simplification-1] large reduction 11% >= 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 1001 conflicts
c [simpleprobe-2] all 3421 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2130 variables remain 62% (1291 retained 38%)
c [simpleprobe-2] removed 0 variables, found 1 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6842 literals 100%
c [treelook-1] scheduling used 294000 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300167 steps
c [treelook-1] 5636 literals remain 82%
c [treelook-1] 3031 variables remain to probed next time 89%
c [treelook-1] removed 0 variables, found 9 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 371 sched 11%, 0 failed, 0 lifted, 16 hbrs
c [decomp-6] removed 1 variables
c [basicprobe-1-1] 379 sched 11%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-1-2] 379 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 1 variables, found 19 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3420 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 222 blocked clauses
c [block-1] 222 < 1/100 * 68314 = 683 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3542 clauses out of 21756 (16%) of length 7
c [cce-1-1] eliminated 430 clauses out of 20546 (2%) of length 6
c [cce-1-1] eliminated 2640 clauses out of 13626 (19%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6612 large clauses in 30000014 steps
c [cce-1-1] allowing another 15000007 steps for small clauses
c [cce-1-1] scheduling 4507 clauses = 246 binary + 4261 ternary
c [cce-1-1] tried to eliminate 4507 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 2%
c [cce-1-1] eliminated 1064 ternary clauses 25%
c [cce-1-1] eliminated 1068 small clauses 24%
c [cce-1-1] eliminated 1068 small clauses in 16177818 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 7680 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 6911107 steps for small clauses
c [cce-1-2] scheduling 3439 clauses = 242 binary + 3197 ternary
c [cce-1-2] tried to eliminate 3439 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 7680 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3420 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 727 not tried 21% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 30 = 1% variables out of 3420 scheduled
c [elim-2] 30 < 1/100 * 3420 = 34 considered unsuccessful
c [bca-1] limit of 10000000 steps and 119446 added (scaled 2)
c [bca-1] 4743 out of 6782 literals actually usable 70%
c [bca-1] added 0 blocked clauses in 32065 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1546 pos 45.6% + 1844 neg 54.4% = 3390 sched 100.0% ret 0
c [sweep-1-1] 516390 steps 599 queries 167.22 avg class size
c [sweep-1-1] 9158 decisions 599 SAT calls 21.49 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 6 variables
c [sweep-1-1] removed 6 vars (0 failed, 3 eqs, 4 impls)
c [sweep-1-2] 1543 pos 45.6% + 1841 neg 54.4% = 3384 sched 100.0% ret 0
c [sweep-1-2] 483908 steps 578 queries 193.61 avg class size
c [sweep-1-2] 8773 decisions 579 SAT calls 21.56 avg env size
c [sweep-1-2] 7 variables remain 0% (3376 retained 100%)
c [decomp-9] removed 4 variables
c [sweep-1-2] removed 4 vars (0 failed, 2 eqs, 4 impls)
c [sweep-1] removed 10 vars in TOTAL (2 rounds, 1175 queries)
c [sort-queue-2] sorted 3380 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 3008 (89%), zero 372 (11%)
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 1.2% (3380 remain 88%)
c [simplification-2] removed 8890 irredundant clauses 13.0% (59426 remain 78%)
c [simplification-2] maximum reduction of 13% = max (1%, 13%)
c [simplification-2] large reduction 13% >= 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3002 conflicts
c [quatres-1] found 7441 quaternary clauses 13% in total
c [quatres-1-1] added 29 double-self-subsuming ternary resolvents
c [quatres-1-2] added 110 single-self-subsuming ternary resolvents
c [quatres-1-2] added 278 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 3380 free variables schedulable
c [ternres-1] 148 ternary resolvents (15 bin, 133 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 5 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 6 out of 6 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 3916 xors of average arity 4.9
c [gauss-1] connected 19038 occurrences of 821 variables (average 23.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 1214 occurrences of 821 variables (average 1.5)
c [gauss-1] fully completed
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, 69 tauts, 0 hbrs, 124 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 8 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 16995 (0%) of length 7
c [cce-2-1] eliminated 162 clauses out of 20531 (1%) of length 6
c [cce-2-1] eliminated 65 clauses out of 11092 (1%) of length 5
c [cce-2-1] eliminated 297 clauses out of 6833 (4%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 526 large clauses in 29369511 steps
c [cce-2-1] allowing another 14684755 steps for small clauses
c [cce-2-1] scheduling 744 clauses = 261 binary + 483 ternary
c [cce-2-1] tried to eliminate 744 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 1%
c [cce-2-1] eliminated 46 ternary clauses 10%
c [cce-2-1] eliminated 49 small clauses 7%
c [cce-2-1] eliminated 49 small clauses in 14831790 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 575 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 7584134 steps for small clauses
c [cce-2-2] scheduling 695 clauses = 258 binary + 437 ternary
c [cce-2-2] tried to eliminate 695 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 575 covered clauses in TOTAL during 2 rounds
c [cce-2] 575 < 1/100 * 59422 = 594 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2 pos 28.6% + 5 neg 71.4% = 7 sched 0.2% ret 3371
c [sweep-2-1] 2775 steps 6 queries 2.83 avg class size
c [sweep-2-1] 72 decisions 5 SAT calls 17.80 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] 1649 pos 48.8% + 1729 neg 51.2% = 3378 sched 100.0% ret 0
c [sweep-2-2] 523579 steps 550 queries 166.73 avg class size
c [sweep-2-2] 9531 decisions 548 SAT calls 23.79 avg env size
c [sweep-2-2] fully completed sweeping round
c [decomp-12] removed 1 variables
c [sweep-2-2] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2-3] 1648 pos 48.8% + 1729 neg 51.2% = 3377 sched 100.0% ret 0
c [sweep-2-3] 473742 steps 523 queries 199.52 avg class size
c [sweep-2-3] 8750 decisions 524 SAT calls 23.54 avg env size
c [sweep-2-3] 70 variables remain 2% (3307 retained 98%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-2] 1 < 1/1000 * 3378 = 3 considered unsuccessful
c [sweep-2] removed 1 vars in TOTAL (3 rounds, 1076 queries)
c [sort-queue-3] sorted 3377 enqueued variables after 3002 conflicts
c [score-dist-3] active 0 (0%), one 3277 (97%), zero 100 (3%)
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 3 variables 0.1% (3377 remain 88%)
c [simplification-3] removed 579 irredundant clauses 1.0% (58846 remain 77%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23002 (soft 13002 + delta 10000)
c [simplification-3] new conflict limit 13002 (hard 23002)
c 
c [simplification-4] limit 13002 conflicts (hard 23002) hit after 13002 conflicts
c [quatres-2] found 8140 quaternary clauses 13% in total
c [quatres-2-1] added 44 double-self-subsuming ternary resolvents
c [quatres-2-2] added 231 single-self-subsuming ternary resolvents
c [quatres-2-2] added 313 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3377 free variables schedulable
c [ternres-2] 121 ternary resolvents (13 bin, 108 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3147 literals 47%
c [treelook-2] scheduling used 150064 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150197 steps
c [treelook-2] 2506 literals remain 37%
c [treelook-2] 2410 variables remain to probed next time 71%
c [treelook-2] removed 0 variables, found 14 hbrs
c [transred-2] limit 269879 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3377 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 2 blocked clauses
c [block-2] 2 < 1/100 * 58844 = 588 considered unsuccessful
c [elim-3] 727 variables 22% will be scheduled this time
c [elim-3] scheduled 727 variables 22%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 309 not tried 9% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 727 scheduled
c [bca-2] limit of 10000000 steps and 118154 added (scaled 2)
c [bca-2] 877 out of 6756 literals actually usable 13%
c [bca-2] added 0 blocked clauses in 18650 steps
c [sort-queue-4] sorted 3377 enqueued variables after 13002 conflicts
c [score-dist-4] active 0 (0%), one 3303 (98%), zero 74 (2%)
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 0 variables 0.0% (3377 remain 88%)
c [simplification-4] removed 19 irredundant clauses 0.0% (58827 remain 77%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58002 (soft 43002 + delta 15000)
c [simplification-4] new conflict limit 43002 (hard 58002)
c 
c [simplification-5] limit 43002 conflicts (hard 58002) hit after 43002 conflicts
c [quatres-3] found 10094 quaternary clauses 15% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 39 double-self-subsuming ternary resolvents
c [quatres-3-2] added 329 single-self-subsuming ternary resolvents
c [quatres-3-2] added 423 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3377 free variables schedulable
c [ternres-3] 57 ternary resolvents (6 bin, 51 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1102 xors of average arity 4.4
c [gauss-2] connected 4886 occurrences of 313 variables (average 15.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 [basicprobe-2] limit 6355379 penalty 0 = 0 + 0
c [basicprobe-2-0] 488 sched 14%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-2-1] 491 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 13 hbrs
c [bate-1] eliminated 23 asymmetric tautologies during probing
c [transred-3] limit 1271075 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 16528 (0%) of length 7
c [cce-3-1] eliminated 25 clauses out of 20681 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 27 large clauses in 15000013 steps
c [cce-3-1] allowing another 7500006 steps for small clauses
c [cce-3-1] scheduling 3596 clauses = 277 binary + 3319 ternary
c [cce-3-1] tried to eliminate 3596 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 12 ternary clauses 0%
c [cce-3-1] eliminated 13 small clauses 0%
c [cce-3-1] eliminated 13 small clauses in 8523723 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 40 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3238164 steps for small clauses
c [cce-3-2] scheduling 3583 clauses = 276 binary + 3307 ternary
c [cce-3-2] tried to eliminate 3583 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 40 covered clauses in TOTAL during 2 rounds
c [cce-3] 40 < 1/100 * 58804 = 588 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 34 pos 48.6% + 36 neg 51.4% = 70 sched 2.1% ret 3307
c [sweep-3-1] 96516 steps 43 queries 13.21 avg class size
c [sweep-3-1] 1842 decisions 42 SAT calls 64.24 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 1733 pos 51.3% + 1644 neg 48.7% = 3377 sched 100.0% ret 0
c [sweep-3-2] 406696 steps 130 queries 270.43 avg class size
c [sweep-3-2] 6590 decisions 129 SAT calls 80.53 avg env size
c [sweep-3-2] 1174 variables remain 35% (2203 retained 65%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 171 queries)
c [sort-queue-5] sorted 3377 enqueued variables after 43002 conflicts
c [score-dist-5] active 0 (0%), one 3339 (99%), zero 38 (1%)
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% (3377 remain 88%)
c [simplification-5] removed 63 irredundant clauses 0.1% (58764 remain 77%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133002 (soft 103002 + delta 30000)
c [simplification-5] new conflict limit 103002 (hard 133002)
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 -   14.9    3377    58764     75858   28695   3558   164   12   317   14   4%    697  114   11    7  170%
c 
c [simplification-6] limit 103002 conflicts (hard 133002) hit after 103002 conflicts
c [quatres-4] found 13218 quaternary clauses 17% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 40 double-self-subsuming ternary resolvents
c [quatres-4-2] added 445 single-self-subsuming ternary resolvents
c [quatres-4-2] added 358 quaternary resolvents
c [ternres-4] limit 4204660 with penalty 0 = 0 + 0
c [ternres-4] all 3377 free variables schedulable
c [ternres-4] 48 ternary resolvents (5 bin, 43 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 525582 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 16 at-most-two constraints of average size 4.1
c [card-3] using previous limit 525582 for elimination
c [card-3] 19 out of 19 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 210233 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 98 tauts, 0 hbrs, 1538 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 15 transitive binary clauses
c [sort-queue-6] sorted 3377 enqueued variables after 103002 conflicts
c [score-dist-6] active 0 (0%), one 3355 (99%), zero 22 (1%)
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% (3377 remain 88%)
c [simplification-6] removed 9 irredundant clauses 0.0% (58755 remain 77%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 283002 (soft 223002 + delta 60000)
c [simplification-6] new conflict limit 223002 (hard 283002)
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 -   25.6    3377    58755    130454   36089   4496   171   14   327    9   4%    882   56   12   10  121%
c -   37.0    3377    58755    184689   44731   4767   175   16   324   10   5%    962   15   15   13  117%
c 
c [simplification-7] limit 223002 conflicts (hard 283002) hit after 223002 conflicts
c [quatres-5] found 17452 quaternary clauses 19% in total
c [quatres-5-1] removed 12 duplicate quaternary clauses
c [quatres-5-1] added 41 double-self-subsuming ternary resolvents
c [quatres-5-2] added 385 single-self-subsuming ternary resolvents
c [quatres-5-2] added 223 quaternary resolvents
c [ternres-5] limit 10995904 with penalty 0 = 0 + 0
c [ternres-5] all 3377 free variables schedulable
c [ternres-5] 15 ternary resolvents (2 bin, 13 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 2105 schedulable variables 62%
c [simpleprobe-3] limit 21991809 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 17 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 14 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3377 variables 100%
c [block-3] limit of 27489761 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] scheduling all variables this time
c [elim-4] scheduled 3377 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1099590455 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 3 variables 0% in round 1 in 44327080 steps
c [elim-4-1] backward subsumption/strengthening limit 44327000
c [elim-4-1-1] backward checking 1176 touched variables 35%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 0 clauses in 598320 steps
c [elim-4-1] rescheduled 9 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 34920 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 0% variables out of 3377 scheduled
c [elim-4] 3 < 1/100 * 3377 = 33 considered unsuccessful
c [bca-3] limit of 10000000 steps and 117730 added (scaled 2)
c [bca-3] 135 out of 6750 literals actually usable 2%
c [bca-3] added 0 blocked clauses in 82004 steps
c [sort-queue-7] sorted 3374 enqueued variables after 223002 conflicts
c [score-dist-7] active 0 (0%), one 3366 (100%), zero 8 (0%)
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 3 variables 0.1% (3374 remain 88%)
c [simplification-7] removed 140 irredundant clauses 0.2% (58615 remain 77%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 583002 (soft 463002 + delta 120000)
c [simplification-7] new conflict limit 463002 (hard 583002)
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 -   48.6    3374    58615    236434   45789   5326   179   17   343   17   5%    996   12   17   14  119%
c -   58.2    3374    58615    294289   54595   5450   179   18   361   18   5%   1012    7   19   16  122%
c -   66.6    3374    58615    349772   60846   5573   180   19   349   19   5%   1019  -13   20   17  116%
c -   74.7    3374    58615    404823   65940   5687   182   19   369   19   5%   1022   -1   18   18  100%
c -   82.6    3374    58615    459835   70097   5758   182   20   377   20   5%   1023    2   23   19  122%
c 
c [simplification-8] limit 463002 conflicts (hard 583002) hit after 463002 conflicts
c [quatres-6] found 21987 quaternary clauses 19% in total
c [quatres-6-1] removed 27 duplicate quaternary clauses
c [quatres-6-1] added 23 double-self-subsuming ternary resolvents
c [quatres-6-2] added 307 single-self-subsuming ternary resolvents
c [quatres-6-2] added 193 quaternary resolvents
c [ternres-6] limit 21374819 with penalty 0 = 0 + 0
c [ternres-6] all 3374 free variables schedulable
c [ternres-6] 12 ternary resolvents (3 bin, 9 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1068740 penalty 2 = 2 + 0
c [gauss-3] extracted 250 xors of average arity 3.0
c [gauss-3] connected 750 occurrences of 69 variables (average 10.9)
c [gauss-3] limit 1068740 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 3 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 267185245 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 63 clauses out of 21196 (0%) of length 6
c [cce-4-1] eliminated 59 clauses out of 11142 (1%) of length 5
c [cce-4-1] eliminated 75 clauses out of 6287 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 197 large clauses in 28746489 steps
c [cce-4-1] allowing another 14373244 steps for small clauses
c [cce-4-1] scheduling 3642 clauses = 291 binary + 3351 ternary
c [cce-4-1] tried to eliminate 3642 small clauses 100%
c [cce-4-1] eliminated 7 ternary clauses 0%
c [cce-4-1] eliminated 7 small clauses 0%
c [cce-4-1] eliminated 7 small clauses in 15349322 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 204 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14324630 steps for small clauses
c [cce-4-2] scheduling 3635 clauses = 291 binary + 3344 ternary
c [cce-4-2] tried to eliminate 3635 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 204 covered clauses in TOTAL during 2 rounds
c [cce-4] 204 < 1/100 * 58615 = 586 considered unsuccessful
c [sweep-4] limit 1603111 penalty 2 = 2 + 0
c [sweep-4-1] 602 pos 51.3% + 571 neg 48.7% = 1173 sched 34.8% ret 2201
c [sweep-4-1] 664842 steps 265 queries 73.20 avg class size
c [sweep-4-1] 10331 decisions 264 SAT calls 62.05 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] 1721 pos 51.0% + 1653 neg 49.0% = 3374 sched 100.0% ret 0
c [sweep-4-2] 934924 steps 316 queries 94.67 avg class size
c [sweep-4-2] 14786 decisions 315 SAT calls 76.48 avg env size
c [sweep-4-2] fully completed sweeping round
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4-3] 1721 pos 51.0% + 1653 neg 49.0% = 3374 sched 100.0% ret 0
c [sweep-4-3] 3709 steps 2 queries 1687.00 avg class size
c [sweep-4-3] 100 decisions 1 SAT calls 164.00 avg env size
c [sweep-4-3] 3374 variables remain 100% (0 retained 0%)
c [sweep-4-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (3 rounds, 580 queries)
c [sort-queue-8] sorted 3374 enqueued variables after 463002 conflicts
c [score-dist-8] active 0 (0%), one 3374 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (3374 remain 88%)
c [simplification-8] removed 204 irredundant clauses 0.3% (58411 remain 77%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 240000
c [simplification-8] new conflict interval 480000
c [simplification-8] penalized conflict interval 480000 = 1 * 480000
c [simplification-8] hard conflict limit 1183002 (soft 943002 + delta 240000)
c [simplification-8] new conflict limit 943002 (hard 1183002)
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 -   91.7    3374    58411    515573   73925   6114   186   23   403   13   6%   1024   19   28   20  138%
c -   99.5    3374    58411    572366   77753   6141   186   24   391   22   6%   1024    0   26   22  121%
c -  107.6    3374    58411    629875   81575   6166   187   25   390   22   6%   1024   -2   27   23  117%
c -  116.0    3374    58411    688013   85330   6194   187   25   414   23   6%   1024   14   28   24  116%
c -  124.4    3374    58411    746701   89429   6210   187   26   417   23   6%   1024   10   29   25  118%
c -  133.0    3374    58411    805357   92967   6235   187   26   409   24   6%   1024   -3   24   25   94%
c -  141.8    3374    58411    864605   96666   6264   188   26   392   24   7%   1024  -22   31   26  119%
c -  150.9    3374    58411    923975  100401   6278   188   26   431   15   6%   1024   15   23   26   88%
c 
c [simplification-9] limit 943002 conflicts (hard 1183002) hit after 943002 conflicts
c [quatres-7] found 25650 quaternary clauses 18% in total
c [quatres-7-1] removed 70 duplicate quaternary clauses
c [quatres-7-1] added 9 double-self-subsuming ternary resolvents
c [quatres-7-2] added 149 single-self-subsuming ternary resolvents
c [quatres-7-2] added 90 quaternary resolvents
c [ternres-7] limit 42877606 with penalty 0 = 0 + 0
c [ternres-7] all 3374 free variables schedulable
c [ternres-7] 3 ternary resolvents (2 bin, 1 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3 transitive binary clauses
c [sort-queue-9] sorted 3374 enqueued variables after 943002 conflicts
c [score-dist-9] active 0 (0%), one 3374 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (3374 remain 88%)
c [simplification-9] removed 0 irredundant clauses 0.0% (58411 remain 77%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 480000
c [simplification-9] new conflict interval 960000
c [simplification-9] penalized conflict interval 960000 = 1 * 960000
c [simplification-9] hard conflict limit 2383002 (soft 1903002 + delta 480000)
c [simplification-9] new conflict limit 1903002 (hard 2383002)
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 -  160.2    3374    58411    983332  103675   6443   187   27   430   15   6%   1024   13   31   27  117%
c -  169.4    3374    58411   1043068  107126   6451   187   27   426   16   6%   1024    8   29   27  106%
c -  178.9    3374    58411   1102910  110028   6457   187   28   436   16   6%   1024   17   32   28  117%
c -  188.9    3374    58411   1163424  112839   6462   187   29   426   26   7%   1024    6   27   28   95%
c -  198.6    3374    58411   1224604  117002   6467   187   29   427   27   7%   1024    6   32   29  110%
c -  208.7    3374    58411   1285148  119709   6471   187   29   425   16   7%   1024    4   33   29  115%
c -  218.7    3374    58411   1346408  122431   6477   187   30   422   27   7%   1024    6   35   29  123%
c -  229.2    3374    58411   1408563  124988   6484   187   29   401   28   7%   1024  -16   32   29  112%
c -  239.7    3374    58411   1471440  127797   6492   187   29   423   28   7%   1024    4   24   29   81%
c -  250.5    3374    58411   1534769  130553   6493   187   29   409   17   7%   1024  -14   26   29   89%
c -  261.6    3374    58411   1598615  133359   6500   187   31   427   18   7%   1024    1   30   30  101%
c -  272.7    3374    58411   1663051  136537   6502   187   30   421   30   7%   1024   -6   28   30   93%
c -  283.8    3374    58411   1727556  139676   6507   187   31   423   18   7%   1024   -2   36   31  115%
c -  294.8    3374    58411   1792159  142424   6511   187   31   412   30   7%   1024  -18   30   31   95%
c -  306.1    3374    58411   1856924  144834   6514   187   33   432   31   8%   1024    1   37   32  117%
c 
c [simplification-10] limit 1903002 conflicts (hard 2383002) hit after 1904299 conflicts
c [quatres-8] found 28514 quaternary clauses 16% in total
c [quatres-8-1] removed 126 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 65 single-self-subsuming ternary resolvents
c [quatres-8-2] added 96 quaternary resolvents
c [ternres-8] limit 96899605 with penalty 0 = 0 + 0
c [ternres-8] all 3374 free variables schedulable
c [ternres-8] 22 ternary resolvents (3 bin, 19 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6056225 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 13 at-most-two constraints of average size 4.1
c [card-4] using previous limit 6056225 for elimination
c [card-4] 15 out of 15 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-3] limit 2422490 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 4897 literals 73%
c [treelook-3] scheduling used 863819 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2422490 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1114866 steps
c [treelook-3] fully completed tree based probing
c [unhide-4] limit 2422490 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 206 tauts, 0 hbrs, 21457 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [sort-queue-10] sorted 3374 enqueued variables after 1904299 conflicts
c [score-dist-10] active 0 (0%), one 3374 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (3374 remain 88%)
c [simplification-10] removed 3 irredundant clauses 0.0% (58408 remain 76%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 3404299 (soft 2904299 + delta 500000)
c [simplification-10] new conflict limit 2904299 (hard 3404299)
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 -  318.6    3374    58408   1922388  147627   6429   187   32   438   31   7%   1024    9   32   32  100%
c -  330.1    3374    58408   1987981  149903   6435   187   33   421   31   8%   1024  -11   28   33   85%
c -  342.1    3374    58408   2054402  152862   6439   187   34   437   19   8%   1024    7   28   33   85%
c -  353.7    3374    58408   2120863  155976   6442   187   34   440   20   8%   1024    9   39   33  117%
c -  365.6    3374    58408   2187235  157958   6443   187   34   435   32   8%   1024    5   36   33  107%
c -  377.7    3374    58408   2254532  160452   6446   187   33   444   20   8%   1024   13   31   33   94%
c -  390.0    3374    58408   2322281  162353   6446   187   33   435   20   8%   1024    5   43   33  129%
c -  402.7    3374    58408   2391163  164504   6447   187   34   434   21   8%   1024   -0   39   33  117%
c -  415.9    3374    58408   2460701  166684   6448   187   34   422   21   8%   1024   -7   39   34  115%
c -  428.9    3374    58408   2531062  168907   6451   187   33   426   21   8%   1024   -4   26   34   76%
c -  442.4    3374    58408   2602009  171469   6453   187   35   436   21   8%   1024    3   42   34  123%
c -  456.3    3374    58408   2673420  173214   6455   187   35   431   21   8%   1024   -2   39   34  114%
c -  470.1    3374    58408   2745958  176236   6457   187   34   421   22   8%   1024  -14   39   34  114%
c -  484.3    3374    58408   2818505  178000   6461   187   36   425   22   8%   1024   -8   41   34  121%
c -  499.0    3374    58408   2892296  180269   6464   187   32   427   22   8%   1024   -3   28   34   81%
c 
c [simplification-11] limit 2904299 conflicts (hard 3404299) hit after 2904299 conflicts
c [quatres-9] found 29925 quaternary clauses 14% in total
c [quatres-9-1] removed 102 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 46 single-self-subsuming ternary resolvents
c [quatres-9-2] added 50 quaternary resolvents
c [ternres-9] limit 164090442 with penalty 0 = 0 + 0
c [ternres-9] all 3374 free variables schedulable
c [ternres-9] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 0 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3374 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 3374 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 2 variables 0% in round 1 in 43809239 steps
c [elim-5-1] backward subsumption/strengthening limit 43809200
c [elim-5-1-1] backward checking 276 touched variables 8%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 2 clauses in 177289 steps
c [elim-5-1] rescheduled 6 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 35326 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 3374 scheduled
c [elim-5] 2 < 1/100 * 3374 = 33 considered unsuccessful
c [bca-4] limit of 10000000 steps and 117300 added (scaled 2)
c [bca-4] 3 out of 6746 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 191938 steps
c [sort-queue-11] sorted 3372 enqueued variables after 2904299 conflicts
c [score-dist-11] active 0 (0%), one 3372 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2 variables 0.1% (3372 remain 88%)
c [simplification-11] removed 8 irredundant clauses 0.0% (58400 remain 76%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
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 4404299 (soft 3904299 + delta 500000)
c [simplification-11] new conflict limit 3904299 (hard 4404299)
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 -  514.7    3372    58400   2966568  182698   6501   185   36   416   22   9%   1024  -15   40   35  116%
c -  529.6    3372    58400   3041291  184952   6502   185   34   425   22   8%   1024   -6   29   35   84%
c -  544.8    3372    58400   3116568  186328   6502   185   35   450   23   8%   1024   14   32   35   92%
c -  560.7    3372    58400   3193356  188011   6506   185   36   431   23   8%   1024   -4   38   35  109%
c -  576.5    3372    58400   3271571  191621   6508   185   36   442   23   8%   1024   10   36   35  102%
c -  592.5    3372    58400   3348958  193663   6509   185   35   437   38   8%   1024    3   33   35   95%
c -  609.0    3372    58400   3427291  196064   6509   185   37   425   24   9%   1024   -7   41   36  115%
c -  625.4    3372    58400   3506004  198010   6510   185   36   429   24   8%   1024    1   38   36  108%
c -  641.9    3372    58400   3585779  200740   6511   185   35   422   24   8%   1024   -3   31   35   89%
c -  658.9    3372    58400   3665863  203332   6514   185   37   436   24   8%   1024    8   36   36  103%
c -  676.1    3372    58400   3745980  204929   6516   185   36   446   25   8%   1024   14   33   36   92%
c -  693.8    3372    58400   3827310  207237   6520   185   38   433   25   9%   1024    3   49   36  137%
c 
c [simplification-12] limit 3904299 conflicts (hard 4404299) hit after 3904299 conflicts
c [quatres-10] found 30786 quaternary clauses 13% in total
c [quatres-10-1] removed 97 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 15 single-self-subsuming ternary resolvents
c [quatres-10-2] added 39 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3372 free variables schedulable
c [ternres-10] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6011518 penalty 3 = 3 + 0
c [gauss-4] extracted 5142 xors of average arity 5.1
c [gauss-4] connected 26106 occurrences of 1040 variables (average 25.1)
c [gauss-4] limit 6011518 penalty 3 = 3 + 0
c [gauss-4] connected 4842 occurrences of 1040 variables (average 4.7)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 200000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 530 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [cce-5] limit of 150287970 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 2 clauses out of 21321 (0%) of length 6
c [cce-5-1] eliminated 9 clauses out of 11103 (0%) of length 5
c [cce-5-1] eliminated 9 clauses out of 6252 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 20 large clauses in 31651230 steps
c [cce-5-1] allowing another 15825615 steps for small clauses
c [cce-5-1] scheduling 836 clauses = 291 binary + 545 ternary
c [cce-5-1] tried to eliminate 836 small clauses 100%
c [cce-5-1] eliminated 11 ternary clauses 2%
c [cce-5-1] eliminated 11 small clauses 1%
c [cce-5-1] eliminated 11 small clauses in 16026720 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 31 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 15799277 steps for small clauses
c [cce-5-2] scheduling 825 clauses = 291 binary + 534 ternary
c [cce-5-2] tried to eliminate 825 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 31 covered clauses in TOTAL during 2 rounds
c [cce-5] 31 < 1/100 * 58400 = 584 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 90172781 penalty 3 = 3 + 0
c [sweep-5-1] 1691 pos 50.1% + 1681 neg 49.9% = 3372 sched 100.0% ret 0
c [sweep-5-1] 2555149 steps 198 queries 79.56 avg class size
c [sweep-5-1] 19352 decisions 197 SAT calls 1027.52 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] 1691 pos 50.1% + 1681 neg 49.9% = 3372 sched 100.0% ret 0
c [sweep-5-2] 2396378 steps 194 queries 112.16 avg class size
c [sweep-5-2] 19132 decisions 193 SAT calls 1038.24 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] 1691 pos 50.1% + 1681 neg 49.9% = 3372 sched 100.0% ret 0
c [sweep-5-3] 2400050 steps 206 queries 73.84 avg class size
c [sweep-5-3] 20242 decisions 205 SAT calls 1102.40 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, 595 queries)
c [sort-queue-12] sorted 3372 enqueued variables after 3904299 conflicts
c [score-dist-12] active 0 (0%), one 3372 (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% (3372 remain 88%)
c [simplification-12] removed 31 irredundant clauses 0.1% (58369 remain 76%)
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 5404299 (soft 4904299 + delta 500000)
c [simplification-12] new conflict limit 4904299 (hard 5404299)
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 -  714.5    3372    58369   3909050  209369   6553   185   36   433   24   8%   1024   -2   38   36  107%
c -  732.3    3372    58369   3991570  211190   6554   185   36   430   25   8%   1024   -9   42   36  117%
c -  751.0    3372    58369   4075031  213856   6556   185   39   419   25   9%   1024  -12   37   36  101%
c -  769.7    3372    58369   4158852  215717   6556   185   37   419   25   9%   1024  -12   38   36  104%
c -  788.6    3372    58369   4243616  218027   6556   185   37   443   26   8%   1024   11   32   37   87%
c -  807.8    3372    58369   4328896  219882   6558   185   36   432   26   8%   1024   -3   33   36   91%
c -  826.8    3372    58369   4415038  223105   6558   185   39   433   26   9%   1024   -3   43   36  118%
c -  846.4    3372    58369   4500940  224092   6558   185   36   435   26   8%   1024    1   30   36   82%
c -  866.7    3372    58369   4588747  226336   6560   185   37   434   27   9%   1024   -1   38   37  104%
c -  887.1    3372    58369   4676810  228653   6560   185   37   440   27   8%   1024    5   38   37  103%
c -  907.4    3372    58369   4765519  230669   6564   185   37   441   27   8%   1024   11   42   36  116%
c -  928.0    3372    58369   4855184  233584   6564   185   38   437   27   9%   1024    1   42   37  116%
c 
c [simplification-13] limit 4904299 conflicts (hard 5404299) hit after 4904299 conflicts
c [quatres-11] found 31355 quaternary clauses 12% in total
c [quatres-11-1] removed 65 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 9 single-self-subsuming ternary resolvents
c [quatres-11-2] added 29 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 3372 free variables schedulable
c [ternres-11] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-11] fully completed ternary resolution
c [transred-10] limit 1000000 with penalty 1 = 1 + 0
c [transred-10] removed 0 transitive binary clauses
c [sort-queue-13] sorted 3372 enqueued variables after 4904299 conflicts
c [score-dist-13] active 0 (0%), one 3372 (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 0 variables 0.0% (3372 remain 88%)
c [simplification-13] removed 0 irredundant clauses 0.0% (58369 remain 76%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] hard conflict limit 7904299 (soft 6904299 + delta 1000000)
c [simplification-13] new conflict limit 6904299 (hard 7904299)
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 -  949.7    3372    58369   4944676  235183   6574   185   38   427   27   9%   1024   -7   31   37   84%
c -  970.6    3372    58369   5035492  238235   6577   185   35   443   27   8%   1024   10   44   37  120%
c -  992.1    3372    58369   5125881  238943   6577   185   35   430   28   8%   1024   -4   31   36   86%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 23 basic ate = 22 trn 96% + 1 lrg 4% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 324657 steps
c bkwd: tried 5469 clauses, 10841 lits, 1.98 lits/clause
c bkwd: checked 529087 occs, 96.74 occs/clause, 48.80 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 37 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 85 large (0% self)
c blkd: 4 bces, 224 removed, 3096070 resolutions, 6334057 steps
c blkd: 28 blocking literals 0%, 0 pure
c bump: 5123133 bumped seen, 434882747 lits 84.9 on average
c card: 4 count, 0 units, 0 am1, 9794941 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1400 subsumed
c card: 9 at-most-one constraints found, average size 3.00
c card: 9 at-most-one constraints used 100%, average size 3.00
c card: 41 at-most-two constraints found, average size 4.10
c card: 40 at-most-two constraints used 98%, average size 4.10
c cces: 5 cces, 8530 eliminated, 8528 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: 1006239 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 48 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 209 equivalent 5%
c deco: 1098 decision-only clauses 0%, 42% reduction
c decs: 40077580 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 161 eliminated 4%, 0 pure 0%
c elms: 9 rounds, 1.8 rounds/bve
c elms: 161 small 100%, 0 large 0%
c elms: 1366 tried small, 162 succeeded 12%, 1204 failed 88%
c elms: 2208 subsumed, 3093 strengthened, 0 blocked
c elms: 1132147 copies, 2865410 resolutions, 375711 ipos
c elms: 214003 subchks, 143052 strchks
c gaus: 4 extractions, 10410 extracted, 4.9 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 20160810 steps, 10080405 extr 50%, 415585 elim 2%
c glue: 31.5 orig avg, 31.5 real avg, 4.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 102 = 28 simple 27% + 68 trn 67% + 6 lrg 6%, 36 sub 35%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5123133 clauses, 62.7 length
c lrnd: 321049397 lits = 337874342 orig - 16824945 removed 5%
c lrnd: 2440403 uips 48%, 2119520 flips 41%
c mins: 4716055 mins 92%, 31 bin 0%, 397082 size 8%
c mins: 246622640 poisoned searches, 20698400 hits, 8% hit rate
c mins: 511609300 used twice searches, 104461632 hits, 20% hit rate
c move: moved 1392, 8 bin 1%, 1384 trn 99%
c otfs: 42755 driving 51%, 41852 restarting 49%
c otfs: str 84607, 82874 red 98%, 1733 irr 2%
c otfs: str 84607, 0 bin 0%, 91 trn 0%, 84516 lrg 100%
c otfs: sub 505, 502 red 99%, 3 irr 1%
c otfs: sub 505, 0 bin 0%, 18 trn 4%, 487 lrg 96%
c phas: 1 computed, 3421 set, 1481 pos (43%), 1940 neg (57%)
c prbs: 3 basic, 5276 probed, 0 failed, 0 lifted
c prbs: 3 simple, 16387 probed, 61 failed, 119 eqs
c prbs: 3 treelook, 6744 probed, 0 failed, 0 lifted
c prom: 696131 locked 17% out of 4031292 tried
c prps: 574828953 props, 14 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 2092 quat, 2091 self1, 229 self2, 508 dup
c queu: 13 sorted, 40077580 next (175 steps 0.00)
c queu: 434930956 enq (0 steps 0.00), 434882747 deq 100%
c redc: 924 clauses 0%, 592323 tried 11%, 1 sat 0%
c redc: 952 lits 0%, 4888364 tried 1%, 1 sat 0%
c redc: 54 times jump level reduced, 10.7 levels on average
c reds: 73 count, 70725.3 conflicts per reduce
c reds: 0 memlim 0%, 73 arith 100%
c reds: 3091924 collected 64%, 1725080 retired 36%
c rmbd: 23 removed, 12 red 52%
c rsts: 37457 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5123133 count (8457068 tried 1.7), 25470 sub out of 5121206 (0.5%)
c swps: 5 count, 13 rounds, 3597 queries (276.7/round)
c swps: 3601 sat calls, 12 unsat (0.8% success rate)
c swps: 128659 decisions 35.7, 2942 conflicts 0.8
c swps; 152.7 avg class size, 203.6 avg environment size
c swps: 0 failed, 12 impls, 6 equivs
c swp0: 1196 type 0 queries, 35 unsat (2.9%), 1195 sat (99.9%)
c swp1: 2401 type 1 queries, 157 unsat (6.5%), 2396 sat (99.8%)
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: 90401700 calls to obtain time
c tops: 546 fixed 13%, 0 its, 0.00 confs/it
c trds: 10 transitive reductions, 53 removed, 0 failed
c trds: 67174 nodes, 4487 edges, 6423 steps
c trim: 206149 words, 0.8 MB
c trnr: 11 count, 49 bin, 397 trn, 20068201 steps
c unhd: 4 count, 6 rounds, 4129050 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: 1035 tauts, 0 bin 0%, 740 trn 71%, 292 lrg 28%
c unhd: 1035 tauts, 3 stamp 0%, 569 red 55%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 23141 str, 0 bin 0%, 55 trn 0%, 23086 lrg 100%, 23079 red 100%
c vars: 3372 remaining 79% and 916 removed 21% out of 4288
c vars: 546 fixed 13%, 161 eliminated 4%, 209 equivalent 5%
c vsts: 34786366404 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 60.5 search visits per propagation, 6735.5 per conflict
c wchs: 11221397509 pushed, 16275484 enlarged, 1202 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5123298       3091924       1725080     229585464      45022310       2582261
c 
c  0 0        212766   4       346   0         0   0 190122933  83< 34004267  76   1959581  76     6.7
c  1 5        255466   5    120225   4    115435   7  21549046   9   4237809   9<   266787  10<    0.7
c  2 6        840731  16    451062  15    369422  21   9475009   4   2464113   5    145705   6     1.1
c  3 9        849250  17    495781  16    341144  20   2973425   1   1211669   3     56186   2     1.1
c  4 14       674987  13    434082  14    232226  13<  1715076   1    859275   2     37499   1     1.3
c  5 21       550604  11<   369184  12<   174316  10   1126769   0    623811   1     27661   1     1.7
c  6 30       433901   8    297991  10    130438   8    757837   0    445541   1     20716   1     2.1
c  7 41       349797   7    245457   8     99777   6    544760   0    333537   1     16219   1     2.6
c  8 54       283041   6    202686   7     76578   4    409585   0    259687   1     13716   1     3.0
c  9 69       225622   4    163362   5     58898   3    312260   0    201500   0     11361   0     3.3
c 10 86       302889   6    218098   7     79635   5    407270   0    264718   1     17079   1     6.7
c 11 126      138641   3     90489   3     45218   3    184022   0    111317   0      9009   0     5.1
c 12 230        5590   0      3154   0      1988   0      7455   0      5057   0       742   0     0.3
c 13 534          13   0         7   0         5   0        17   0         9   0         0   0     0.0
c 
c avg                  4.7           5.1           4.4           0.4           0.7           0.7
c std                  2.8           2.7           2.6           1.1           1.7           1.7
c 
c   28.862   3% bump
c   27.680   3% decide
c    3.066   0% cce
c 
c    5.604 < 1% rest (below)
c 
c    2.018   0% elim
c    1.906   0% sweep
c    1.076   0% quatres
c    0.709   0% probe
c    0.621   0% unhide
c    0.508   0% block
c    0.395   0% gauss
c    0.146   0% card
c    0.118   0% bca
c    0.110   0% ternres
c    0.014   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.404   0% preprocessing     3%
c   11.798   1% inprocessing     97%
c ==================================
c   12.201   1% simplifying
c  987.780  99% search
c ==================================
c  999.982 100% all
c 
c       5162946 conflicts,        5163.0 confs/sec
c          1664 ternaries,        3102.7 confs/ternary
c            47 binaries,       109849.9 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            73 reductions,          0.1 redus/sec,  70725.3 confs/reduction
c         37457 restarts,           37.5 rests/sec,    137.8 confs/restart
c      40077580 decisions,       40078.3 decis/sec,      7.8 decis/conflict
c     574828953 propagations,   574839.4 props/sec,     14.3 props/decision
c 
c 1000.0 seconds, 108.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
