c launch: /data/cnf/sc2014/app/003-80-8.cnf.bz2
c host: atom27
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-80-8.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/003-80-8.cnf.bz2
c no embedded options
c found 'p cnf 13408 478484' header
c read 13408 variables, 478484 clauses, 3138516 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 13021 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   13021   308391         0       0      0     0    0     0   17   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 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 416 variables
c [simpleprobe-1] all 12992 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 17 variables
c [simpleprobe-1] 4953 variables remain 38% (8022 retained 62%)
c [simpleprobe-1] removed 17 variables, found 4 hbrs, 6 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 6 failed, 805 tauts, 0 hbrs, 15 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12973 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 461 variables 4% in round 1 in 2096408 steps
c [elim-1-1] backward subsumption/strengthening limit 2096400
c [elim-1-1-1] backward checking 2387 touched variables 18%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 7 and strengthened 101 clauses in 1438372 steps
c [elim-1-1] rescheduled 145 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 55325 steps
c [elim-1-2] backward subsumption/strengthening limit 55300
c [elim-1-2-1] backward checking 19 touched variables 0%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 55301 steps
c [elim-1-2] fully rescheduled 12509 variables 96%
c [elim-1-3] no variable eliminated in round 3 in 1615915 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 464 = 4% variables out of 12973 scheduled
c [phase-count-1] 301523 negative 99.5% of 302987 except 1464 0.5%
c [phase-count-1] 299384 positive 98.8% of 302987 except 3603 1.2%
c [phase-count-1] less non-negative clauses 1464 than limit 30200 (10.0%)
c [phase-count-1] non-pos/non-neg = 3603/1464 = 2.46 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 12509 negative 100%
c [sort-queue-1] sorted 12509 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12509 (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 510 variables 3.9% (12509 remain 96%)
c [simplification-1] removed 5404 irredundant clauses 1.8% (302987 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] hard conflict limit 14000 (soft 4000 + delta 10000)
c [simplification-1] new conflict limit 4000 (hard 14000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    1.5   12508   302986       877     648     61    15    2    72   23   2%      4   72    8    0 6691%
c i    1.6   12507   302986      1157     877     68    16    2    89   23   2%      4   88    8    0 5644%
c i    1.6   12506   302985      1319    1006     71    18    2    96   23   2%      4   95    8    0 4741%
c i    1.7   12505   302984      2243    1711    131    31    3   137   23   2%      6  135    7    0 2803%
c 
c [simplification-2] limit 4000 conflicts (hard 14000) hit after 4000 conflicts
c [decomp-3] removed 6 variables
c [simpleprobe-2] 4764 schedulable variables 38%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 4731 variables remain 38% (7772 retained 62%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6034 literals 24%
c [treelook-1] scheduling used 300029 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300176 steps
c [treelook-1] 5040 literals remain 20%
c [treelook-1] 2815 variables remain to probed next time 23%
c [treelook-1] removed 0 variables, found 2 hbrs
c [basicprobe-1] limit 2423416 based on 302927 irredundant clauses
c [basicprobe-1-0] 529 sched 4%, 0 failed, 0 lifted, 32 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 535 sched 4%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 535 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 2 variables, found 33 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 19 tauts, 0 hbrs, 109 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12501 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 1218 blocked clauses
c [block-1] 1218 < 1/100 * 302919 = 3029 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8126 clauses out of 103741 (8%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 8126 large clauses in 30000005 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 10814 clauses = 326 binary + 10488 ternary
c [cce-1-1] tried to eliminate 10814 small clauses 100%
c [cce-1-1] eliminated 10 binary clauses 3%
c [cce-1-1] eliminated 1056 ternary clauses 10%
c [cce-1-1] eliminated 1066 small clauses 10%
c [cce-1-1] eliminated 1066 small clauses in 18978237 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 9192 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 5510894 steps for small clauses
c [cce-1-2] scheduling 9748 clauses = 316 binary + 9432 ternary
c [cce-1-2] tried to eliminate 9748 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 9192 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12501 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 9232 not tried 74% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 247 = 2% variables out of 12501 scheduled
c [bca-1] limit of 10000000 steps and 557126 added (scaled 2)
c [bca-1] 19772 out of 24510 literals actually usable 81%
c [bca-1] added 0 blocked clauses in 186897 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3139 pos 25.6% + 9115 neg 74.4% = 12254 sched 100.0% ret 0
c [sweep-1-1] 1000433 steps 403 queries 2228.52 avg class size
c [sweep-1-1] 9712 decisions 402 SAT calls 31.56 avg env size
c [sweep-1-1] 9441 variables remain 77% (2813 retained 23%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 402 queries)
c [sort-queue-2] sorted 12254 enqueued variables after 4000 conflicts
c [score-dist-2] active 0 (0%), one 4805 (39%), zero 7449 (61%)
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 251 variables 2.0% (12254 remain 94%)
c [simplification-2] removed 24669 irredundant clauses 8.1% (278313 remain 90%)
c [simplification-2] maximum reduction of 8% = max (2%, 8%)
c [simplification-2] large reduction 8% >= 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 16000 (soft 6000 + delta 10000)
c [simplification-2] new conflict limit 6000 (hard 16000)
c 
c [simplification-3] limit 6000 conflicts (hard 16000) hit after 6000 conflicts
c [quatres-1] found 34174 quaternary clauses 13% in total
c [quatres-1-1] added 21 double-self-subsuming ternary resolvents
c [quatres-1-2] added 129 single-self-subsuming ternary resolvents
c [quatres-1-2] added 334 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 12254 free variables schedulable
c [ternres-1] 232 ternary resolvents (10 bin, 222 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 4 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4 out of 4 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 1125 xors of average arity 4.9
c [gauss-1] connected 5481 occurrences of 349 variables (average 15.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2 variables
c [transred-1] limit 278307 based on 278307 irredundant clauses
c [transred-1] removed 6 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 181 clauses out of 88017 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 181 large clauses in 30000017 steps
c [cce-2-1] allowing another 15000008 steps for small clauses
c [cce-2-1] scheduling 9699 clauses = 309 binary + 9390 ternary
c [cce-2-1] tried to eliminate 9699 small clauses 100%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 8 small clauses 0%
c [cce-2-1] eliminated 8 small clauses in 18366011 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 189 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 5817035 steps for small clauses
c [cce-2-2] scheduling 9691 clauses = 309 binary + 9382 ternary
c [cce-2-2] tried to eliminate 9691 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 189 covered clauses in TOTAL during 2 rounds
c [cce-2] 189 < 1/100 * 278307 = 2783 considered unsuccessful
c [elim-3] 9232 variables 75% will be scheduled this time
c [elim-3] scheduled 9232 variables 75%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 7192 not tried 59% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9232 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2184 pos 23.1% + 7255 neg 76.9% = 9439 sched 77.0% ret 2813
c [sweep-2-1] 1002177 steps 492 queries 1606.69 avg class size
c [sweep-2-1] 9864 decisions 491 SAT calls 26.79 avg env size
c [sweep-2-1] 6669 variables remain 54% (5583 retained 46%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 491 queries)
c [sort-queue-3] sorted 12252 enqueued variables after 6000 conflicts
c [score-dist-3] active 0 (0%), one 6578 (54%), zero 5674 (46%)
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 2 variables 0.0% (12252 remain 94%)
c [simplification-3] removed 6066 irredundant clauses 2.2% (272247 remain 88%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 10666
c [simplification-3] penalized conflict interval 10666 = 1 * 10666
c [simplification-3] hard conflict limit 26666 (soft 16666 + delta 10000)
c [simplification-3] new conflict limit 16666 (hard 26666)
c 
c [simplification-4] limit 16666 conflicts (hard 26666) hit after 16666 conflicts
c [quatres-2] found 34738 quaternary clauses 13% in total
c [quatres-2-1] added 27 double-self-subsuming ternary resolvents
c [quatres-2-2] added 142 single-self-subsuming ternary resolvents
c [quatres-2-2] added 270 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12252 free variables schedulable
c [ternres-2] 75 ternary resolvents (11 bin, 64 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-11] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1132 literals 5%
c [treelook-2] scheduling used 150033 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150190 steps
c [treelook-2] 592 literals remain 2%
c [treelook-2] 592 variables remain to probed next time 5%
c [treelook-2] removed 0 variables, found 11 hbrs
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 16 tauts, 0 hbrs, 160 literals
c [transred-2] limit 350148 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12251 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 164 blocked clauses
c [block-2] 164 < 1/100 * 272244 = 2722 considered unsuccessful
c [bca-2] limit of 10000000 steps and 544660 added (scaled 2)
c [bca-2] 14325 out of 24488 literals actually usable 58%
c [bca-2] added 0 blocked clauses in 142525 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1854 pos 27.8% + 4807 neg 72.2% = 6661 sched 54.4% ret 5582
c [sweep-3-1] 1000172 steps 619 queries 943.71 avg class size
c [sweep-3-1] 13344 decisions 619 SAT calls 28.47 avg env size
c [sweep-3-1] 4064 variables remain 33% (8179 retained 67%)
c [decomp-13] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 618 queries)
c [sort-queue-4] sorted 12242 enqueued variables after 16666 conflicts
c [score-dist-4] active 0 (0%), one 8205 (67%), zero 4037 (33%)
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 10 variables 0.1% (12242 remain 94%)
c [simplification-4] removed 168 irredundant clauses 0.1% (272079 remain 88%)
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 30666
c [simplification-4] penalized conflict interval 30666 = 1 * 30666
c [simplification-4] hard conflict limit 62665 (soft 47332 + delta 15333)
c [simplification-4] new conflict limit 47332 (hard 62665)
c 
c [simplification-5] limit 47332 conflicts (hard 62665) hit after 47332 conflicts
c [quatres-3] found 36137 quaternary clauses 13% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 30 double-self-subsuming ternary resolvents
c [quatres-3-2] added 211 single-self-subsuming ternary resolvents
c [quatres-3-2] added 265 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12242 free variables schedulable
c [ternres-3] 47 ternary resolvents (4 bin, 43 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 24 xors of average arity 3.0
c [gauss-2] connected 72 occurrences of 12 variables (average 6.0)
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 6245801 penalty 0 = 0 + 0
c [basicprobe-2-0] 579 sched 5%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-2-1] 585 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 8 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [transred-3] limit 1249160 with penalty 0 = 0 + 0
c [transred-3] removed 5 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500028 steps for small clauses
c [cce-3-1] scheduling 9735 clauses = 312 binary + 9423 ternary
c [cce-3-1] tried to eliminate 9735 small clauses 100%
c [cce-3-1] eliminated 7 ternary clauses 0%
c [cce-3-1] eliminated 7 small clauses 0%
c [cce-3-1] eliminated 7 small clauses in 11464661 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 7 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 1767699 steps for small clauses
c [cce-3-2] scheduling 9728 clauses = 312 binary + 9416 ternary
c [cce-3-2] tried to eliminate 4134 small clauses 42%
c [cce-3-2] incomplete small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 7 covered clauses in TOTAL during 2 rounds
c [cce-3] 7 < 1/100 * 272075 = 2720 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12242 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 249832060 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 5 variables 0% in round 1 in 245558416 steps
c [elim-4-1] backward subsumption/strengthening limit 4273644
c [elim-4-1-1] backward checking 11135 touched variables 91%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 16 and strengthened 7 clauses in 4077974 steps
c [elim-4-1] rescheduled 28 variables 0% by backward subsumption
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 5 = 0% variables out of 12242 scheduled
c [elim-4] 5 < 1/100 * 12242 = 122 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1049 pos 25.8% + 3012 neg 74.2% = 4061 sched 33.2% ret 8176
c [sweep-4-1] 1000032 steps 790 queries 501.87 avg class size
c [sweep-4-1] 14955 decisions 789 SAT calls 25.27 avg env size
c [sweep-4-1] 1562 variables remain 13% (10675 retained 87%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 789 queries)
c [sort-queue-5] sorted 12237 enqueued variables after 47332 conflicts
c [score-dist-5] active 0 (0%), one 9808 (80%), zero 2429 (20%)
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 5 variables 0.0% (12237 remain 94%)
c [simplification-5] removed 1327 irredundant clauses 0.5% (270752 remain 88%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30666
c [simplification-5] new conflict interval 61332
c [simplification-5] penalized conflict interval 61332 = 1 * 61332
c [simplification-5] hard conflict limit 139330 (soft 108664 + delta 30666)
c [simplification-5] new conflict limit 108664 (hard 139330)
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 -   22.5   12237   270752     72395   19497   2727   140   12   325   23   4%    667  129   12    7  180%
c 
c [simplification-6] limit 108664 conflicts (hard 139330) hit after 108664 conflicts
c [quatres-4] found 38160 quaternary clauses 14% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 30 double-self-subsuming ternary resolvents
c [quatres-4-2] added 254 single-self-subsuming ternary resolvents
c [quatres-4-2] added 420 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 12237 free variables schedulable
c [ternres-4] 41 ternary resolvents (4 bin, 37 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 15 at-most-two constraints of average size 4.1
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 [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 5 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 382 pos 24.5% + 1180 neg 75.5% = 1562 sched 12.8% ret 10675
c [sweep-5-1] 492030 steps 777 queries 180.64 avg class size
c [sweep-5-1] 11450 decisions 776 SAT calls 20.11 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] 4243 pos 34.7% + 7994 neg 65.3% = 12237 sched 100.0% ret 0
c [sweep-5-2] 3430773 steps 1823 queries 606.54 avg class size
c [sweep-5-2] 42365 decisions 1822 SAT calls 32.26 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-5-3] 4243 pos 34.7% + 7994 neg 65.3% = 12237 sched 100.0% ret 0
c [sweep-5-3] 3369531 steps 1782 queries 592.63 avg class size
c [sweep-5-3] 41777 decisions 1781 SAT calls 33.46 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, 4379 queries)
c [sort-queue-6] sorted 12237 enqueued variables after 108664 conflicts
c [score-dist-6] active 0 (0%), one 11777 (96%), zero 460 (4%)
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% (12237 remain 94%)
c [simplification-6] removed 0 irredundant clauses 0.0% (270752 remain 88%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 61332
c [simplification-6] new conflict interval 122664
c [simplification-6] penalized conflict interval 122664 = 1 * 122664
c [simplification-6] hard conflict limit 292660 (soft 231328 + delta 61332)
c [simplification-6] new conflict limit 231328 (hard 292660)
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 -   31.6   12237   270752    140239   30487   3552   163   11   440   24   2%    897  150   10   10  100%
c -   38.4   12237   270752    205317   43500   3956   173   12   452   26   3%    977   64   13   11  116%
c 
c [simplification-7] limit 231328 conflicts (hard 292660) hit after 231328 conflicts
c [quatres-5] found 43516 quaternary clauses 15% in total
c [quatres-5-1] removed 5 duplicate quaternary clauses
c [quatres-5-1] added 92 double-self-subsuming ternary resolvents
c [quatres-5-2] added 508 single-self-subsuming ternary resolvents
c [quatres-5-2] added 493 quaternary resolvents
c [ternres-5] limit 6347645 with penalty 0 = 0 + 0
c [ternres-5] all 12237 free variables schedulable
c [ternres-5] 25 ternary resolvents (5 bin, 20 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 4629 schedulable variables 38%
c [simpleprobe-3] limit 12695291 penalty 1 = 1 + 0
c [simpleprobe-3] 2346 variables remain 19% (9891 retained 81%)
c [simpleprobe-3] removed 0 variables, found 16 hbrs, 0 units
c [unhide-4] limit 317382 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 189 tauts, 0 hbrs, 348 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 7 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12237 variables 100%
c [block-3] limit of 15869114 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 270752 = 2707 considered unsuccessful
c [bca-3] limit of 10000000 steps and 542002 added (scaled 2)
c [bca-3] 8759 out of 24476 literals actually usable 36%
c [bca-3] added 0 blocked clauses in 145109 steps
c [sort-queue-7] sorted 12237 enqueued variables after 231328 conflicts
c [score-dist-7] active 0 (0%), one 11832 (97%), zero 405 (3%)
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% (12237 remain 94%)
c [simplification-7] removed 1 irredundant clauses 0.0% (270751 remain 88%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 122664
c [simplification-7] new conflict interval 245328
c [simplification-7] penalized conflict interval 245328 = 1 * 245328
c [simplification-7] hard conflict limit 599320 (soft 476656 + delta 122664)
c [simplification-7] new conflict limit 476656 (hard 599320)
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 -   46.4   12237   270751    265384   49100   4638   209   13   497   26   3%   1005   59   14   12  120%
c -   52.2   12237   270751    330194   59701   4953   226   13   565   27   2%   1017   73   14   12  116%
c -   59.3   12237   270751    391349   65905   5145   231   14   508   27   3%   1021   -1   15   13  115%
c -   63.6   12237   270751    458998   81712   5501   247   14   544   28   3%   1023   25   15   13  117%
c 
c [simplification-8] limit 476656 conflicts (hard 599320) hit after 476657 conflicts
c [quatres-6] found 50455 quaternary clauses 15% in total
c [quatres-6-1] removed 8 duplicate quaternary clauses
c [quatres-6-1] added 79 double-self-subsuming ternary resolvents
c [quatres-6-2] added 715 single-self-subsuming ternary resolvents
c [quatres-6-2] added 616 quaternary resolvents
c [ternres-6] limit 11643301 with penalty 0 = 0 + 0
c [ternres-6] all 12237 free variables schedulable
c [ternres-6] 55 ternary resolvents (5 bin, 50 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 582165 penalty 2 = 2 + 0
c [gauss-3] extracted 8 xors of average arity 3.0
c [gauss-3] connected 24 occurrences of 6 variables (average 4.0)
c [gauss-3] limit 582165 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 6 transitive binary clauses
c [transred-6] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 145541265 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 74 clauses out of 77109 (0%) of length 7
c [cce-4-1] eliminated 1060 clauses out of 89617 (1%) of length 6
c [cce-4-1] eliminated 6224 clauses out of 60280 (10%) of length 5
c [cce-4-1] eliminated 252 clauses out of 33083 (1%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 7610 large clauses in 145541418 steps
c [cce-4-1] allowing another 72770709 steps for small clauses
c [cce-4-1] scheduling 9875 clauses = 326 binary + 9549 ternary
c [cce-4-1] tried to eliminate 9875 small clauses 100%
c [cce-4-1] eliminated 2 binary clauses 1%
c [cce-4-1] eliminated 18 ternary clauses 0%
c [cce-4-1] eliminated 20 small clauses 0%
c [cce-4-1] eliminated 25 small clauses in 76231013 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 7635 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 34655161 steps for small clauses
c [cce-4-2] scheduling 9855 clauses = 324 binary + 9531 ternary
c [cce-4-2] tried to eliminate 9855 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 7635 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 12236 variables 100%
c [elim-5] limit of 58216506 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 5322 not tried 43% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 12236 scheduled
c [sweep-6] limit 1746495 penalty 1 = 1 + 0
c [sweep-6-1] 5603 pos 45.8% + 6633 neg 54.2% = 12236 sched 100.0% ret 0
c [sweep-6-1] 1747811 steps 461 queries 1462.00 avg class size
c [sweep-6-1] 18533 decisions 460 SAT calls 58.78 avg env size
c [sweep-6-1] 6938 variables remain 57% (5298 retained 43%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 460 queries)
c [sort-queue-8] sorted 12236 enqueued variables after 476657 conflicts
c [score-dist-8] active 0 (0%), one 11986 (98%), zero 250 (2%)
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 1 variables 0.0% (12236 remain 94%)
c [simplification-8] removed 7728 irredundant clauses 2.9% (263023 remain 85%)
c [simplification-8] maximum reduction of 3% = max (0%, 3%)
c [simplification-8] geometric conflict interval increment 61332 = 245328 / 4
c [simplification-8] new conflict interval 306660
c [simplification-8] penalized conflict interval 306660 = 1 * 306660
c [simplification-8] hard conflict limit 936647 (soft 783317 + delta 153330)
c [simplification-8] new conflict limit 783317 (hard 936647)
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 -   73.4   12236   263023    511602   84402   6394   249   15   564   28   3%   1024   44   15   14  105%
c -   78.6   12236   263023    569419   90400   6530   251   15   519   29   3%   1024  -24   15   14  108%
c -   84.4   12236   263023    642778   94676   6631   251   16   587   29   3%   1024  123   18   16  114%
c -   90.0   12236   263023    701151  100575   6712   253   16   567   30   3%   1024   39   15   16   93%
c 
c [simplification-9] limit 783317 conflicts (hard 936647) hit after 789384 conflicts
c [quatres-7] found 56061 quaternary clauses 16% in total
c [quatres-7-1] removed 19 duplicate quaternary clauses
c [quatres-7-1] added 81 double-self-subsuming ternary resolvents
c [quatres-7-2] added 596 single-self-subsuming ternary resolvents
c [quatres-7-2] added 488 quaternary resolvents
c [ternres-7] limit 17829690 with penalty 0 = 0 + 0
c [ternres-7] all 12236 free variables schedulable
c [ternres-7] 9 ternary resolvents (1 bin, 8 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 [sort-queue-9] sorted 12236 enqueued variables after 789384 conflicts
c [score-dist-9] active 0 (0%), one 12099 (99%), zero 137 (1%)
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% (12236 remain 94%)
c [simplification-9] removed 0 irredundant clauses 0.0% (263023 remain 85%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 306660
c [simplification-9] new conflict interval 613320
c [simplification-9] penalized conflict interval 613320 = 1 * 613320
c [simplification-9] hard conflict limit 1709364 (soft 1402704 + delta 306660)
c [simplification-9] new conflict limit 1402704 (hard 1709364)
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 -   96.0   12236   263023    795561  109861   7563   254   17   654   30   3%   1024  270   17   19   92%
c -   99.3   12236   263023    851059  121228   7647   255   15   694   31   2%   1024  174   14   17   78%
c -  101.9   12236   263023    897340  124974   7688   258   17   640   31   3%   1024   43   17   17  102%
c -  104.2   12236   263023    942452  127540   7735   259   14   591   31   2%   1024    3   15   16   91%
c -  106.4   12236   263023    987286  128229   7812   261   16   626   31   3%   1024   23   19   16  118%
c -  109.0   12236   263023   1034157  129708   7862   262   17   626   32   3%   1024  -18   18   16  116%
c -  111.9   12236   263023   1082422  130503   7930   264   17   657   31   3%   1024    5   18   16  111%
c -  114.8   12236   263023   1132547  134424   7972   265   16   704   32   2%   1024   18   16   16  102%
c -  117.5   12236   263023   1181377  136348   8024   267   14   714   32   2%   1024   55   18   16  116%
c -  120.6   12236   263023   1230561  137856   8083   268   16   606   32   3%   1024  -53   18   16  116%
c -  124.4   12236   263023   1283024  138297   8177   274   15   605   33   2%   1024  -31   15   16   96%
c -  127.7   12236   263023   1336674  144286   8226   275   17   603   33   3%   1024  -28   15   16   94%
c -  131.4   12236   263023   1387518  144447   8294   275   18   557   33   3%   1024  -69   20   17  117%
c 
c [simplification-10] limit 1402704 conflicts (hard 1709364) hit after 1404850 conflicts
c [quatres-8] found 61184 quaternary clauses 17% in total
c [quatres-8-1] removed 9 duplicate quaternary clauses
c [quatres-8-1] added 52 double-self-subsuming ternary resolvents
c [quatres-8-2] added 551 single-self-subsuming ternary resolvents
c [quatres-8-2] added 305 quaternary resolvents
c [ternres-8] limit 27645218 with penalty 0 = 0 + 0
c [ternres-8] all 12236 free variables schedulable
c [ternres-8] 16 ternary resolvents (1 bin, 15 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1727826 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 18 at-most-two constraints of average size 4.1
c [card-4] using previous limit 1727826 for elimination
c [card-4] 20 out of 20 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-3] limit 691130 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 907 literals 4%
c [treelook-3] scheduling used 691191 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 691130 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 254328 steps
c [treelook-3] 0 literals remain 0%
c [treelook-3] 0 variables remain to probed next time 0%
c [treelook-3] removed 0 variables, found 3 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 4 transitive binary clauses
c [cce-5] limit of 69113046 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 76591 (0%) of length 7
c [cce-5-1] eliminated 3 clauses out of 88930 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 7 large clauses in 69113063 steps
c [cce-5-1] allowing another 34556531 steps for small clauses
c [cce-5-1] scheduling 9926 clauses = 332 binary + 9594 ternary
c [cce-5-1] tried to eliminate 9926 small clauses 100%
c [cce-5-1] eliminated 9 ternary clauses 0%
c [cce-5-1] eliminated 9 small clauses 0%
c [cce-5-1] eliminated 9 small clauses in 38241501 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 16 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 15435784 steps for small clauses
c [cce-5-2] scheduling 9917 clauses = 332 binary + 9585 ternary
c [cce-5-2] tried to eliminate 9917 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 16 covered clauses in TOTAL during 2 rounds
c [cce-5] 16 < 1/100 * 263023 = 2630 considered unsuccessful
c [sort-queue-10] sorted 12236 enqueued variables after 1404850 conflicts
c [score-dist-10] active 0 (0%), one 12102 (99%), zero 134 (1%)
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% (12236 remain 94%)
c [simplification-10] removed 16 irredundant clauses 0.0% (263007 remain 85%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 613320
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 2904850 (soft 2404850 + delta 500000)
c [simplification-10] new conflict limit 2404850 (hard 2904850)
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 -  138.1   12236   263007   1441074  144964   8907   275   15   436   33   3%   1024 -167   13   17   78%
c -  141.9   12236   263007   1496874  149266   8924   275   16   726   33   2%   1024  115   15   17   90%
c -  145.2   12236   263007   1550487  152200   8946   275   18   599   33   3%   1024  -52   17   17  101%
c -  148.2   12236   263007   1603347  154694   8951   275   18   708   34   2%   1024   74   19   17  111%
c -  151.5   12236   263007   1655286  154940   8965   275   18   597   34   3%   1024  -34   18   17  106%
c -  154.9   12236   263007   1709485  156792   8985   275   18   633   34   3%   1024   -7   19   17  107%
c -  158.5   12236   263007   1764870  159253   9016   275   15   729   34   2%   1024   69   14   17   80%
c -  163.2   12236   263007   1823143  159731   9096   275   13   670   35   2%   1024   13   11   17   63%
c -  168.2   12236   263007   1884592  163015   9123   275   18   614   35   3%   1024  -26   18   17  104%
c -  176.4   12236   263007   1957187  164124   9410   275   16   637   35   2%   1024   17   17   16  106%
c -  182.5   12236   263007   2042349  179464   9725   288   14   611   36   2%   1024   -0   17   15  115%
c -  186.9   12236   263007   2117889  193906   9981   293   16   553   37   3%   1024  -43   16   15  103%
c -  190.7   12236   263007   2179626  198249  10094   294   17   649   37   3%   1024   47   19   16  121%
c -  194.5   12236   263007   2242657  199893  10204   298   16   565   37   3%   1024  -12   17   16  107%
c -  198.4   12236   263007   2306365  201963  10296   298   17   626   38   3%   1024   23   19   16  115%
c -  202.6   12236   263007   2371891  203330  10386   299   17   529   37   3%   1024  -94   18   17  109%
c 
c [simplification-11] limit 2404850 conflicts (hard 2904850) hit after 2404851 conflicts
c [quatres-9] found 72797 quaternary clauses 17% in total
c [quatres-9-1] removed 35 duplicate quaternary clauses
c [quatres-9-1] added 139 double-self-subsuming ternary resolvents
c [quatres-9-2] added 1062 single-self-subsuming ternary resolvents
c [quatres-9-2] added 780 quaternary resolvents
c [ternres-9] limit 45447046 with penalty 0 = 0 + 0
c [ternres-9] all 12236 free variables schedulable
c [ternres-9] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-5] limit 1136176 with penalty 3 = 3 + 0
c [unhide-5-6] 0 units, 0 failed, 114 tauts, 0 hbrs, 433 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12236 variables 100%
c [block-4] limit of 56808807 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 [bca-4] limit of 10000000 steps and 526502 added (scaled 2)
c [bca-4] 826 out of 24474 literals actually usable 3%
c [bca-4] added 0 blocked clauses in 240682 steps
c [sweep-7] limit 3408528 penalty 2 = 2 + 0
c [sweep-7-1] 3352 pos 48.3% + 3586 neg 51.7% = 6938 sched 56.7% ret 5298
c [sweep-7-1] 3183992 steps 1482 queries 286.66 avg class size
c [sweep-7-1] 36864 decisions 1481 SAT calls 38.52 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 5957 pos 48.7% + 6279 neg 51.3% = 12236 sched 100.0% ret 0
c [sweep-7-2] 227097 steps 27 queries 3837.37 avg class size
c [sweep-7-2] 1885 decisions 26 SAT calls 143.81 avg env size
c [sweep-7-2] 11890 variables remain 97% (346 retained 3%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (2 rounds, 1507 queries)
c [sort-queue-11] sorted 12236 enqueued variables after 2404851 conflicts
c [score-dist-11] active 0 (0%), one 12216 (100%), zero 20 (0%)
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% (12236 remain 94%)
c [simplification-11] removed 6 irredundant clauses 0.0% (263001 remain 85%)
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 3904851 (soft 3404851 + delta 500000)
c [simplification-11] new conflict limit 3404851 (hard 3904851)
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 -  211.6   12236   263001   2439958  204095  11524   299   18   612   38   3%   1024   -1   20   17  120%
c -  220.5   12236   263001   2521251  211933  11647   299   14   603   39   2%   1024   -1   13   16   82%
c -  228.1   12236   263001   2603721  220796  11767   299   15   540   40   3%   1024  -55   22   16  136%
c -  239.2   12236   263001   2689207  225153  12053   301   16   604   40   3%   1024  -20   17   16  106%
c -  254.4   12236   263001   2783916  233488  12406   301   17   717   41   2%   1024  137   16   17   98%
c -  267.0   12236   263001   2879328  247244  12626   302   17   611   42   3%   1024   54   21   18  118%
c -  272.1   12236   263001   2962175  269486  12656   303   16   543   43   3%   1024  -43   19   17  113%
c -  278.7   12236   263001   3026506  266170  12751   303   19   585   43   3%   1024  -13   21   18  115%
c -  286.2   12236   263001   3099160  265073  12831   303   19   626   43   3%   1024   24   22   18  117%
c -  298.6   12236   263001   3179817  265554  12991   303   20   647   44   3%   1024   38   21   19  110%
c -  307.5   12236   263001   3266054  277179  13062   303   16   872   44   2%   1024  178   20   19  106%
c -  313.3   12236   263001   3343413  287651  13120   303   19   615   45   3%   1024 -130   21   18  114%
c -  323.4   12236   263001   3415591  281604  13199   303   23   586   45   4%   1024  -67   25   19  130%
c 
c [simplification-12] limit 3404851 conflicts (hard 3904851) hit after 3441625 conflicts
c [quatres-10] found 91635 quaternary clauses 18% in total
c [quatres-10-1] removed 70 duplicate quaternary clauses
c [quatres-10-1] added 71 double-self-subsuming ternary resolvents
c [quatres-10-2] added 1075 single-self-subsuming ternary resolvents
c [quatres-10-2] added 386 quaternary resolvents
c [ternres-10] limit 75363254 with penalty 0 = 0 + 0
c [ternres-10] all 12236 free variables schedulable
c [ternres-10] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1884081 penalty 3 = 3 + 0
c [gauss-4] extracted 29 xors of average arity 3.0
c [gauss-4] connected 87 occurrences of 12 variables (average 7.2)
c [gauss-4] limit 1884081 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 188408135 penalty 1 = 1 + 0
c [basicprobe-3-0] 767 sched 6%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 768 sched 6%, 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-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2 transitive binary clauses
c [elim-6] 5322 variables 43% will be scheduled this time
c [elim-6] scheduled 5322 variables 43%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1335 not tried 11% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 5322 scheduled
c [sort-queue-12] sorted 12236 enqueued variables after 3441625 conflicts
c [score-dist-12] active 0 (0%), one 12228 (100%), zero 8 (0%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (12236 remain 94%)
c [simplification-12] removed 242 irredundant clauses 0.1% (262759 remain 85%)
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 4941625 (soft 4441625 + delta 500000)
c [simplification-12] new conflict limit 4441625 (hard 4941625)
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 -  334.4   12236   262759   3496549  286692  14345   302   19   621   45   3%   1024    5   22   19  117%
c -  345.0   12236   262759   3578037  289038  14372   302   20   592   45   3%   1024  -12   15   20   78%
c -  350.1   12236   262759   3659769  305143  14376   302   19   488   46   4%   1024  -75   17   19   89%
c -  355.7   12236   262759   3725625  304544  14384   302   22   573   47   4%   1024  -31   26   18  145%
c -  364.1   12236   262759   3795830  298312  14406   302   21   568   46   4%   1024  -54   23   19  122%
c -  369.5   12236   262759   3874109  307885  14413   302   18   416   47   4%   1024 -190   18   19   94%
c -  373.6   12236   262759   3945660  311917  14419   302   17   637   47   3%   1024   30   21   18  116%
c -  381.1   12236   262759   4016781  306417  14432   302   21   573   47   4%   1024  -32   18   19   97%
c -  391.4   12236   262759   4099393  306059  14450   302   19   657   47   3%   1024   46   18   19   94%
c -  399.7   12236   262759   4185798  317240  14469   302   19   586   47   3%   1024  -56   18   20   91%
c -  407.3   12236   262759   4264757  318878  14484   302   20   692   48   3%   1024   45   20   20  103%
c -  415.6   12236   262759   4343106  318930  14499   302   19   625   48   3%   1024   10   20   19  105%
c -  422.9   12236   262759   4426360  323471  14511   302   20   674   48   3%   1024   35   21   19  109%
c 
c [simplification-13] limit 4441625 conflicts (hard 4941625) hit after 4441626 conflicts
c [quatres-11] found 96934 quaternary clauses 18% in total
c [quatres-11-1] removed 86 duplicate quaternary clauses
c [quatres-11-1] added 18 double-self-subsuming ternary resolvents
c [quatres-11-2] added 407 single-self-subsuming ternary resolvents
c [quatres-11-2] added 112 quaternary resolvents
c [ternres-11] limit 100351784 with penalty 0 = 0 + 0
c [ternres-11] all 12236 free variables schedulable
c [ternres-11] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 0 transitive binary clauses
c [cce-6] limit of 125439730 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 16 clauses out of 89996 (0%) of length 6
c [cce-6-1] eliminated 31 clauses out of 53885 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 47 large clauses in 125439808 steps
c [cce-6-1] allowing another 62719904 steps for small clauses
c [cce-6-1] scheduling 10143 clauses = 337 binary + 9806 ternary
c [cce-6-1] tried to eliminate 10143 small clauses 100%
c [cce-6-1] eliminated 4 ternary clauses 0%
c [cce-6-1] eliminated 4 small clauses 0%
c [cce-6-1] eliminated 4 small clauses in 66323988 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 51 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 29557896 steps for small clauses
c [cce-6-2] scheduling 10139 clauses = 337 binary + 9802 ternary
c [cce-6-2] tried to eliminate 10139 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 51 covered clauses in TOTAL during 2 rounds
c [cce-6] 51 < 1/100 * 262759 = 2627 considered unsuccessful
c [sort-queue-13] sorted 12236 enqueued variables after 4441626 conflicts
c [score-dist-13] active 0 (0%), one 12231 (100%), zero 5 (0%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 0 variables 0.0% (12236 remain 94%)
c [simplification-13] removed 51 irredundant clauses 0.0% (262708 remain 85%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
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 5941626 (soft 5441626 + delta 500000)
c [simplification-13] new conflict limit 5441626 (hard 5941626)
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 -  438.1   12236   262708   4507907  322496  14952   302   20   527   48   4%   1024 -111   18   21   84%
c -  447.8   12236   262708   4595235  330240  14971   302   19   599   47   3%   1024  -34   19   20   95%
c -  451.7   12236   262708   4679651  340821  14972   302   14   713   48   2%   1024   50   11   17   67%
c -  459.6   12236   262708   4753457  335281  15003   304   18   575   49   3%   1024  -57   17   18   93%
c -  465.3   12236   262708   4836093  340150  15013   306   19   630   49   3%   1024    8   20   18  110%
c -  471.6   12236   262708   4915924  342354  15026   307   15   710   49   2%   1024  104   13   18   73%
c -  482.8   12236   262708   4997549  339842  15043   309   22   516   50   4%   1024  -80   23   20  117%
c -  496.3   12236   262708   5085369  340484  15062   309   20   638   50   3%   1024   62   18   22   82%
c -  502.3   12236   262708   5175387  356444  15062   309   18   713   51   2%   1024   33   20   19  108%
c -  511.6   12236   262708   5251821  352045  15069   309   18   689   51   3%   1024   40   16   19   84%
c -  522.6   12236   262708   5336546  352732  15089   309   19   608   51   3%   1024    4   19   20   94%
c -  528.4   12236   262708   5424369  361668  15091   309   17   656   51   3%   1024   22   25   18  140%
c 
c [simplification-14] limit 5441626 conflicts (hard 5941626) hit after 5444103 conflicts
c [quatres-12] found 101056 quaternary clauses 18% in total
c [quatres-12-1] removed 63 duplicate quaternary clauses
c [quatres-12-1] added 14 double-self-subsuming ternary resolvents
c [quatres-12-2] added 233 single-self-subsuming ternary resolvents
c [quatres-12-2] added 102 quaternary resolvents
c [ternres-12] limit 127854201 with penalty 0 = 0 + 0
c [ternres-12] all 12236 free variables schedulable
c [ternres-12] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-12] fully completed ternary resolution
c [sort-queue-14] sorted 12236 enqueued variables after 5444103 conflicts
c [score-dist-14] active 0 (0%), one 12231 (100%), zero 5 (0%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 0 variables 0.0% (12236 remain 94%)
c [simplification-14] removed 0 irredundant clauses 0.0% (262708 remain 85%)
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 8444103 (soft 7444103 + delta 1000000)
c [simplification-14] new conflict limit 7444103 (hard 8444103)
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 -  540.0   12236   262708   5505364  355733  15338   309   23   576   51   4%   1024  -15   21   20  106%
c -  548.1   12236   262708   5593994  364156  15340   309   21   624   52   3%   1024   12   19   19   99%
c -  559.6   12236   262708   5678064  362920  15343   309   13   685   52   2%   1024   52   13   19   66%
c -  568.9   12236   262708   5765768  366138  15349   309   24   574   52   4%   1024  -67   33   20  164%
c -  578.2   12236   262708   5852521  368958  15352   309   20   752   53   3%   1024   45   20   20   96%
c -  585.0   12236   262708   5939980  370681  15365   309   19   614   53   3%   1024 -106   22   19  113%
c -  590.5   12236   262708   6026119  375015  15366   309   18   570   52   3%   1024  -85   21   18  116%
c -  600.2   12236   262708   6112957  372729  15370   309   25   535   53   5%   1024  -18   22   19  117%
c -  608.7   12236   262708   6204508  378559  15373   311   20   585   53   3%   1024   -7   20   19  103%
c 1  632.6   12236   262708   6286154  455568  15386   311   27   638   87   4%   1024   30   34   26  132%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 2 basic ate = 2 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 715213 steps
c bkwd: tried 13402 clauses, 26717 lits, 1.99 lits/clause
c bkwd: checked 1584594 occs, 118.24 occs/clause, 59.31 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 21 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 107 large (0% self)
c blkd: 4 bces, 1383 removed, 19913678 resolutions, 34850501 steps
c blkd: 159 blocking literals 1%, 8 pure
c bump: 5929460 bumped seen, 298636300 lits 50.4 on average
c card: 4 count, 0 units, 0 am1, 5820359 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1319 subsumed
c card: 7 at-most-one constraints found, average size 3.00
c card: 7 at-most-one constraints used 100%, average size 3.00
c card: 43 at-most-two constraints found, average size 4.05
c card: 43 at-most-two constraints used 100%, average size 4.05
c cces: 6 cces, 17085 eliminated, 17083 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: 3617000 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 54 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 46 equivalent 0%
c deco: 1415 decision-only clauses 0%, 58% reduction
c decs: 49307202 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 723 eliminated 5%, 0 pure 0%
c elms: 9 rounds, 1.5 rounds/bve
c elms: 711 small 98%, 4 large 1%
c elms: 2631 tried small, 711 succeeded 27%, 1920 failed 73%
c elms: 17652 subsumed, 9391 strengthened, 0 blocked
c elms: 3728821 copies, 10551993 resolutions, 739649 ipos
c elms: 940963 subchks, 566173 strchks
c gaus: 4 extractions, 1186 extracted, 4.8 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10933286 steps, 5466643 extr 50%, 21448 elim 0%
c glue: 17.7 orig avg, 17.7 real avg, 3.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 87 = 20 simple 23% + 60 trn 69% + 7 lrg 8%, 31 sub 36%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5929460 clauses, 34.6 length
c lrnd: 205111078 lits = 213173456 orig - 8062378 removed 4%
c lrnd: 1312848 uips 22%, 4153840 flips 70%
c mins: 5508895 mins 93%, 89 bin 0%, 416616 size 7%
c mins: 124746441 poisoned searches, 14665950 hits, 12% hit rate
c mins: 308745330 used twice searches, 70672627 hits, 23% hit rate
c move: moved 1410, 12 bin 1%, 1398 trn 99%
c otfs: 367045 driving 35%, 668230 restarting 65%
c otfs: str 1035275, 1030491 red 100%, 4784 irr 0%
c otfs: str 1035275, 0 bin 0%, 127 trn 0%, 1035148 lrg 100%
c otfs: sub 6919, 6914 red 100%, 5 irr 0%
c otfs: sub 6919, 0 bin 0%, 31 trn 0%, 6888 lrg 100%
c phas: 1 computed, 12509 set, 0 pos (0%), 12509 neg (100%)
c prbs: 3 basic, 8596 probed, 0 failed, 0 lifted
c prbs: 3 simple, 26953 probed, 6 failed, 1 eqs
c prbs: 3 treelook, 2441 probed, 0 failed, 0 lifted
c prom: 548352 locked 29% out of 1899218 tried
c prps: 457914004 props, 9 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 4571 quat, 5883 self1, 654 self2, 307 dup
c queu: 14 sorted, 49307202 next (137 steps 0.00)
c queu: 298821328 enq (0 steps 0.00), 298636300 deq 100%
c redc: 222 clauses 0%, 671287 tried 11%, 1 sat 0%
c redc: 225 lits 0%, 5977763 tried 3%, 1 sat 0%
c redc: 15 times jump level reduced, 9.1 levels on average
c reds: 87 count, 72254.6 conflicts per reduce
c reds: 0 memlim 0%, 87 arith 100%
c reds: 4037200 collected 77%, 1239511 retired 23%
c rmbd: 15 removed, 2 red 13%
c rsts: 35652 restarts 99%, 318 skipped 1%
c rsts: 318 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5929460 count (6880450 tried 1.2), 179294 sub out of 5925997 (3.0%)
c swps: 7 count, 10 rounds, 8646 queries (864.6/round)
c swps: 8647 sat calls, 1 unsat (1.2% success rate)
c swps: 200749 decisions 23.2, 10351 conflicts 1.2
c swps; 714.1 avg class size, 33.0 avg environment size
c swps: 0 failed, 3 impls, 0 equivs
c swp0: 2878 type 0 queries, 7 unsat (0.2%), 2878 sat (100.0%)
c swp1: 5768 type 1 queries, 70 unsat (1.2%), 5768 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: 110473639 calls to obtain time
c tops: 403 fixed 3%, 4 its, 1571538.50 confs/it
c trds: 11 transitive reductions, 54 removed, 1 failed
c trds: 267391 nodes, 5930 edges, 7509 steps
c trim: 2347306 words, 9.0 MB
c trnr: 12 count, 41 bin, 498 trn, 29793555 steps
c unhd: 5 count, 6 rounds, 3890548 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 6 failed, 6 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1143 tauts, 0 bin 0%, 864 trn 76%, 275 lrg 24%
c unhd: 1143 tauts, 4 stamp 0%, 612 red 54%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1065 str, 0 bin 0%, 58 trn 5%, 1007 lrg 95%, 992 red 93%
c vars: 12236 remaining 91% and 1172 removed 9% out of 13408
c vars: 403 fixed 3%, 723 eliminated 5%, 46 equivalent 0%
c vsts: 15654592062 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 34.2 search visits per propagation, 2488.8 per conflict
c wchs: 6404426061 pushed, 29092091 enlarged, 578 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5930568       4037200       1239511      93559657      21537390       2135058
c 
c  0 0        351757   6      8459   0         0   0  73859682  79  10949419  51    782547  37    10.0
c  1 5        323771   5     87832   2    216985  18   6162707   7<  1348413   6    180216   8     0.8
c  2 6        806516  14    400096  10    352595  28   6582001   7   3148775  15<   438857  21<    2.3
c  3 9       1353473  23   1070211  27    243128  20<  2773016   3   2330277  11    356035  17     3.5
c  4 14      1481577  25<  1254889  31<   156681  13   2091426   2   2041455   9    249975  12     5.7
c  5 21       880878  15    697292  17    108011   9   1157967   1   1030250   5     85537   4     3.4
c  6 30       395828   7    300550   7     69630   6    504782   1    401383   2     25389   1     2.1
c  7 41       177700   3    122828   3     42162   3    226591   0    161595   1      8747   0     1.5
c  8 54        80439   1     50873   1     23755   2    102615   0     66103   0      3493   0     1.1
c  9 69        38173   1     22496   1     12634   1     48105   0     29222   0      1717   0     1.1
c 10 86        28620   0     15817   0     10065   1     35800   0     20941   0      1399   0     1.7
c 11 126        8521   0      4483   0      3068   0     10768   0      6283   0       612   0     1.2
c 12 230        1900   0       861   0       443   0      2395   0      2039   0       396   0     1.1
c 13 534        1415   0       513   0       354   0      1802   0      1235   0       138   0     1.0
c 
c avg                  3.6           4.0           3.2           0.5           1.5           1.8
c std                  1.8           1.5           2.0           1.2           1.9           1.7
c 
c   35.305   6% decide
c   25.445   4% bump
c    8.781   1% cce
c    7.096   1% elim
c    3.276   1% quatres
c    3.218   1% sweep
c 
c    6.916 < 1% rest (below)
c 
c    2.546   0% block
c    2.232   0% probe
c    0.702   0% gauss
c    0.634   0% bca
c    0.404   0% unhide
c    0.191   0% ternres
c    0.150   0% card
c    0.056   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.311   0% preprocessing     4%
c   31.506   5% inprocessing     96%
c ==================================
c   32.817   5% simplifying
c  599.753  95% search
c ==================================
c  632.571 100% all
c 
c       6286154 conflicts,        9937.5 confs/sec
c          3010 ternaries,        2088.4 confs/ternary
c           127 binaries,        49497.3 confs/binary
c             4 iterations,    1571538.5 confs/iteration
c 
c            87 reductions,          0.1 redus/sec,  72254.6 confs/reduction
c         35652 restarts,           56.4 rests/sec,    176.3 confs/restart
c      49307202 decisions,       77947.3 decis/sec,      7.8 decis/conflict
c     457914004 propagations,   723893.5 props/sec,      9.3 props/decision
c 
c 632.6 seconds, 114.9 MB
c launch: done
