c launch: /data/cnf/sc2014/app/post-c32s-ss-8.cnf.bz2
c host: atom19
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=3
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] SUM (--score=3)
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 1001 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] all 9671 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 120 variables
c [simpleprobe-2] 2964 variables remain 31% (6587 retained 69%)
c [simpleprobe-2] removed 120 variables, found 1978 hbrs, 118 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19102 literals 100%
c [treelook-1] scheduling used 189294 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300245 steps
c [treelook-1] 18648 literals remain 98%
c [treelook-1] 9549 variables remain to probed next time 100%
c [decomp-5] removed 21 variables
c [treelook-1] removed 21 variables, found 3194 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2309 probes remain 24% after last round
c [basicprobe-1-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 10 variables, found 6381 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 18 units, 0 failed, 356 tauts, 0 hbrs, 402 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9502 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 5290 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 208 (1%) of length 8
c [cce-1-1] eliminated 2 clauses out of 582 (0%) of length 7
c [cce-1-1] eliminated 9 clauses out of 278 (3%) of length 5
c [cce-1-1] eliminated 82 clauses out of 7550 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 95 large clauses in 6918972 steps
c [cce-1-1] allowing another 3459486 steps for small clauses
c [cce-1-1] scheduling 21384 clauses = 12616 binary + 8768 ternary
c [cce-1-1] tried to eliminate 21384 small clauses 100%
c [cce-1-1] eliminated 2516 binary clauses 20%
c [cce-1-1] eliminated 649 ternary clauses 7%
c [cce-1-1] eliminated 3165 small clauses 15%
c [cce-1-1] eliminated 3165 small clauses in 12412491 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3260 covered clauses in round 1
c [cce-1-2] eliminated 37 clauses out of 7468 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 37 large clauses in 5275760 steps
c [cce-1-2] allowing another 2637880 steps for small clauses
c [cce-1-2] scheduling 18219 clauses = 10100 binary + 8119 ternary
c [cce-1-2] tried to eliminate 18219 small clauses 100%
c [cce-1-2] eliminated 69 binary clauses 1%
c [cce-1-2] eliminated 53 ternary clauses 1%
c [cce-1-2] eliminated 122 small clauses 1%
c [cce-1-2] eliminated 122 small clauses in 9027584 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 159 covered clauses in round 2
c [cce-1-3] eliminated 63 clauses out of 7431 (1%) of length 4
c [cce-1-3] incomplete large round (ACCE)
c [cce-1-3] eliminated 63 large clauses in 8559926 steps
c [cce-1-3] allowing another 4279963 steps for small clauses
c [cce-1-3] scheduling 18097 clauses = 10031 binary + 8066 ternary
c [cce-1-3] tried to eliminate 10787 small clauses 60%
c [cce-1-3] eliminated 98 binary clauses 1%
c [cce-1-3] eliminated 13 ternary clauses 0%
c [cce-1-3] eliminated 111 small clauses 1%
c [cce-1-3] eliminated 111 small clauses in 8559932 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 174 covered clauses in round 3
c [cce-1] eliminated 3593 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9502 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 1759 variables 19% in round 1 in 4514993 steps
c [elim-2-1] backward subsumption/strengthening limit 4514900
c [elim-2-1-1] backward checking 5688 touched variables 60%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 28 and strengthened 16 clauses in 614342 steps
c [elim-2-1] rescheduled 102 variables 1% by backward subsumption
c [elim-2-2] eliminated 3 variables 0% in round 2 in 209562 steps
c [elim-2-2] backward subsumption/strengthening limit 209500
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 1 clauses in 30217 steps
c [elim-2-2] rescheduled 6 variables 0% by backward subsumption
c [elim-2-3] no variable eliminated in round 3 in 6653 steps
c [elim-2] fully completed in 3 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 1762 = 19% variables out of 9502 scheduled
c [bca-1] limit of 10000000 steps and 68832 added (scaled 2)
c [bca-1] 14583 out of 15482 literals actually usable 94%
c [bca-1] added 14 blocked clauses in 36285 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2841 pos 36.7% + 4899 neg 63.3% = 7740 sched 100.0% ret 0
c [sweep-1-1] 1000873 steps 307 queries 319.90 avg class size
c [sweep-1-1] 3797 decisions 315 SAT calls 27.30 avg env size
c [sweep-1-1] 5559 variables remain 72% (2181 retained 28%)
c [decomp-6] removed 23 variables
c [sweep-1-1] removed 23 vars (0 failed, 27 eqs, 18 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 23 vars in TOTAL (1 rounds, 306 queries)
c [sort-queue-2] sorted 2215 enqueued variables after 1001 conflicts
c [score-dist-2] active 5502 (71%), one 0 (0%), zero 2215 (29%)
c [score-dist-2] max exp 518, different 17 (3%)
c [score-dist-2] median active exp 512, avg 511.5
c [simplification-2] removed 1958 variables 20.2% (7717 remain 16%)
c [simplification-2] removed 11733 irredundant clauses 25.6% (34113 remain 25%)
c [simplification-2] maximum reduction of 26% = max (20%, 26%)
c [simplification-2] large reduction 26% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 7158 quaternary clauses 65% in total
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3545 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 7717 free variables schedulable
c [ternres-1] 9248 ternary resolvents (28 bin, 9220 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 364 at-most-one constraints of average size 3.0
c [card-2] found 15 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 379 out of 379 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 75 at-most-one constraints, 37 used 49%
c [card-2] exported 40 binary clauses, 1.1 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 5 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15423 literals 100%
c [treelook-2] scheduling used 261591 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 301069 steps
c [treelook-2] 14897 literals remain 97%
c [treelook-2] 7710 variables remain to probed next time 100%
c [decomp-8] removed 8 variables
c [treelook-2] removed 8 variables, found 1521 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 55 tauts, 0 hbrs, 685 literals
c [transred-1] limit 175665 with penalty 0 = 0 + 0
c [transred-1] removed 241 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7704 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 3 blocked clauses
c [block-2] 3 < 1/100 * 34061 = 340 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 79 (1%) of length 10
c [cce-2-1] eliminated 6 clauses out of 610 (1%) of length 7
c [cce-2-1] eliminated 3 clauses out of 2008 (0%) of length 6
c [cce-2-1] eliminated 61 clauses out of 451 (14%) of length 5
c [cce-2-1] eliminated 41 clauses out of 6815 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 112 large clauses in 4809592 steps
c [cce-2-1] allowing another 2404796 steps for small clauses
c [cce-2-1] scheduling 14932 clauses = 5006 binary + 9926 ternary
c [cce-2-1] tried to eliminate 14932 small clauses 100%
c [cce-2-1] eliminated 73 binary clauses 1%
c [cce-2-1] eliminated 1099 ternary clauses 11%
c [cce-2-1] eliminated 1172 small clauses 8%
c [cce-2-1] eliminated 1172 small clauses in 7097314 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 1284 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 2301548 steps for small clauses
c [cce-2-2] scheduling 13760 clauses = 4933 binary + 8827 ternary
c [cce-2-2] tried to eliminate 13760 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 1284 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 7704 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 235 variables 3% in round 1 in 4269121 steps
c [elim-3-1] backward subsumption/strengthening limit 4269100
c [elim-3-1-1] backward checking 1250 touched variables 16%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 4 and strengthened 28 clauses in 173485 steps
c [elim-3-1] rescheduled 61 variables 1% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 88789 steps
c [elim-3-2] backward subsumption/strengthening limit 88700
c [elim-3-2-1] backward checking 20 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 17500 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 238 = 3% variables out of 7704 scheduled
c [bca-2] limit of 10000000 steps and 65433 added (scaled 2)
c [bca-2] 7542 out of 14934 literals actually usable 51%
c [bca-2] added 11 blocked clauses in 22398 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2473 pos 45.6% + 2955 neg 54.4% = 5428 sched 72.7% ret 2038
c [sweep-2-1] 1004163 steps 276 queries 210.36 avg class size
c [sweep-2-1] 2764 decisions 275 SAT calls 28.35 avg env size
c [sweep-2-1] 4294 variables remain 58% (3172 retained 42%)
c [decomp-9] removed 40 variables
c [sweep-2-1] removed 40 vars (0 failed, 46 eqs, 24 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 40 vars in TOTAL (1 rounds, 275 queries)
c [sort-queue-3] sorted 1415 enqueued variables after 3001 conflicts
c [score-dist-3] active 6011 (81%), one 0 (0%), zero 1415 (19%)
c [score-dist-3] max exp 522, different 21 (4%)
c [score-dist-3] median active exp 515, avg 514.1
c [simplification-3] removed 291 variables 3.8% (7426 remain 15%)
c [simplification-3] removed 1735 irredundant clauses 5.1% (32378 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 10142 quaternary clauses 72% in total
c [quatres-2-1] removed 8 duplicate quaternary clauses
c [quatres-2-2] added 19 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1574 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7426 free variables schedulable
c [ternres-2] 733 ternary resolvents (16 bin, 717 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-10] removed 2 variables
c [basicprobe-2] limit 1587999 penalty 0 = 0 + 0
c [basicprobe-2-0] 2141 sched 29%, 3 failed, 0 lifted, 12448 hbrs
c [decomp-11] removed 3 variables
c [basicprobe-2-1] 1663 probes remain 22% after last round
c [basicprobe-2-1] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 3 variables, found 12513 hbrs
c [bate-1] eliminated 88 asymmetric tautologies during probing
c [transred-2] limit 317599 with penalty 0 = 0 + 0
c [transred-2] removed 477 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 9 clauses out of 2062 (0%) of length 6
c [cce-3-1] eliminated 31 clauses out of 425 (7%) of length 5
c [cce-3-1] eliminated 130 clauses out of 6629 (2%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 170 large clauses in 12291526 steps
c [cce-3-1] allowing another 6145763 steps for small clauses
c [cce-3-1] scheduling 13199 clauses = 4324 binary + 8875 ternary
c [cce-3-1] tried to eliminate 13199 small clauses 100%
c [cce-3-1] eliminated 294 binary clauses 7%
c [cce-3-1] eliminated 995 ternary clauses 11%
c [cce-3-1] eliminated 1289 small clauses 10%
c [cce-3-1] eliminated 1289 small clauses in 10636599 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 1459 covered clauses in round 1
c [cce-3-2] eliminated 3 clauses out of 2053 (0%) of length 6
c [cce-3-2] eliminated 1 clauses out of 394 (0%) of length 5
c [cce-3-2] eliminated 107 clauses out of 6499 (2%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 111 large clauses in 12506093 steps
c [cce-3-2] allowing another 6253046 steps for small clauses
c [cce-3-2] scheduling 11910 clauses = 4030 binary + 7880 ternary
c [cce-3-2] tried to eliminate 11910 small clauses 100%
c [cce-3-2] eliminated 29 binary clauses 1%
c [cce-3-2] eliminated 47 ternary clauses 1%
c [cce-3-2] eliminated 76 small clauses 1%
c [cce-3-2] eliminated 76 small clauses in 10205493 steps
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 187 covered clauses in round 2
c [cce-3-3] eliminated 2 clauses out of 2050 (0%) of length 6
c [cce-3-3] eliminated 41 clauses out of 6392 (1%) of length 4
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] eliminated 43 large clauses in 9157912 steps
c [cce-3-3] allowing another 4578956 steps for small clauses
c [cce-3-3] scheduling 11834 clauses = 4001 binary + 7833 ternary
c [cce-3-3] tried to eliminate 11834 small clauses 100%
c [cce-3-3] eliminated 19 binary clauses 0%
c [cce-3-3] eliminated 17 ternary clauses 0%
c [cce-3-3] eliminated 36 small clauses 0%
c [cce-3-3] eliminated 36 small clauses in 8460783 steps
c [cce-3-3] completed small round (ACCE)
c [cce-3-3] eliminated 79 covered clauses in round 3
c [cce-3] eliminated 1725 covered clauses in TOTAL during 3 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7421 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 284 variables 4% in round 1 in 4187887 steps
c [elim-4-1] backward subsumption/strengthening limit 4187800
c [elim-4-1-1] backward checking 1489 touched variables 20%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 13 and strengthened 32 clauses in 170067 steps
c [elim-4-1] rescheduled 106 variables 1% by backward subsumption
c [elim-4-2] eliminated 3 variables 0% in round 2 in 48916 steps
c [elim-4-2] backward subsumption/strengthening limit 48900
c [elim-4-2-1] backward checking 27 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 18166 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 287 = 4% variables out of 7421 scheduled
c [bca-3] limit of 10000000 steps and 61006 added (scaled 2)
c [bca-3] 6393 out of 14270 literals actually usable 45%
c [bca-3] added 6 blocked clauses in 21446 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1924 pos 46.7% + 2192 neg 53.3% = 4116 sched 57.7% ret 3018
c [sweep-3-1] 1002841 steps 276 queries 222.93 avg class size
c [sweep-3-1] 2777 decisions 279 SAT calls 30.41 avg env size
c [sweep-3-1] 3168 variables remain 44% (3966 retained 56%)
c [decomp-12] removed 38 variables
c [sweep-3-1] removed 38 vars (0 failed, 39 eqs, 30 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 38 vars in TOTAL (1 rounds, 275 queries)
c [sort-queue-4] sorted 1178 enqueued variables after 5002 conflicts
c [score-dist-4] active 5918 (83%), one 0 (0%), zero 1178 (17%)
c [score-dist-4] max exp 523, different 22 (4%)
c [score-dist-4] median active exp 516, avg 516.0
c [simplification-4] removed 330 variables 4.4% (7096 remain 15%)
c [simplification-4] removed 2219 irredundant clauses 6.9% (30159 remain 22%)
c [simplification-4] maximum reduction of 7% = max (4%, 7%)
c [simplification-4] large reduction 7% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17002 (soft 7002 + delta 10000)
c [simplification-4] new conflict limit 7002 (hard 17002)
c 
c [simplification-5] limit 7002 conflicts (hard 17002) hit after 7002 conflicts
c [quatres-3] found 10404 quaternary clauses 71% in total
c [quatres-3-1] removed 9 duplicate quaternary clauses
c [quatres-3-2] added 14 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1312 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7096 free variables schedulable
c [ternres-3] 589 ternary resolvents (5 bin, 584 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 3670 xors of average arity 3.0
c [gauss-2] connected 10982 occurrences of 973 variables (average 11.3)
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 [simpleprobe-3] 1884 schedulable variables 27%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-14] removed 20 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 20 variables, found 320 hbrs, 0 units
c [unhide-4] limit 50000 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 2718 tauts, 0 hbrs, 5006 literals
c [transred-3] limit 433747 with penalty 0 = 0 + 0
c [transred-3] removed 252 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 7076 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 5 blocked clauses
c [block-3] 5 < 1/100 * 30111 = 301 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 619 (0%) of length 7
c [cce-4-1] eliminated 6 clauses out of 2101 (0%) of length 6
c [cce-4-1] eliminated 70 clauses out of 643 (11%) of length 5
c [cce-4-1] eliminated 57 clauses out of 5833 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 134 large clauses in 3771855 steps
c [cce-4-1] allowing another 1885927 steps for small clauses
c [cce-4-1] scheduling 12515 clauses = 3449 binary + 9066 ternary
c [cce-4-1] tried to eliminate 12515 small clauses 100%
c [cce-4-1] eliminated 27 binary clauses 1%
c [cce-4-1] eliminated 247 ternary clauses 3%
c [cce-4-1] eliminated 274 small clauses 2%
c [cce-4-1] eliminated 274 small clauses in 5276179 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 408 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 1851797 steps for small clauses
c [cce-4-2] scheduling 12241 clauses = 3422 binary + 8819 ternary
c [cce-4-2] tried to eliminate 12241 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 408 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7076 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 104 variables 1% in round 1 in 4109273 steps
c [elim-5-1] backward subsumption/strengthening limit 4109200
c [elim-5-1-1] backward checking 744 touched variables 11%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 13 clauses in 88556 steps
c [elim-5-1] rescheduled 54 variables 1% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 16708 steps
c [elim-5-2] backward subsumption/strengthening limit 16700
c [elim-5-2-1] backward checking 7 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 1 clauses in 12826 steps
c [elim-5-2] rescheduled 4 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 1247 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 105 = 1% variables out of 7076 scheduled
c [bca-4] limit of 10000000 steps and 59609 added (scaled 2)
c [bca-4] 5578 out of 13944 literals actually usable 40%
c [bca-4] added 7 blocked clauses in 20993 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1307 pos 42.1% + 1795 neg 57.9% = 3102 sched 44.5% ret 3869
c [sweep-4-1] 1003589 steps 327 queries 124.38 avg class size
c [sweep-4-1] 2875 decisions 326 SAT calls 28.85 avg env size
c [sweep-4-1] 2412 variables remain 35% (4559 retained 65%)
c [decomp-15] removed 46 variables
c [sweep-4-1] removed 46 vars (0 failed, 57 eqs, 31 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 46 vars in TOTAL (1 rounds, 326 queries)
c [sort-queue-5] sorted 1016 enqueued variables after 7002 conflicts
c [score-dist-5] active 5909 (85%), one 0 (0%), zero 1016 (15%)
c [score-dist-5] max exp 525, different 21 (4%)
c [score-dist-5] median active exp 517, avg 517.2
c [simplification-5] removed 171 variables 2.4% (6925 remain 14%)
c [simplification-5] removed 726 irredundant clauses 2.4% (29433 remain 22%)
c [simplification-5] maximum reduction of 2% = max (2%, 2%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 6666
c [simplification-5] penalized conflict interval 6666 = 1 * 6666
c [simplification-5] hard conflict limit 23668 (soft 13668 + delta 10000)
c [simplification-5] new conflict limit 13668 (hard 23668)
c 
c [simplification-6] limit 13668 conflicts (hard 23668) hit after 13668 conflicts
c [quatres-4] found 11111 quaternary clauses 72% in total
c [quatres-4-1] removed 53 duplicate quaternary clauses
c [quatres-4-2] added 20 single-self-subsuming ternary resolvents
c [quatres-4-2] added 194 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6925 free variables schedulable
c [ternres-4] 638 ternary resolvents (12 bin, 626 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 115 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] 115 out of 115 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-16] removed 1 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 13847 literals 100%
c [treelook-3] scheduling used 300002 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301457 steps
c [treelook-3] 13429 literals remain 97%
c [treelook-3] 6923 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 408 hbrs
c [transred-4] limit 922440 with penalty 0 = 0 + 0
c [transred-4] removed 804 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 8 clauses out of 2131 (0%) of length 6
c [cce-5-1] eliminated 28 clauses out of 659 (4%) of length 5
c [cce-5-1] eliminated 137 clauses out of 5688 (2%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 173 large clauses in 11321479 steps
c [cce-5-1] allowing another 5660739 steps for small clauses
c [cce-5-1] scheduling 11024 clauses = 3221 binary + 7803 ternary
c [cce-5-1] tried to eliminate 11024 small clauses 100%
c [cce-5-1] eliminated 71 binary clauses 2%
c [cce-5-1] eliminated 250 ternary clauses 3%
c [cce-5-1] eliminated 321 small clauses 3%
c [cce-5-1] eliminated 321 small clauses in 9064992 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 494 covered clauses in round 1
c [cce-5-2] eliminated 8 clauses out of 2123 (0%) of length 6
c [cce-5-2] eliminated 3 clauses out of 631 (0%) of length 5
c [cce-5-2] eliminated 91 clauses out of 5551 (2%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 102 large clauses in 10830359 steps
c [cce-5-2] allowing another 5415179 steps for small clauses
c [cce-5-2] scheduling 10703 clauses = 3150 binary + 7553 ternary
c [cce-5-2] tried to eliminate 10703 small clauses 100%
c [cce-5-2] eliminated 16 binary clauses 1%
c [cce-5-2] eliminated 20 ternary clauses 0%
c [cce-5-2] eliminated 36 small clauses 0%
c [cce-5-2] eliminated 36 small clauses in 8646227 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 138 covered clauses in round 2
c [cce-5-3] eliminated 3 clauses out of 2115 (0%) of length 6
c [cce-5-3] eliminated 2 clauses out of 628 (0%) of length 5
c [cce-5-3] eliminated 76 clauses out of 5460 (1%) of length 4
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] eliminated 81 large clauses in 10634058 steps
c [cce-5-3] allowing another 5317029 steps for small clauses
c [cce-5-3] scheduling 10667 clauses = 3134 binary + 7533 ternary
c [cce-5-3] tried to eliminate 10667 small clauses 100%
c [cce-5-3] eliminated 21 binary clauses 1%
c [cce-5-3] eliminated 10 ternary clauses 0%
c [cce-5-3] eliminated 31 small clauses 0%
c [cce-5-3] eliminated 31 small clauses in 8523488 steps
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 112 covered clauses in round 3
c [cce-5] eliminated 744 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6924 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 141 variables 2% in round 1 in 4059760 steps
c [elim-6-1] backward subsumption/strengthening limit 4059700
c [elim-6-1-1] backward checking 823 touched variables 12%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 2 and strengthened 21 clauses in 95905 steps
c [elim-6-1] rescheduled 64 variables 1% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 30339 steps
c [elim-6-2] backward subsumption/strengthening limit 30300
c [elim-6-2-1] backward checking 24 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 2 clauses in 15611 steps
c [elim-6-2] rescheduled 10 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 2767 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 144 = 2% variables out of 6924 scheduled
c [bca-5] limit of 10000000 steps and 57495 added (scaled 2)
c [bca-5] 4872 out of 13562 literals actually usable 36%
c [bca-5] added 2 blocked clauses in 21579 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1459 pos 63.1% + 855 neg 36.9% = 2314 sched 34.1% ret 4466
c [sweep-5-1] 3091315 steps 1340 queries 24.24 avg class size
c [sweep-5-1] 9266 decisions 1264 SAT calls 29.55 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-18] removed 212 variables
c [sweep-5-1] removed 212 vars (0 failed, 276 eqs, 225 impls)
c [sweep-5-2] 4037 pos 61.5% + 2531 neg 38.5% = 6568 sched 100.0% ret 0
c [sweep-5-2] 5398955 steps 1500 queries 26.24 avg class size
c [sweep-5-2] 13975 decisions 1402 SAT calls 34.70 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-19] removed 78 variables
c [sweep-5-2] removed 78 vars (0 failed, 176 eqs, 181 impls)
c [sweep-5-3] 3994 pos 61.5% + 2496 neg 38.5% = 6490 sched 100.0% ret 0
c [sweep-5-3] 1515628 steps 225 queries 100.28 avg class size
c [sweep-5-3] 4514 decisions 217 SAT calls 46.87 avg env size
c [sweep-5-3] 3178 variables remain 49% (3312 retained 51%)
c [decomp-20] removed 2 variables
c [sweep-5-3] removed 2 vars (0 failed, 10 eqs, 11 impls)
c [sweep-5] removed 292 vars in TOTAL (3 rounds, 3062 queries)
c [sort-queue-6] sorted 628 enqueued variables after 13668 conflicts
c [score-dist-6] active 5860 (90%), one 0 (0%), zero 628 (10%)
c [score-dist-6] max exp 527, different 22 (4%)
c [score-dist-6] median active exp 520, avg 520.0
c [simplification-6] removed 437 variables 6.3% (6488 remain 13%)
c [simplification-6] removed 1631 irredundant clauses 5.5% (27802 remain 20%)
c [simplification-6] maximum reduction of 6% = max (6%, 6%)
c [simplification-6] large reduction 6% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 25668 (soft 15668 + delta 10000)
c [simplification-6] new conflict limit 15668 (hard 25668)
c 
c [simplification-7] limit 15668 conflicts (hard 25668) hit after 15668 conflicts
c [quatres-5] found 9957 quaternary clauses 69% in total
c [quatres-5-1] removed 236 duplicate quaternary clauses
c [quatres-5-2] added 23 single-self-subsuming ternary resolvents
c [quatres-5-2] added 105 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6488 free variables schedulable
c [ternres-5] 1458 ternary resolvents (16 bin, 1442 trn)
c [ternres-5] fully completed ternary resolution
c [basicprobe-3] limit 5343122 penalty 0 = 0 + 0
c [basicprobe-3-0] 1325 sched 20%, 1 failed, 0 lifted, 561 hbrs
c [decomp-22] removed 1 variables
c [basicprobe-3-1] 1668 sched 26%, 1 failed, 0 lifted, 129 hbrs
c [decomp-23] removed 1 variables
c [basicprobe-3-2] 1642 sched 25%, 0 failed, 0 lifted, 21 hbrs
c [decomp-24] removed 1 variables
c [basicprobe-3-3] 1632 sched 25%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-4] 1627 sched 25%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-5] 496 probes remain 8% after last round
c [basicprobe-3-5] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-5] removed 3 variables, found 732 hbrs
c [bate-2] eliminated 8 asymmetric tautologies during probing
c [transred-5] limit 1068624 with penalty 0 = 0 + 0
c [transred-5] removed 1649 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 622 (0%) of length 7
c [cce-6-1] eliminated 7 clauses out of 2161 (0%) of length 6
c [cce-6-1] eliminated 64 clauses out of 775 (8%) of length 5
c [cce-6-1] eliminated 66 clauses out of 4906 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 138 large clauses in 2990864 steps
c [cce-6-1] allowing another 1495432 steps for small clauses
c [cce-6-1] scheduling 11390 clauses = 2772 binary + 8618 ternary
c [cce-6-1] tried to eliminate 11390 small clauses 100%
c [cce-6-1] eliminated 33 binary clauses 1%
c [cce-6-1] eliminated 169 ternary clauses 2%
c [cce-6-1] eliminated 202 small clauses 2%
c [cce-6-1] eliminated 202 small clauses in 4354893 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 340 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 1458610 steps for small clauses
c [cce-6-2] scheduling 11188 clauses = 2739 binary + 8449 ternary
c [cce-6-2] tried to eliminate 11188 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 340 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6485 variables 100%
c [elim-7] limit of 21372489 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 151 variables 2% in round 1 in 4040085 steps
c [elim-7-1] backward subsumption/strengthening limit 4040000
c [elim-7-1-1] backward checking 1238 touched variables 19%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 7 and strengthened 23 clauses in 132100 steps
c [elim-7-1] rescheduled 94 variables 1% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 43920 steps
c [elim-7-2] backward subsumption/strengthening limit 43900
c [elim-7-2-1] backward checking 16 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 15456 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 153 = 2% variables out of 6485 scheduled
c [bca-6] limit of 10000000 steps and 54966 added (scaled 2)
c [bca-6] 4460 out of 12666 literals actually usable 35%
c [bca-6] added 9 blocked clauses in 20868 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 1773 pos 57.7% + 1301 neg 42.3% = 3074 sched 48.5% ret 3258
c [sweep-6-1] 1001238 steps 252 queries 155.73 avg class size
c [sweep-6-1] 2994 decisions 244 SAT calls 33.20 avg env size
c [sweep-6-1] 2105 variables remain 33% (4227 retained 67%)
c [decomp-27] removed 5 variables
c [sweep-6-1] removed 5 vars (0 failed, 12 eqs, 14 impls)
c [sweep-6] 5 < 1/1000 * 6332 = 6 considered unsuccessful
c [sweep-6] removed 5 vars in TOTAL (1 rounds, 251 queries)
c [sort-queue-7] sorted 624 enqueued variables after 15668 conflicts
c [score-dist-7] active 5703 (90%), one 0 (0%), zero 624 (10%)
c [score-dist-7] max exp 528, different 23 (4%)
c [score-dist-7] median active exp 520, avg 520.4
c [simplification-7] removed 161 variables 2.5% (6327 remain 13%)
c [simplification-7] removed 590 irredundant clauses 2.1% (27212 remain 20%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 13332
c [simplification-7] penalized conflict interval 13332 = 1 * 13332
c [simplification-7] hard conflict limit 39000 (soft 29000 + delta 10000)
c [simplification-7] new conflict limit 29000 (hard 39000)
c 
c [simplification-8] limit 29000 conflicts (hard 39000) hit after 29001 conflicts
c [quatres-6] found 9398 quaternary clauses 67% in total
c [quatres-6-1] removed 7 duplicate quaternary clauses
c [quatres-6-2] added 17 single-self-subsuming ternary resolvents
c [quatres-6-2] added 343 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6327 free variables schedulable
c [ternres-6] 313 ternary resolvents (9 bin, 304 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1940 xors of average arity 3.0
c [gauss-3] connected 5761 occurrences of 995 variables (average 5.8)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] all 6327 free variables schedulable
c [simpleprobe-4] limit 9069290 penalty 0 = 0 + 0
c [decomp-29] removed 49 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 49 variables, found 758 hbrs, 3 units
c [unhide-5] limit 113366 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 402 tauts, 0 hbrs, 35527 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1419 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6278 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 2 blocked clauses
c [block-4] 2 < 1/100 * 27078 = 270 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 77 (1%) of length 10
c [cce-7-1] eliminated 1 clauses out of 270 (0%) of length 8
c [cce-7-1] eliminated 1 clauses out of 622 (0%) of length 7
c [cce-7-1] eliminated 3 clauses out of 2133 (0%) of length 6
c [cce-7-1] eliminated 37 clauses out of 774 (5%) of length 5
c [cce-7-1] eliminated 235 clauses out of 4877 (5%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 278 large clauses in 10077565 steps
c [cce-7-1] allowing another 5038782 steps for small clauses
c [cce-7-1] scheduling 9847 clauses = 2495 binary + 7352 ternary
c [cce-7-1] tried to eliminate 9847 small clauses 100%
c [cce-7-1] eliminated 64 binary clauses 3%
c [cce-7-1] eliminated 312 ternary clauses 4%
c [cce-7-1] eliminated 376 small clauses 4%
c [cce-7-1] eliminated 376 small clauses in 7923050 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 654 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 2130 (0%) of length 6
c [cce-7-2] eliminated 3 clauses out of 737 (0%) of length 5
c [cce-7-2] eliminated 50 clauses out of 4642 (1%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 54 large clauses in 9748182 steps
c [cce-7-2] allowing another 4874091 steps for small clauses
c [cce-7-2] scheduling 9471 clauses = 2431 binary + 7040 ternary
c [cce-7-2] tried to eliminate 9471 small clauses 100%
c [cce-7-2] eliminated 7 binary clauses 0%
c [cce-7-2] eliminated 19 ternary clauses 0%
c [cce-7-2] eliminated 26 small clauses 0%
c [cce-7-2] eliminated 26 small clauses in 7637158 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 80 covered clauses in round 2
c [cce-7-3] eliminated 3 clauses out of 2129 (0%) of length 6
c [cce-7-3] eliminated 2 clauses out of 734 (0%) of length 5
c [cce-7-3] eliminated 45 clauses out of 4592 (1%) of length 4
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 50 large clauses in 9623821 steps
c [cce-7-3] allowing another 4811910 steps for small clauses
c [cce-7-3] scheduling 9445 clauses = 2424 binary + 7021 ternary
c [cce-7-3] tried to eliminate 9445 small clauses 100%
c [cce-7-3] eliminated 10 binary clauses 0%
c [cce-7-3] eliminated 15 ternary clauses 0%
c [cce-7-3] eliminated 25 small clauses 0%
c [cce-7-3] eliminated 25 small clauses in 7561972 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 75 covered clauses in round 3
c [cce-7] eliminated 809 covered clauses in TOTAL during 3 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6278 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 906929020 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 152 variables 2% in round 1 in 3939700 steps
c [elim-8-1] backward subsumption/strengthening limit 3939700
c [elim-8-1-1] backward checking 969 touched variables 15%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 12 and strengthened 44 clauses in 118720 steps
c [elim-8-1] rescheduled 176 variables 3% by backward subsumption
c [elim-8-2] eliminated 10 variables 0% in round 2 in 97646 steps
c [elim-8-2] backward subsumption/strengthening limit 97600
c [elim-8-2-1] backward checking 71 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 1 and strengthened 8 clauses in 22284 steps
c [elim-8-2] rescheduled 24 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 7561 steps
c [elim-8-3] backward subsumption/strengthening limit 7500
c [elim-8-3-1] backward checking 9 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 1 clauses in 7501 steps
c [elim-8] incomplete 5 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 163 = 3% variables out of 6278 scheduled
c [bca-7] limit of 10000000 steps and 52598 added (scaled 2)
c [bca-7] 3970 out of 12232 literals actually usable 32%
c [bca-7] added 5 blocked clauses in 28360 steps
c [sort-queue-8] sorted 567 enqueued variables after 29001 conflicts
c [score-dist-8] active 5548 (91%), one 0 (0%), zero 567 (9%)
c [score-dist-8] max exp 530, different 25 (5%)
c [score-dist-8] median active exp 523, avg 522.4
c [simplification-8] removed 212 variables 3.4% (6115 remain 13%)
c [simplification-8] removed 1175 irredundant clauses 4.3% (26037 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 17332
c [simplification-8] penalized conflict interval 17332 = 1 * 17332
c [simplification-8] hard conflict limit 56333 (soft 46333 + delta 10000)
c [simplification-8] new conflict limit 46333 (hard 56333)
c 
c [simplification-9] limit 46333 conflicts (hard 56333) hit after 46333 conflicts
c [quatres-7] found 8863 quaternary clauses 65% in total
c [quatres-7-1] removed 24 duplicate quaternary clauses
c [quatres-7-2] added 13 single-self-subsuming ternary resolvents
c [quatres-7-2] added 286 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 6115 free variables schedulable
c [ternres-7] 274 ternary resolvents (11 bin, 263 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1014 transitive binary clauses
c [transred-7] found 2 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 79 (1%) of length 10
c [cce-8-1] eliminated 5 clauses out of 2144 (0%) of length 6
c [cce-8-1] eliminated 27 clauses out of 818 (3%) of length 5
c [cce-8-1] eliminated 95 clauses out of 4612 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 128 large clauses in 2703206 steps
c [cce-8-1] allowing another 1351603 steps for small clauses
c [cce-8-1] scheduling 10426 clauses = 2273 binary + 8153 ternary
c [cce-8-1] tried to eliminate 10426 small clauses 100%
c [cce-8-1] eliminated 5 binary clauses 0%
c [cce-8-1] eliminated 19 ternary clauses 0%
c [cce-8-1] eliminated 24 small clauses 0%
c [cce-8-1] eliminated 30 small clauses in 3881108 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 158 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1322995 steps for small clauses
c [cce-8-2] scheduling 10402 clauses = 2268 binary + 8134 ternary
c [cce-8-2] tried to eliminate 10402 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 158 covered clauses in TOTAL during 2 rounds
c [cce-8] 158 < 1/100 * 26035 = 260 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 6113 variables 100%
c [elim-9] limit of 74760240 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 26 variables 0% in round 1 in 3892040 steps
c [elim-9-1] backward subsumption/strengthening limit 3892000
c [elim-9-1-1] backward checking 199 touched variables 3%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 9 clauses in 38474 steps
c [elim-9-1] rescheduled 21 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 8950 steps
c [elim-9-2] backward subsumption/strengthening limit 8900
c [elim-9-2-1] backward checking 8 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 8901 steps
c [elim-9-2] fully rescheduled 6086 variables 100%
c [elim-9-3] eliminated 2 variables 0% in round 3 in 3884572 steps
c [elim-9-3] backward subsumption/strengthening limit 3884500
c [elim-9-3-1] backward checking 18 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 11178 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 29 = 0% variables out of 6113 scheduled
c [elim-9] 29 < 1/100 * 6113 = 61 considered unsuccessful
c [bca-8] limit of 10000000 steps and 52199 added (scaled 2)
c [bca-8] 3562 out of 12170 literals actually usable 29%
c [bca-8] added 1 blocked clauses in 39563 steps
c [sweep-7] limit 560701 penalty 1 = 1 + 0
c [sweep-7-1] 1206 pos 61.9% + 743 neg 38.1% = 1949 sched 32.0% ret 4135
c [sweep-7-1] 566479 steps 97 queries 138.72 avg class size
c [sweep-7-1] 1719 decisions 95 SAT calls 49.76 avg env size
c [sweep-7-1] 1616 variables remain 27% (4468 retained 73%)
c [decomp-31] removed 1 variables
c [sweep-7-1] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-7] 1 < 1/1000 * 6084 = 6 considered unsuccessful
c [sweep-7] removed 1 vars in TOTAL (1 rounds, 96 queries)
c [sort-queue-9] sorted 545 enqueued variables after 46333 conflicts
c [score-dist-9] active 5538 (91%), one 0 (0%), zero 545 (9%)
c [score-dist-9] max exp 531, different 26 (5%)
c [score-dist-9] median active exp 525, avg 524.0
c [simplification-9] removed 32 variables 0.5% (6083 remain 13%)
c [simplification-9] removed 203 irredundant clauses 0.8% (25834 remain 19%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 27332
c [simplification-9] penalized conflict interval 27332 = 1 * 27332
c [simplification-9] hard conflict limit 87331 (soft 73665 + delta 13666)
c [simplification-9] new conflict limit 73665 (hard 87331)
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 -   35.9    6083    25834     70866   29509  15539 14769   60    63   16  95%    671   19   59   30  196%
c 
c [simplification-10] limit 73665 conflicts (hard 87331) hit after 73665 conflicts
c [quatres-8] found 8947 quaternary clauses 65% in total
c [quatres-8-2] added 11 single-self-subsuming ternary resolvents
c [quatres-8-2] added 64 quaternary resolvents
c [ternres-8] limit 7224402 with penalty 0 = 0 + 0
c [ternres-8] all 6083 free variables schedulable
c [ternres-8] 80 ternary resolvents (8 bin, 72 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 451525 penalty 3 = 3 + 0
c [card-4] found 188 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 451525 for elimination
c [card-4] 188 out of 188 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-4] limit 361220 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 12165 literals 100%
c [treelook-4] scheduling used 342108 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 361220 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 363841 steps
c [treelook-4] 11448 literals remain 94%
c [treelook-4] 6046 variables remain to probed next time 99%
c [decomp-33] removed 5 variables
c [treelook-4] removed 5 variables, found 241 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 931 transitive binary clauses
c [bca-9] limit of 10000000 steps and 52175 added (scaled 2)
c [bca-9] 3769 out of 12158 literals actually usable 31%
c [bca-9] added 1 blocked clauses in 40912 steps
c [sort-queue-10] sorted 545 enqueued variables after 73665 conflicts
c [score-dist-10] active 5533 (91%), one 0 (0%), zero 545 (9%)
c [score-dist-10] max exp 533, different 28 (5%)
c [score-dist-10] median active exp 526, avg 524.9
c [simplification-10] removed 5 variables 0.1% (6078 remain 13%)
c [simplification-10] removed 10 irredundant clauses 0.0% (25824 remain 19%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 27332
c [simplification-10] new conflict interval 54664
c [simplification-10] penalized conflict interval 54664 = 1 * 54664
c [simplification-10] hard conflict limit 155661 (soft 128329 + delta 27332)
c [simplification-10] new conflict limit 128329 (hard 155661)
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 -   45.5    6078    25824     98389   30909  15613 14080   55    57   17  96%    792    8   55   39  139%
c 
c [simplification-11] limit 128329 conflicts (hard 155661) hit after 128331 conflicts
c [quatres-9] found 9005 quaternary clauses 65% in total
c [quatres-9-1] removed 8 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 16 quaternary resolvents
c [ternres-9] limit 14712480 with penalty 0 = 0 + 0
c [ternres-9] all 6078 free variables schedulable
c [ternres-9] 54 ternary resolvents (9 bin, 45 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-4] limit 73562404 penalty 0 = 0 + 0
c [basicprobe-4-0] 542 sched 9%, 0 failed, 0 lifted, 112 hbrs
c [basicprobe-4-1] 1419 sched 23%, 0 failed, 0 lifted, 123 hbrs
c [basicprobe-4-2] 1385 sched 23%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-3] 1379 sched 23%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-4] 1377 sched 23%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-5] 1375 sched 23%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-4-6] 1373 sched 23%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-7] 1371 sched 23%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-8] 1370 sched 23%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] removed 0 variables, found 281 hbrs
c [bate-3] eliminated 3 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 802 transitive binary clauses
c [cce-9] limit of 36781202 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 6 clauses out of 2151 (0%) of length 6
c [cce-9-1] eliminated 21 clauses out of 809 (3%) of length 5
c [cce-9-1] eliminated 76 clauses out of 4508 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 103 large clauses in 9684307 steps
c [cce-9-1] allowing another 4842153 steps for small clauses
c [cce-9-1] scheduling 10343 clauses = 2258 binary + 8085 ternary
c [cce-9-1] tried to eliminate 10343 small clauses 100%
c [cce-9-1] eliminated 25 binary clauses 1%
c [cce-9-1] eliminated 436 ternary clauses 5%
c [cce-9-1] eliminated 461 small clauses 4%
c [cce-9-1] eliminated 461 small clauses in 9341169 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 564 covered clauses in round 1
c [cce-9-2] eliminated 2 clauses out of 2145 (0%) of length 6
c [cce-9-2] eliminated 4 clauses out of 788 (1%) of length 5
c [cce-9-2] eliminated 51 clauses out of 4432 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 57 large clauses in 9897797 steps
c [cce-9-2] allowing another 4948898 steps for small clauses
c [cce-9-2] scheduling 9882 clauses = 2233 binary + 7649 ternary
c [cce-9-2] tried to eliminate 9882 small clauses 100%
c [cce-9-2] eliminated 10 binary clauses 0%
c [cce-9-2] eliminated 26 ternary clauses 0%
c [cce-9-2] eliminated 36 small clauses 0%
c [cce-9-2] eliminated 36 small clauses in 9261847 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 93 covered clauses in round 2
c [cce-9-3] eliminated 3 clauses out of 2143 (0%) of length 6
c [cce-9-3] eliminated 5 clauses out of 784 (1%) of length 5
c [cce-9-3] eliminated 41 clauses out of 4381 (1%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 49 large clauses in 9791858 steps
c [cce-9-3] allowing another 4895929 steps for small clauses
c [cce-9-3] scheduling 9846 clauses = 2223 binary + 7623 ternary
c [cce-9-3] tried to eliminate 9846 small clauses 100%
c [cce-9-3] eliminated 5 binary clauses 0%
c [cce-9-3] eliminated 12 ternary clauses 0%
c [cce-9-3] eliminated 17 small clauses 0%
c [cce-9-3] eliminated 17 small clauses in 9173816 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 66 covered clauses in round 3
c [cce-9] eliminated 723 covered clauses in TOTAL during 3 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 6078 variables 100%
c [elim-10] limit of 147124809 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 110 variables 2% in round 1 in 3830595 steps
c [elim-10-1] backward subsumption/strengthening limit 3830500
c [elim-10-1-1] backward checking 750 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 16 clauses in 82116 steps
c [elim-10-1] rescheduled 60 variables 1% by backward subsumption
c [elim-10-2] eliminated 6 variables 0% in round 2 in 21306 steps
c [elim-10-2] backward subsumption/strengthening limit 21300
c [elim-10-2-1] backward checking 44 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 8 clauses in 17933 steps
c [elim-10-2] rescheduled 26 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 12334 steps
c [elim-10-3] backward subsumption/strengthening limit 12300
c [elim-10-3-1] backward checking 21 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 1 clauses in 12301 steps
c [elim-10] incomplete 4 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 119 = 2% variables out of 6078 scheduled
c [bca-10] limit of 10000000 steps and 50412 added (scaled 2)
c [bca-10] 3744 out of 11920 literals actually usable 31%
c [bca-10] added 1 blocked clauses in 58204 steps
c [sort-queue-11] sorted 544 enqueued variables after 128331 conflicts
c [score-dist-11] active 5415 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-11] max exp 534, different 29 (5%)
c [score-dist-11] median active exp 527, avg 525.8
c [simplification-11] removed 119 variables 2.0% (5959 remain 12%)
c [simplification-11] removed 882 irredundant clauses 3.4% (24942 remain 18%)
c [simplification-11] maximum reduction of 3% = max (2%, 3%)
c [simplification-11] geometric conflict interval increment 13666 = 54664 / 4
c [simplification-11] new conflict interval 68330
c [simplification-11] penalized conflict interval 68330 = 1 * 68330
c [simplification-11] hard conflict limit 230826 (soft 196661 + delta 34165)
c [simplification-11] new conflict limit 196661 (hard 230826)
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 -   65.8    5959    24942    139988   30809  15575 12123   55    57   16  96%    901    3   54   46  118%
c -   81.5    5959    24942    183520   26225  15576 12124   46    57   20  81%    961    2   39   48   82%
c 
c [simplification-12] limit 196661 conflicts (hard 230826) hit after 196856 conflicts
c [quatres-10] found 8529 quaternary clauses 63% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 3 single-self-subsuming ternary resolvents
c [quatres-10-2] added 147 quaternary resolvents
c [ternres-10] limit 24265349 with penalty 0 = 0 + 0
c [ternres-10] all 5959 free variables schedulable
c [ternres-10] 183 ternary resolvents (18 bin, 165 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 606633 penalty 3 = 3 + 0
c [gauss-4] extracted 2742 xors of average arity 3.0
c [gauss-4] connected 8226 occurrences of 901 variables (average 9.1)
c [gauss-4] limit 606633 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 5959 free variables schedulable
c [simpleprobe-5] limit 97061397 penalty 0 = 0 + 0
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 0 variables, found 476 hbrs, 0 units
c [unhide-6] limit 606633 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 3314 tauts, 0 hbrs, 144442 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 477 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5959 variables 100%
c [block-5] limit of 30331686 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 13 blocked clauses
c [block-5] 13 < 1/100 * 24934 = 249 considered unsuccessful
c [cce-10] limit of 121326746 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 613 (0%) of length 7
c [cce-10-1] eliminated 3 clauses out of 2071 (0%) of length 6
c [cce-10-1] eliminated 13 clauses out of 837 (2%) of length 5
c [cce-10-1] eliminated 59 clauses out of 4323 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 76 large clauses in 2375128 steps
c [cce-10-1] allowing another 1187564 steps for small clauses
c [cce-10-1] scheduling 9752 clauses = 2216 binary + 7536 ternary
c [cce-10-1] tried to eliminate 9752 small clauses 100%
c [cce-10-1] eliminated 10 binary clauses 0%
c [cce-10-1] eliminated 29 ternary clauses 0%
c [cce-10-1] eliminated 39 small clauses 0%
c [cce-10-1] eliminated 39 small clauses in 3386128 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 115 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1175314 steps for small clauses
c [cce-10-2] scheduling 9713 clauses = 2206 binary + 7507 ternary
c [cce-10-2] tried to eliminate 9713 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 115 covered clauses in TOTAL during 2 rounds
c [cce-10] 115 < 1/100 * 24921 = 249 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 5957 variables 100%
c [elim-11] limit of 485306987 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 83 variables 1% in round 1 in 3809987 steps
c [elim-11-1] backward subsumption/strengthening limit 3809900
c [elim-11-1-1] backward checking 581 touched variables 10%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 20 clauses in 68852 steps
c [elim-11-1] rescheduled 73 variables 1% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 27265 steps
c [elim-11-2] backward subsumption/strengthening limit 27200
c [elim-11-2-1] backward checking 14 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 12257 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 85 = 1% variables out of 5957 scheduled
c [bca-11] limit of 10000000 steps and 49920 added (scaled 2)
c [bca-11] 3901 out of 11746 literals actually usable 33%
c [bca-11] added 6 blocked clauses in 44164 steps
c [sweep-8] limit 1819901 penalty 2 = 2 + 0
c [sweep-8-1] 895 pos 59.6% + 607 neg 40.4% = 1502 sched 25.6% ret 4370
c [sweep-8-1] 1821262 steps 776 queries 20.57 avg class size
c [sweep-8-1] 6850 decisions 762 SAT calls 24.72 avg env size
c [sweep-8-1] 25 variables remain 0% (5847 retained 100%)
c [decomp-45] removed 11 variables
c [sweep-8-1] removed 11 vars (0 failed, 20 eqs, 50 impls)
c [sweep-8] removed 11 vars in TOTAL (1 rounds, 775 queries)
c [sort-queue-12] sorted 544 enqueued variables after 196856 conflicts
c [score-dist-12] active 5317 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-12] max exp 536, different 31 (6%)
c [score-dist-12] median active exp 527, avg 526.6
c [simplification-12] removed 98 variables 1.6% (5861 remain 12%)
c [simplification-12] removed 269 irredundant clauses 1.1% (24673 remain 18%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 22776 = 68330 / 3
c [simplification-12] new conflict interval 91106
c [simplification-12] penalized conflict interval 91106 = 1 * 91106
c [simplification-12] hard conflict limit 333515 (soft 287962 + delta 45553)
c [simplification-12] new conflict limit 287962 (hard 333515)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   96.5    5861    24673    221652   30743  15116  8937   39    47   16  82%    989   -9   37   44   85%
c -  111.3    5861    24673    255319   30801  15118  8937   39    40   20  98%   1003   -9   39   42   93%
c -  128.1    5861    24673    293594   32102  15118  8937   37    37   20  99%   1012   -7   37   40   93%
c -  144.7    5861    24673    332724   29109  15118  8937   36    39   20  93%   1018   -3   36   39   92%
c 
c [simplification-13] limit 287962 conflicts (hard 333515) hit after 333516 conflicts
c [quatres-11] found 8327 quaternary clauses 63% in total
c [quatres-11-1] removed 13 duplicate quaternary clauses
c [quatres-11-2] added 19 single-self-subsuming ternary resolvents
c [quatres-11-2] added 177 quaternary resolvents
c [ternres-11] limit 48758630 with penalty 0 = 0 + 0
c [ternres-11] all 5861 free variables schedulable
c [ternres-11] 352 ternary resolvents (33 bin, 319 trn)
c [ternres-11] fully completed ternary resolution
c [treelook-5] limit 4875863 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11697 literals 100%
c [treelook-5] scheduling used 312110 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4875863 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1859282 steps
c [treelook-5] fully completed tree based probing
c [decomp-47] removed 18 variables
c [treelook-5] removed 19 variables, found 803 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 989 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5842 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 16 variables 0% in round 1 in 3792260 steps
c [elim-12-1] backward subsumption/strengthening limit 3792200
c [elim-12-1-1] backward checking 140 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 2 clauses in 21364 steps
c [elim-12-1] rescheduled 12 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 5054 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 16 = 0% variables out of 5842 scheduled
c [elim-12] 16 < 1/100 * 5842 = 58 considered unsuccessful
c [bca-12] limit of 10000000 steps and 49715 added (scaled 2)
c [bca-12] 4537 out of 11654 literals actually usable 39%
c [bca-12] added 2 blocked clauses in 39913 steps
c [sort-queue-13] sorted 544 enqueued variables after 333516 conflicts
c [score-dist-13] active 5282 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-13] max exp 537, different 32 (6%)
c [score-dist-13] median active exp 528, avg 527.8
c [simplification-13] removed 35 variables 0.6% (5826 remain 12%)
c [simplification-13] removed 81 irredundant clauses 0.3% (24592 remain 18%)
c [simplification-13] maximum reduction of 1% = max (1%, 0%)
c [simplification-13] geometric conflict interval increment 45553 = 91106 / 2
c [simplification-13] new conflict interval 136659
c [simplification-13] penalized conflict interval 136659 = 1 * 136659
c [simplification-13] hard conflict limit 538504 (soft 470175 + delta 68329)
c [simplification-13] new conflict limit 470175 (hard 538504)
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 -  159.1    5826    24592    382961   30987  15330  8598   16    76   18  21%   1021   18   16   29   56%
c -  173.1    5826    24592    423902   29306  15334  8601   38    43   18  88%   1022  -14   38   31  124%
c -  184.0    5826    24592    460904   33160  15335  8601   38    40   28  95%   1023  -10   38   34  113%
c -  193.8    5826    24592    494896   31707  15338  8602   37    40   28  94%   1023   -7   36   35  102%
c -  202.6    5826    24592    530977   30932  15339  8602   35    38   29  93%   1024   -5   34   35   97%
c 
c [simplification-14] limit 470175 conflicts (hard 538504) hit after 538505 conflicts
c [quatres-12] found 8416 quaternary clauses 63% in total
c [quatres-12-1] removed 9 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [quatres-12-2] added 60 quaternary resolvents
c [ternres-12] limit 73160177 with penalty 0 = 0 + 0
c [ternres-12] all 5826 free variables schedulable
c [ternres-12] 98 ternary resolvents (18 bin, 80 trn)
c [ternres-12] fully completed ternary resolution
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 536 transitive binary clauses
c [cce-11] limit of 182900443 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 6 clauses out of 2112 (0%) of length 6
c [cce-11-1] eliminated 24 clauses out of 872 (3%) of length 5
c [cce-11-1] eliminated 112 clauses out of 4296 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 142 large clauses in 10131905 steps
c [cce-11-1] allowing another 5065952 steps for small clauses
c [cce-11-1] scheduling 9487 clauses = 2123 binary + 7364 ternary
c [cce-11-1] tried to eliminate 9487 small clauses 100%
c [cce-11-1] eliminated 38 binary clauses 2%
c [cce-11-1] eliminated 86 ternary clauses 1%
c [cce-11-1] eliminated 124 small clauses 1%
c [cce-11-1] eliminated 124 small clauses in 9246023 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 266 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 2106 (0%) of length 6
c [cce-11-2] eliminated 2 clauses out of 848 (0%) of length 5
c [cce-11-2] eliminated 12 clauses out of 4184 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 15 large clauses in 9706753 steps
c [cce-11-2] allowing another 4853376 steps for small clauses
c [cce-11-2] scheduling 9363 clauses = 2085 binary + 7278 ternary
c [cce-11-2] tried to eliminate 9363 small clauses 100%
c [cce-11-2] eliminated 2 binary clauses 0%
c [cce-11-2] eliminated 9 ternary clauses 0%
c [cce-11-2] eliminated 11 small clauses 0%
c [cce-11-2] eliminated 11 small clauses in 8964885 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 26 covered clauses in round 2
c [cce-11-3] eliminated 1 clauses out of 2105 (0%) of length 6
c [cce-11-3] eliminated 2 clauses out of 846 (0%) of length 5
c [cce-11-3] eliminated 8 clauses out of 4172 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 11 large clauses in 9596161 steps
c [cce-11-3] allowing another 4798080 steps for small clauses
c [cce-11-3] scheduling 9352 clauses = 2083 binary + 7269 ternary
c [cce-11-3] tried to eliminate 9352 small clauses 100%
c [cce-11-3] eliminated 2 binary clauses 0%
c [cce-11-3] eliminated 2 ternary clauses 0%
c [cce-11-3] eliminated 4 small clauses 0%
c [cce-11-3] eliminated 4 small clauses in 8905272 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 15 covered clauses in round 3
c [cce-11] eliminated 307 covered clauses in TOTAL during 3 rounds
c [bca-13] limit of 10000000 steps and 49102 added (scaled 2)
c [bca-13] 4751 out of 11654 literals actually usable 41%
c [bca-13] added 1 blocked clauses in 49152 steps
c [sweep-9] limit 10974026 penalty 1 = 1 + 0
c [sweep-9-1] 21 pos 100.0% + 0 neg 0.0% = 21 sched 0.4% ret 5805
c [sweep-9-1] 56407 steps 15 queries 4.67 avg class size
c [sweep-9-1] 216 decisions 14 SAT calls 34.57 avg env size
c [sweep-9-1] fully completed sweeping round
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9-2] 3259 pos 55.9% + 2567 neg 44.1% = 5826 sched 100.0% ret 0
c [sweep-9-2] 5203978 steps 1039 queries 29.73 avg class size
c [sweep-9-2] 12779 decisions 1041 SAT calls 29.41 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-50] removed 2 variables
c [sweep-9-2] removed 2 vars (0 failed, 4 eqs, 15 impls)
c [sweep-9-3] 3257 pos 55.9% + 2567 neg 44.1% = 5824 sched 100.0% ret 0
c [sweep-9-3] 5369124 steps 1049 queries 26.63 avg class size
c [sweep-9-3] 12586 decisions 1052 SAT calls 31.63 avg env size
c [sweep-9-3] fully completed sweeping round
c [decomp-51] removed 2 variables
c [sweep-9-3] removed 2 vars (0 failed, 6 eqs, 16 impls)
c [sweep-9] 4 < 1/1000 * 5826 = 5 considered unsuccessful
c [sweep-9] removed 4 vars in TOTAL (3 rounds, 2100 queries)
c [sort-queue-14] sorted 544 enqueued variables after 538505 conflicts
c [score-dist-14] active 5278 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-14] max exp 538, different 33 (6%)
c [score-dist-14] median active exp 531, avg 529.2
c [simplification-14] removed 4 variables 0.1% (5822 remain 12%)
c [simplification-14] removed 317 irredundant clauses 1.3% (24275 remain 18%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 68329 = 136659 / 2
c [simplification-14] new conflict interval 204988
c [simplification-14] penalized conflict interval 204988 = 1 * 204988
c [simplification-14] hard conflict limit 845987 (soft 743493 + delta 102494)
c [simplification-14] new conflict limit 743493 (hard 845987)
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 -  216.0    5822    24275    569892   34347  15611  8264   35    37   22  95%   1024   -5   33   36   94%
c -  225.3    5822    24275    605929   34508  15611  8264   35    36   22  98%   1024   -4   35   36   99%
c -  238.1    5822    24275    643786   34314  15612  8264   35    35   23  99%   1024   -3   34   35   95%
c -  255.6    5822    24275    714246   34978  15614  8264   13    73   23  17%   1024   21   12   25   49%
c 
c [simplification-15] limit 743493 conflicts (hard 845987) hit after 743493 conflicts
c [quatres-13] found 8392 quaternary clauses 62% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-2] added 7 single-self-subsuming ternary resolvents
c [quatres-13-2] added 40 quaternary resolvents
c [ternres-13] limit 96176741 with penalty 0 = 0 + 0
c [ternres-13] all 5822 free variables schedulable
c [ternres-13] 133 ternary resolvents (25 bin, 108 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 3005523 penalty 4 = 4 + 0
c [card-5] found 193 at-most-one constraints of average size 3.0
c [card-5] found 87 at-most-two constraints of average size 4.0
c [card-5] using previous limit 3005523 for elimination
c [card-5] 280 out of 280 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 152 at-most-one constraints, 72 used 47%
c [card-5] exported 72 binary clauses, 1.0 per/constraint
c [basicprobe-5] limit 200000000 penalty 1 = 1 + 0
c [basicprobe-5-0] 1102 sched 19%, 2 failed, 0 lifted, 22 hbrs
c [decomp-53] removed 2 variables
c [basicprobe-5-1] 1088 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-1] fully completed probing
c [basicprobe-5-1] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-5-1] removed 2 variables, found 22 hbrs
c [bate-4] eliminated 2 asymmetric tautologies during probing
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 645 transitive binary clauses
c [cce-12] limit of 480883709 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 3 clauses out of 844 (0%) of length 5
c [cce-12-1] eliminated 2 clauses out of 4158 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 5 large clauses in 2321225 steps
c [cce-12-1] allowing another 1160612 steps for small clauses
c [cce-12-1] scheduling 8761 clauses = 2090 binary + 6671 ternary
c [cce-12-1] tried to eliminate 8761 small clauses 100%
c [cce-12-1] eliminated 6 binary clauses 0%
c [cce-12-1] eliminated 49 ternary clauses 1%
c [cce-12-1] eliminated 55 small clauses 1%
c [cce-12-1] eliminated 55 small clauses in 2917562 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 60 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1145999 steps for small clauses
c [cce-12-2] scheduling 8706 clauses = 2084 binary + 6622 ternary
c [cce-12-2] tried to eliminate 8706 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 60 covered clauses in TOTAL during 2 rounds
c [cce-12] 60 < 1/100 * 24260 = 242 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5820 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 65 variables 1% in round 1 in 3764491 steps
c [elim-13-1] backward subsumption/strengthening limit 3764400
c [elim-13-1-1] backward checking 458 touched variables 8%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 11 clauses in 55455 steps
c [elim-13-1] rescheduled 58 variables 1% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 22691 steps
c [elim-13-2] backward subsumption/strengthening limit 22600
c [elim-13-2-1] backward checking 17 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 2 clauses in 14887 steps
c [elim-13-2] rescheduled 6 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 7376 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 67 = 1% variables out of 5820 scheduled
c [bca-14] limit of 10000000 steps and 48785 added (scaled 2)
c [bca-14] 4693 out of 11508 literals actually usable 41%
c [bca-14] added 3 blocked clauses in 49185 steps
c [sort-queue-15] sorted 544 enqueued variables after 743493 conflicts
c [score-dist-15] active 5209 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-15] max exp 539, different 34 (6%)
c [score-dist-15] median active exp 532, avg 529.7
c [simplification-15] removed 69 variables 1.2% (5753 remain 12%)
c [simplification-15] removed 149 irredundant clauses 0.6% (24126 remain 18%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 102494 = 204988 / 2
c [simplification-15] new conflict interval 307482
c [simplification-15] penalized conflict interval 307482 = 1 * 307482
c [simplification-15] hard conflict limit 1204716 (soft 1050975 + delta 153741)
c [simplification-15] new conflict limit 1050975 (hard 1204716)
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 -  283.8    5753    24126    828373   35317  15499  7284   39    45   20  86%   1024  -12   38   23  167%
c -  297.9    5753    24126    867636   36826  15500  7284   36    39   21  92%   1024  -11   36   29  123%
c -  314.0    5753    24126    907569   37355  15501  7285   30    33   21  90%   1024  -11   29   31   93%
c -  325.9    5753    24126    946492   33963  15506  7288   34    36   30  94%   1024   -5   36   32  113%
c -  340.2    5753    24126    989923   34283  15507  7288   35    37   31  95%   1024   -2   35   33  106%
c -  354.3    5753    24126   1035971   37609  15509  7288   34    34   32  99%   1024   -2   35   33  107%
c -  367.0    5753    24126   1077607   39202  15511  7288   30    35   32  87%   1024   -1   27   33   83%
c -  379.4    5753    24126   1122187   37687  15511  7288   32    33   31  98%   1024   -2   33   32  103%
c -  392.6    5753    24126   1169377   39574  15518  7290   23    29   31  79%   1024   -3   21   30   71%
c 
c [simplification-16] limit 1050975 conflicts (hard 1204716) hit after 1175188 conflicts
c [quatres-14] found 8291 quaternary clauses 62% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 12 single-self-subsuming ternary resolvents
c [quatres-14-2] added 104 quaternary resolvents
c [ternres-14] limit 157683682 with penalty 0 = 0 + 0
c [ternres-14] all 5753 free variables schedulable
c [ternres-14] 144 ternary resolvents (26 bin, 118 trn)
c [ternres-14] fully completed ternary resolution
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 369 transitive binary clauses
c [transred-14] found 1 units
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5752 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 5 variables 0% in round 1 in 3751616 steps
c [elim-14-1] backward subsumption/strengthening limit 3751600
c [elim-14-1-1] backward checking 45 touched variables 1%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 1 clauses in 17809 steps
c [elim-14-1] rescheduled 5 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 6573 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 5 = 0% variables out of 5752 scheduled
c [elim-14] 5 < 1/100 * 5752 = 57 considered unsuccessful
c [bca-15] limit of 10000000 steps and 48766 added (scaled 2)
c [bca-15] 4637 out of 11496 literals actually usable 40%
c [bca-15] added 1 blocked clauses in 54661 steps
c [sort-queue-16] sorted 544 enqueued variables after 1175188 conflicts
c [score-dist-16] active 5203 (91%), one 0 (0%), zero 544 (9%)
c [score-dist-16] max exp 541, different 36 (7%)
c [score-dist-16] median active exp 533, avg 530.8
c [simplification-16] removed 6 variables 0.1% (5747 remain 12%)
c [simplification-16] removed 10 irredundant clauses 0.0% (24116 remain 18%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 307482
c [simplification-16] new conflict interval 614964
c [simplification-16] penalized conflict interval 614964 = 1 * 614964
c [simplification-16] hard conflict limit 2097634 (soft 1790152 + delta 307482)
c [simplification-16] new conflict limit 1790152 (hard 2097634)
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 -  403.6    5747    24116   1217482   41156  15653  6931   21    28   21  73%   1024   -4   20   25   79%
c -  412.5    5747    24116   1261789   41442  15661  6934   22    29   21  77%   1024   -2   24   22  108%
c -  424.9    5747    24116   1307745   39846  15676  6939   20    26   29  76%   1024   -4   18   22   81%
c -  438.5    5747    24116   1358508   39240  15695  6945   18    27   29  66%   1024   -2   18   21   86%
c -  453.4    5747    24116   1411201   43880  15703  6945   20    27   30  74%   1024   -1   19   21   91%
c -  463.7    5747    24116   1462079   43946  15724  6948   41    93   31  44%   1024   56   49   21  233%
c -  475.3    5747    24116   1510728   43052  15726  6948   51    73   34  70%   1024   12   52   36  146%
c -  487.4    5747    24116   1560237   45100  15729  6949   42    63   51  68%   1024   -3   44   41  107%
c -  499.5    5747    24116   1608887   42849  15733  6950   36    53   50  68%   1024   -8   34   39   87%
c -  513.8    5747    24116   1660563   45428  15734  6951   34    41   50  83%   1024  -11   33   37   90%
c -  528.5    5747    24116   1709894   46194  15743  6953   37    50   51  73%   1024   -0   38   36  107%
c -  546.0    5747    24116   1759900   47070  15743  6953   35    43   51  83%   1024   -3   37   36  105%
c -  562.5    5747    24116   1809095   44022  15744  6953   35    39   50  88%   1024   -4   34   36   97%
c -  581.0    5747    24116   1862470   44571  15746  6954   36    38   51  93%   1024   -2   36   36  101%
c 
c [simplification-17] limit 1790152 conflicts (hard 2097634) hit after 1879158 conflicts
c [quatres-15] found 8557 quaternary clauses 58% in total
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 13 single-self-subsuming ternary resolvents
c [quatres-15-2] added 103 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 5747 free variables schedulable
c [ternres-15] 113 ternary resolvents (24 bin, 89 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 3095431 penalty 4 = 4 + 0
c [gauss-5] extracted 5916 xors of average arity 3.0
c [gauss-5] connected 17736 occurrences of 953 variables (average 18.6)
c [gauss-5] limit 3095431 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-55] removed 1 variables
c [simpleprobe-6] all 5746 free variables schedulable
c [simpleprobe-6] limit 100000000 penalty 1 = 1 + 0
c [decomp-56] removed 4 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 4 variables, found 735 hbrs, 0 units
c [unhide-7] limit 1250000 with penalty 4 = 4 + 0
c [unhide-7-8] 0 units, 0 failed, 1906 tauts, 0 hbrs, 445583 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 356 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5742 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 17 blocked clauses
c [block-6] 17 < 1/100 * 24093 = 240 considered unsuccessful
c [cce-13] boosting limit by 10
c [cce-13] limit of 6190862695 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 2 clauses out of 2027 (0%) of length 6
c [cce-13-1] eliminated 11 clauses out of 883 (1%) of length 5
c [cce-13-1] eliminated 91 clauses out of 4189 (2%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 104 large clauses in 9485809 steps
c [cce-13-1] allowing another 4742904 steps for small clauses
c [cce-13-1] scheduling 9274 clauses = 2076 binary + 7198 ternary
c [cce-13-1] tried to eliminate 9274 small clauses 100%
c [cce-13-1] eliminated 32 binary clauses 2%
c [cce-13-1] eliminated 94 ternary clauses 1%
c [cce-13-1] eliminated 126 small clauses 1%
c [cce-13-1] eliminated 126 small clauses in 8738841 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 230 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 2025 (0%) of length 6
c [cce-13-2] eliminated 4 clauses out of 4098 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 5 large clauses in 9056364 steps
c [cce-13-2] allowing another 4528182 steps for small clauses
c [cce-13-2] scheduling 9148 clauses = 2044 binary + 7104 ternary
c [cce-13-2] tried to eliminate 9148 small clauses 100%
c [cce-13-2] eliminated 2 binary clauses 0%
c [cce-13-2] eliminated 6 ternary clauses 0%
c [cce-13-2] eliminated 8 small clauses 0%
c [cce-13-2] eliminated 8 small clauses in 8463164 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 13 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 872 (0%) of length 5
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 1 large clauses in 8978929 steps
c [cce-13-3] allowing another 4489464 steps for small clauses
c [cce-13-3] scheduling 9140 clauses = 2042 binary + 7098 ternary
c [cce-13-3] tried to eliminate 9140 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 1 covered clauses in round 3
c [cce-13] eliminated 244 covered clauses in TOTAL during 3 rounds
c [bca-16] limit of 10000000 steps and 48199 added (scaled 2)
c [bca-16] 3892 out of 11480 literals actually usable 34%
c [bca-16] added 2 blocked clauses in 69862 steps
c [sweep-10] limit 18572588 penalty 2 = 2 + 0
c [sweep-10-1] 3605 pos 62.8% + 2134 neg 37.2% = 5739 sched 100.0% ret 0
c [sweep-10-1] 5995198 steps 848 queries 31.40 avg class size
c [sweep-10-1] 13484 decisions 850 SAT calls 35.70 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-57] removed 1 variables
c [sweep-10-1] removed 1 vars (0 failed, 2 eqs, 11 impls)
c [sweep-10-2] 3604 pos 62.8% + 2134 neg 37.2% = 5738 sched 100.0% ret 0
c [sweep-10-2] 5619611 steps 838 queries 26.63 avg class size
c [sweep-10-2] 12912 decisions 838 SAT calls 34.63 avg env size
c [sweep-10-2] fully completed sweeping round
c [sweep-10-2] removed 0 vars (0 failed, 1 eqs, 9 impls)
c [sweep-10-3] 3604 pos 62.8% + 2134 neg 37.2% = 5738 sched 100.0% ret 0
c [sweep-10-3] 5334057 steps 878 queries 20.22 avg class size
c [sweep-10-3] 12491 decisions 877 SAT calls 30.98 avg env size
c [sweep-10-3] fully completed sweeping round
c [sweep-10-3] removed 0 vars (0 failed, 1 eqs, 6 impls)
c [sweep-10] 1 < 1/1000 * 5739 = 5 considered unsuccessful
c [sweep-10] removed 1 vars in TOTAL (3 rounds, 2561 queries)
c [sort-queue-17] sorted 539 enqueued variables after 1879158 conflicts
c [score-dist-17] active 5199 (91%), one 0 (0%), zero 539 (9%)
c [score-dist-17] max exp 542, different 36 (7%)
c [score-dist-17] median active exp 537, avg 534.2
c [simplification-17] removed 9 variables 0.2% (5738 remain 12%)
c [simplification-17] removed 286 irredundant clauses 1.2% (23830 remain 18%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 307482 = 614964 / 2
c [simplification-17] new conflict interval 922446
c [simplification-17] penalized conflict interval 922446 = 1 * 922446
c [simplification-17] hard conflict limit 3262827 (soft 2801604 + delta 461223)
c [simplification-17] new conflict limit 2801604 (hard 3262827)
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 -  605.7    5738    23830   1915974   47097  15418  6291   36    39   26  93%   1024   -1   37   36  102%
c -  627.3    5738    23830   1968997   47673  15418  6291   36    38   27  93%   1024   -1   36   37   97%
c -  648.6    5738    23830   2023998   45635  15418  6291   36    39   26  92%   1024    0   36   36   99%
c -  669.3    5738    23830   2086904   48022  15418  6291   35    36   26  97%   1024   -1   34   35   97%
c -  690.1    5738    23830   2155455   47963  15418  6291   34    35   36  98%   1024   -2   34   35   99%
c -  710.9    5738    23830   2213653   49731  15418  6292   35    37   37  95%   1024   -0   34   35   97%
c -  732.1    5738    23830   2268259   48909  15419  6292   36    38   37  96%   1024    0   35   36   99%
c -  755.5    5738    23830   2324662   44092  15419  6292   35    36   38  97%   1024   -0   35   35  100%
c -  784.9    5738    23830   2389809   48020  15420  6292   35    37   39  94%   1024    1   35   35  101%
c -  806.5    5738    23830   2457714   51767  15420  6293   33    34   39  96%   1024   -1   33   34   97%
c -  826.5    5738    23830   2520284   52014  15421  6293   36    39   39  93%   1024    3   38   33  114%
c -  850.3    5738    23830   2578994   52249  15421  6293   36    37   39  96%   1024    1   35   35  100%
c -  876.4    5738    23830   2641413   50167  15422  6293   34    35   38  96%   1024   -0   34   34  101%
c -  901.5    5738    23830   2705560   48824  15422  6293   31    33   38  95%   1024   -2   30   33   92%
c -  935.8    5738    23830   2774509   52815  15424  6293   31    34   39  92%   1024   -1   30   33   91%
c 
c [simplification-18] limit 2801604 conflicts (hard 3262827) hit after 2828995 conflicts
c [quatres-16] found 8633 quaternary clauses 57% in total
c [quatres-16-1] removed 7 duplicate quaternary clauses
c [quatres-16-2] added 15 single-self-subsuming ternary resolvents
c [quatres-16-2] added 112 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 5738 free variables schedulable
c [ternres-16] 310 ternary resolvents (36 bin, 274 trn)
c [ternres-16] fully completed ternary resolution
c [treelook-6] limit 43766874 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 11476 literals 100%
c [treelook-6] scheduling used 536153 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 43766874 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1437829 steps
c [treelook-6] fully completed tree based probing
c [decomp-61] removed 1 variables
c [treelook-6] removed 1 variables, found 222 hbrs
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 628 transitive binary clauses
c [cce-14] limit of 2147483647 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 871 (0%) of length 5
c [cce-14-1] eliminated 6 clauses out of 4089 (0%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 8 large clauses in 2240120 steps
c [cce-14-1] allowing another 1120060 steps for small clauses
c [cce-14-1] scheduling 8606 clauses = 2052 binary + 6554 ternary
c [cce-14-1] tried to eliminate 8606 small clauses 100%
c [cce-14-1] eliminated 5 binary clauses 0%
c [cce-14-1] eliminated 27 ternary clauses 0%
c [cce-14-1] eliminated 32 small clauses 0%
c [cce-14-1] eliminated 32 small clauses in 2831687 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 40 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1104513 steps for small clauses
c [cce-14-2] scheduling 8574 clauses = 2047 binary + 6527 ternary
c [cce-14-2] tried to eliminate 8574 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 40 covered clauses in TOTAL during 2 rounds
c [cce-14] 40 < 1/100 * 23825 = 238 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 5737 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 102 variables 2% in round 1 in 3741620 steps
c [elim-15-1] backward subsumption/strengthening limit 3741600
c [elim-15-1-1] backward checking 689 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 2 and strengthened 22 clauses in 87263 steps
c [elim-15-1] rescheduled 79 variables 1% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 155401 steps
c [elim-15-2] backward subsumption/strengthening limit 155400
c [elim-15-2-1] backward checking 15 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 12719 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 104 = 2% variables out of 5737 scheduled
c [bca-17] limit of 10000000 steps and 47832 added (scaled 2)
c [bca-17] 3967 out of 11268 literals actually usable 35%
c [bca-17] added 0 blocked clauses in 87837 steps
c [sort-queue-18] sorted 539 enqueued variables after 2828995 conflicts
c [score-dist-18] active 5094 (90%), one 0 (0%), zero 539 (10%)
c [score-dist-18] max exp 543, different 37 (7%)
c [score-dist-18] median active exp 538, avg 535.4
c [simplification-18] removed 105 variables 1.8% (5633 remain 12%)
c [simplification-18] removed 182 irredundant clauses 0.8% (23648 remain 17%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 307482 = 922446 / 3
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 4328995 (soft 3828995 + delta 500000)
c [simplification-18] new conflict limit 3828995 (hard 4328995)
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 -  979.0    5633    23648   2862475   53336  15366  5418   38    43   22  88%   1024    3   37   33  112%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 101 basic ate = 98 trn 97% + 3 lrg 3% in 4 updates
c bcas: 17 count, 72 added (35 skipped), 705382 steps
c bkwd: tried 92327 clauses, 184445 lits, 2.00 lits/clause
c bkwd: checked 1615551 occs, 17.50 occs/clause, 8.76 occs/lit
c bkwd: subsumed 0 binary, 50 ternary, 57 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 386 large (0% self)
c blkd: 6 bces, 5330 removed, 890962 resolutions, 2438404 steps
c blkd: 4133 blocking literals 4%, 5 pure
c bump: 2911381 bumped seen, 1079944508 lits 370.9 on average
c card: 5 count, 0 units, 112 am1, 8360150 steps
c card: 73 rescheduled, 674 eliminated, 66950 resolved, 5178 subsumed
c card: 860 at-most-one constraints found, average size 3.01
c card: 860 at-most-one constraints used 100%, average size 3.01
c card: 102 at-most-two constraints found, average size 4.00
c card: 102 at-most-two constraints used 100%, average size 4.00
c cces: 14 cces, 10544 eliminated, 8204 ate 78%, 2340 abce 22%
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: 118 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 61 decompositions, 3426 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 5845430 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 38675 eliminated 72%, 5 pure 0%
c elms: 46 rounds, 3.1 rounds/bve
c elms: 38290 small 99%, 375 large 1%
c elms: 78275 tried small, 38290 succeeded 49%, 39985 failed 51%
c elms: 1079 subsumed, 2790 strengthened, 153 blocked
c elms: 2619896 copies, 2742399 resolutions, 2271011 ipos
c elms: 410023 subchks, 280484 strchks
c gaus: 5 extractions, 20208 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10049822 steps, 5024911 extr 50%, 1351825 elim 13%
c glue: 33.4 orig avg, 33.4 real avg, 5.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 35437 = 4521 simple 13% + 28582 trn 81% + 2334 lrg 7%, 1090 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2911380 clauses, 73.6 length
c lrnd: 214340255 lits = 512869341 orig - 298529086 removed 58%
c lrnd: 512637 uips 18%, 1892807 flips 65%
c mins: 2907980 mins 100%, 594 bin 0%, 2807 size 0%
c mins: 1102189862 poisoned searches, 55517236 hits, 5% hit rate
c mins: 1556617613 used twice searches, 32066797 hits, 2% hit rate
c move: moved 13503, 4703 bin 35%, 8800 trn 65%
c otfs: 1900 driving 26%, 5272 restarting 74%
c otfs: str 7172, 6851 red 96%, 321 irr 4%
c otfs: str 7172, 0 bin 0%, 220 trn 3%, 6952 lrg 97%
c otfs: sub 1919, 1919 red 100%, 0 irr 0%
c otfs: sub 1919, 0 bin 0%, 4 trn 0%, 1915 lrg 100%
c phas: 1 computed, 9675 set, 3115 pos (32%), 6560 neg (68%)
c prbs: 5 basic, 53696 probed, 17 failed, 0 lifted
c prbs: 6 simple, 154362 probed, 334 failed, 1187 eqs
c prbs: 6 treelook, 25214 probed, 1 failed, 0 lifted
c prom: 23220 locked 0% out of 15637536 tried
c prps: 1644892660 props, 281 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 16 count, 8182 quat, 195 self1, 4 self2, 392 dup
c queu: 18 sorted, 5845430 next (214875 steps 0.04)
c queu: 1080021010 enq (2009026559 steps 1.86), 1079944508 deq 100%
c redc: 634 clauses 6%, 10815 tried 0%, 4 sat 0%
c redc: 769 lits 1%, 94523 tried 0%, 4 sat 0%
c redc: 66 times jump level reduced, 13.3 levels on average
c reds: 56 count, 51947.1 conflicts per reduce
c reds: 0 memlim 0%, 56 arith 100%
c reds: 2170159 collected 90%, 238430 retired 10%
c rmbd: 306 removed, 306 red 100%
c rsts: 7891 restarts 55%, 6562 skipped 45%
c rsts: 6562 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2911380 count (6462763 tried 2.2), 361426 sub out of 2908435 (12.4%)
c swps: 10 count, 16 rounds, 10027 queries (626.7/round)
c swps: 9851 sat calls, 502 unsat (0.4% success rate)
c swps: 115999 decisions 11.8, 4245 conflicts 0.4
c swps; 54.6 avg class size, 31.8 avg environment size
c swps: 0 failed, 644 impls, 678 equivs
c swp0: 3336 type 0 queries, 1247 unsat (37.4%), 3257 sat (97.6%)
c swp1: 6691 type 1 queries, 3419 unsat (51.1%), 6092 sat (91.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 17514036 calls to obtain time
c tops: 6018 fixed 11%, 0 its, 0.00 confs/it
c trds: 16 transitive reductions, 11589 removed, 3 failed
c trds: 178458 nodes, 160527 edges, 3593940 steps
c trim: 2365532 words, 9.0 MB
c trnr: 16 count, 294 bin, 14426 trn, 53985804 steps
c unhd: 7 count, 8 rounds, 4815615 steps
c unhd: 8 non-trivial sccs of average size 2.0
c unhd: 34 units, 34 bin, 0 trn, 0 lrg
c unhd: 134 failed, 134 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 8769 tauts, 88 bin 1%, 1573 trn 18%, 61 lrg 1%
c unhd: 8769 tauts, 7047 stamp 80%, 8715 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 631664 str, 34 bin 0%, 541 trn 0%, 631089 lrg 100%, 630213 red 100%
c vars: 5633 remaining 10% and 48119 removed 90% out of 53752
c vars: 6018 fixed 11%, 38675 eliminated 72%, 3426 equivalent 6%
c vsts: 45015203182 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 27.4 search visits per propagation, 15457.6 per conflict
c wchs: 2188984537 pushed, 6902826 enlarged, 197 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2916617       2170159        238430     229103693     155673093       1680163
c 
c  0 0         12826   0        12   0         0   0 139277412  61  90692286  58    355239  21     0.2
c  1 5          2394   0         7   0      1512   1  18440187   8< 11492990   7<    42738   3     0.0
c  2 6         22983   1      1018   0      9256   4  30529482  13  21169348  14    122238   7     0.5
c  3 9        138897   5     20945   1     27846  12  18242522   8  12719154   8    152105   9     3.6
c  4 14       196679   7    122034   6     25161  11   7629289   3   5822352   4    149329   9<    7.7
c  5 21       285050  10    215753  10     22252   9<  6949336   3   6017006   4    271917  16     9.5
c  6 30      1887207  65<  1500308  69<   144924  61   7075672   3   6813698   4    521599  31    27.6
c  7 41       231432   8    199459   9      6203   3    755908   0    756087   0     56383   3    16.9
c  8 54       133051   5    106000   5      1251   1    187931   0    177379   0      7906   0    16.0
c  9 69         4831   0      3958   0        22   0     13933   0     11061   0       705   0     3.0
c 10 86         1267   0       665   0         3   0      2021   0      1732   0         4   0     0.8
c 
c avg                  5.7           6.0           5.2           1.1           1.2           3.7
c std                  1.1           0.9           1.3           1.7           1.8           2.4
c 
c  206.385  21% bump
c   17.215   2% cce
c    3.660   0% elim
c 
c    9.150 < 1% rest (below)
c 
c    3.580   0% decide
c    2.750   0% sweep
c    2.663   0% probe
c    1.318   0% unhide
c    0.624   0% bca
c    0.478   0% ternres
c    0.370   0% quatres
c    0.319   0% gauss
c    0.284   0% block
c    0.205   0% transred
c    0.140   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.878   0% preprocessing     3%
c   30.584   3% inprocessing     97%
c ==================================
c   31.462   3% simplifying
c  968.504  97% search
c ==================================
c  999.967 100% all
c 
c       2909036 conflicts,        2909.1 confs/sec
c           660 ternaries,        4407.6 confs/ternary
c           195 binaries,        14918.1 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            56 reductions,          0.1 redus/sec,  51947.1 confs/reduction
c          7891 restarts,            7.9 rests/sec,    368.7 confs/restart
c       5845430 decisions,        5845.6 decis/sec,      2.0 decis/conflict
c    1644892660 propagations,  1644947.1 props/sec,    281.4 props/decision
c 
c 1000.0 seconds, 82.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
