c launch: /data/cnf/sc2014/app/post-c32s-ss-8.cnf.bz2
c host: atom27
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/post-c32s-ss-8.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/post-c32s-ss-8.cnf.bz2
c no embedded options
c found 'p cnf 53752 148393' header
c read 53752 variables, 148393 clauses, 346249 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=4
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 48583 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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   48583   135726         0       0      0     0    0     0    9   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 7404 variables
c [simpleprobe-1] all 46348 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 1082 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1082 variables, found 254 hbrs, 213 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 16 units, 134 failed, 18 tauts, 0 hbrs, 19 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 45069 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 35310 variables 78% in round 1 in 5737591 steps
c [elim-1-1] backward subsumption/strengthening limit 5737500
c [elim-1-1-1] backward checking 36479 touched variables 81%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 17 and strengthened 104 clauses in 1166004 steps
c [elim-1-1] rescheduled 251 variables 1% by backward subsumption
c [elim-1-2] eliminated 83 variables 0% in round 2 in 82262 steps
c [elim-1-2] backward subsumption/strengthening limit 82200
c [elim-1-2-1] backward checking 344 touched variables 1%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 9 and strengthened 0 clauses in 82201 steps
c [elim-1-2] rescheduled 35 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 22059 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 35394 = 79% variables out of 45069 scheduled
c [phase-count-1] 42196 negative 92.0% of 45846 except 3650 8.0%
c [phase-count-1] 40305 positive 87.9% of 45846 except 5541 12.1%
c [phase-1] phase bias: 3115 positive 32%, 6560 negative 68%
c [sort-queue-1] sorted 9675 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 9675 (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 38812 variables 80.0% (9675 remain 20%)
c [simplification-1] removed 89880 irredundant clauses 66.2% (45846 remain 34%)
c [simplification-1] maximum reduction of 80% = max (80%, 66%)
c [simplification-1] large reduction 80% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 2 variables
c [simpleprobe-2] all 9673 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 146 variables
c [simpleprobe-2] 2790 variables remain 29% (6737 retained 71%)
c [simpleprobe-2] removed 146 variables, found 1985 hbrs, 146 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19054 literals 100%
c [treelook-1] scheduling used 188863 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301271 steps
c [treelook-1] 18584 literals remain 98%
c [treelook-1] 9527 variables remain to probed next time 100%
c [decomp-5] removed 13 variables
c [treelook-1] removed 13 variables, found 2962 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2325 probes remain 24% after last round
c [basicprobe-1-0] removed 0 variables, found 6295 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 344 tauts, 0 hbrs, 404 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9514 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 5282 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 207 (0%) of length 8
c [cce-1-1] eliminated 3 clauses out of 583 (1%) of length 7
c [cce-1-1] eliminated 8 clauses out of 283 (3%) of length 5
c [cce-1-1] eliminated 83 clauses out of 7553 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 95 large clauses in 6922425 steps
c [cce-1-1] allowing another 3461212 steps for small clauses
c [cce-1-1] scheduling 21384 clauses = 12610 binary + 8774 ternary
c [cce-1-1] tried to eliminate 21384 small clauses 100%
c [cce-1-1] eliminated 2750 binary clauses 22%
c [cce-1-1] eliminated 635 ternary clauses 7%
c [cce-1-1] eliminated 3385 small clauses 16%
c [cce-1-1] eliminated 3385 small clauses in 11980036 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3480 covered clauses in round 1
c [cce-1-2] eliminated 41 clauses out of 7470 (1%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 41 large clauses in 5101681 steps
c [cce-1-2] allowing another 2550840 steps for small clauses
c [cce-1-2] scheduling 17999 clauses = 9860 binary + 8139 ternary
c [cce-1-2] tried to eliminate 17999 small clauses 100%
c [cce-1-2] eliminated 59 binary clauses 1%
c [cce-1-2] eliminated 59 ternary clauses 1%
c [cce-1-2] eliminated 118 small clauses 1%
c [cce-1-2] eliminated 118 small clauses in 8175805 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 159 covered clauses in round 2
c [cce-1-3] eliminated 50 clauses out of 7429 (1%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 50 large clauses in 9835587 steps
c [cce-1-3] allowing another 4917793 steps for small clauses
c [cce-1-3] scheduling 17881 clauses = 9801 binary + 8080 ternary
c [cce-1-3] tried to eliminate 13799 small clauses 77%
c [cce-1-3] eliminated 115 binary clauses 1%
c [cce-1-3] eliminated 14 ternary clauses 0%
c [cce-1-3] eliminated 129 small clauses 1%
c [cce-1-3] eliminated 129 small clauses in 9844176 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 179 covered clauses in round 3
c [cce-1] eliminated 3818 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9514 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 1762 variables 19% in round 1 in 4494946 steps
c [elim-2-1] backward subsumption/strengthening limit 4494900
c [elim-2-1-1] backward checking 5707 touched variables 60%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 12 and strengthened 24 clauses in 622463 steps
c [elim-2-1] rescheduled 92 variables 1% by backward subsumption
c [elim-2-2] eliminated 8 variables 0% in round 2 in 228504 steps
c [elim-2-2] backward subsumption/strengthening limit 228500
c [elim-2-2-1] backward checking 38 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 1 and strengthened 8 clauses in 32317 steps
c [elim-2-2] rescheduled 14 variables 0% by backward subsumption
c [elim-2-3] eliminated 1 variables 0% in round 3 in 32845 steps
c [elim-2-3] backward subsumption/strengthening limit 32800
c [elim-2-3-1] backward checking 0 touched variables 0%
c [elim-2-3-1] fully completed backward checking in 1 rounds
c [elim-2-3] subsumed 0 and strengthened 0 clauses in 26925 steps
c [elim-2] fully completed in 3 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 1771 = 19% variables out of 9514 scheduled
c [bca-1] limit of 10000000 steps and 68522 added (scaled 2)
c [bca-1] 14588 out of 15488 literals actually usable 94%
c [bca-1] added 17 blocked clauses in 36497 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2849 pos 36.8% + 4894 neg 63.2% = 7743 sched 100.0% ret 0
c [sweep-1-1] 1001872 steps 316 queries 254.63 avg class size
c [sweep-1-1] 3416 decisions 325 SAT calls 27.17 avg env size
c [sweep-1-1] 5599 variables remain 72% (2144 retained 28%)
c [decomp-6] removed 39 variables
c [sweep-1-1] removed 39 vars (0 failed, 41 eqs, 20 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 39 vars in TOTAL (1 rounds, 315 queries)
c [sort-queue-2] sorted 2058 enqueued variables after 1000 conflicts
c [score-dist-2] active 5646 (73%), one 0 (0%), zero 2058 (27%)
c [score-dist-2] max exp 508, different 10 (2%)
c [score-dist-2] median active exp 502, avg 502.4
c [simplification-2] removed 1971 variables 20.4% (7704 remain 16%)
c [simplification-2] removed 11925 irredundant clauses 26.0% (33921 remain 25%)
c [simplification-2] maximum reduction of 26% = max (20%, 26%)
c [simplification-2] large reduction 26% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3002 conflicts
c [quatres-1] found 7322 quaternary clauses 66% in total
c [quatres-1-2] added 9 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3563 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 7704 free variables schedulable
c [ternres-1] 9035 ternary resolvents (23 bin, 9012 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 357 at-most-one constraints of average size 3.0
c [card-2] found 19 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 376 out of 376 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 79 at-most-one constraints, 37 used 47%
c [card-2] exported 41 binary clauses, 1.1 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5932 xors of average arity 3.0
c [gauss-1] connected 17768 occurrences of 961 variables (average 18.5)
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-7] removed 2 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15404 literals 100%
c [treelook-2] scheduling used 261150 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 301025 steps
c [treelook-2] 14897 literals remain 97%
c [treelook-2] 7702 variables remain to probed next time 100%
c [decomp-8] removed 5 variables
c [treelook-2] removed 5 variables, found 1807 hbrs
c [transred-1] limit 128696 with penalty 0 = 0 + 0
c [transred-1] removed 215 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7697 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 9 blocked clauses
c [block-2] 9 < 1/100 * 33901 = 339 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 80 (1%) of length 10
c [cce-2-1] eliminated 3 clauses out of 277 (1%) of length 8
c [cce-2-1] eliminated 3 clauses out of 603 (0%) of length 7
c [cce-2-1] eliminated 4 clauses out of 1909 (0%) of length 6
c [cce-2-1] eliminated 61 clauses out of 462 (13%) of length 5
c [cce-2-1] eliminated 54 clauses out of 6989 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 126 large clauses in 4753376 steps
c [cce-2-1] allowing another 2376688 steps for small clauses
c [cce-2-1] scheduling 14764 clauses = 4674 binary + 10090 ternary
c [cce-2-1] tried to eliminate 14764 small clauses 100%
c [cce-2-1] eliminated 34 binary clauses 1%
c [cce-2-1] eliminated 1052 ternary clauses 10%
c [cce-2-1] eliminated 1086 small clauses 7%
c [cce-2-1] eliminated 1086 small clauses in 6759835 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 1212 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2270694 steps for small clauses
c [cce-2-2] scheduling 13678 clauses = 4640 binary + 9038 ternary
c [cce-2-2] tried to eliminate 13678 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 1212 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 7697 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 203 variables 3% in round 1 in 4235757 steps
c [elim-3-1] backward subsumption/strengthening limit 4235700
c [elim-3-1-1] backward checking 1129 touched variables 15%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 10 and strengthened 5 clauses in 135240 steps
c [elim-3-1] rescheduled 38 variables 0% by backward subsumption
c [elim-3-2] eliminated 2 variables 0% in round 2 in 43905 steps
c [elim-3-2] backward subsumption/strengthening limit 43900
c [elim-3-2-1] backward checking 10 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 0 and strengthened 0 clauses in 14263 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 205 = 3% variables out of 7697 scheduled
c [bca-2] limit of 10000000 steps and 65316 added (scaled 2)
c [bca-2] 7290 out of 14986 literals actually usable 49%
c [bca-2] added 7 blocked clauses in 21770 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1971 pos 35.8% + 3527 neg 64.2% = 5498 sched 73.4% ret 1994
c [sweep-2-1] 1001873 steps 265 queries 138.27 avg class size
c [sweep-2-1] 2829 decisions 263 SAT calls 27.22 avg env size
c [sweep-2-1] 4394 variables remain 59% (3098 retained 41%)
c [decomp-9] removed 35 variables
c [sweep-2-1] removed 35 vars (0 failed, 38 eqs, 22 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 35 vars in TOTAL (1 rounds, 264 queries)
c [sort-queue-3] sorted 1563 enqueued variables after 3002 conflicts
c [score-dist-3] active 5894 (79%), one 0 (0%), zero 1563 (21%)
c [score-dist-3] max exp 508, different 18 (4%)
c [score-dist-3] median active exp 502, avg 499.6
c [simplification-3] removed 247 variables 3.2% (7457 remain 15%)
c [simplification-3] removed 1595 irredundant clauses 4.7% (32326 remain 24%)
c [simplification-3] maximum reduction of 5% = max (3%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15002 (soft 5002 + delta 10000)
c [simplification-3] new conflict limit 5002 (hard 15002)
c 
c [simplification-4] limit 5002 conflicts (hard 15002) hit after 5002 conflicts
c [quatres-2] found 10538 quaternary clauses 72% in total
c [quatres-2-1] removed 7 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 30 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2314 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7457 free variables schedulable
c [ternres-2] 569 ternary resolvents (8 bin, 561 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-10] removed 11 variables
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 53 tauts, 0 hbrs, 1884 literals
c [transred-2] limit 271635 with penalty 0 = 0 + 0
c [transred-2] removed 436 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 270 (0%) of length 8
c [cce-3-1] eliminated 1 clauses out of 612 (0%) of length 7
c [cce-3-1] eliminated 2 clauses out of 1923 (0%) of length 6
c [cce-3-1] eliminated 47 clauses out of 461 (10%) of length 5
c [cce-3-1] eliminated 111 clauses out of 6734 (2%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 162 large clauses in 11518299 steps
c [cce-3-1] allowing another 5759149 steps for small clauses
c [cce-3-1] scheduling 13020 clauses = 4012 binary + 9008 ternary
c [cce-3-1] tried to eliminate 13020 small clauses 100%
c [cce-3-1] eliminated 165 binary clauses 4%
c [cce-3-1] eliminated 414 ternary clauses 5%
c [cce-3-1] eliminated 579 small clauses 4%
c [cce-3-1] eliminated 579 small clauses in 11569003 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 741 covered clauses in round 1
c [cce-3-2] eliminated 2 clauses out of 414 (0%) of length 5
c [cce-3-2] eliminated 128 clauses out of 6623 (2%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 130 large clauses in 11580459 steps
c [cce-3-2] allowing another 5790229 steps for small clauses
c [cce-3-2] scheduling 12441 clauses = 3847 binary + 8594 ternary
c [cce-3-2] tried to eliminate 12441 small clauses 100%
c [cce-3-2] eliminated 25 binary clauses 1%
c [cce-3-2] eliminated 48 ternary clauses 1%
c [cce-3-2] eliminated 73 small clauses 1%
c [cce-3-2] eliminated 73 small clauses in 11243955 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 203 covered clauses in round 2
c [cce-3-3] eliminated 3 clauses out of 1921 (0%) of length 6
c [cce-3-3] eliminated 1 clauses out of 412 (0%) of length 5
c [cce-3-3] eliminated 3 clauses out of 6495 (0%) of length 4
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] eliminated 7 large clauses in 7187043 steps
c [cce-3-3] allowing another 3593521 steps for small clauses
c [cce-3-3] scheduling 12368 clauses = 3822 binary + 8546 ternary
c [cce-3-3] tried to eliminate 8365 small clauses 68%
c [cce-3-3] eliminated 1 binary clauses 0%
c [cce-3-3] eliminated 3 ternary clauses 0%
c [cce-3-3] eliminated 4 small clauses 0%
c [cce-3-3] eliminated 4 small clauses in 7187042 steps
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 11 covered clauses in round 3
c [cce-3] eliminated 955 covered clauses in TOTAL during 3 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7446 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 202 variables 3% in round 1 in 4188296 steps
c [elim-4-1] backward subsumption/strengthening limit 4188200
c [elim-4-1-1] backward checking 1078 touched variables 14%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 15 and strengthened 48 clauses in 128708 steps
c [elim-4-1] rescheduled 113 variables 2% by backward subsumption
c [elim-4-2] eliminated 4 variables 0% in round 2 in 118046 steps
c [elim-4-2] backward subsumption/strengthening limit 118000
c [elim-4-2-1] backward checking 35 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 5 clauses in 22725 steps
c [elim-4-2] rescheduled 19 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 48917 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 206 = 3% variables out of 7446 scheduled
c [bca-3] limit of 10000000 steps and 62562 added (scaled 2)
c [bca-3] 5599 out of 14482 literals actually usable 39%
c [bca-3] added 11 blocked clauses in 20788 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1784 pos 42.2% + 2444 neg 57.8% = 4228 sched 58.4% ret 3012
c [sweep-3-1] 1000243 steps 246 queries 231.24 avg class size
c [sweep-3-1] 2470 decisions 252 SAT calls 29.63 avg env size
c [sweep-3-1] 3337 variables remain 46% (3903 retained 54%)
c [decomp-11] removed 30 variables
c [sweep-3-1] removed 30 vars (0 failed, 31 eqs, 25 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 30 vars in TOTAL (1 rounds, 245 queries)
c [sort-queue-4] sorted 1067 enqueued variables after 5002 conflicts
c [score-dist-4] active 6143 (85%), one 0 (0%), zero 1067 (15%)
c [score-dist-4] max exp 508, different 25 (5%)
c [score-dist-4] median active exp 501, avg 498.4
c [simplification-4] removed 247 variables 3.3% (7210 remain 15%)
c [simplification-4] removed 1366 irredundant clauses 4.2% (30960 remain 23%)
c [simplification-4] maximum reduction of 4% = max (3%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 19002 (soft 9002 + delta 10000)
c [simplification-4] new conflict limit 9002 (hard 19002)
c 
c [simplification-5] limit 9002 conflicts (hard 19002) hit after 9003 conflicts
c [quatres-3] found 11972 quaternary clauses 72% in total
c [quatres-3-1] removed 37 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 26 single-self-subsuming ternary resolvents
c [quatres-3-2] added 594 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7210 free variables schedulable
c [ternres-3] 790 ternary resolvents (11 bin, 779 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4108 xors of average arity 3.0
c [gauss-2] connected 12258 occurrences of 991 variables (average 12.4)
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 [decomp-12] removed 5 variables
c [basicprobe-2] limit 1375315 penalty 1 = 1 + 0
c [basicprobe-2-0] 2068 sched 29%, 1 failed, 0 lifted, 9601 hbrs
c [decomp-13] removed 1 variables
c [basicprobe-2-1] 1895 probes remain 26% after last round
c [basicprobe-2-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 1 variables, found 9646 hbrs
c [bate-1] eliminated 85 asymmetric tautologies during probing
c [transred-3] limit 550126 with penalty 0 = 0 + 0
c [transred-3] removed 1161 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 7204 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 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 * 30857 = 308 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 81 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 103 (1%) of length 9
c [cce-4-1] eliminated 1 clauses out of 271 (0%) of length 8
c [cce-4-1] eliminated 1 clauses out of 620 (0%) of length 7
c [cce-4-1] eliminated 15 clauses out of 1992 (1%) of length 6
c [cce-4-1] eliminated 47 clauses out of 544 (9%) of length 5
c [cce-4-1] eliminated 58 clauses out of 6227 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 124 large clauses in 3874892 steps
c [cce-4-1] allowing another 1937446 steps for small clauses
c [cce-4-1] scheduling 12521 clauses = 3670 binary + 8851 ternary
c [cce-4-1] tried to eliminate 12521 small clauses 100%
c [cce-4-1] eliminated 32 binary clauses 1%
c [cce-4-1] eliminated 794 ternary clauses 9%
c [cce-4-1] eliminated 826 small clauses 7%
c [cce-4-1] eliminated 826 small clauses in 4958596 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 950 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 1898560 steps for small clauses
c [cce-4-2] scheduling 11695 clauses = 3638 binary + 8057 ternary
c [cce-4-2] tried to eliminate 11695 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 950 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7204 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 171 variables 2% in round 1 in 4099207 steps
c [elim-5-1] backward subsumption/strengthening limit 4099200
c [elim-5-1-1] backward checking 1044 touched variables 14%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 10 clauses in 113064 steps
c [elim-5-1] rescheduled 31 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 10344 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 171 = 2% variables out of 7204 scheduled
c [bca-4] limit of 10000000 steps and 60011 added (scaled 2)
c [bca-4] 4592 out of 14068 literals actually usable 33%
c [bca-4] added 4 blocked clauses in 20999 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1364 pos 41.8% + 1898 neg 58.2% = 3262 sched 46.4% ret 3771
c [sweep-4-1] 1000207 steps 282 queries 183.61 avg class size
c [sweep-4-1] 2766 decisions 269 SAT calls 29.75 avg env size
c [sweep-4-1] 2598 variables remain 37% (4435 retained 63%)
c [decomp-14] removed 47 variables
c [sweep-4-1] removed 47 vars (0 failed, 53 eqs, 37 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 47 vars in TOTAL (1 rounds, 281 queries)
c [sort-queue-5] sorted 901 enqueued variables after 9003 conflicts
c [score-dist-5] active 6085 (87%), one 0 (0%), zero 901 (13%)
c [score-dist-5] max exp 508, different 38 (7%)
c [score-dist-5] median active exp 501, avg 495.9
c [simplification-5] removed 224 variables 3.1% (6986 remain 14%)
c [simplification-5] removed 1318 irredundant clauses 4.3% (29642 remain 22%)
c [simplification-5] maximum reduction of 4% = max (3%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 8000
c [simplification-5] penalized conflict interval 8000 = 1 * 8000
c [simplification-5] hard conflict limit 27003 (soft 17003 + delta 10000)
c [simplification-5] new conflict limit 17003 (hard 27003)
c 
c [simplification-6] limit of 327 binary hit after 327 binaries
c [quatres-4] found 12044 quaternary clauses 70% in total
c [quatres-4-1] removed 41 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 16 single-self-subsuming ternary resolvents
c [quatres-4-2] added 424 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6986 free variables schedulable
c [ternres-4] 623 ternary resolvents (14 bin, 609 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 106 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 106 out of 106 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 3 variables
c [simpleprobe-3] 1691 schedulable variables 24%
c [simpleprobe-3] limit 3439359 penalty 0 = 0 + 0
c [decomp-16] removed 32 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 32 variables, found 513 hbrs, 0 units
c [transred-4] limit 859839 with penalty 0 = 0 + 0
c [transred-4] removed 1155 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 625 (0%) of length 7
c [cce-5-1] eliminated 4 clauses out of 2043 (0%) of length 6
c [cce-5-1] eliminated 35 clauses out of 553 (6%) of length 5
c [cce-5-1] eliminated 161 clauses out of 5982 (3%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 201 large clauses in 11749737 steps
c [cce-5-1] allowing another 5874868 steps for small clauses
c [cce-5-1] scheduling 11652 clauses = 3122 binary + 8530 ternary
c [cce-5-1] tried to eliminate 11652 small clauses 100%
c [cce-5-1] eliminated 59 binary clauses 2%
c [cce-5-1] eliminated 371 ternary clauses 4%
c [cce-5-1] eliminated 430 small clauses 4%
c [cce-5-1] eliminated 430 small clauses in 10950283 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 631 covered clauses in round 1
c [cce-5-2] eliminated 1 clauses out of 624 (0%) of length 7
c [cce-5-2] eliminated 3 clauses out of 2039 (0%) of length 6
c [cce-5-2] eliminated 1 clauses out of 518 (0%) of length 5
c [cce-5-2] eliminated 100 clauses out of 5821 (2%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 105 large clauses in 11096546 steps
c [cce-5-2] allowing another 5548273 steps for small clauses
c [cce-5-2] scheduling 11222 clauses = 3063 binary + 8159 ternary
c [cce-5-2] tried to eliminate 11222 small clauses 100%
c [cce-5-2] eliminated 26 binary clauses 1%
c [cce-5-2] eliminated 32 ternary clauses 0%
c [cce-5-2] eliminated 58 small clauses 1%
c [cce-5-2] eliminated 58 small clauses in 10409877 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 163 covered clauses in round 2
c [cce-5-3] eliminated 2 clauses out of 2036 (0%) of length 6
c [cce-5-3] eliminated 3 clauses out of 517 (1%) of length 5
c [cce-5-3] eliminated 38 clauses out of 5721 (1%) of length 4
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] eliminated 43 large clauses in 8639841 steps
c [cce-5-3] allowing another 4319920 steps for small clauses
c [cce-5-3] scheduling 11164 clauses = 3037 binary + 8127 ternary
c [cce-5-3] tried to eliminate 10002 small clauses 90%
c [cce-5-3] eliminated 3 binary clauses 0%
c [cce-5-3] eliminated 8 ternary clauses 0%
c [cce-5-3] eliminated 11 small clauses 0%
c [cce-5-3] eliminated 11 small clauses in 8639841 steps
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 54 covered clauses in round 3
c [cce-5] eliminated 848 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6951 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 165 variables 2% in round 1 in 4058724 steps
c [elim-6-1] backward subsumption/strengthening limit 4058700
c [elim-6-1-1] backward checking 1007 touched variables 14%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 3 and strengthened 17 clauses in 108072 steps
c [elim-6-1] rescheduled 69 variables 1% by backward subsumption
c [elim-6-2] eliminated 2 variables 0% in round 2 in 24489 steps
c [elim-6-2] backward subsumption/strengthening limit 24400
c [elim-6-2-1] backward checking 18 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 1 clauses in 16622 steps
c [elim-6-2] rescheduled 5 variables 0% by backward subsumption
c [elim-6-3] eliminated 3 variables 0% in round 3 in 1825 steps
c [elim-6-3] backward subsumption/strengthening limit 1800
c [elim-6-3-1] backward checking 11 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 0 and strengthened 2 clauses in 1801 steps
c [elim-6] incomplete 7 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 170 = 2% variables out of 6951 scheduled
c [bca-5] limit of 10000000 steps and 57457 added (scaled 2)
c [bca-5] 3626 out of 13564 literals actually usable 27%
c [bca-5] added 3 blocked clauses in 21519 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1295 pos 52.3% + 1182 neg 47.7% = 2477 sched 36.5% ret 4304
c [sweep-5-1] 3649134 steps 1259 queries 34.99 avg class size
c [sweep-5-1] 11499 decisions 1128 SAT calls 31.09 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 209 variables
c [sweep-5-1] removed 209 vars (0 failed, 284 eqs, 228 impls)
c [sweep-5-2] 3179 pos 48.4% + 3393 neg 51.6% = 6572 sched 100.0% ret 0
c [sweep-5-2] 6011950 steps 1408 queries 33.06 avg class size
c [sweep-5-2] 15981 decisions 1293 SAT calls 35.88 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-18] removed 88 variables
c [sweep-5-2] removed 88 vars (0 failed, 188 eqs, 177 impls)
c [sweep-5-3] 3146 pos 48.5% + 3338 neg 51.5% = 6484 sched 100.0% ret 0
c [sweep-5-3] 344059 steps 39 queries 690.82 avg class size
c [sweep-5-3] 1122 decisions 38 SAT calls 58.68 avg env size
c [sweep-5-3] 5989 variables remain 92% (495 retained 8%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 297 vars in TOTAL (3 rounds, 2703 queries)
c [sort-queue-6] sorted 682 enqueued variables after 14215 conflicts
c [score-dist-6] active 5802 (89%), one 0 (0%), zero 682 (11%)
c [score-dist-6] max exp 510, different 59 (12%)
c [score-dist-6] median active exp 503, avg 499.2
c [simplification-6] removed 502 variables 7.2% (6484 remain 13%)
c [simplification-6] removed 1825 irredundant clauses 6.2% (27817 remain 20%)
c [simplification-6] maximum reduction of 7% = max (7%, 6%)
c [simplification-6] forced so keeping old conflict interval 8000
c [simplification-6] conflict limit remains at 17003 (hard 27003)
c [simplification-6] new binary interval 1000
c 
c [simplification-7] limit 17003 conflicts (hard 27003) hit after 17003 conflicts
c [quatres-5] found 11013 quaternary clauses 66% in total
c [quatres-5-1] removed 293 duplicate quaternary clauses
c [quatres-5-2] added 36 single-self-subsuming ternary resolvents
c [quatres-5-2] added 237 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6484 free variables schedulable
c [ternres-5] 1434 ternary resolvents (14 bin, 1420 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 5 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 12958 literals 100%
c [treelook-3] scheduling used 297058 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301922 steps
c [treelook-3] 12530 literals remain 97%
c [treelook-3] 6457 variables remain to probed next time 100%
c [decomp-21] removed 6 variables
c [treelook-3] removed 6 variables, found 262 hbrs
c [unhide-4] limit 52902 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 8009 tauts, 0 hbrs, 9632 literals
c [transred-5] limit 1058040 with penalty 0 = 0 + 0
c [transred-5] removed 1010 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 7 clauses out of 2013 (0%) of length 6
c [cce-6-1] eliminated 70 clauses out of 697 (10%) of length 5
c [cce-6-1] eliminated 92 clauses out of 4917 (2%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 169 large clauses in 2779544 steps
c [cce-6-1] allowing another 1389772 steps for small clauses
c [cce-6-1] scheduling 10878 clauses = 2692 binary + 8186 ternary
c [cce-6-1] tried to eliminate 10878 small clauses 100%
c [cce-6-1] eliminated 37 binary clauses 1%
c [cce-6-1] eliminated 244 ternary clauses 3%
c [cce-6-1] eliminated 281 small clauses 3%
c [cce-6-1] eliminated 281 small clauses in 3772602 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 450 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 1359360 steps for small clauses
c [cce-6-2] scheduling 10597 clauses = 2655 binary + 7942 ternary
c [cce-6-2] tried to eliminate 10597 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 450 covered clauses in TOTAL during 2 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 6473 variables 100%
c [elim-7] limit of 21160819 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 231 variables 4% in round 1 in 4047748 steps
c [elim-7-1] backward subsumption/strengthening limit 4047700
c [elim-7-1-1] backward checking 1564 touched variables 24%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 5 and strengthened 23 clauses in 180097 steps
c [elim-7-1] rescheduled 93 variables 1% by backward subsumption
c [elim-7-2] eliminated 6 variables 0% in round 2 in 114955 steps
c [elim-7-2] backward subsumption/strengthening limit 114900
c [elim-7-2-1] backward checking 53 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 1 and strengthened 4 clauses in 24091 steps
c [elim-7-2] rescheduled 17 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 12707 steps
c [elim-7-3] backward subsumption/strengthening limit 12700
c [elim-7-3-1] backward checking 8 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 1 and strengthened 3 clauses in 12701 steps
c [elim-7] incomplete 7 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 238 = 4% variables out of 6473 scheduled
c [bca-6] limit of 10000000 steps and 54483 added (scaled 2)
c [bca-6] 3261 out of 12472 literals actually usable 26%
c [bca-6] added 3 blocked clauses in 19944 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 2687 pos 46.7% + 3071 neg 53.3% = 5758 sched 92.3% ret 477
c [sweep-6-1] 1048357 steps 119 queries 423.38 avg class size
c [sweep-6-1] 2870 decisions 117 SAT calls 43.39 avg env size
c [sweep-6-1] 4408 variables remain 71% (1827 retained 29%)
c [decomp-22] removed 4 variables
c [sweep-6-1] removed 4 vars (0 failed, 2 eqs, 3 impls)
c [sweep-6] 4 < 1/1000 * 6235 = 6 considered unsuccessful
c [sweep-6] removed 4 vars in TOTAL (1 rounds, 118 queries)
c [sort-queue-7] sorted 607 enqueued variables after 17003 conflicts
c [score-dist-7] active 5624 (90%), one 0 (0%), zero 607 (10%)
c [score-dist-7] max exp 509, different 67 (13%)
c [score-dist-7] median active exp 499, avg 496.0
c [simplification-7] removed 253 variables 3.9% (6231 remain 13%)
c [simplification-7] removed 846 irredundant clauses 3.0% (26971 remain 20%)
c [simplification-7] maximum reduction of 4% = max (4%, 3%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 12000
c [simplification-7] penalized conflict interval 12000 = 1 * 12000
c [simplification-7] hard conflict limit 39003 (soft 29003 + delta 10000)
c [simplification-7] new conflict limit 29003 (hard 39003)
c 
c [simplification-8] limit 29003 conflicts (hard 39003) hit after 29003 conflicts
c [quatres-6] found 10112 quaternary clauses 62% in total
c [quatres-6-1] removed 20 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 32 single-self-subsuming ternary resolvents
c [quatres-6-2] added 501 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6231 free variables schedulable
c [ternres-6] 956 ternary resolvents (42 bin, 914 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 2181 xors of average arity 3.0
c [gauss-3] connected 6496 occurrences of 832 variables (average 7.8)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 2 variables
c [basicprobe-3] limit 8716024 penalty 0 = 0 + 0
c [basicprobe-3-0] 1276 sched 20%, 2 failed, 0 lifted, 713 hbrs
c [decomp-24] removed 3 variables
c [basicprobe-3-1] 1237 sched 20%, 0 failed, 0 lifted, 99 hbrs
c [basicprobe-3-2] 1204 sched 19%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-3-3] 1199 sched 19%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-3-4] 1190 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-3-5] 1187 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-3-6] 1187 sched 19%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-7] 1187 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-3-8] 1185 sched 19%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 3 variables, found 892 hbrs
c [bate-2] eliminated 2 asymmetric tautologies during probing
c [transred-6] limit 1743204 with penalty 0 = 0 + 0
c [transred-6] removed 1096 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6226 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 3 blocked clauses
c [block-4] 3 < 1/100 * 26943 = 269 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 632 (0%) of length 7
c [cce-7-1] eliminated 4 clauses out of 2029 (0%) of length 6
c [cce-7-1] eliminated 72 clauses out of 758 (9%) of length 5
c [cce-7-1] eliminated 305 clauses out of 4939 (6%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 382 large clauses in 9887355 steps
c [cce-7-1] allowing another 4943677 steps for small clauses
c [cce-7-1] scheduling 10115 clauses = 2455 binary + 7660 ternary
c [cce-7-1] tried to eliminate 10115 small clauses 100%
c [cce-7-1] eliminated 95 binary clauses 4%
c [cce-7-1] eliminated 452 ternary clauses 6%
c [cce-7-1] eliminated 547 small clauses 5%
c [cce-7-1] eliminated 547 small clauses in 7867711 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 929 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 2025 (0%) of length 6
c [cce-7-2] eliminated 2 clauses out of 686 (0%) of length 5
c [cce-7-2] eliminated 61 clauses out of 4634 (1%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 64 large clauses in 9538644 steps
c [cce-7-2] allowing another 4769322 steps for small clauses
c [cce-7-2] scheduling 9568 clauses = 2360 binary + 7208 ternary
c [cce-7-2] tried to eliminate 9568 small clauses 100%
c [cce-7-2] eliminated 12 binary clauses 1%
c [cce-7-2] eliminated 29 ternary clauses 0%
c [cce-7-2] eliminated 41 small clauses 0%
c [cce-7-2] eliminated 41 small clauses in 7429843 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 105 covered clauses in round 2
c [cce-7-3] eliminated 3 clauses out of 2024 (0%) of length 6
c [cce-7-3] eliminated 4 clauses out of 684 (1%) of length 5
c [cce-7-3] eliminated 46 clauses out of 4573 (1%) of length 4
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 53 large clauses in 9387196 steps
c [cce-7-3] allowing another 4693598 steps for small clauses
c [cce-7-3] scheduling 9527 clauses = 2348 binary + 7179 ternary
c [cce-7-3] tried to eliminate 9527 small clauses 100%
c [cce-7-3] eliminated 10 binary clauses 0%
c [cce-7-3] eliminated 22 ternary clauses 0%
c [cce-7-3] eliminated 32 small clauses 0%
c [cce-7-3] eliminated 32 small clauses in 7332217 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 85 covered clauses in round 3
c [cce-7] eliminated 1119 covered clauses in TOTAL during 3 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 6226 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 697281920 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 206 variables 3% in round 1 in 3922936 steps
c [elim-8-1] backward subsumption/strengthening limit 3922900
c [elim-8-1-1] backward checking 1280 touched variables 21%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 18 and strengthened 49 clauses in 152172 steps
c [elim-8-1] rescheduled 175 variables 3% by backward subsumption
c [elim-8-2] eliminated 12 variables 0% in round 2 in 110614 steps
c [elim-8-2] backward subsumption/strengthening limit 110600
c [elim-8-2-1] backward checking 80 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 3 and strengthened 4 clauses in 24834 steps
c [elim-8-2] rescheduled 21 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 10427 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 218 = 4% variables out of 6226 scheduled
c [bca-7] limit of 10000000 steps and 51592 added (scaled 2)
c [bca-7] 2097 out of 12018 literals actually usable 17%
c [bca-7] added 4 blocked clauses in 22913 steps
c [sort-queue-8] sorted 330 enqueued variables after 29003 conflicts
c [score-dist-8] active 5678 (95%), one 0 (0%), zero 330 (5%)
c [score-dist-8] max exp 510, different 109 (21%)
c [score-dist-8] median active exp 495, avg 487.7
c [simplification-8] removed 223 variables 3.6% (6008 remain 12%)
c [simplification-8] removed 1436 irredundant clauses 5.3% (25535 remain 19%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 41003 (soft 31003 + delta 10000)
c [simplification-8] new conflict limit 31003 (hard 41003)
c 
c [simplification-9] limit 31003 conflicts (hard 41003) hit after 31003 conflicts
c [quatres-7] found 9473 quaternary clauses 61% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-2] added 25 single-self-subsuming ternary resolvents
c [quatres-7-2] added 252 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 6008 free variables schedulable
c [ternres-7] 427 ternary resolvents (23 bin, 404 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-4] all 6008 free variables schedulable
c [simpleprobe-4] limit 7475187 penalty 0 = 0 + 0
c [decomp-33] removed 27 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 27 variables, found 717 hbrs, 2 units
c [transred-7] limit 1868796 with penalty 0 = 0 + 0
c [transred-7] removed 931 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 632 (0%) of length 7
c [cce-8-1] eliminated 12 clauses out of 2081 (1%) of length 6
c [cce-8-1] eliminated 37 clauses out of 816 (5%) of length 5
c [cce-8-1] eliminated 178 clauses out of 4563 (4%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 228 large clauses in 2505389 steps
c [cce-8-1] allowing another 1252694 steps for small clauses
c [cce-8-1] scheduling 9104 clauses = 2153 binary + 6951 ternary
c [cce-8-1] tried to eliminate 9104 small clauses 100%
c [cce-8-1] eliminated 12 binary clauses 1%
c [cce-8-1] eliminated 23 ternary clauses 0%
c [cce-8-1] eliminated 35 small clauses 0%
c [cce-8-1] eliminated 35 small clauses in 3081613 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 263 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1215692 steps for small clauses
c [cce-8-2] scheduling 9069 clauses = 2141 binary + 6928 ternary
c [cce-8-2] tried to eliminate 9069 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 263 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 5981 variables 100%
c [elim-9] limit of 37375937 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 69 variables 1% in round 1 in 3856830 steps
c [elim-9-1] backward subsumption/strengthening limit 3856800
c [elim-9-1-1] backward checking 479 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 7 and strengthened 16 clauses in 62090 steps
c [elim-9-1] rescheduled 84 variables 1% by backward subsumption
c [elim-9-2] eliminated 4 variables 0% in round 2 in 38105 steps
c [elim-9-2] backward subsumption/strengthening limit 38100
c [elim-9-2-1] backward checking 30 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 1 clauses in 14583 steps
c [elim-9-2] rescheduled 4 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 1314 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 73 = 1% variables out of 5981 scheduled
c [bca-8] limit of 10000000 steps and 50706 added (scaled 2)
c [bca-8] 1910 out of 11818 literals actually usable 16%
c [bca-8] added 0 blocked clauses in 22713 steps
c [sweep-7] limit 500000 penalty 1 = 1 + 0
c [sweep-7-1] 2119 pos 51.3% + 2009 neg 48.7% = 4128 sched 69.9% ret 1780
c [sweep-7-1] 502594 steps 56 queries 481.14 avg class size
c [sweep-7-1] 1389 decisions 55 SAT calls 48.78 avg env size
c [sweep-7-1] 3617 variables remain 61% (2291 retained 39%)
c [decomp-34] removed 2 variables
c [sweep-7-1] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-7] 2 < 1/1000 * 5908 = 5 considered unsuccessful
c [sweep-7] removed 2 vars in TOTAL (1 rounds, 55 queries)
c [sort-queue-9] sorted 295 enqueued variables after 31003 conflicts
c [score-dist-9] active 5611 (95%), one 0 (0%), zero 295 (5%)
c [score-dist-9] max exp 509, different 114 (22%)
c [score-dist-9] median active exp 499, avg 489.4
c [simplification-9] removed 102 variables 1.7% (5906 remain 12%)
c [simplification-9] removed 449 irredundant clauses 1.8% (25086 remain 18%)
c [simplification-9] maximum reduction of 2% = max (2%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 18666
c [simplification-9] penalized conflict interval 18666 = 1 * 18666
c [simplification-9] hard conflict limit 59669 (soft 49669 + delta 10000)
c [simplification-9] new conflict limit 49669 (hard 59669)
c 
c [simplification-10] limit 49669 conflicts (hard 59669) hit after 49670 conflicts
c [quatres-8] found 9615 quaternary clauses 57% in total
c [quatres-8-1] removed 23 duplicate quaternary clauses
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 42 single-self-subsuming ternary resolvents
c [quatres-8-2] added 233 quaternary resolvents
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 5906 free variables schedulable
c [ternres-8] 348 ternary resolvents (23 bin, 325 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 130 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 130 out of 130 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-35] removed 2 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 11789 literals 100%
c [treelook-4] scheduling used 300002 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 300218 steps
c [treelook-4] 11188 literals remain 95%
c [treelook-4] 5885 variables remain to probed next time 100%
c [decomp-36] removed 4 variables
c [treelook-4] removed 4 variables, found 286 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 753 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 286 (0%) of length 8
c [cce-9-1] eliminated 9 clauses out of 2067 (0%) of length 6
c [cce-9-1] eliminated 26 clauses out of 817 (3%) of length 5
c [cce-9-1] eliminated 111 clauses out of 4426 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 147 large clauses in 9352963 steps
c [cce-9-1] allowing another 4676481 steps for small clauses
c [cce-9-1] scheduling 9761 clauses = 2081 binary + 7680 ternary
c [cce-9-1] tried to eliminate 9761 small clauses 100%
c [cce-9-1] eliminated 33 binary clauses 2%
c [cce-9-1] eliminated 409 ternary clauses 5%
c [cce-9-1] eliminated 442 small clauses 5%
c [cce-9-1] eliminated 442 small clauses in 8744016 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 589 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 2058 (0%) of length 6
c [cce-9-2] eliminated 2 clauses out of 791 (0%) of length 5
c [cce-9-2] eliminated 34 clauses out of 4315 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 37 large clauses in 8937674 steps
c [cce-9-2] allowing another 4468837 steps for small clauses
c [cce-9-2] scheduling 9319 clauses = 2048 binary + 7271 ternary
c [cce-9-2] tried to eliminate 9319 small clauses 100%
c [cce-9-2] eliminated 13 binary clauses 1%
c [cce-9-2] eliminated 37 ternary clauses 1%
c [cce-9-2] eliminated 50 small clauses 1%
c [cce-9-2] eliminated 50 small clauses in 8369438 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 87 covered clauses in round 2
c [cce-9-3] eliminated 2 clauses out of 2057 (0%) of length 6
c [cce-9-3] eliminated 3 clauses out of 789 (0%) of length 5
c [cce-9-3] eliminated 17 clauses out of 4281 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 22 large clauses in 8827593 steps
c [cce-9-3] allowing another 4413796 steps for small clauses
c [cce-9-3] scheduling 9269 clauses = 2035 binary + 7234 ternary
c [cce-9-3] tried to eliminate 9269 small clauses 100%
c [cce-9-3] eliminated 8 ternary clauses 0%
c [cce-9-3] eliminated 8 small clauses 0%
c [cce-9-3] eliminated 8 small clauses in 8278633 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 30 covered clauses in round 3
c [cce-9] eliminated 706 covered clauses in TOTAL during 3 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 5900 variables 100%
c [elim-10] limit of 59417937 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 106 variables 2% in round 1 in 3817722 steps
c [elim-10-1] backward subsumption/strengthening limit 3817700
c [elim-10-1-1] backward checking 719 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 4 and strengthened 16 clauses in 93705 steps
c [elim-10-1] rescheduled 61 variables 1% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 30310 steps
c [elim-10-2] backward subsumption/strengthening limit 30300
c [elim-10-2-1] backward checking 30 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 1 clauses in 14714 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 3070 steps
c [elim-10-3] backward subsumption/strengthening limit 3000
c [elim-10-3-1] backward checking 10 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 1 clauses in 3001 steps
c [elim-10] incomplete 4 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 111 = 2% variables out of 5900 scheduled
c [sort-queue-10] sorted 54 enqueued variables after 49670 conflicts
c [score-dist-10] active 5735 (99%), one 0 (0%), zero 54 (1%)
c [score-dist-10] max exp 508, different 157 (31%)
c [score-dist-10] median active exp 496, avg 484.0
c [simplification-10] removed 117 variables 2.0% (5789 remain 12%)
c [simplification-10] removed 831 irredundant clauses 3.3% (24255 remain 18%)
c [simplification-10] maximum reduction of 3% = max (2%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 23666
c [simplification-10] penalized conflict interval 23666 = 1 * 23666
c [simplification-10] hard conflict limit 85169 (soft 73336 + delta 11833)
c [simplification-10] new conflict limit 73336 (hard 85169)
c 
c [simplification-11] limit 73336 conflicts (hard 85169) hit after 73336 conflicts
c [quatres-9] found 9540 quaternary clauses 52% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 31 single-self-subsuming ternary resolvents
c [quatres-9-2] added 229 quaternary resolvents
c [ternres-9] limit 4193499 with penalty 0 = 0 + 0
c [ternres-9] all 5789 free variables schedulable
c [ternres-9] 226 ternary resolvents (14 bin, 212 trn)
c [ternres-9] 76 variables remain 1% (5713 retained 99%)
c [basicprobe-4] limit 20967499 penalty 0 = 0 + 0
c [basicprobe-4-0] 1125 sched 19%, 2 failed, 0 lifted, 400 hbrs
c [decomp-38] removed 3 variables
c [basicprobe-4-1] 1052 sched 18%, 1 failed, 0 lifted, 35 hbrs
c [decomp-39] removed 1 variables
c [basicprobe-4-2] 1038 sched 18%, 0 failed, 0 lifted, 6 hbrs
c [decomp-40] removed 1 variables
c [basicprobe-4-3] 1035 sched 18%, 0 failed, 0 lifted, 3 hbrs
c [decomp-41] removed 1 variables
c [basicprobe-4-4] 1034 sched 18%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-4] removed 6 variables, found 444 hbrs
c [bate-3] eliminated 1 asymmetric tautologies during probing
c [unhide-5] limit 104837 with penalty 3 = 3 + 0
c [unhide-5-5] 0 units, 0 failed, 273 tauts, 0 hbrs, 42252 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 782 transitive binary clauses
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 5 clauses out of 2069 (0%) of length 6
c [cce-10-1] eliminated 20 clauses out of 826 (2%) of length 5
c [cce-10-1] eliminated 62 clauses out of 4336 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 87 large clauses in 2300615 steps
c [cce-10-1] allowing another 1150307 steps for small clauses
c [cce-10-1] scheduling 8704 clauses = 1997 binary + 6707 ternary
c [cce-10-1] tried to eliminate 8704 small clauses 100%
c [cce-10-1] eliminated 8 binary clauses 0%
c [cce-10-1] eliminated 14 ternary clauses 0%
c [cce-10-1] eliminated 22 small clauses 0%
c [cce-10-1] eliminated 22 small clauses in 2848577 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 109 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1140173 steps for small clauses
c [cce-10-2] scheduling 8682 clauses = 1989 binary + 6693 ternary
c [cce-10-2] tried to eliminate 8682 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 109 covered clauses in TOTAL during 2 rounds
c [cce-10] 109 < 1/100 * 24226 = 242 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 5783 variables 100%
c [elim-11] limit of 83869999 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 27 variables 0% in round 1 in 3778073 steps
c [elim-11-1] backward subsumption/strengthening limit 3778000
c [elim-11-1-1] backward checking 221 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 1 clauses in 30770 steps
c [elim-11-1] rescheduled 6 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 2532 steps
c [elim-11-2] backward subsumption/strengthening limit 2500
c [elim-11-2-1] backward checking 9 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 2501 steps
c [elim-11-2] rescheduled 8 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 2708 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 28 = 0% variables out of 5783 scheduled
c [elim-11] 28 < 1/100 * 5783 = 57 considered unsuccessful
c [bca-9] limit of 10000000 steps and 48666 added (scaled 2)
c [bca-9] 415 out of 11512 literals actually usable 4%
c [bca-9] added 0 blocked clauses in 51101 steps
c [sort-queue-11] sorted 21 enqueued variables after 73336 conflicts
c [score-dist-11] active 5734 (100%), one 0 (0%), zero 21 (0%)
c [score-dist-11] max exp 510, different 194 (38%)
c [score-dist-11] median active exp 495, avg 479.1
c [simplification-11] removed 34 variables 0.6% (5755 remain 12%)
c [simplification-11] removed 184 irredundant clauses 0.8% (24071 remain 18%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 11833 = 23666 / 2
c [simplification-11] new conflict interval 35499
c [simplification-11] penalized conflict interval 35499 = 1 * 35499
c [simplification-11] hard conflict limit 126584 (soft 108835 + delta 17749)
c [simplification-11] new conflict limit 108835 (hard 126584)
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 -   30.7    5755    24071     84960   28619  16060  7814   12    54   10  22%    739   17   13    8  153%
c 
c [simplification-12] limit 108835 conflicts (hard 126584) hit after 108835 conflicts
c [quatres-10] found 9903 quaternary clauses 47% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 39 single-self-subsuming ternary resolvents
c [quatres-10-2] added 217 quaternary resolvents
c [ternres-10] limit 6051742 with penalty 0 = 0 + 0
c [ternres-10] 75 schedulable variables 1%
c [ternres-10] 52 ternary resolvents (4 bin, 48 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 1129 xors of average arity 3.0
c [gauss-4] connected 3387 occurrences of 765 variables (average 4.4)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 5755 free variables schedulable
c [simpleprobe-5] limit 24206968 penalty 0 = 0 + 0
c [decomp-43] removed 2 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 2 variables, found 691 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 971 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5753 variables 100%
c [block-5] limit of 7564677 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 4 blocked clauses
c [block-5] 4 < 1/100 * 24067 = 240 considered unsuccessful
c [sweep-8] limit 453880 penalty 2 = 2 + 0
c [sweep-8-1] 1781 pos 51.0% + 1710 neg 49.0% = 3491 sched 60.7% ret 2262
c [sweep-8-1] 454451 steps 20 queries 400.40 avg class size
c [sweep-8-1] 758 decisions 19 SAT calls 69.95 avg env size
c [sweep-8-1] 3367 variables remain 59% (2386 retained 41%)
c [decomp-44] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-8] 1 < 1/1000 * 5753 = 5 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 19 queries)
c [sort-queue-12] sorted 18 enqueued variables after 108835 conflicts
c [score-dist-12] active 5734 (100%), one 0 (0%), zero 18 (0%)
c [score-dist-12] max exp 509, different 222 (44%)
c [score-dist-12] median active exp 499, avg 479.6
c [simplification-12] removed 3 variables 0.1% (5752 remain 12%)
c [simplification-12] removed 10 irredundant clauses 0.0% (24061 remain 18%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 35499
c [simplification-12] new conflict interval 70998
c [simplification-12] penalized conflict interval 70998 = 1 * 70998
c [simplification-12] hard conflict limit 215332 (soft 179833 + delta 35499)
c [simplification-12] new conflict limit 179833 (hard 215332)
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 -   36.2    5752    24061    125178   35467  16314  7614   12    48   10  25%    870    5   10   10   98%
c -   40.6    5752    24061    161983   38735  16414  7638   12    44   11  27%    936    0   18   11  168%
c 
c [simplification-13] limit 179833 conflicts (hard 215332) hit after 185653 conflicts
c [quatres-11] found 10533 quaternary clauses 40% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 29 single-self-subsuming ternary resolvents
c [quatres-11-2] added 115 quaternary resolvents
c [ternres-11] limit 9688266 with penalty 0 = 0 + 0
c [ternres-11] all 5752 free variables schedulable
c [ternres-11] 639 ternary resolvents (38 bin, 601 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-45] removed 2 variables
c [treelook-5] limit 968826 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11481 literals 100%
c [treelook-5] scheduling used 352102 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 968826 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 970426 steps
c [treelook-5] 8263 literals remain 72%
c [treelook-5] 5326 variables remain to probed next time 93%
c [decomp-46] removed 9 variables
c [treelook-5] removed 12 variables, found 546 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1015 transitive binary clauses
c [cce-11] limit of 24220667 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 639 (0%) of length 7
c [cce-11-1] eliminated 6 clauses out of 2035 (0%) of length 6
c [cce-11-1] eliminated 30 clauses out of 830 (4%) of length 5
c [cce-11-1] eliminated 92 clauses out of 4262 (2%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 129 large clauses in 8814069 steps
c [cce-11-1] allowing another 4407034 steps for small clauses
c [cce-11-1] scheduling 9054 clauses = 1973 binary + 7081 ternary
c [cce-11-1] tried to eliminate 9054 small clauses 100%
c [cce-11-1] eliminated 26 binary clauses 1%
c [cce-11-1] eliminated 92 ternary clauses 1%
c [cce-11-1] eliminated 118 small clauses 1%
c [cce-11-1] eliminated 118 small clauses in 8130148 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 247 covered clauses in round 1
c [cce-11-2] eliminated 7 clauses out of 2029 (0%) of length 6
c [cce-11-2] eliminated 5 clauses out of 800 (1%) of length 5
c [cce-11-2] eliminated 30 clauses out of 4170 (1%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 42 large clauses in 8475438 steps
c [cce-11-2] allowing another 4237719 steps for small clauses
c [cce-11-2] scheduling 8936 clauses = 1947 binary + 6989 ternary
c [cce-11-2] tried to eliminate 8936 small clauses 100%
c [cce-11-2] eliminated 13 binary clauses 1%
c [cce-11-2] eliminated 13 ternary clauses 0%
c [cce-11-2] eliminated 26 small clauses 0%
c [cce-11-2] eliminated 26 small clauses in 7914812 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 68 covered clauses in round 2
c [cce-11-3] eliminated 2 clauses out of 2022 (0%) of length 6
c [cce-11-3] eliminated 3 clauses out of 795 (0%) of length 5
c [cce-11-3] eliminated 16 clauses out of 4140 (0%) of length 4
c [cce-11-3] incomplete large round (ACCE)
c [cce-11-3] eliminated 21 large clauses in 8175729 steps
c [cce-11-3] allowing another 4087864 steps for small clauses
c [cce-11-3] scheduling 8910 clauses = 1934 binary + 6976 ternary
c [cce-11-3] tried to eliminate 8910 small clauses 100%
c [cce-11-3] eliminated 6 binary clauses 0%
c [cce-11-3] eliminated 8 ternary clauses 0%
c [cce-11-3] eliminated 14 small clauses 0%
c [cce-11-3] eliminated 14 small clauses in 7751338 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 35 covered clauses in round 3
c [cce-11] eliminated 350 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5738 variables 100%
c [elim-12] limit of 96882669 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 95 variables 2% in round 1 in 3733836 steps
c [elim-12-1] backward subsumption/strengthening limit 3733800
c [elim-12-1-1] backward checking 517 touched variables 9%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 8 clauses in 64782 steps
c [elim-12-1] rescheduled 26 variables 0% by backward subsumption
c [elim-12-2] eliminated 4 variables 0% in round 2 in 9586 steps
c [elim-12-2] backward subsumption/strengthening limit 9500
c [elim-12-2-1] backward checking 28 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 2 clauses in 9501 steps
c [elim-12-2] rescheduled 7 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 5738 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 99 = 2% variables out of 5738 scheduled
c [sort-queue-13] sorted 34 enqueued variables after 185653 conflicts
c [score-dist-13] active 5605 (99%), one 34 (1%), zero 0 (0%)
c [score-dist-13] max exp 509, different 215 (42%)
c [score-dist-13] median active exp 501, avg 480.5
c [simplification-13] removed 113 variables 2.0% (5639 remain 12%)
c [simplification-13] removed 541 irredundant clauses 2.2% (23520 remain 17%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 23666 = 70998 / 3
c [simplification-13] new conflict interval 94664
c [simplification-13] penalized conflict interval 94664 = 1 * 94664
c [simplification-13] hard conflict limit 327649 (soft 280317 + delta 47332)
c [simplification-13] new conflict limit 280317 (hard 327649)
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.0    5639    23520    203810   39877  16640  6765   12    38   11  30%    978   -5   16   11  144%
c -   52.1    5639    23520    240720   42415  16735  6776   11    34   11  32%    998  -10    9   11   81%
c -   56.8    5639    23520    280117   45601  16802  6784   10    33   12  31%   1010   -6   11   11  108%
c 
c [simplification-14] limit 280317 conflicts (hard 327649) hit after 287433 conflicts
c [quatres-12] found 10450 quaternary clauses 33% in total
c [quatres-12-1] removed 7 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 40 single-self-subsuming ternary resolvents
c [quatres-12-2] added 152 quaternary resolvents
c [ternres-12] limit 14361247 with penalty 0 = 0 + 0
c [ternres-12] all 5639 free variables schedulable
c [ternres-12] 256 ternary resolvents (24 bin, 232 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-5] limit 71806237 penalty 0 = 0 + 0
c [basicprobe-5-0] 997 sched 18%, 2 failed, 0 lifted, 91 hbrs
c [decomp-48] removed 3 variables
c [basicprobe-5-1] 975 sched 17%, 3 failed, 0 lifted, 11 hbrs
c [decomp-49] removed 4 variables
c [basicprobe-5-2] 971 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-3] 971 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 7 variables, found 103 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 677 transitive binary clauses
c [cce-12] limit of 71806237 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 640 (0%) of length 7
c [cce-12-1] eliminated 2 clauses out of 2025 (0%) of length 6
c [cce-12-1] eliminated 24 clauses out of 826 (3%) of length 5
c [cce-12-1] eliminated 90 clauses out of 4110 (2%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 117 large clauses in 2189734 steps
c [cce-12-1] allowing another 1094867 steps for small clauses
c [cce-12-1] scheduling 8803 clauses = 1874 binary + 6929 ternary
c [cce-12-1] tried to eliminate 8803 small clauses 100%
c [cce-12-1] eliminated 7 binary clauses 0%
c [cce-12-1] eliminated 16 ternary clauses 0%
c [cce-12-1] eliminated 23 small clauses 0%
c [cce-12-1] eliminated 23 small clauses in 3033219 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 140 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1076324 steps for small clauses
c [cce-12-2] scheduling 8780 clauses = 1867 binary + 6913 ternary
c [cce-12-2] tried to eliminate 8780 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 140 covered clauses in TOTAL during 2 rounds
c [cce-12] 140 < 1/100 * 23497 = 234 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5632 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 40 variables 1% in round 1 in 3692025 steps
c [elim-13-1] backward subsumption/strengthening limit 3692000
c [elim-13-1-1] backward checking 257 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 8 clauses in 46181 steps
c [elim-13-1] rescheduled 21 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 10737 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 40 = 1% variables out of 5632 scheduled
c [elim-13] 40 < 1/100 * 5632 = 56 considered unsuccessful
c [bca-10] limit of 10000000 steps and 47060 added (scaled 2)
c [bca-10] 774 out of 11186 literals actually usable 7%
c [bca-10] added 2 blocked clauses in 51379 steps
c [sort-queue-14] sorted 98 enqueued variables after 287433 conflicts
c [score-dist-14] active 5494 (98%), one 98 (2%), zero 0 (0%)
c [score-dist-14] max exp 510, different 230 (45%)
c [score-dist-14] median active exp 502, avg 479.5
c [simplification-14] removed 47 variables 0.8% (5592 remain 12%)
c [simplification-14] removed 252 irredundant clauses 1.1% (23268 remain 17%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 47332 = 94664 / 2
c [simplification-14] new conflict interval 141996
c [simplification-14] penalized conflict interval 141996 = 1 * 141996
c [simplification-14] hard conflict limit 500427 (soft 429429 + delta 70998)
c [simplification-14] new conflict limit 429429 (hard 500427)
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 -   62.5    5592    23268    321489   48462  16781  6044   10    35   12  30%   1016   -5    9   11   86%
c -   67.5    5592    23268    360154   51797  16825  6051   11    35   13  31%   1020   -1   11   11  104%
c -   72.3    5592    23268    399265   55078  16857  6061   10    31   12  33%   1022   -5   11   11  104%
c 
c [simplification-15] limit 429429 conflicts (hard 500427) hit after 429431 conflicts
c [quatres-13] found 10755 quaternary clauses 27% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-1] added 5 double-self-subsuming ternary resolvents
c [quatres-13-2] added 28 single-self-subsuming ternary resolvents
c [quatres-13-2] added 254 quaternary resolvents
c [ternres-13] limit 21472521 with penalty 0 = 0 + 0
c [ternres-13] all 5592 free variables schedulable
c [ternres-13] 245 ternary resolvents (21 bin, 224 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 671016 penalty 4 = 4 + 0
c [card-5] found 159 at-most-one constraints of average size 3.0
c [card-5] found 138 at-most-two constraints of average size 4.0
c [card-5] using previous limit 671016 for elimination
c [card-5] 296 out of 297 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] all 5592 free variables schedulable
c [simpleprobe-6] limit 85890084 penalty 0 = 0 + 0
c [decomp-52] removed 1 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1 variables, found 782 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 989 transitive binary clauses
c [sort-queue-15] sorted 118 enqueued variables after 429431 conflicts
c [score-dist-15] active 5473 (98%), one 118 (2%), zero 0 (0%)
c [score-dist-15] max exp 510, different 186 (36%)
c [score-dist-15] median active exp 500, avg 486.1
c [simplification-15] removed 1 variables 0.0% (5591 remain 12%)
c [simplification-15] removed 2 irredundant clauses 0.0% (23266 remain 17%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 141996
c [simplification-15] new conflict interval 283992
c [simplification-15] penalized conflict interval 283992 = 1 * 283992
c [simplification-15] hard conflict limit 855419 (soft 713423 + delta 141996)
c [simplification-15] new conflict limit 713423 (hard 855419)
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 -   77.5    5591    23266    438369   57061  17154  5879   11    40   13  28%   1023    3   13   11  119%
c -   83.0    5591    23266    478905   59334  17175  5882   12    33   13  37%   1023   -3   17   11  146%
c -   89.3    5591    23266    521385   62927  17204  5887   11    27   14  39%   1024   -8   11   11   96%
c -   95.2    5591    23266    562782   65664  17228  5893   11    35   14  32%   1024    2   12   11  105%
c -  101.3    5591    23266    605245   68062  17244  5896   11    22   15  50%   1024   -9   12   11  105%
c -  107.6    5591    23266    648416   70675  17268  5902   11    33   21  35%   1024    3   14   11  124%
c -  113.9    5591    23266    691865   73113  17282  5905   11    37   15  30%   1024    6   10   11   90%
c 
c [simplification-16] limit 713423 conflicts (hard 855419) hit after 713423 conflicts
c [quatres-14] found 11830 quaternary clauses 22% in total
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 21 single-self-subsuming ternary resolvents
c [quatres-14-2] added 108 quaternary resolvents
c [ternres-14] limit 38687896 with penalty 0 = 0 + 0
c [ternres-14] all 5591 free variables schedulable
c [ternres-14] 135 ternary resolvents (27 bin, 108 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-53] removed 1 variables
c [treelook-6] limit 3868789 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10832 literals 97%
c [treelook-6] scheduling used 404564 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3868789 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1495397 steps
c [treelook-6] fully completed tree based probing
c [decomp-54] removed 3 variables
c [treelook-6] removed 3 variables, found 325 hbrs
c [unhide-6] limit 483598 with penalty 4 = 4 + 0
c [unhide-6-6] 0 units, 0 failed, 2935 tauts, 0 hbrs, 93589 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 482 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 967197400 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 5 clauses out of 1928 (0%) of length 6
c [cce-13-1] eliminated 29 clauses out of 756 (4%) of length 5
c [cce-13-1] eliminated 105 clauses out of 4114 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 139 large clauses in 7592722 steps
c [cce-13-1] allowing another 3796361 steps for small clauses
c [cce-13-1] scheduling 8797 clauses = 1901 binary + 6896 ternary
c [cce-13-1] tried to eliminate 8797 small clauses 100%
c [cce-13-1] eliminated 62 binary clauses 3%
c [cce-13-1] eliminated 139 ternary clauses 2%
c [cce-13-1] eliminated 201 small clauses 2%
c [cce-13-1] eliminated 201 small clauses in 7231219 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 340 covered clauses in round 1
c [cce-13-2] eliminated 2 clauses out of 727 (0%) of length 5
c [cce-13-2] eliminated 8 clauses out of 4009 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 10 large clauses in 7257205 steps
c [cce-13-2] allowing another 3628602 steps for small clauses
c [cce-13-2] scheduling 8596 clauses = 1839 binary + 6757 ternary
c [cce-13-2] tried to eliminate 8596 small clauses 100%
c [cce-13-2] eliminated 8 binary clauses 0%
c [cce-13-2] eliminated 12 ternary clauses 0%
c [cce-13-2] eliminated 20 small clauses 0%
c [cce-13-2] eliminated 20 small clauses in 6994736 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 30 covered clauses in round 2
c [cce-13-3] eliminated 5 clauses out of 4001 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 5 large clauses in 7202534 steps
c [cce-13-3] allowing another 3601267 steps for small clauses
c [cce-13-3] scheduling 8576 clauses = 1831 binary + 6745 ternary
c [cce-13-3] tried to eliminate 8576 small clauses 100%
c [cce-13-3] eliminated 1 binary clauses 0%
c [cce-13-3] eliminated 2 ternary clauses 0%
c [cce-13-3] eliminated 3 small clauses 0%
c [cce-13-3] eliminated 3 small clauses in 6957755 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 8 covered clauses in round 3
c [cce-13] eliminated 378 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5587 variables 100%
c [elim-14] limit of 386878961 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 167 variables 3% in round 1 in 3681879 steps
c [elim-14-1] backward subsumption/strengthening limit 3681800
c [elim-14-1-1] backward checking 897 touched variables 16%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 9 and strengthened 34 clauses in 109579 steps
c [elim-14-1] rescheduled 110 variables 2% by backward subsumption
c [elim-14-2] eliminated 3 variables 0% in round 2 in 109643 steps
c [elim-14-2] backward subsumption/strengthening limit 109600
c [elim-14-2-1] backward checking 34 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 2 and strengthened 4 clauses in 18072 steps
c [elim-14-2] rescheduled 15 variables 0% by backward subsumption
c [elim-14-3] eliminated 2 variables 0% in round 3 in 11932 steps
c [elim-14-3] backward subsumption/strengthening limit 11900
c [elim-14-3-1] backward checking 11 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 11901 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 172 = 3% variables out of 5587 scheduled
c [bca-11] limit of 10000000 steps and 45795 added (scaled 2)
c [bca-11] 704 out of 10832 literals actually usable 6%
c [bca-11] added 0 blocked clauses in 80384 steps
c [sweep-9] limit 1450796 penalty 3 = 3 + 0
c [sweep-9-1] 1769 pos 56.5% + 1360 neg 43.5% = 3129 sched 57.8% ret 2286
c [sweep-9-1] 1593532 steps 50 queries 172.70 avg class size
c [sweep-9-1] 2225 decisions 49 SAT calls 79.37 avg env size
c [sweep-9-1] 2179 variables remain 40% (3236 retained 60%)
c [decomp-55] removed 1 variables
c [sweep-9-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9] 1 < 1/1000 * 5415 = 5 considered unsuccessful
c [sweep-9] removed 1 vars in TOTAL (1 rounds, 49 queries)
c [sort-queue-16] sorted 200 enqueued variables after 713423 conflicts
c [score-dist-16] active 5214 (96%), one 200 (4%), zero 0 (0%)
c [score-dist-16] max exp 510, different 176 (34%)
c [score-dist-16] median active exp 502, avg 490.3
c [simplification-16] removed 177 variables 3.2% (5414 remain 11%)
c [simplification-16] removed 633 irredundant clauses 2.7% (22633 remain 17%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 70998 = 283992 / 4
c [simplification-16] new conflict interval 354990
c [simplification-16] penalized conflict interval 354990 = 1 * 354990
c [simplification-16] hard conflict limit 1245908 (soft 1068413 + delta 177495)
c [simplification-16] new conflict limit 1068413 (hard 1245908)
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 -  123.7    5414    22633    744701   69548  15793  3869   11    25   19  44%   1024   -7    9   11   86%
c -  130.4    5414    22633    789744   72926  15822  3888   11    41   14  28%   1024   10   11   11   95%
c -  137.2    5414    22633    837620   76407  15862  3901   11    27   21  40%   1024   -5   14   10  131%
c -  144.1    5414    22633    884573   80323  15888  3904   10    32   21  31%   1024    1    9   11   90%
c -  152.1    5414    22633    932556   83666  15903  3910   11    23   23  50%   1024   -6    9   11   87%
c -  160.9    5414    22633    981020   86237  15918  3910   11    28   16  38%   1024    1   12   10  116%
c -  168.7    5414    22633   1028872   88813  15929  3913   12    33   23  36%   1024    4   13   11  122%
c 
c [simplification-17] limit 1068413 conflicts (hard 1245908) hit after 1072480 conflicts
c [quatres-15] found 12225 quaternary clauses 18% in total
c [quatres-15-1] removed 25 duplicate quaternary clauses
c [quatres-15-1] added 6 double-self-subsuming ternary resolvents
c [quatres-15-2] added 74 single-self-subsuming ternary resolvents
c [quatres-15-2] added 284 quaternary resolvents
c [ternres-15] limit 62834413 with penalty 0 = 0 + 0
c [ternres-15] all 5414 free variables schedulable
c [ternres-15] 516 ternary resolvents (32 bin, 484 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 785430 penalty 4 = 4 + 0
c [gauss-5] extracted 4052 xors of average arity 3.0
c [gauss-5] connected 12154 occurrences of 920 variables (average 13.2)
c [gauss-5] limit 785430 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-56] removed 1 variables
c [basicprobe-6] limit 314172068 penalty 0 = 0 + 0
c [basicprobe-6-0] 929 sched 17%, 5 failed, 0 lifted, 106 hbrs
c [decomp-57] removed 7 variables
c [basicprobe-6-1] 909 sched 17%, 1 failed, 0 lifted, 13 hbrs
c [decomp-58] removed 1 variables
c [basicprobe-6-2] 906 sched 17%, 0 failed, 0 lifted, 5 hbrs
c [decomp-59] removed 1 variables
c [basicprobe-6-3] 904 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-3] fully completed probing
c [basicprobe-6-3] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-6-3] removed 9 variables, found 124 hbrs
c [bate-4] eliminated 1 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 286 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5404 variables 100%
c [block-6] limit of 39271508 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 18 blocked clauses
c [block-6] 18 < 1/100 * 22582 = 225 considered unsuccessful
c [cce-14] limit of 314172068 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 4 clauses out of 1973 (0%) of length 6
c [cce-14-1] eliminated 38 clauses out of 810 (5%) of length 5
c [cce-14-1] eliminated 105 clauses out of 3975 (3%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 147 large clauses in 2040316 steps
c [cce-14-1] allowing another 1020158 steps for small clauses
c [cce-14-1] scheduling 8022 clauses = 1742 binary + 6280 ternary
c [cce-14-1] tried to eliminate 8022 small clauses 100%
c [cce-14-1] eliminated 10 binary clauses 1%
c [cce-14-1] eliminated 44 ternary clauses 1%
c [cce-14-1] eliminated 54 small clauses 1%
c [cce-14-1] eliminated 54 small clauses in 2561452 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 201 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1003915 steps for small clauses
c [cce-14-2] scheduling 7968 clauses = 1732 binary + 6236 ternary
c [cce-14-2] tried to eliminate 7968 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 201 covered clauses in TOTAL during 2 rounds
c [cce-14] 201 < 1/100 * 22564 = 225 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 5404 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 51 variables 1% in round 1 in 3640259 steps
c [elim-15-1] backward subsumption/strengthening limit 3640200
c [elim-15-1-1] backward checking 400 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 3 and strengthened 7 clauses in 54589 steps
c [elim-15-1] rescheduled 30 variables 1% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 17773 steps
c [elim-15-2] backward subsumption/strengthening limit 17700
c [elim-15-2-1] backward checking 7 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 1 clauses in 10341 steps
c [elim-15-2] rescheduled 4 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 1458 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 52 = 1% variables out of 5404 scheduled
c [elim-15] 52 < 1/100 * 5404 = 54 considered unsuccessful
c [sort-queue-17] sorted 194 enqueued variables after 1072480 conflicts
c [score-dist-17] active 5158 (96%), one 194 (4%), zero 0 (0%)
c [score-dist-17] max exp 509, different 190 (37%)
c [score-dist-17] median active exp 500, avg 482.0
c [simplification-17] removed 62 variables 1.1% (5352 remain 11%)
c [simplification-17] removed 338 irredundant clauses 1.5% (22295 remain 16%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 177495 = 354990 / 2
c [simplification-17] new conflict interval 532485
c [simplification-17] penalized conflict interval 532485 = 1 * 532485
c [simplification-17] hard conflict limit 1871207 (soft 1604965 + delta 266242)
c [simplification-17] new conflict limit 1604965 (hard 1871207)
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 -  180.8    5352    22295   1090700   88514  16112  3643    8    23   16  36%   1024   -5    8   10   74%
c -  188.6    5352    22295   1140464   90978  16130  3647   12    30   24  41%   1024    1   11   11  100%
c -  196.5    5352    22295   1191749   94583  16143  3651   12    33   24  36%   1024    4   11   10  107%
c -  205.9    5352    22295   1244379   97764  16154  3655    9    21   24  41%   1024   -5    9   10   90%
c -  214.9    5352    22295   1295352  100470  16163  3656   11    30   24  35%   1024    5   13   11  125%
c -  224.9    5352    22295   1347567  102580  16170  3659   10    24   25  43%   1024   -2   11   11  103%
c -  233.9    5352    22295   1401436  105785  16181  3662   12    25   25  48%   1024   -1   13   11  120%
c -  243.9    5352    22295   1459077  108524  16204  3668    8    30   19  28%   1024    2    9   10   94%
c -  253.3    5352    22295   1511839  111839  16213  3668   10    22   28  48%   1024   -5    9   11   82%
c -  264.2    5352    22295   1564772  113900  16217  3668   11    27   28  41%   1024    1   12   11  101%
c -  276.6    5352    22295   1621155  115908  16226  3668   10    22   28  44%   1024   -2   10   11   93%
c 
c [simplification-18] limit 1604965 conflicts (hard 1871207) hit after 1621530 conflicts
c [quatres-16] found 12945 quaternary clauses 15% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-1] added 5 double-self-subsuming ternary resolvents
c [quatres-16-2] added 52 single-self-subsuming ternary resolvents
c [quatres-16-2] added 140 quaternary resolvents
c [ternres-16] limit 106414343 with penalty 0 = 0 + 0
c [ternres-16] all 5352 free variables schedulable
c [ternres-16] 184 ternary resolvents (30 bin, 154 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-60] removed 1 variables
c [simpleprobe-7] all 5351 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-61] removed 2 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 2 variables, found 637 hbrs, 1 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 599 transitive binary clauses
c [transred-16] found 1 units
c [sort-queue-18] sorted 210 enqueued variables after 1621530 conflicts
c [score-dist-18] active 5132 (96%), one 210 (4%), zero 0 (0%)
c [score-dist-18] max exp 509, different 157 (31%)
c [score-dist-18] median active exp 500, avg 490.1
c [simplification-18] removed 10 variables 0.2% (5342 remain 11%)
c [simplification-18] removed 40 irredundant clauses 0.2% (22255 remain 16%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 532485
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 3121530 (soft 2621530 + delta 500000)
c [simplification-18] new conflict limit 2621530 (hard 3121530)
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 -  287.4    5342    22255   1676774  118122  16381  3708   10    20   25  51%   1024   -4    9   11   78%
c -  300.1    5342    22255   1732312  120826  16387  3710   10    23   20  46%   1024   -0    8   12   67%
c -  312.5    5342    22255   1789253  123939  16389  3710    9    24   30  37%   1024    3    9   11   89%
c -  325.2    5342    22255   1847098  126591  16400  3712   11    17   30  68%   1024   -5    9   11   84%
c -  339.1    5342    22255   1905312  128735  16404  3714   11    19   30  61%   1024   -3   11   11  102%
c -  353.2    5342    22255   1965184  131463  16413  3716   10    22   30  49%   1024    0   11   11  103%
c -  367.1    5342    22255   2024358  133507  16420  3717   10    24   30  42%   1024    2    9   11   82%
c -  381.6    5342    22255   2084304  136740  16422  3719    9    19   31  50%   1024   -2    8   11   75%
c i  393.5    5341    22255   2131064  178826  16451  3731    8    15   44  57%   1024   -5    6   10   65%
c i  396.7    5327    22255   2141320  187727  16464  3738    8    14   44  56% -27901   -5    6   10   66%
c i  396.8    5326    22255   2141461  187806  16471  3742    8    14   44  56% -27859   -5    6   10   60%
c i  396.9    5178    22255   2141657  187933  16475  3746    8    13   44  57% -27798   -6    6   10   57%
c i  396.9    5157    22255   2141725  187977  16478  3747    8    13   44  57% -27776   -6    6   10   58%
c i  396.9    5139    22255   2141743  187981  16482  3748    8    13   44  57% -27770   -6    5   10   56%
c i  396.9    5115    22255   2141750  187981  16483  3748    8    13   44  57% -27768   -6    5   10   56%
c i  396.9    4917    22255   2141756  187981  16485  3749    8    13   44  57% -27766   -6    5   10   55%
c i  396.9    4869    22255   2141760  187982  16485  3751    8    13   44  57% -27764   -6    5   10   54%
c 0  396.9    4867    22255   2141760  187982  16485  3751    8    13   44  57% -27764   -6    5   10   54%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 89 basic ate = 85 trn 96% + 4 lrg 4% in 4 updates
c bcas: 11 count, 51 added (1 skipped), 370007 steps
c bkwd: tried 95791 clauses, 191342 lits, 2.00 lits/clause
c bkwd: checked 1685787 occs, 17.60 occs/clause, 8.81 occs/lit
c bkwd: subsumed 0 binary, 42 ternary, 81 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 409 large (0% self)
c blkd: 6 bces, 5317 removed, 884054 resolutions, 2422112 steps
c blkd: 4181 blocking literals 4%, 0 pure
c bump: 2093037 bumped seen, 155269273 lits 74.2 on average
c card: 5 count, 0 units, 41 am1, 5831343 steps
c card: 54 rescheduled, 474 eliminated, 16346 resolved, 3185 subsumed
c card: 752 at-most-one constraints found, average size 3.01
c card: 752 at-most-one constraints used 100%, average size 3.01
c card: 157 at-most-two constraints found, average size 4.00
c card: 156 at-most-two constraints used 99%, average size 4.00
c cces: 14 cces, 11499 eliminated, 8801 ate 77%, 2698 abce 23%
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: 494642 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 113 gcs, 0 rescored clauses, 8162 rescored vars
c dcps: 61 decompositions, 3429 equivalent 6%
c deco: 2 decision-only clauses 0%, 52% reduction
c decs: 13344400 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 38947 eliminated 72%, 43 pure 0%
c elms: 48 rounds, 3.2 rounds/bve
c elms: 38522 small 99%, 382 large 1%
c elms: 76879 tried small, 38522 succeeded 50%, 38357 failed 50%
c elms: 1102 subsumed, 3086 strengthened, 234 blocked
c elms: 2448839 copies, 2563385 resolutions, 2178385 ipos
c elms: 380932 subchks, 260563 strchks
c gaus: 5 extractions, 17402 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8169212 steps, 4084606 extr 50%, 1177322 elim 14%
c glue: 10.8 orig avg, 10.8 real avg, 2.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 34137 = 5579 simple 16% + 26663 trn 78% + 1895 lrg 6%, 1240 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2093037 clauses, 23.4 length
c lrnd: 48891646 lits = 85155827 orig - 36264181 removed 43%
c lrnd: 825741 uips 39%, 595096 flips 28%
c mins: 2056188 mins 98%, 897 bin 0%, 35950 size 2%
c mins: 146792908 poisoned searches, 10385826 hits, 7% hit rate
c mins: 219224984 used twice searches, 10567937 hits, 5% hit rate
c move: moved 13904, 4836 bin 35%, 9068 trn 65%
c otfs: 50882 driving 65%, 27847 restarting 35%
c otfs: str 78729, 77922 red 99%, 807 irr 1%
c otfs: str 78729, 0 bin 0%, 380 trn 0%, 78349 lrg 100%
c otfs: sub 785, 785 red 100%, 0 irr 0%
c otfs: sub 785, 0 bin 0%, 14 trn 2%, 771 lrg 98%
c phas: 1 computed, 9675 set, 3115 pos (32%), 6560 neg (68%)
c prbs: 6 basic, 54398 probed, 17 failed, 0 lifted
c prbs: 7 simple, 164764 probed, 362 failed, 1166 eqs
c prbs: 6 treelook, 15996 probed, 2 failed, 0 lifted
c prom: 722830 locked 7% out of 9814680 tried
c prps: 648860132 props, 48 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 16 count, 9617 quat, 530 self1, 39 self2, 506 dup
c queu: 18 sorted, 13344400 next (844712 steps 0.06)
c queu: 198569886 enq (327453892 steps 1.65), 155269273 deq 78%
c redc: 39789 clauses 10%, 408936 tried 19%, 23 sat 0%
c redc: 47628 lits 1%, 4280500 tried 5%, 23 sat 0%
c redc: 922 times jump level reduced, 7.5 levels on average
c reds: 42 count, 50994.3 conflicts per reduce
c reds: 0 memlim 0%, 42 arith 100%
c reds: 1480872 collected 87%, 217293 retired 13%
c rmbd: 190 removed, 186 red 98%
c rsts: 33434 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 17 confs 94%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 0 trns 0%
c subl: 2093037 count (882166 tried 0.4), 153217 sub out of 2088230 (7.3%)
c swps: 9 count, 11 rounds, 4049 queries (368.1/round)
c swps: 3808 sat calls, 399 unsat (0.6% success rate)
c swps: 47325 decisions 12.4, 2159 conflicts 0.6
c swps; 108.0 avg class size, 33.6 avg environment size
c swps: 0 failed, 513 impls, 640 equivs
c swp0: 1346 type 0 queries, 590 unsat (43.8%), 1258 sat (93.5%)
c swp1: 2703 type 1 queries, 1866 unsat (69.0%), 2151 sat (79.6%)
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: 30891598 calls to obtain time
c tops: 6509 fixed 12%, 9 its, 237973.33 confs/it
c trds: 16 transitive reductions, 12558 removed, 1 failed
c trds: 180742 nodes, 144933 edges, 3015799 steps
c trim: 949987 words, 3.6 MB
c trnr: 16 count, 348 bin, 16087 trn, 76867262 steps
c unhd: 6 count, 6 rounds, 4093721 steps
c unhd: 124 non-trivial sccs of average size 2.0
c unhd: 16 units, 16 bin, 0 trn, 0 lrg
c unhd: 134 failed, 134 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 11632 tauts, 26 bin 0%, 1998 trn 17%, 197 lrg 2%
c unhd: 11632 tauts, 9411 stamp 81%, 11589 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 147780 str, 16 bin 0%, 513 trn 0%, 147251 lrg 100%, 146398 red 99%
c vars: 4867 remaining 9% and 48885 removed 91% out of 53752
c vars: 6509 fixed 12%, 38947 eliminated 72%, 3429 equivalent 6%
c vsts: 15792392131 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 24.4 search visits per propagation, 7360.6 per conflict
c wchs: 2657010055 pushed, 6913401 enlarged, 209 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2097847       1480872        217293     141408788      40210301        837478
c 
c  0 0        128382   6      4447   0         0   0  82688066  58  19769355  49    338788  40     3.8
c  1 5        134101   6     90926   6     17736   8  21842999  15<  6396697  16<    94499  11<    0.8
c  2 6        572704  27    442848  30     49192  23  28705553  20   9886475  25    217080  26     2.4
c  3 9        738451  35<   558316  38<    75459  35<  6669155   5   3301440   8    133370  16     3.2
c  4 14       415847  20    306674  21     56293  26   1255049   1    720776   2     43498   5     2.7
c  5 21        94234   4     67835   5     15783   7    220962   0    120491   0      9091   1     0.8
c  6 30        11898   1      8364   1      2338   1     23371   0     12987   0      1022   0     0.4
c  7 41         2035   0      1382   0       442   0      3365   0      1919   0       118   0     0.1
c  8 54          148   0        61   0        37   0       206   0       124   0        11   0     0.0
c  9 69           43   0        17   0        11   0        58   0        35   0         1   0     0.0
c 10 86            2   0         1   0         1   0         2   0         1   0         0   0     0.0
c 11 126           2   0         1   0         1   0         2   0         1   0         0   0     0.0
c 
c avg                  2.7           2.9           3.1           0.7           1.0           1.4
c std                  1.2           1.0           1.1           1.0           1.1           1.4
c 
c   21.571   5% bump
c   15.960   4% cce
c    9.363   2% decide
c    5.159   1% rescore
c    3.392   1% elim
c 
c    6.264 < 1% rest (below)
c 
c    2.503   1% probe
c    1.079   0% sweep
c    0.621   0% quatres
c    0.593   0% ternres
c    0.419   0% unhide
c    0.262   0% block
c    0.255   0% gauss
c    0.227   0% bca
c    0.197   0% transred
c    0.109   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.875   0% preprocessing     3%
c   25.768   6% inprocessing     97%
c ==================================
c   26.643   7% simplifying
c  370.249  93% search
c ==================================
c  396.894 100% all
c 
c       2141760 conflicts,        5396.3 confs/sec
c          2367 ternaries,         904.8 confs/ternary
c           962 binaries,         2226.4 confs/binary
c             9 iterations,     237973.3 confs/iteration
c 
c            42 reductions,          0.1 redus/sec,  50994.3 confs/reduction
c         33434 restarts,           84.2 rests/sec,     64.1 confs/restart
c      13344400 decisions,       33622.1 decis/sec,      6.2 decis/conflict
c     648860132 propagations,  1634846.8 props/sec,     48.6 props/decision
c 
c 396.9 seconds, 46.7 MB
c launch: done
