c launch: /data/cnf/sc2014/app/post-c32s-ss-8.cnf.bz2
c host: atom24
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=6
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] AVG (--score=6)
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 [simpleprobe-2] all 9675 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 147 variables
c [simpleprobe-2] 2901 variables remain 30% (6627 retained 70%)
c [simpleprobe-2] removed 147 variables, found 1989 hbrs, 146 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19056 literals 100%
c [treelook-1] scheduling used 189326 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301136 steps
c [treelook-1] 18610 literals remain 98%
c [treelook-1] 9528 variables remain to probed next time 100%
c [decomp-5] removed 23 variables
c [treelook-1] removed 23 variables, found 3680 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2310 probes remain 24% after last round
c [basicprobe-1-0] removed 0 variables, found 5891 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 542 tauts, 0 hbrs, 432 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9505 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 5298 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 2 clauses out of 584 (0%) of length 7
c [cce-1-1] eliminated 1 clauses out of 1775 (0%) of length 6
c [cce-1-1] eliminated 7 clauses out of 282 (2%) of length 5
c [cce-1-1] eliminated 84 clauses out of 7532 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 95 large clauses in 6891631 steps
c [cce-1-1] allowing another 3445815 steps for small clauses
c [cce-1-1] scheduling 21397 clauses = 12587 binary + 8810 ternary
c [cce-1-1] tried to eliminate 21397 small clauses 100%
c [cce-1-1] eliminated 2427 binary clauses 19%
c [cce-1-1] eliminated 585 ternary clauses 7%
c [cce-1-1] eliminated 3012 small clauses 14%
c [cce-1-1] eliminated 3012 small clauses in 12623674 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3107 covered clauses in round 1
c [cce-1-2] eliminated 36 clauses out of 7448 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 36 large clauses in 5335275 steps
c [cce-1-2] allowing another 2667637 steps for small clauses
c [cce-1-2] scheduling 18385 clauses = 10160 binary + 8225 ternary
c [cce-1-2] tried to eliminate 18385 small clauses 100%
c [cce-1-2] eliminated 76 binary clauses 1%
c [cce-1-2] eliminated 55 ternary clauses 1%
c [cce-1-2] eliminated 131 small clauses 1%
c [cce-1-2] eliminated 131 small clauses in 9340727 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 167 covered clauses in round 2
c [cce-1-3] eliminated 52 clauses out of 7412 (1%) of length 4
c [cce-1-3] incomplete large round (ACCE)
c [cce-1-3] eliminated 52 large clauses in 8035601 steps
c [cce-1-3] allowing another 4017800 steps for small clauses
c [cce-1-3] scheduling 18254 clauses = 10084 binary + 8170 ternary
c [cce-1-3] tried to eliminate 10103 small clauses 55%
c [cce-1-3] eliminated 91 binary clauses 1%
c [cce-1-3] eliminated 11 ternary clauses 0%
c [cce-1-3] eliminated 102 small clauses 1%
c [cce-1-3] eliminated 102 small clauses in 8035602 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 154 covered clauses in round 3
c [cce-1] eliminated 3428 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9505 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 1697 variables 18% in round 1 in 4496638 steps
c [elim-2-1] backward subsumption/strengthening limit 4496600
c [elim-2-1-1] backward checking 5639 touched variables 59%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 28 and strengthened 24 clauses in 609281 steps
c [elim-2-1] rescheduled 112 variables 1% by backward subsumption
c [elim-2-2] eliminated 5 variables 0% in round 2 in 179948 steps
c [elim-2-2] backward subsumption/strengthening limit 179900
c [elim-2-2-1] backward checking 15 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 27097 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 1702 = 18% variables out of 9505 scheduled
c [bca-1] limit of 10000000 steps and 69290 added (scaled 2)
c [bca-1] 14395 out of 15608 literals actually usable 92%
c [bca-1] added 10 blocked clauses in 35725 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2791 pos 35.8% + 5012 neg 64.2% = 7803 sched 100.0% ret 0
c [sweep-1-1] 1001765 steps 287 queries 289.79 avg class size
c [sweep-1-1] 3452 decisions 280 SAT calls 28.23 avg env size
c [sweep-1-1] 5571 variables remain 71% (2232 retained 29%)
c [decomp-6] removed 33 variables
c [sweep-1-1] removed 33 vars (0 failed, 38 eqs, 27 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 33 vars in TOTAL (1 rounds, 286 queries)
c [sort-queue-2] sorted 1777 enqueued variables after 1000 conflicts
c [score-dist-2] active 5993 (77%), one 0 (0%), zero 1777 (23%)
c [score-dist-2] max exp 511, different 9 (2%)
c [score-dist-2] median active exp 510, avg 510.3
c [simplification-2] removed 1905 variables 19.7% (7770 remain 16%)
c [simplification-2] removed 11529 irredundant clauses 25.1% (34317 remain 25%)
c [simplification-2] maximum reduction of 25% = max (20%, 25%)
c [simplification-2] large reduction 25% >= 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 3001 conflicts
c [quatres-1] found 7132 quaternary clauses 65% in total
c [quatres-1-2] added 8 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3256 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 7770 free variables schedulable
c [ternres-1] 8967 ternary resolvents (33 bin, 8934 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 378 at-most-one constraints of average size 3.0
c [card-2] found 24 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 402 out of 402 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 70 at-most-one constraints, 30 used 43%
c [card-2] exported 38 binary clauses, 1.3 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5940 xors of average arity 3.0
c [gauss-1] connected 17784 occurrences of 965 variables (average 18.4)
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 4 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15532 literals 100%
c [treelook-2] scheduling used 254553 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 303544 steps
c [treelook-2] 15096 literals remain 97%
c [treelook-2] 7766 variables remain to probed next time 100%
c [decomp-8] removed 2 variables
c [treelook-2] removed 2 variables, found 2081 hbrs
c [transred-1] limit 224006 with penalty 0 = 0 + 0
c [transred-1] removed 332 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7764 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 5 blocked clauses
c [block-2] 5 < 1/100 * 34304 = 343 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 3 clauses out of 616 (0%) of length 7
c [cce-2-1] eliminated 2 clauses out of 1971 (0%) of length 6
c [cce-2-1] eliminated 75 clauses out of 477 (16%) of length 5
c [cce-2-1] eliminated 69 clauses out of 6864 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 149 large clauses in 4915250 steps
c [cce-2-1] allowing another 2457625 steps for small clauses
c [cce-2-1] scheduling 15087 clauses = 5247 binary + 9840 ternary
c [cce-2-1] tried to eliminate 15087 small clauses 100%
c [cce-2-1] eliminated 92 binary clauses 2%
c [cce-2-1] eliminated 1132 ternary clauses 12%
c [cce-2-1] eliminated 1224 small clauses 8%
c [cce-2-1] eliminated 1224 small clauses in 7360585 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 1373 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2318089 steps for small clauses
c [cce-2-2] scheduling 13863 clauses = 5155 binary + 8708 ternary
c [cce-2-2] tried to eliminate 13863 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 1373 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 7764 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 256 variables 3% in round 1 in 4284371 steps
c [elim-3-1] backward subsumption/strengthening limit 4284300
c [elim-3-1-1] backward checking 1348 touched variables 17%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 5 and strengthened 17 clauses in 172239 steps
c [elim-3-1] rescheduled 67 variables 1% by backward subsumption
c [elim-3-2] eliminated 2 variables 0% in round 2 in 169836 steps
c [elim-3-2] backward subsumption/strengthening limit 169800
c [elim-3-2-1] backward checking 17 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 15419 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 258 = 3% variables out of 7764 scheduled
c [bca-2] limit of 10000000 steps and 65705 added (scaled 2)
c [bca-2] 7056 out of 15014 literals actually usable 47%
c [bca-2] added 4 blocked clauses in 20862 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1909 pos 35.1% + 3535 neg 64.9% = 5444 sched 72.5% ret 2062
c [sweep-2-1] 1000911 steps 251 queries 305.55 avg class size
c [sweep-2-1] 2387 decisions 258 SAT calls 26.74 avg env size
c [sweep-2-1] 4451 variables remain 59% (3055 retained 41%)
c [decomp-9] removed 45 variables
c [sweep-2-1] removed 45 vars (0 failed, 47 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 45 vars in TOTAL (1 rounds, 250 queries)
c [sort-queue-3] sorted 726 enqueued variables after 3001 conflicts
c [score-dist-3] active 6735 (90%), one 0 (0%), zero 726 (10%)
c [score-dist-3] max exp 513, different 9 (2%)
c [score-dist-3] median active exp 512, avg 512.1
c [simplification-3] removed 309 variables 4.0% (7461 remain 15%)
c [simplification-3] removed 1814 irredundant clauses 5.3% (32503 remain 24%)
c [simplification-3] maximum reduction of 5% = max (4%, 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 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5002 conflicts
c [quatres-2] found 10017 quaternary clauses 71% in total
c [quatres-2-1] removed 7 duplicate quaternary clauses
c [quatres-2-2] added 20 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2444 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7461 free variables schedulable
c [ternres-2] 945 ternary resolvents (18 bin, 927 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-10] removed 5 variables
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 69 tauts, 0 hbrs, 513 literals
c [transred-2] limit 381424 with penalty 0 = 0 + 0
c [transred-2] removed 510 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 79 (1%) of length 10
c [cce-3-1] eliminated 1 clauses out of 612 (0%) of length 7
c [cce-3-1] eliminated 5 clauses out of 2026 (0%) of length 6
c [cce-3-1] eliminated 29 clauses out of 440 (7%) of length 5
c [cce-3-1] eliminated 140 clauses out of 6617 (2%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 176 large clauses in 13200904 steps
c [cce-3-1] allowing another 6600452 steps for small clauses
c [cce-3-1] scheduling 13117 clauses = 4348 binary + 8769 ternary
c [cce-3-1] tried to eliminate 13117 small clauses 100%
c [cce-3-1] eliminated 251 binary clauses 6%
c [cce-3-1] eliminated 433 ternary clauses 5%
c [cce-3-1] eliminated 684 small clauses 5%
c [cce-3-1] eliminated 684 small clauses in 13041921 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 860 covered clauses in round 1
c [cce-3-2] eliminated 2 clauses out of 2021 (0%) of length 6
c [cce-3-2] eliminated 98 clauses out of 6477 (2%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 100 large clauses in 13086359 steps
c [cce-3-2] allowing another 6543179 steps for small clauses
c [cce-3-2] scheduling 12433 clauses = 4097 binary + 8336 ternary
c [cce-3-2] tried to eliminate 12433 small clauses 100%
c [cce-3-2] eliminated 34 binary clauses 1%
c [cce-3-2] eliminated 49 ternary clauses 1%
c [cce-3-2] eliminated 83 small clauses 1%
c [cce-3-2] eliminated 83 small clauses in 12546668 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 183 covered clauses in round 2
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] allowing another 2205706 steps for small clauses
c [cce-3-3] scheduling 12350 clauses = 4063 binary + 8287 ternary
c [cce-3-3] tried to eliminate 4516 small clauses 37%
c [cce-3-3] eliminated 1 binary clauses 0%
c [cce-3-3] eliminated 1 small clauses 0%
c [cce-3-3] eliminated 1 small clauses in 4411483 steps
c [cce-3-3] incomplete small round (ACCE)
c [cce-3-3] eliminated 1 covered clauses in round 3
c [cce-3] eliminated 1044 covered clauses in TOTAL during 3 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7456 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 184 variables 2% in round 1 in 4288938 steps
c [elim-4-1] backward subsumption/strengthening limit 4288900
c [elim-4-1-1] backward checking 946 touched variables 13%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 25 and strengthened 39 clauses in 117846 steps
c [elim-4-1] rescheduled 128 variables 2% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 60464 steps
c [elim-4-2] backward subsumption/strengthening limit 60400
c [elim-4-2-1] backward checking 11 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 15664 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 186 = 2% variables out of 7456 scheduled
c [bca-3] limit of 10000000 steps and 62857 added (scaled 2)
c [bca-3] 4986 out of 14542 literals actually usable 34%
c [bca-3] added 3 blocked clauses in 18983 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1704 pos 39.5% + 2615 neg 60.5% = 4319 sched 59.4% ret 2951
c [sweep-3-1] 1001643 steps 286 queries 271.20 avg class size
c [sweep-3-1] 2856 decisions 295 SAT calls 26.69 avg env size
c [sweep-3-1] 3383 variables remain 47% (3887 retained 53%)
c [decomp-11] removed 39 variables
c [sweep-3-1] removed 39 vars (0 failed, 46 eqs, 20 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 39 vars in TOTAL (1 rounds, 285 queries)
c [sort-queue-4] sorted 502 enqueued variables after 5002 conflicts
c [score-dist-4] active 6729 (93%), one 0 (0%), zero 502 (7%)
c [score-dist-4] max exp 514, different 8 (2%)
c [score-dist-4] median active exp 513, avg 513.1
c [simplification-4] removed 230 variables 3.1% (7231 remain 15%)
c [simplification-4] removed 1415 irredundant clauses 4.4% (31088 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 9002 conflicts
c [quatres-3] found 11726 quaternary clauses 71% in total
c [quatres-3-1] removed 34 duplicate quaternary clauses
c [quatres-3-2] added 28 single-self-subsuming ternary resolvents
c [quatres-3-2] added 317 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7231 free variables schedulable
c [ternres-3] 706 ternary resolvents (15 bin, 691 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4130 xors of average arity 3.0
c [gauss-2] connected 12330 occurrences of 989 variables (average 12.5)
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 6 variables
c [basicprobe-2] limit 1786798 penalty 1 = 1 + 0
c [basicprobe-2-0] 2094 sched 29%, 0 failed, 0 lifted, 10515 hbrs
c [basicprobe-2-1] 1195 probes remain 17% after last round
c [basicprobe-2-1] removed 0 variables, found 10618 hbrs
c [bate-1] eliminated 73 asymmetric tautologies during probing
c [transred-3] limit 714719 with penalty 0 = 0 + 0
c [transred-3] removed 1152 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 7225 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 3 blocked clauses
c [block-3] 3 < 1/100 * 30999 = 309 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 630 (0%) of length 7
c [cce-4-1] eliminated 11 clauses out of 2099 (1%) of length 6
c [cce-4-1] eliminated 48 clauses out of 529 (9%) of length 5
c [cce-4-1] eliminated 55 clauses out of 6161 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 115 large clauses in 4025974 steps
c [cce-4-1] allowing another 2012987 steps for small clauses
c [cce-4-1] scheduling 12827 clauses = 3899 binary + 8928 ternary
c [cce-4-1] tried to eliminate 12827 small clauses 100%
c [cce-4-1] eliminated 46 binary clauses 1%
c [cce-4-1] eliminated 778 ternary clauses 9%
c [cce-4-1] eliminated 824 small clauses 6%
c [cce-4-1] eliminated 824 small clauses in 5346861 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 939 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 1961213 steps for small clauses
c [cce-4-2] scheduling 12003 clauses = 3853 binary + 8150 ternary
c [cce-4-2] tried to eliminate 12003 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 939 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7225 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 170 variables 2% in round 1 in 4168807 steps
c [elim-5-1] backward subsumption/strengthening limit 4168800
c [elim-5-1-1] backward checking 976 touched variables 14%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 4 and strengthened 17 clauses in 112541 steps
c [elim-5-1] rescheduled 59 variables 1% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 20797 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 170 = 2% variables out of 7225 scheduled
c [bca-4] limit of 10000000 steps and 60216 added (scaled 2)
c [bca-4] 3554 out of 14112 literals actually usable 25%
c [bca-4] added 0 blocked clauses in 18011 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1167 pos 35.4% + 2133 neg 64.6% = 3300 sched 46.8% ret 3755
c [sweep-4-1] 1000937 steps 292 queries 181.03 avg class size
c [sweep-4-1] 2605 decisions 269 SAT calls 31.21 avg env size
c [sweep-4-1] 2646 variables remain 38% (4409 retained 62%)
c [decomp-14] removed 63 variables
c [sweep-4-1] removed 63 vars (0 failed, 78 eqs, 55 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 63 vars in TOTAL (1 rounds, 291 queries)
c [sort-queue-5] sorted 284 enqueued variables after 9002 conflicts
c [score-dist-5] active 6708 (96%), one 0 (0%), zero 284 (4%)
c [score-dist-5] max exp 515, different 9 (2%)
c [score-dist-5] median active exp 514, avg 514.0
c [simplification-5] removed 239 variables 3.3% (6992 remain 14%)
c [simplification-5] removed 1376 irredundant clauses 4.4% (29712 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 27002 (soft 17002 + delta 10000)
c [simplification-5] new conflict limit 17002 (hard 27002)
c 
c [simplification-6] limit of 266 binary hit after 266 binaries
c [quatres-4] found 11628 quaternary clauses 67% in total
c [quatres-4-1] removed 43 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 42 single-self-subsuming ternary resolvents
c [quatres-4-2] added 729 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6992 free variables schedulable
c [ternres-4] 796 ternary resolvents (14 bin, 782 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 121 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] 121 out of 121 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 6 variables
c [simpleprobe-3] 1810 schedulable variables 26%
c [simpleprobe-3] limit 5515198 penalty 0 = 0 + 0
c [decomp-16] removed 32 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 32 variables, found 695 hbrs, 0 units
c [transred-4] limit 1378799 with penalty 0 = 0 + 0
c [transred-4] removed 1400 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 9 clauses out of 2142 (0%) of length 6
c [cce-5-1] eliminated 49 clauses out of 527 (9%) of length 5
c [cce-5-1] eliminated 212 clauses out of 5894 (4%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 270 large clauses in 11531295 steps
c [cce-5-1] allowing another 5765647 steps for small clauses
c [cce-5-1] scheduling 11746 clauses = 3344 binary + 8402 ternary
c [cce-5-1] tried to eliminate 11746 small clauses 100%
c [cce-5-1] eliminated 105 binary clauses 3%
c [cce-5-1] eliminated 345 ternary clauses 4%
c [cce-5-1] eliminated 450 small clauses 4%
c [cce-5-1] eliminated 450 small clauses in 10957690 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 720 covered clauses in round 1
c [cce-5-2] eliminated 7 clauses out of 2133 (0%) of length 6
c [cce-5-2] eliminated 3 clauses out of 478 (1%) of length 5
c [cce-5-2] eliminated 86 clauses out of 5682 (2%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 96 large clauses in 11158740 steps
c [cce-5-2] allowing another 5579370 steps for small clauses
c [cce-5-2] scheduling 11296 clauses = 3239 binary + 8057 ternary
c [cce-5-2] tried to eliminate 11296 small clauses 100%
c [cce-5-2] eliminated 31 binary clauses 1%
c [cce-5-2] eliminated 19 ternary clauses 0%
c [cce-5-2] eliminated 50 small clauses 0%
c [cce-5-2] eliminated 50 small clauses in 10580683 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 146 covered clauses in round 2
c [cce-5-3] eliminated 6 clauses out of 2126 (0%) of length 6
c [cce-5-3] eliminated 43 clauses out of 5596 (1%) of length 4
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] eliminated 49 large clauses in 8461635 steps
c [cce-5-3] allowing another 4230817 steps for small clauses
c [cce-5-3] scheduling 11246 clauses = 3208 binary + 8038 ternary
c [cce-5-3] tried to eliminate 9542 small clauses 85%
c [cce-5-3] eliminated 7 binary clauses 0%
c [cce-5-3] eliminated 9 ternary clauses 0%
c [cce-5-3] eliminated 16 small clauses 0%
c [cce-5-3] eliminated 16 small clauses in 8461628 steps
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 65 covered clauses in round 3
c [cce-5] eliminated 931 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6954 variables 100%
c [elim-6] limit of 27575992 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 193 variables 3% in round 1 in 4074033 steps
c [elim-6-1] backward subsumption/strengthening limit 4074000
c [elim-6-1-1] backward checking 1119 touched variables 16%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 10 and strengthened 32 clauses in 124722 steps
c [elim-6-1] rescheduled 123 variables 2% by backward subsumption
c [elim-6-2] eliminated 5 variables 0% in round 2 in 54891 steps
c [elim-6-2] backward subsumption/strengthening limit 54800
c [elim-6-2-1] backward checking 38 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 2 and strengthened 4 clauses in 20492 steps
c [elim-6-2] rescheduled 16 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 10177 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 198 = 3% variables out of 6954 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 815 pos 32.7% + 1677 neg 67.3% = 2492 sched 36.9% ret 4264
c [sweep-5-1] 4546522 steps 1324 queries 21.86 avg class size
c [sweep-5-1] 12639 decisions 1211 SAT calls 32.32 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 217 variables
c [sweep-5-1] removed 217 vars (0 failed, 268 eqs, 253 impls)
c [sweep-5-2] 2450 pos 37.5% + 4089 neg 62.5% = 6539 sched 100.0% ret 0
c [sweep-5-2] 5454778 steps 883 queries 41.97 avg class size
c [sweep-5-2] 12566 decisions 822 SAT calls 38.30 avg env size
c [sweep-5-2] 1063 variables remain 16% (5476 retained 84%)
c [decomp-18] removed 47 variables
c [sweep-5-2] removed 47 vars (0 failed, 107 eqs, 77 impls)
c [sweep-5] removed 264 vars in TOTAL (2 rounds, 2205 queries)
c [sort-queue-6] sorted 66 enqueued variables after 15768 conflicts
c [score-dist-6] active 6426 (99%), one 0 (0%), zero 66 (1%)
c [score-dist-6] max exp 515, different 7 (1%)
c [score-dist-6] median active exp 515, avg 514.9
c [simplification-6] removed 500 variables 7.2% (6492 remain 13%)
c [simplification-6] removed 1922 irredundant clauses 6.5% (27790 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 17002 (hard 27002)
c [simplification-6] new binary interval 1000
c 
c [simplification-7] limit 17002 conflicts (hard 27002) hit after 17003 conflicts
c [quatres-5] found 10780 quaternary clauses 65% in total
c [quatres-5-1] removed 253 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 42 single-self-subsuming ternary resolvents
c [quatres-5-2] added 215 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6492 free variables schedulable
c [ternres-5] 1450 ternary resolvents (19 bin, 1431 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 12984 literals 100%
c [treelook-3] scheduling used 295888 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301646 steps
c [treelook-3] 12505 literals remain 96%
c [treelook-3] 6467 variables remain to probed next time 100%
c [decomp-20] removed 3 variables
c [treelook-3] removed 3 variables, found 190 hbrs
c [unhide-4] limit 74799 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 7920 tauts, 0 hbrs, 4448 literals
c [transred-5] limit 1495992 with penalty 0 = 0 + 0
c [transred-5] removed 1071 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 629 (0%) of length 7
c [cce-6-1] eliminated 4 clauses out of 2059 (0%) of length 6
c [cce-6-1] eliminated 54 clauses out of 668 (8%) of length 5
c [cce-6-1] eliminated 103 clauses out of 4838 (2%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 162 large clauses in 2791130 steps
c [cce-6-1] allowing another 1395565 steps for small clauses
c [cce-6-1] scheduling 10900 clauses = 2868 binary + 8032 ternary
c [cce-6-1] tried to eliminate 10900 small clauses 100%
c [cce-6-1] eliminated 57 binary clauses 2%
c [cce-6-1] eliminated 151 ternary clauses 2%
c [cce-6-1] eliminated 208 small clauses 2%
c [cce-6-1] eliminated 208 small clauses in 4031171 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 370 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 1360433 steps for small clauses
c [cce-6-2] scheduling 10692 clauses = 2811 binary + 7881 ternary
c [cce-6-2] tried to eliminate 10692 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 370 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6489 variables 100%
c [elim-7] limit of 29919852 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 225 variables 3% in round 1 in 4014495 steps
c [elim-7-1] backward subsumption/strengthening limit 4014400
c [elim-7-1-1] backward checking 1451 touched variables 22%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 32 clauses in 166939 steps
c [elim-7-1] rescheduled 121 variables 2% by backward subsumption
c [elim-7-2] eliminated 5 variables 0% in round 2 in 73167 steps
c [elim-7-2] backward subsumption/strengthening limit 73100
c [elim-7-2-1] backward checking 36 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 1 and strengthened 3 clauses in 17632 steps
c [elim-7-2] rescheduled 11 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 4087 steps
c [elim-7-3] backward subsumption/strengthening limit 4000
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 0 and strengthened 3 clauses in 4001 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 231 = 4% variables out of 6489 scheduled
c [bca-5] limit of 10000000 steps and 54592 added (scaled 2)
c [bca-5] 1937 out of 12518 literals actually usable 15%
c [bca-5] added 8 blocked clauses in 17239 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 428 pos 43.5% + 557 neg 56.5% = 985 sched 15.7% ret 5273
c [sweep-6-1] 1002632 steps 372 queries 33.82 avg class size
c [sweep-6-1] 3646 decisions 354 SAT calls 30.76 avg env size
c [sweep-6-1] 374 variables remain 6% (5884 retained 94%)
c [decomp-21] removed 22 variables
c [sweep-6-1] removed 22 vars (0 failed, 30 eqs, 49 impls)
c [sweep-6] removed 22 vars in TOTAL (1 rounds, 371 queries)
c [sort-queue-7] sorted 31 enqueued variables after 17003 conflicts
c [score-dist-7] active 6205 (100%), one 0 (0%), zero 31 (0%)
c [score-dist-7] max exp 516, different 8 (2%)
c [score-dist-7] median active exp 515, avg 515.1
c [simplification-7] removed 256 variables 3.9% (6236 remain 13%)
c [simplification-7] removed 798 irredundant clauses 2.9% (26992 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  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.3    6235    26992     24320   18754  15687 12589    9    78   10  12%    306   57    9    2  375%
c 
c [simplification-8] limit 29003 conflicts (hard 39003) hit after 29004 conflicts
c [quatres-6] found 10175 quaternary clauses 60% in total
c [quatres-6-1] removed 26 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 49 single-self-subsuming ternary resolvents
c [quatres-6-2] added 602 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6235 free variables schedulable
c [ternres-6] 1003 ternary resolvents (35 bin, 968 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 2290 xors of average arity 3.0
c [gauss-3] connected 6828 occurrences of 764 variables (average 8.9)
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-22] removed 1 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 933 transitive binary clauses
c [transred-6] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 6233 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 4 blocked clauses
c [block-4] 4 < 1/100 * 26975 = 269 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 6 clauses out of 2050 (0%) of length 6
c [cce-7-1] eliminated 61 clauses out of 760 (8%) of length 5
c [cce-7-1] eliminated 321 clauses out of 4887 (7%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 388 large clauses in 9856767 steps
c [cce-7-1] allowing another 4928383 steps for small clauses
c [cce-7-1] scheduling 10206 clauses = 2516 binary + 7690 ternary
c [cce-7-1] tried to eliminate 10206 small clauses 100%
c [cce-7-1] eliminated 85 binary clauses 3%
c [cce-7-1] eliminated 246 ternary clauses 3%
c [cce-7-1] eliminated 331 small clauses 3%
c [cce-7-1] eliminated 331 small clauses in 9253684 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 719 covered clauses in round 1
c [cce-7-2] eliminated 3 clauses out of 2044 (0%) of length 6
c [cce-7-2] eliminated 3 clauses out of 699 (0%) of length 5
c [cce-7-2] eliminated 42 clauses out of 4566 (1%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 48 large clauses in 9284194 steps
c [cce-7-2] allowing another 4642097 steps for small clauses
c [cce-7-2] scheduling 9875 clauses = 2431 binary + 7444 ternary
c [cce-7-2] tried to eliminate 9875 small clauses 100%
c [cce-7-2] eliminated 9 binary clauses 0%
c [cce-7-2] eliminated 14 ternary clauses 0%
c [cce-7-2] eliminated 23 small clauses 0%
c [cce-7-2] eliminated 23 small clauses in 8797686 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 71 covered clauses in round 2
c [cce-7-3] eliminated 3 clauses out of 2041 (0%) of length 6
c [cce-7-3] eliminated 2 clauses out of 696 (0%) of length 5
c [cce-7-3] eliminated 29 clauses out of 4524 (1%) of length 4
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 34 large clauses in 9145980 steps
c [cce-7-3] allowing another 4572990 steps for small clauses
c [cce-7-3] scheduling 9852 clauses = 2422 binary + 7430 ternary
c [cce-7-3] tried to eliminate 9852 small clauses 100%
c [cce-7-3] eliminated 1 binary clauses 0%
c [cce-7-3] eliminated 15 ternary clauses 0%
c [cce-7-3] eliminated 16 small clauses 0%
c [cce-7-3] eliminated 16 small clauses in 8709094 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 50 covered clauses in round 3
c [cce-7] eliminated 840 covered clauses in TOTAL during 3 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 6233 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 955817620 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 143 variables 2% in round 1 in 3920154 steps
c [elim-8-1] backward subsumption/strengthening limit 3920100
c [elim-8-1-1] backward checking 974 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 5 and strengthened 32 clauses in 118196 steps
c [elim-8-1] rescheduled 119 variables 2% by backward subsumption
c [elim-8-2] eliminated 6 variables 0% in round 2 in 65786 steps
c [elim-8-2] backward subsumption/strengthening limit 65700
c [elim-8-2-1] backward checking 45 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 4 clauses in 18817 steps
c [elim-8-2] rescheduled 16 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 4365 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 149 = 2% variables out of 6233 scheduled
c [bca-6] limit of 10000000 steps and 52358 added (scaled 2)
c [bca-6] 780 out of 12170 literals actually usable 6%
c [bca-6] added 0 blocked clauses in 22526 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 183 pos 51.4% + 173 neg 48.6% = 356 sched 5.9% ret 5728
c [sweep-7-1] 1002496 steps 223 queries 15.46 avg class size
c [sweep-7-1] 3136 decisions 213 SAT calls 36.01 avg env size
c [sweep-7-1] 5 variables remain 0% (6079 retained 100%)
c [decomp-23] removed 16 variables
c [sweep-7-1] removed 16 vars (0 failed, 15 eqs, 35 impls)
c [sweep-7] removed 16 vars in TOTAL (1 rounds, 222 queries)
c [score-dist-8] active 6068 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 516, different 7 (1%)
c [score-dist-8] median active exp 516, avg 515.9
c [simplification-8] removed 167 variables 2.7% (6068 remain 12%)
c [simplification-8] removed 1113 irredundant clauses 4.1% (25879 remain 19%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 16000
c [simplification-8] penalized conflict interval 16000 = 1 * 16000
c [simplification-8] hard conflict limit 55004 (soft 45004 + delta 10000)
c [simplification-8] new conflict limit 45004 (hard 55004)
c 
c [simplification-9] limit 45004 conflicts (hard 55004) hit after 45004 conflicts
c [quatres-7] found 10305 quaternary clauses 57% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 78 single-self-subsuming ternary resolvents
c [quatres-7-2] added 535 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 6068 free variables schedulable
c [ternres-7] 498 ternary resolvents (31 bin, 467 trn)
c [ternres-7] 19 variables remain 0% (6049 retained 100%)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 812 transitive binary clauses
c [transred-7] found 1 units
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 637 (0%) of length 7
c [cce-8-1] eliminated 2 clauses out of 2036 (0%) of length 6
c [cce-8-1] eliminated 32 clauses out of 779 (4%) of length 5
c [cce-8-1] eliminated 218 clauses out of 4581 (5%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 253 large clauses in 2560060 steps
c [cce-8-1] allowing another 1280030 steps for small clauses
c [cce-8-1] scheduling 9610 clauses = 2328 binary + 7282 ternary
c [cce-8-1] tried to eliminate 9610 small clauses 100%
c [cce-8-1] eliminated 22 binary clauses 1%
c [cce-8-1] eliminated 36 ternary clauses 0%
c [cce-8-1] eliminated 58 small clauses 1%
c [cce-8-1] eliminated 64 small clauses in 3507605 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 317 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1226089 steps for small clauses
c [cce-8-2] scheduling 9552 clauses = 2306 binary + 7246 ternary
c [cce-8-2] tried to eliminate 9552 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 317 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 6067 variables 100%
c [elim-9] limit of 71247433 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 64 variables 1% in round 1 in 3851101 steps
c [elim-9-1] backward subsumption/strengthening limit 3851100
c [elim-9-1-1] backward checking 459 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 5 and strengthened 29 clauses in 64648 steps
c [elim-9-1] rescheduled 71 variables 1% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 31909 steps
c [elim-9-2] backward subsumption/strengthening limit 31900
c [elim-9-2-1] backward checking 17 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 12136 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 66 = 1% variables out of 6067 scheduled
c [sweep-8] limit 1068711 penalty 0 = 0 + 0
c [sweep-8-1] 2 pos 50.0% + 2 neg 50.0% = 4 sched 0.1% ret 5997
c [sweep-8-1] 28863 steps 4 queries 2.25 avg class size
c [sweep-8-1] 76 decisions 3 SAT calls 51.33 avg env size
c [sweep-8-1] fully completed sweeping round
c [sweep-8-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8-2] 2972 pos 49.5% + 3029 neg 50.5% = 6001 sched 100.0% ret 0
c [sweep-8-2] 1041235 steps 54 queries 312.22 avg class size
c [sweep-8-2] 2313 decisions 53 SAT calls 94.08 avg env size
c [sweep-8-2] 4521 variables remain 75% (1480 retained 25%)
c [sweep-8-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-8] removed 0 vars in TOTAL (2 rounds, 56 queries)
c [score-dist-9] active 6001 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 517, different 7 (1%)
c [score-dist-9] median active exp 517, avg 516.9
c [simplification-9] removed 67 variables 1.1% (6001 remain 12%)
c [simplification-9] removed 434 irredundant clauses 1.7% (25445 remain 19%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 22666
c [simplification-9] penalized conflict interval 22666 = 1 * 22666
c [simplification-9] hard conflict limit 79003 (soft 67670 + delta 11333)
c [simplification-9] new conflict limit 67670 (hard 79003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   25.3    6000    25445     53875   40533  16779  9651    9    64   13  14%    321   27    8    5  181%
c i   26.1    5999    25445     57817   43957  16818  9660    9    62   13  15%    -70   24    9    5  190%
c 
c [simplification-10] limit 67670 conflicts (hard 79003) hit after 67671 conflicts
c [quatres-8] found 10773 quaternary clauses 53% in total
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 52 single-self-subsuming ternary resolvents
c [quatres-8-2] added 312 quaternary resolvents
c [ternres-8] limit 5190135 with penalty 0 = 0 + 0
c [ternres-8] 19 schedulable variables 0%
c [ternres-8] 269 ternary resolvents (0 bin, 269 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 324383 penalty 3 = 3 + 0
c [card-4] found 144 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 324383 for elimination
c [card-4] 144 out of 144 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-27] removed 5 variables
c [basicprobe-3] limit 6487669 penalty 2 = 2 + 0
c [basicprobe-3-0] 800 sched 13%, 0 failed, 0 lifted, 674 hbrs
c [decomp-28] removed 1 variables
c [basicprobe-3-1] 1111 sched 19%, 1 failed, 0 lifted, 193 hbrs
c [decomp-29] removed 4 variables
c [basicprobe-3-2] 1053 sched 18%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-3-3] 1047 sched 17%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-3-4] 1042 sched 17%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-5] 1040 sched 17%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-6] 1039 sched 17%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-7] 1039 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-8] 1039 sched 17%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 5 variables, found 911 hbrs
c [bate-2] eliminated 4 asymmetric tautologies during probing
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1168 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 4 clauses out of 12 (33%) of length 13
c [cce-9-1] eliminated 16 clauses out of 44 (36%) of length 12
c [cce-9-1] eliminated 4 clauses out of 44 (9%) of length 10
c [cce-9-1] eliminated 16 clauses out of 90 (18%) of length 9
c [cce-9-1] eliminated 40 clauses out of 220 (18%) of length 8
c [cce-9-1] eliminated 130 clauses out of 641 (20%) of length 7
c [cce-9-1] eliminated 406 clauses out of 2018 (20%) of length 6
c [cce-9-1] eliminated 56 clauses out of 765 (7%) of length 5
c [cce-9-1] eliminated 223 clauses out of 4426 (5%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 895 large clauses in 7166582 steps
c [cce-9-1] allowing another 3583291 steps for small clauses
c [cce-9-1] scheduling 9884 clauses = 2310 binary + 7574 ternary
c [cce-9-1] tried to eliminate 9884 small clauses 100%
c [cce-9-1] eliminated 75 binary clauses 3%
c [cce-9-1] eliminated 699 ternary clauses 9%
c [cce-9-1] eliminated 774 small clauses 8%
c [cce-9-1] eliminated 774 small clauses in 6097396 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 1669 covered clauses in round 1
c [cce-9-2] eliminated 6 clauses out of 1612 (0%) of length 6
c [cce-9-2] eliminated 39 clauses out of 4203 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 45 large clauses in 6758601 steps
c [cce-9-2] allowing another 3379300 steps for small clauses
c [cce-9-2] scheduling 9110 clauses = 2235 binary + 6875 ternary
c [cce-9-2] tried to eliminate 9110 small clauses 100%
c [cce-9-2] eliminated 12 binary clauses 1%
c [cce-9-2] eliminated 27 ternary clauses 0%
c [cce-9-2] eliminated 39 small clauses 0%
c [cce-9-2] eliminated 39 small clauses in 5635099 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 84 covered clauses in round 2
c [cce-9-3] eliminated 9 clauses out of 1606 (1%) of length 6
c [cce-9-3] eliminated 3 clauses out of 709 (0%) of length 5
c [cce-9-3] eliminated 18 clauses out of 4164 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 30 large clauses in 6656229 steps
c [cce-9-3] allowing another 3328114 steps for small clauses
c [cce-9-3] scheduling 9071 clauses = 2223 binary + 6848 ternary
c [cce-9-3] tried to eliminate 9071 small clauses 100%
c [cce-9-3] eliminated 6 binary clauses 0%
c [cce-9-3] eliminated 9 ternary clauses 0%
c [cce-9-3] eliminated 15 small clauses 0%
c [cce-9-3] eliminated 15 small clauses in 5567976 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 45 covered clauses in round 3
c [cce-9] eliminated 1798 covered clauses in TOTAL during 3 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 5991 variables 100%
c [elim-10] limit of 103802705 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 475 variables 8% in round 1 in 3493788 steps
c [elim-10-1] backward subsumption/strengthening limit 3493700
c [elim-10-1-1] backward checking 1143 touched variables 19%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 7 and strengthened 15 clauses in 127541 steps
c [elim-10-1] rescheduled 77 variables 1% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 32755 steps
c [elim-10-2] backward subsumption/strengthening limit 32700
c [elim-10-2-1] backward checking 7 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 1 clauses in 13226 steps
c [elim-10-2] rescheduled 4 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 930 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 476 = 8% variables out of 5991 scheduled
c [bca-7] limit of 10000000 steps and 46850 added (scaled 2)
c [bca-7] 239 out of 11032 literals actually usable 2%
c [bca-7] added 0 blocked clauses in 43331 steps
c [score-dist-10] active 5515 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 517, different 4 (1%)
c [score-dist-10] median active exp 517, avg 517.0
c [simplification-10] removed 483 variables 8.1% (5515 remain 11%)
c [simplification-10] removed 2276 irredundant clauses 8.9% (23169 remain 17%)
c [simplification-10] maximum reduction of 9% = max (8%, 9%)
c [simplification-10] large reduction 9% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 79671 (soft 69671 + delta 10000)
c [simplification-10] new conflict limit 69671 (hard 79671)
c 
c [simplification-11] limit 69671 conflicts (hard 79671) hit after 69672 conflicts
c [quatres-9] found 9927 quaternary clauses 54% in total
c [quatres-9-1] removed 11 duplicate quaternary clauses
c [quatres-9-2] added 13 single-self-subsuming ternary resolvents
c [quatres-9-2] added 286 quaternary resolvents
c [ternres-9] limit 5320604 with penalty 0 = 0 + 0
c [ternres-9] all 5515 free variables schedulable
c [ternres-9] 738 ternary resolvents (33 bin, 705 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-36] removed 1 variables
c [simpleprobe-4] all 5514 free variables schedulable
c [simpleprobe-4] limit 21282418 penalty 0 = 0 + 0
c [decomp-37] removed 24 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 24 variables, found 920 hbrs, 0 units
c [unhide-5] limit 133015 with penalty 3 = 3 + 0
c [unhide-5-5] 0 units, 0 failed, 342 tauts, 0 hbrs, 12413 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1080 transitive binary clauses
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 9 clauses out of 1572 (1%) of length 6
c [cce-10-1] eliminated 19 clauses out of 777 (2%) of length 5
c [cce-10-1] eliminated 78 clauses out of 4219 (2%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 106 large clauses in 2111012 steps
c [cce-10-1] allowing another 1055506 steps for small clauses
c [cce-10-1] scheduling 8746 clauses = 2072 binary + 6674 ternary
c [cce-10-1] tried to eliminate 8746 small clauses 100%
c [cce-10-1] eliminated 10 binary clauses 0%
c [cce-10-1] eliminated 17 ternary clauses 0%
c [cce-10-1] eliminated 27 small clauses 0%
c [cce-10-1] eliminated 27 small clauses in 2818464 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 133 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1039330 steps for small clauses
c [cce-10-2] scheduling 8719 clauses = 2062 binary + 6657 ternary
c [cce-10-2] tried to eliminate 8719 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 133 covered clauses in TOTAL during 2 rounds
c [cce-10] 133 < 1/100 * 23106 = 231 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 5490 variables 100%
c [elim-11] limit of 106412091 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 45 variables 1% in round 1 in 3453761 steps
c [elim-11-1] backward subsumption/strengthening limit 3453700
c [elim-11-1-1] backward checking 299 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 1 clauses in 34724 steps
c [elim-11-1] rescheduled 12 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 4104 steps
c [elim-11-2] backward subsumption/strengthening limit 4100
c [elim-11-2-1] backward checking 8 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 2 and strengthened 1 clauses in 4101 steps
c [elim-11-2] rescheduled 7 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 3643 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 46 = 1% variables out of 5490 scheduled
c [elim-11] 46 < 1/100 * 5490 = 54 considered unsuccessful
c [sweep-9] limit 798090 penalty 1 = 1 + 0
c [sweep-9-1] 2422 pos 59.5% + 1649 neg 40.5% = 4071 sched 74.8% ret 1373
c [sweep-9-1] 816507 steps 39 queries 326.46 avg class size
c [sweep-9-1] 1918 decisions 38 SAT calls 84.03 avg env size
c [sweep-9-1] 3280 variables remain 60% (2164 retained 40%)
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9] removed 0 vars in TOTAL (1 rounds, 38 queries)
c [score-dist-11] active 5444 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 518, different 5 (1%)
c [score-dist-11] median active exp 518, avg 517.6
c [simplification-11] removed 71 variables 1.3% (5444 remain 11%)
c [simplification-11] removed 265 irredundant clauses 1.1% (22904 remain 17%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 11333 = 22666 / 2
c [simplification-11] new conflict interval 33999
c [simplification-11] penalized conflict interval 33999 = 1 * 33999
c [simplification-11] hard conflict limit 120670 (soft 103671 + delta 16999)
c [simplification-11] new conflict limit 103671 (hard 120670)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   34.7    5443    22904     86998   58722  15960  7453    9    54   15  17%    277    9    8    7  129%
c -   35.6    5443    22904     91286   22964  15987  7467    9    52   11  18%   -103    7    9    7  133%
c 
c [simplification-12] limit 103671 conflicts (hard 120670) hit after 103672 conflicts
c [quatres-10] found 10402 quaternary clauses 50% in total
c [quatres-10-1] removed 26 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 67 single-self-subsuming ternary resolvents
c [quatres-10-2] added 245 quaternary resolvents
c [ternres-10] limit 7714628 with penalty 0 = 0 + 0
c [ternres-10] all 5443 free variables schedulable
c [ternres-10] 417 ternary resolvents (30 bin, 387 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 937 xors of average arity 3.0
c [gauss-4] connected 2810 occurrences of 636 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 [treelook-4] limit 771462 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 10866 literals 100%
c [treelook-4] scheduling used 284794 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 771462 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 771469 steps
c [treelook-4] 8165 literals remain 75%
c [treelook-4] 5050 variables remain to probed next time 93%
c [decomp-40] removed 2 variables
c [treelook-4] removed 2 variables, found 531 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1026 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5441 variables 100%
c [block-5] limit of 9643285 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 486 blocked clauses
c [score-dist-12] active 5270 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 518, different 5 (1%)
c [score-dist-12] median active exp 518, avg 518.0
c [simplification-12] removed 173 variables 3.2% (5270 remain 11%)
c [simplification-12] removed 518 irredundant clauses 2.3% (22386 remain 16%)
c [simplification-12] maximum reduction of 3% = max (3%, 2%)
c [simplification-12] geometric conflict interval increment 8499 = 33999 / 4
c [simplification-12] new conflict interval 42498
c [simplification-12] penalized conflict interval 42498 = 1 * 42498
c [simplification-12] hard conflict limit 167419 (soft 146170 + delta 21249)
c [simplification-12] new conflict limit 146170 (hard 167419)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   42.7    5269    22386    130003   55587  16061  6869   10    62   14  16%    396   11   11    8  133%
c -   44.9    5269    22386    143914   30511  16096  6880    9    72   12  13%    -36   16   10    8  122%
c 
c [simplification-13] limit 146170 conflicts (hard 167419) hit after 146177 conflicts
c [quatres-11] found 10826 quaternary clauses 45% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 32 single-self-subsuming ternary resolvents
c [quatres-11-2] added 101 quaternary resolvents
c [ternres-11] limit 10321185 with penalty 0 = 0 + 0
c [ternres-11] all 5269 free variables schedulable
c [ternres-11] 160 ternary resolvents (22 bin, 138 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-41] removed 3 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 703 transitive binary clauses
c [cce-11] limit of 25802964 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 8 clauses out of 24 (33%) of length 10
c [cce-11-1] eliminated 4 clauses out of 46 (9%) of length 9
c [cce-11-1] eliminated 28 clauses out of 145 (19%) of length 8
c [cce-11-1] eliminated 83 clauses out of 433 (19%) of length 7
c [cce-11-1] eliminated 219 clauses out of 1428 (15%) of length 6
c [cce-11-1] eliminated 53 clauses out of 755 (7%) of length 5
c [cce-11-1] eliminated 198 clauses out of 4119 (5%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 593 large clauses in 4678102 steps
c [cce-11-1] allowing another 2339051 steps for small clauses
c [cce-11-1] scheduling 8621 clauses = 2024 binary + 6597 ternary
c [cce-11-1] tried to eliminate 8621 small clauses 100%
c [cce-11-1] eliminated 52 binary clauses 3%
c [cce-11-1] eliminated 101 ternary clauses 2%
c [cce-11-1] eliminated 153 small clauses 2%
c [cce-11-1] eliminated 153 small clauses in 4376831 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 746 covered clauses in round 1
c [cce-11-2] eliminated 4 clauses out of 350 (1%) of length 7
c [cce-11-2] eliminated 2 clauses out of 1209 (0%) of length 6
c [cce-11-2] eliminated 2 clauses out of 702 (0%) of length 5
c [cce-11-2] eliminated 26 clauses out of 3921 (1%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 34 large clauses in 4413229 steps
c [cce-11-2] allowing another 2206614 steps for small clauses
c [cce-11-2] scheduling 8468 clauses = 1972 binary + 6496 ternary
c [cce-11-2] tried to eliminate 8468 small clauses 100%
c [cce-11-2] eliminated 7 binary clauses 0%
c [cce-11-2] eliminated 11 ternary clauses 0%
c [cce-11-2] eliminated 18 small clauses 0%
c [cce-11-2] eliminated 18 small clauses in 4199203 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 52 covered clauses in round 2
c [cce-11-3] eliminated 2 clauses out of 1207 (0%) of length 6
c [cce-11-3] eliminated 2 clauses out of 700 (0%) of length 5
c [cce-11-3] eliminated 13 clauses out of 3895 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 17 large clauses in 4341529 steps
c [cce-11-3] allowing another 2170764 steps for small clauses
c [cce-11-3] scheduling 8450 clauses = 1965 binary + 6485 ternary
c [cce-11-3] tried to eliminate 8450 small clauses 100%
c [cce-11-3] eliminated 6 binary clauses 0%
c [cce-11-3] eliminated 4 ternary clauses 0%
c [cce-11-3] eliminated 10 small clauses 0%
c [cce-11-3] eliminated 10 small clauses in 4155098 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 27 covered clauses in round 3
c [cce-11] eliminated 825 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5267 variables 100%
c [elim-12] limit of 103211857 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 248 variables 5% in round 1 in 3142145 steps
c [elim-12-1] backward subsumption/strengthening limit 3142100
c [elim-12-1-1] backward checking 377 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 8 clauses in 38325 steps
c [elim-12-1] rescheduled 42 variables 1% by backward subsumption
c [elim-12-2] eliminated 8 variables 0% in round 2 in 14275 steps
c [elim-12-2] backward subsumption/strengthening limit 14200
c [elim-12-2-1] backward checking 51 touched variables 1%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 3 and strengthened 5 clauses in 14201 steps
c [elim-12-2] rescheduled 21 variables 0% by backward subsumption
c [elim-12-3] eliminated 2 variables 0% in round 3 in 12564 steps
c [elim-12-3] backward subsumption/strengthening limit 12500
c [elim-12-3-1] backward checking 9 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 10483 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 258 = 5% variables out of 5267 scheduled
c [bca-8] limit of 10000000 steps and 43068 added (scaled 2)
c [bca-8] 503 out of 10020 literals actually usable 5%
c [bca-8] added 0 blocked clauses in 30579 steps
c [score-dist-13] active 5009 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 519, different 4 (1%)
c [score-dist-13] median active exp 519, avg 519.0
c [simplification-13] removed 260 variables 4.9% (5009 remain 10%)
c [simplification-13] removed 1108 irredundant clauses 4.9% (21278 remain 16%)
c [simplification-13] maximum reduction of 5% = max (5%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 158177 (soft 148177 + delta 10000)
c [simplification-13] new conflict limit 148177 (hard 158177)
c 
c [simplification-14] limit 148177 conflicts (hard 158177) hit after 148177 conflicts
c [quatres-12] found 10321 quaternary clauses 46% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 13 single-self-subsuming ternary resolvents
c [quatres-12-2] added 77 quaternary resolvents
c [ternres-12] limit 10413747 with penalty 0 = 0 + 0
c [ternres-12] all 5009 free variables schedulable
c [ternres-12] 128 ternary resolvents (23 bin, 105 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-4] limit 26034369 penalty 1 = 1 + 0
c [basicprobe-4-0] 716 sched 14%, 2 failed, 0 lifted, 186 hbrs
c [decomp-43] removed 3 variables
c [basicprobe-4-1] 686 sched 14%, 1 failed, 0 lifted, 14 hbrs
c [decomp-44] removed 1 variables
c [basicprobe-4-2] 684 sched 14%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-4-3] 682 sched 14%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-4] 682 sched 14%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-5] 681 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 681 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-7] 681 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] 681 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 4 variables, found 226 hbrs
c [bate-3] eliminated 1 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 595 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5005 variables 100%
c [block-6] limit of 26034369 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 20 blocked clauses
c [block-6] 20 < 1/100 * 21257 = 212 considered unsuccessful
c [cce-12] limit of 52068738 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 349 (0%) of length 7
c [cce-12-1] eliminated 2 clauses out of 1205 (0%) of length 6
c [cce-12-1] eliminated 8 clauses out of 725 (1%) of length 5
c [cce-12-1] eliminated 70 clauses out of 3892 (2%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 81 large clauses in 1877825 steps
c [cce-12-1] allowing another 938912 steps for small clauses
c [cce-12-1] scheduling 8449 clauses = 1902 binary + 6547 ternary
c [cce-12-1] tried to eliminate 8449 small clauses 100%
c [cce-12-1] eliminated 3 binary clauses 0%
c [cce-12-1] eliminated 47 ternary clauses 1%
c [cce-12-1] eliminated 50 small clauses 1%
c [cce-12-1] eliminated 50 small clauses in 2862513 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 131 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 911789 steps for small clauses
c [cce-12-2] scheduling 8399 clauses = 1899 binary + 6500 ternary
c [cce-12-2] tried to eliminate 8399 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 131 covered clauses in TOTAL during 2 rounds
c [cce-12] 131 < 1/100 * 21237 = 212 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5004 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 27 variables 1% in round 1 in 3119404 steps
c [elim-13-1] backward subsumption/strengthening limit 3119400
c [elim-13-1-1] backward checking 186 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 1 clauses in 21577 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 2222 steps
c [elim-13-2] backward subsumption/strengthening limit 2200
c [elim-13-2-1] backward checking 5 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 2201 steps
c [elim-13-2] fully rescheduled 4976 variables 99%
c [elim-13-3] eliminated 6 variables 0% in round 3 in 3113420 steps
c [elim-13-3] backward subsumption/strengthening limit 3113400
c [elim-13-3-1] backward checking 37 touched variables 1%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 0 and strengthened 0 clauses in 10493 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 34 = 1% variables out of 5004 scheduled
c [elim-13] 34 < 1/100 * 5004 = 50 considered unsuccessful
c [sweep-10] limit 781031 penalty 2 = 2 + 0
c [sweep-10-1] 1243 pos 42.1% + 1710 neg 57.9% = 2953 sched 59.4% ret 2017
c [sweep-10-1] 792231 steps 94 queries 146.30 avg class size
c [sweep-10-1] 2378 decisions 93 SAT calls 50.01 avg env size
c [sweep-10-1] 2009 variables remain 40% (2961 retained 60%)
c [sweep-10-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-10] removed 0 vars in TOTAL (1 rounds, 93 queries)
c [score-dist-14] active 4970 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-14] max exp 519, different 4 (1%)
c [score-dist-14] median active exp 519, avg 519.0
c [simplification-14] removed 39 variables 0.8% (4970 remain 10%)
c [simplification-14] removed 235 irredundant clauses 1.1% (21043 remain 16%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 21249 = 42498 / 2
c [simplification-14] new conflict interval 63747
c [simplification-14] penalized conflict interval 63747 = 1 * 63747
c [simplification-14] hard conflict limit 243797 (soft 211924 + delta 31873)
c [simplification-14] new conflict limit 211924 (hard 243797)
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 -   53.4    4970    21043    195234   38738  15383  5267    9    53   12  17%    540   -6   11    9  126%
c i   57.5    4969    21043    229546   69184  15446  5291    9    42   17  22%    737  -12    8    9   91%
c -   58.6    4969    21043    240220   44574  15473  5295    9    44   13  20%   -562  -10   10    9  110%
c 
c [simplification-15] limit 211924 conflicts (hard 243797) hit after 243797 conflicts
c [quatres-13] found 10661 quaternary clauses 34% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 34 single-self-subsuming ternary resolvents
c [quatres-13-2] added 137 quaternary resolvents
c [ternres-13] limit 14442867 with penalty 0 = 0 + 0
c [ternres-13] all 4969 free variables schedulable
c [ternres-13] 262 ternary resolvents (35 bin, 227 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 451339 penalty 4 = 4 + 0
c [card-5] found 163 at-most-one constraints of average size 3.0
c [card-5] found 154 at-most-two constraints of average size 4.0
c [card-5] using previous limit 451339 for elimination
c [card-5] 317 out of 317 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-52] removed 2 variables
c [simpleprobe-5] all 4968 free variables schedulable
c [simpleprobe-5] limit 57771471 penalty 0 = 0 + 0
c [decomp-53] removed 1 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1 variables, found 795 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 950 transitive binary clauses
c [score-dist-15] active 4967 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-15] max exp 519, different 4 (1%)
c [score-dist-15] median active exp 519, avg 519.0
c [simplification-15] removed 2 variables 0.0% (4967 remain 10%)
c [simplification-15] removed 8 irredundant clauses 0.0% (21035 remain 15%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 63747
c [simplification-15] new conflict interval 127494
c [simplification-15] penalized conflict interval 127494 = 1 * 127494
c [simplification-15] hard conflict limit 435038 (soft 371291 + delta 63747)
c [simplification-15] new conflict limit 371291 (hard 435038)
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 -   63.6    4967    21035    282022   49607  15780  5189    9    48   13  19%    186   -2    9    9   99%
c -   68.5    4967    21035    323453   53576  15834  5209    9    35   13  26%    579   -9    9    9  102%
c -   73.7    4967    21035    365555   57560  15897  5220    9    34   14  28%    790   -6    9    9   96%
c 
c [simplification-16] limit 371291 conflicts (hard 435038) hit after 371292 conflicts
c [quatres-14] found 11284 quaternary clauses 27% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-1] added 3 double-self-subsuming ternary resolvents
c [quatres-14-2] added 39 single-self-subsuming ternary resolvents
c [quatres-14-2] added 87 quaternary resolvents
c [ternres-14] limit 19592854 with penalty 0 = 0 + 0
c [ternres-14] all 4967 free variables schedulable
c [ternres-14] 180 ternary resolvents (35 bin, 145 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-54] removed 2 variables
c [treelook-5] limit 1959285 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 9629 literals 97%
c [treelook-5] scheduling used 318757 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1959285 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1323164 steps
c [treelook-5] fully completed tree based probing
c [decomp-55] removed 3 variables
c [treelook-5] removed 3 variables, found 457 hbrs
c [unhide-6] limit 244910 with penalty 4 = 4 + 0
c [unhide-6-6] 0 units, 0 failed, 3125 tauts, 0 hbrs, 30826 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 530 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 489821360 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 8 clauses out of 1106 (1%) of length 6
c [cce-13-1] eliminated 15 clauses out of 707 (2%) of length 5
c [cce-13-1] eliminated 78 clauses out of 3892 (2%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 101 large clauses in 4464039 steps
c [cce-13-1] allowing another 2232019 steps for small clauses
c [cce-13-1] scheduling 8341 clauses = 1953 binary + 6388 ternary
c [cce-13-1] tried to eliminate 8341 small clauses 100%
c [cce-13-1] eliminated 70 binary clauses 4%
c [cce-13-1] eliminated 150 ternary clauses 2%
c [cce-13-1] eliminated 220 small clauses 3%
c [cce-13-1] eliminated 220 small clauses in 4160355 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 321 covered clauses in round 1
c [cce-13-2] eliminated 4 clauses out of 692 (1%) of length 5
c [cce-13-2] eliminated 17 clauses out of 3814 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 21 large clauses in 4186177 steps
c [cce-13-2] allowing another 2093088 steps for small clauses
c [cce-13-2] scheduling 8121 clauses = 1883 binary + 6238 ternary
c [cce-13-2] tried to eliminate 8121 small clauses 100%
c [cce-13-2] eliminated 12 binary clauses 1%
c [cce-13-2] eliminated 9 ternary clauses 0%
c [cce-13-2] eliminated 21 small clauses 0%
c [cce-13-2] eliminated 21 small clauses in 3948780 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 42 covered clauses in round 2
c [cce-13-3] eliminated 2 clauses out of 688 (0%) of length 5
c [cce-13-3] eliminated 11 clauses out of 3797 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 13 large clauses in 4132468 steps
c [cce-13-3] allowing another 2066234 steps for small clauses
c [cce-13-3] scheduling 8100 clauses = 1871 binary + 6229 ternary
c [cce-13-3] tried to eliminate 8100 small clauses 100%
c [cce-13-3] eliminated 3 binary clauses 0%
c [cce-13-3] eliminated 3 ternary clauses 0%
c [cce-13-3] eliminated 6 small clauses 0%
c [cce-13-3] eliminated 6 small clauses in 3913775 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 19 covered clauses in round 3
c [cce-13] eliminated 382 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 4962 variables 100%
c [elim-14] limit of 195928544 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 160 variables 3% in round 1 in 3107903 steps
c [elim-14-1] backward subsumption/strengthening limit 3107900
c [elim-14-1-1] backward checking 946 touched variables 19%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 5 and strengthened 27 clauses in 94260 steps
c [elim-14-1] rescheduled 97 variables 2% by backward subsumption
c [elim-14-2] eliminated 5 variables 0% in round 2 in 97891 steps
c [elim-14-2] backward subsumption/strengthening limit 97800
c [elim-14-2-1] backward checking 43 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 3 clauses in 13917 steps
c [elim-14-2] rescheduled 10 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 4001 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 165 = 3% variables out of 4962 scheduled
c [score-dist-16] active 4797 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-16] max exp 520, different 4 (1%)
c [score-dist-16] median active exp 520, avg 520.0
c [simplification-16] removed 170 variables 3.4% (4797 remain 10%)
c [simplification-16] removed 614 irredundant clauses 2.9% (20421 remain 15%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 31873 = 127494 / 4
c [simplification-16] new conflict interval 159367
c [simplification-16] penalized conflict interval 159367 = 1 * 159367
c [simplification-16] hard conflict limit 610342 (soft 530659 + delta 79683)
c [simplification-16] new conflict limit 530659 (hard 610342)
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 -   80.2    4797    20421    413562   58695  14372  3237    9    29   14  31%    911   -8   10    9  108%
c -   84.9    4797    20421    455196   63016  14401  3258    8    23   14  34%    964   -9    9    9   99%
c i   85.2    4796    20421    458751   66371  14409  3262    8    24   17  32%    967   -8    6    9   69%
c -   89.9    4796    20421    499780   67618  14452  3278    9    25   15  36%   -952   -5    8    9   89%
c i   92.5    4795    20421    520455   86259  14481  3288    8    31   18  27%   -417    1    6    9   72%
c i   93.0    4793    20421    524890   89575  14481  3288    8    31   19  25%  -1225    1    6    9   67%
c i   93.3    4792    20421    526299   90899  14489  3291    8    30   19  27%  -1238    0    7    9   77%
c i   93.9    4791    20421    531790   96121  14503  3298    8    26   20  30%  -1096   -4    7    9   86%
c i   94.4    4778    20421    535956  100050  14513  3302    8    22   26  35%  -1046   -8    6    9   72%
c i   94.8    4739    20421    539416  103330  14531  3308    8    24   26  34%  -1001   -6    7    8   83%
c i   94.8    4721    20421    539425  103333  14533  3309    8    24   26  34%  -1001   -6    7    8   81%
c i   94.9    4705    20421    539484  103367  14538  3314    8    23   26  34%  -1003   -6    6    8   75%
c i   94.9    4690    20421    539487  103367  14538  3314    8    23   26  34%  -1003   -6    6    8   75%
c 0   94.9    4646    20421    539487  103367  14538  3314    8    23   26  34%  -1003   -6    6    8   75%
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: 78 basic ate = 77 trn 99% + 1 lrg 1% in 3 updates
c bcas: 8 count, 25 added (2 skipped), 207256 steps
c bkwd: tried 95001 clauses, 189737 lits, 2.00 lits/clause
c bkwd: checked 1642692 occs, 17.29 occs/clause, 8.66 occs/lit
c bkwd: subsumed 0 binary, 68 ternary, 67 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 402 large (0% self)
c blkd: 6 bces, 5816 removed, 862497 resolutions, 2362574 steps
c blkd: 4345 blocking literals 4%, 172 pure
c bump: 518723 bumped seen, 21623907 lits 41.7 on average
c card: 5 count, 0 units, 38 am1, 5528292 steps
c card: 54 rescheduled, 524 eliminated, 17228 resolved, 3549 subsumed
c card: 806 at-most-one constraints found, average size 3.00
c card: 806 at-most-one constraints used 100%, average size 3.00
c card: 178 at-most-two constraints found, average size 4.01
c card: 178 at-most-two constraints used 100%, average size 4.01
c cces: 13 cces, 12505 eliminated, 8856 ate 71%, 3649 abce 29%
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: 103 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 55 decompositions, 3434 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4254466 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 39504 eliminated 73%, 506 pure 1%
c elms: 44 rounds, 3.1 rounds/bve
c elms: 38460 small 97%, 366 large 1%
c elms: 75890 tried small, 38460 succeeded 51%, 37430 failed 49%
c elms: 1193 subsumed, 2870 strengthened, 180 blocked
c elms: 2381253 copies, 2468017 resolutions, 2124509 ipos
c elms: 367999 subchks, 245503 strchks
c gaus: 4 extractions, 13297 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 6516630 steps, 3258315 extr 50%, 844989 elim 13%
c glue: 8.9 orig avg, 8.9 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 34738 = 4653 simple 13% + 27645 trn 80% + 2440 lrg 7%, 1216 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 518723 clauses, 16.7 length
c lrnd: 8658239 lits = 11586406 orig - 2928167 removed 25%
c lrnd: 211676 uips 41%, 177975 flips 34%
c mins: 489619 mins 94%, 953 bin 0%, 28151 size 5%
c mins: 14469026 poisoned searches, 1088589 hits, 8% hit rate
c mins: 24256621 used twice searches, 2440122 hits, 10% hit rate
c move: moved 13831, 4811 bin 35%, 9020 trn 65%
c otfs: 23055 driving 71%, 9383 restarting 29%
c otfs: str 32438, 31807 red 98%, 631 irr 2%
c otfs: str 32438, 0 bin 0%, 332 trn 1%, 32106 lrg 99%
c otfs: sub 387, 387 red 100%, 0 irr 0%
c otfs: sub 387, 0 bin 0%, 21 trn 5%, 366 lrg 95%
c phas: 1 computed, 9675 set, 3115 pos (32%), 6560 neg (68%)
c prbs: 4 basic, 39197 probed, 4 failed, 0 lifted
c prbs: 5 simple, 139228 probed, 359 failed, 1164 eqs
c prbs: 5 treelook, 13641 probed, 0 failed, 0 lifted
c prom: 125982 locked 18% out of 708683 tried
c prps: 161321682 props, 38 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 14 count, 9343 quat, 517 self1, 18 self2, 436 dup
c queu: 7 sorted, 4254466 next (31293 steps 0.01)
c queu: 21690720 enq (584081030 steps 26.93), 21623907 deq 100%
c redc: 19430 clauses 12%, 156606 tried 29%, 27 sat 0%
c redc: 24121 lits 2%, 1558013 tried 13%, 27 sat 0%
c redc: 609 times jump level reduced, 7.6 levels on average
c reds: 10 count, 53948.7 conflicts per reduce
c reds: 0 memlim 0%, 10 arith 100%
c reds: 272529 collected 78%, 78047 retired 22%
c rmbd: 287 removed, 287 red 100%
c rsts: 18780 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: 16 count, 15 confs 94%, 0 vars 0%
c simp: 0 its 0%, 1 bin 6%, 0 trns 0%
c subl: 518723 count (170984 tried 0.3), 33761 sub out of 513908 (6.6%)
c swps: 10 count, 12 rounds, 4097 queries (341.4/round)
c swps: 3889 sat calls, 421 unsat (0.6% success rate)
c swps: 49972 decisions 12.8, 2291 conflicts 0.6
c swps; 101.5 avg class size, 34.3 avg environment size
c swps: 0 failed, 535 impls, 629 equivs
c swp0: 1363 type 0 queries, 558 unsat (40.9%), 1302 sat (95.5%)
c swp1: 2734 type 1 queries, 1931 unsat (70.6%), 2166 sat (79.2%)
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: 9546718 calls to obtain time
c tops: 6168 fixed 11%, 16 its, 33717.94 confs/it
c trds: 14 transitive reductions, 12262 removed, 2 failed
c trds: 161605 nodes, 135867 edges, 2928639 steps
c trim: 215204 words, 0.8 MB
c trnr: 14 count, 343 bin, 16176 trn, 49784178 steps
c unhd: 6 count, 6 rounds, 3542172 steps
c unhd: 134 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: 12016 tauts, 68 bin 1%, 2177 trn 18%, 292 lrg 2%
c unhd: 12016 tauts, 9479 stamp 79%, 11963 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 48651 str, 16 bin 0%, 486 trn 1%, 48149 lrg 99%, 47121 red 97%
c vars: 4646 remaining 9% and 49106 removed 91% out of 53752
c vars: 6168 fixed 11%, 39504 eliminated 73%, 3434 equivalent 6%
c vsts: 2620064262 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 16.3 search visits per propagation, 4810.7 per conflict
c wchs: 396201097 pushed, 5683456 enlarged, 195 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         523251        272529         78047      15847189       3406894        164179
c 
c  0 0         65507  13      1836   1         0   0   9738057  61   1773325  52     68228  42     1.8
c  1 5         50062  10     26284  10      6142   8   1913472  12<   434140  13<    18414  11<    0.6
c  2 6        185966  36<   115396  42     24751  32   3208533  20    815433  24     49120  30     1.5
c  3 9        156837  30     93523  34<    29155  37<   882712   6    322781   9     25157  15     1.4
c  4 14        47996   9     26849  10     12811  16     82012   1     48064   1      2670   2     0.6
c  5 21        11902   2      6107   2      3678   5     16138   0      9431   0       403   0     0.3
c  6 30         3667   1      1941   1      1089   1      4675   0      2808   0       128   0     0.1
c  7 41         1026   0       481   0       332   0      1228   0       703   0        38   0     0.1
c  8 54          203   0        78   0        61   0       262   0       147   0        14   0     0.0
c  9 69           61   0        25   0        19   0        72   0        47   0         6   0     0.0
c 10 86           24   0         9   0         9   0        28   0        15   0         1   0     0.0
c 
c avg                  2.2           2.5           2.8           0.7           1.0           1.3
c std                  1.3           1.0           1.1           1.0           1.2           1.2
c 
c   13.031  14% cce
c    9.338  10% bump
c    3.201   3% elim
c    3.070   3% decide
c    1.639   2% probe
c    1.066   1% sweep
c    0.464   0% quatres
c    0.444   0% ternres
c 
c    1.164 < 1% rest (below)
c 
c    0.284   0% unhide
c    0.246   0% block
c    0.199   0% gauss
c    0.180   0% transred
c    0.147   0% bca
c    0.108   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.874   1% preprocessing     4%
c   20.942  22% inprocessing     96%
c ==================================
c   21.815  23% simplifying
c   73.035  77% search
c ==================================
c   94.851 100% all
c 
c        539487 conflicts,        5687.7 confs/sec
c          2331 ternaries,         231.4 confs/ternary
c           877 binaries,          615.2 confs/binary
c            16 iterations,      33717.9 confs/iteration
c 
c            10 reductions,          0.1 redus/sec,  53948.7 confs/reduction
c         18780 restarts,          198.0 rests/sec,     28.7 confs/restart
c       4254466 decisions,       44854.0 decis/sec,      7.9 decis/conflict
c     161321682 propagations,  1700783.3 props/sec,     37.9 props/decision
c 
c 94.9 seconds, 30.2 MB
c launch: done
