c launch: /data/cnf/sc2014/app/6s168-opt.cnf.bz2
c host: atom08
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/6s168-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s168-opt.cnf.bz2
c no embedded options
c found 'p cnf 5638 16519' header
c read 5638 variables, 16519 clauses, 38543 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=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 5637 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] INC (--score=1)
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    5637    16518         0       0      0     0    0     0    1   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 1 variables
c [simpleprobe-1] all 5637 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 344 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 344 variables, found 665 hbrs, 6 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 5293 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 3981 variables 75% in round 1 in 997203 steps
c [elim-1-1] backward subsumption/strengthening limit 997200
c [elim-1-1-1] backward checking 3799 touched variables 72%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 4 and strengthened 36 clauses in 149817 steps
c [elim-1-1] rescheduled 36 variables 1% by backward subsumption
c [elim-1-2] eliminated 8 variables 0% in round 2 in 10115 steps
c [elim-1-2] backward subsumption/strengthening limit 10100
c [elim-1-2-1] backward checking 15 touched variables 0%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 10101 steps
c [elim-1-2] fully rescheduled 1284 variables 24%
c [elim-1-3] eliminated 37 variables 1% in round 3 in 709025 steps
c [elim-1-3] backward subsumption/strengthening limit 709000
c [elim-1-3-1] backward checking 117 touched variables 2%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 2 and strengthened 11 clauses in 45388 steps
c [elim-1] incomplete 18 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4050 = 77% variables out of 5293 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 6472 negative 95.7% of 6765 except 293 4.3%
c [phase-count-1] 6400 positive 94.6% of 6765 except 365 5.4%
c [phase-1] phase bias: 242 positive 19%, 1001 negative 81%
c [sort-queue-1] sorted 1243 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1243 (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 4394 variables 77.9% (1243 remain 22%)
c [simplification-1] removed 9753 irredundant clauses 59.0% (6765 remain 41%)
c [simplification-1] maximum reduction of 78% = max (78%, 59%)
c [simplification-1] large reduction 78% >= 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 2 variables
c [simpleprobe-2] all 1241 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 0 variables, found 256 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 2482 literals 100%
c [treelook-1] scheduling used 36692 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 149984 steps
c [treelook-1] fully completed tree based probing
c [treelook-1] removed 0 variables, found 169 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 665 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-0] fully completed probing
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 1241 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 3 variables 0% in round 1 in 704106 steps
c [elim-2-1] backward subsumption/strengthening limit 704100
c [elim-2-1-1] backward checking 20 touched variables 2%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 4 clauses in 8732 steps
c [elim-2-1] rescheduled 9 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 4614 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 3 = 0% variables out of 1241 scheduled
c [elim-2] 3 < 1/100 * 1241 = 12 considered unsuccessful
c [sort-queue-2] sorted 379 enqueued variables after 1001 conflicts
c [score-dist-2] active 859 (69%), one 0 (0%), zero 379 (31%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 504, avg 505.3
c [simplification-2] removed 5 variables 0.4% (1238 remain 22%)
c [simplification-2] removed 24 irredundant clauses 0.4% (6741 remain 41%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 20000 = 1 * 20000
c [simplification-2] hard conflict limit 31001 (soft 21001 + delta 10000)
c [simplification-2] new conflict limit 21001 (hard 31001)
c 
c [simplification-3] limit 21001 conflicts (hard 31001) hit after 21002 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 1 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1 out of 1 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [unhide-2] limit 50671 with penalty 1 = 1 + 0
c [unhide-2-3] 0 units, 0 failed, 10 tauts, 0 hbrs, 21588 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 1238 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 64 blocked clauses
c [block-1] 64 < 1/100 * 6741 = 67 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 18 clauses out of 2371 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 18 large clauses in 347862 steps
c [cce-1-1] allowing another 173931 steps for small clauses
c [cce-1-1] scheduling 2676 clauses = 709 binary + 1967 ternary
c [cce-1-1] tried to eliminate 2676 small clauses 100%
c [cce-1-1] eliminated 19 binary clauses 3%
c [cce-1-1] eliminated 39 ternary clauses 2%
c [cce-1-1] eliminated 58 small clauses 2%
c [cce-1-1] eliminated 58 small clauses in 467565 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 76 covered clauses in round 1
c [cce-1-2] eliminated 1 clauses out of 2353 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 1 large clauses in 352773 steps
c [cce-1-2] allowing another 176386 steps for small clauses
c [cce-1-2] scheduling 2618 clauses = 690 binary + 1928 ternary
c [cce-1-2] tried to eliminate 2618 small clauses 100%
c [cce-1-2] eliminated 4 binary clauses 1%
c [cce-1-2] eliminated 4 small clauses 0%
c [cce-1-2] eliminated 4 small clauses in 476874 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 5 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 322548 steps for small clauses
c [cce-1-3] scheduling 2614 clauses = 686 binary + 1928 ternary
c [cce-1-3] tried to eliminate 2614 small clauses 100%
c [cce-1-3] eliminated 1 binary clauses 0%
c [cce-1-3] eliminated 2 ternary clauses 0%
c [cce-1-3] eliminated 3 small clauses 0%
c [cce-1-3] eliminated 3 small clauses in 680134 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 3 covered clauses in round 3
c [cce-1] eliminated 84 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 13686 added (scaled 2)
c [bca-1] 292 out of 2478 literals actually usable 12%
c [bca-1] added 0 blocked clauses in 20253 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 628 pos 50.7% + 610 neg 49.3% = 1238 sched 100.0% ret 0
c [sweep-1-1] 1033152 steps 60 queries 53.78 avg class size
c [sweep-1-1] 3111 decisions 60 SAT calls 101.50 avg env size
c [sweep-1-1] 274 variables remain 22% (964 retained 78%)
c [decomp-7] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 7 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 7 vars in TOTAL (1 rounds, 59 queries)
c [sort-queue-3] sorted 5 enqueued variables after 21002 conflicts
c [score-dist-3] active 1226 (100%), one 0 (0%), zero 5 (0%)
c [score-dist-3] max exp 515, different 13 (3%)
c [score-dist-3] median active exp 512, avg 511.9
c [simplification-3] removed 7 variables 0.6% (1231 remain 22%)
c [simplification-3] removed 159 irredundant clauses 2.4% (6582 remain 40%)
c [simplification-3] maximum reduction of 2% = max (1%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 26666
c [simplification-3] penalized conflict interval 26666 = 1 * 26666
c [simplification-3] hard conflict limit 61001 (soft 47668 + delta 13333)
c [simplification-3] new conflict limit 47668 (hard 61001)
c 
c [simplification-4] limit 47668 conflicts (hard 61001) hit after 47671 conflicts
c [quatres-1] found 2563 quaternary clauses 59% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 93 single-self-subsuming ternary resolvents
c [quatres-1-2] added 69 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 1231 free variables schedulable
c [ternres-1] 773 ternary resolvents (47 bin, 726 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2176 xors of average arity 3.7
c [gauss-1] connected 8024 occurrences of 692 variables (average 11.6)
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-8] removed 3 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 2055 literals 84%
c [treelook-2] scheduling used 150203 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 141246 steps
c [treelook-2] 0 literals remain 0%
c [treelook-2] 0 variables remain to probed next time 0%
c [decomp-9] removed 1 variables
c [treelook-2] removed 1 variables, found 24 hbrs
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 80 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 17 clauses out of 2351 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 17 large clauses in 330430 steps
c [cce-2-1] allowing another 165215 steps for small clauses
c [cce-2-1] scheduling 1966 clauses = 681 binary + 1285 ternary
c [cce-2-1] tried to eliminate 1966 small clauses 100%
c [cce-2-1] eliminated 14 ternary clauses 1%
c [cce-2-1] eliminated 14 small clauses 1%
c [cce-2-1] eliminated 14 small clauses in 363916 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 31 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 164047 steps for small clauses
c [cce-2-2] scheduling 1952 clauses = 681 binary + 1271 ternary
c [cce-2-2] tried to eliminate 1952 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 31 covered clauses in TOTAL during 2 rounds
c [cce-2] 31 < 1/100 * 6574 = 65 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1227 variables 100%
c [elim-3] limit of 21579349 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 22 variables 2% in round 1 in 782637 steps
c [elim-3-1] backward subsumption/strengthening limit 782600
c [elim-3-1-1] backward checking 96 touched variables 8%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 19500 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 22 = 2% variables out of 1227 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 130 pos 48.9% + 136 neg 51.1% = 266 sched 22.1% ret 939
c [sweep-2-1] 1038469 steps 15 queries 24.47 avg class size
c [sweep-2-1] 1039 decisions 14 SAT calls 277.79 avg env size
c [sweep-2-1] 187 variables remain 16% (1018 retained 84%)
c [decomp-10] removed 4 variables
c [sweep-2-1] removed 4 vars (0 failed, 3 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 4 vars in TOTAL (1 rounds, 14 queries)
c [score-dist-4] active 1201 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 516, different 12 (2%)
c [score-dist-4] median active exp 513, avg 512.9
c [simplification-4] removed 30 variables 2.4% (1201 remain 21%)
c [simplification-4] removed 85 irredundant clauses 1.3% (6497 remain 39%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-4] new conflict interval 35554
c [simplification-4] penalized conflict interval 35554 = 1 * 35554
c [simplification-4] hard conflict limit 101002 (soft 83225 + delta 17777)
c [simplification-4] new conflict limit 83225 (hard 101002)
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 -    7.8    1201     6497     54596   26021   1095   473   21    51    8  42%    572   30   21   11  187%
c 
c [simplification-5] limit 83225 conflicts (hard 101002) hit after 83226 conflicts
c [quatres-2] found 2551 quaternary clauses 55% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 67 single-self-subsuming ternary resolvents
c [quatres-2-2] added 101 quaternary resolvents
c [ternres-2] limit 4511495 with penalty 0 = 0 + 0
c [ternres-2] all 1201 free variables schedulable
c [ternres-2] 90 ternary resolvents (31 bin, 59 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-11] removed 2 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 39 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1199 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 1199 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1804598160 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1 variables 0% in round 1 in 745265 steps
c [elim-4-1] backward subsumption/strengthening limit 745200
c [elim-4-1-1] backward checking 7 touched variables 1%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 4462 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1 = 0% variables out of 1199 scheduled
c [elim-4] 1 < 1/100 * 1199 = 11 considered unsuccessful
c [bca-2] limit of 10000000 steps and 13460 added (scaled 2)
c [bca-2] 154 out of 2398 literals actually usable 6%
c [bca-2] added 0 blocked clauses in 45973 steps
c [sweep-3] limit 1353448 penalty 0 = 0 + 0
c [sweep-3-1] 83 pos 44.4% + 104 neg 55.6% = 187 sched 15.6% ret 1011
c [sweep-3-1] 1401347 steps 23 queries 17.09 avg class size
c [sweep-3-1] 1105 decisions 25 SAT calls 171.08 avg env size
c [sweep-3-1] 117 variables remain 10% (1081 retained 90%)
c [decomp-12] removed 5 variables
c [sweep-3-1] removed 5 vars (0 failed, 3 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5 vars in TOTAL (1 rounds, 22 queries)
c [score-dist-5] active 1193 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 517, different 13 (3%)
c [score-dist-5] median active exp 515, avg 514.2
c [simplification-5] removed 8 variables 0.7% (1193 remain 21%)
c [simplification-5] removed 17 irredundant clauses 0.3% (6480 remain 39%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 17777 = 35554 / 2
c [simplification-5] new conflict interval 53331
c [simplification-5] penalized conflict interval 53331 = 1 * 53331
c [simplification-5] hard conflict limit 163222 (soft 136557 + delta 26665)
c [simplification-5] new conflict limit 136557 (hard 163222)
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 -   13.8    1193     6480     91261   27314   1210   457   21    56    8  38%    766   20   21   16  128%
c -   18.5    1193     6480    120693   28259   1228   458   19    31    8  60%    859   -9   17   18   98%
c -   23.8    1193     6480    152189   27550   1237   460   22    33   10  65%    922   -2   25   18  136%
c 
c [simplification-6] limit 136557 conflicts (hard 163222) hit after 152578 conflicts
c [quatres-3] found 2628 quaternary clauses 47% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 5 double-self-subsuming ternary resolvents
c [quatres-3-2] added 26 single-self-subsuming ternary resolvents
c [quatres-3-2] added 56 quaternary resolvents
c [ternres-3] limit 9589913 with penalty 0 = 0 + 0
c [ternres-3] all 1193 free variables schedulable
c [ternres-3] 64 ternary resolvents (35 bin, 29 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 1198739 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] found 6 at-most-two constraints of average size 4.0
c [card-3] using previous limit 1198739 for elimination
c [card-3] 7 out of 7 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2096 xors of average arity 3.7
c [gauss-2] connected 7764 occurrences of 668 variables (average 11.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 1 variables
c [basicprobe-2] limit 23974784 penalty 1 = 1 + 0
c [basicprobe-2-0] 662 sched 56%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-1] 665 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 3 hbrs
c [unhide-3] limit 479495 with penalty 2 = 2 + 0
c [unhide-3-5] 0 units, 0 failed, 256 tauts, 0 hbrs, 22471 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 5 transitive binary clauses
c [cce-3] limit of 23974784 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 4 clauses out of 47 (9%) of length 6
c [cce-3-1] eliminated 14 clauses out of 296 (5%) of length 5
c [cce-3-1] eliminated 5 clauses out of 2297 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 23 large clauses in 699705 steps
c [cce-3-1] allowing another 349852 steps for small clauses
c [cce-3-1] scheduling 2557 clauses = 683 binary + 1874 ternary
c [cce-3-1] tried to eliminate 2557 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 33 ternary clauses 2%
c [cce-3-1] eliminated 34 small clauses 1%
c [cce-3-1] eliminated 34 small clauses in 681469 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 57 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 343000 steps for small clauses
c [cce-3-2] scheduling 2523 clauses = 682 binary + 1841 ternary
c [cce-3-2] tried to eliminate 2523 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 57 covered clauses in TOTAL during 2 rounds
c [cce-3] 57 < 1/100 * 6476 = 64 considered unsuccessful
c [sweep-4] limit 2876974 penalty 0 = 0 + 0
c [sweep-4-1] 61 pos 52.6% + 55 neg 47.4% = 116 sched 9.7% ret 1076
c [sweep-4-1] 755458 steps 55 queries 7.96 avg class size
c [sweep-4-1] 1503 decisions 54 SAT calls 87.93 avg env size
c [sweep-4-1] fully completed sweeping round
c [decomp-15] removed 20 variables
c [sweep-4-1] removed 20 vars (0 failed, 18 eqs, 11 impls)
c [sweep-4-2] 558 pos 47.6% + 614 neg 52.4% = 1172 sched 100.0% ret 0
c [sweep-4-2] 2201739 steps 95 queries 31.87 avg class size
c [sweep-4-2] 3710 decisions 101 SAT calls 102.35 avg env size
c [sweep-4-2] 49 variables remain 4% (1123 retained 96%)
c [decomp-16] removed 24 variables
c [sweep-4-2] removed 24 vars (0 failed, 19 eqs, 8 impls)
c [sweep-4] removed 44 vars in TOTAL (2 rounds, 148 queries)
c [score-dist-6] active 1148 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 518, different 14 (3%)
c [score-dist-6] median active exp 515, avg 515.0
c [simplification-6] removed 45 variables 3.8% (1148 remain 20%)
c [simplification-6] removed 73 irredundant clauses 1.1% (6407 remain 39%)
c [simplification-6] maximum reduction of 4% = max (4%, 1%)
c [simplification-6] geometric conflict interval increment 10666 = 53331 / 5
c [simplification-6] new conflict interval 63997
c [simplification-6] penalized conflict interval 63997 = 1 * 63997
c [simplification-6] hard conflict limit 248573 (soft 216575 + delta 31998)
c [simplification-6] new conflict limit 216575 (hard 248573)
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 -   29.0    1148     6407    185229   26142   1010   431   24    54    9  44%    962   12   24   21  116%
c 
c [simplification-7] limit 216575 conflicts (hard 248573) hit after 216576 conflicts
c [quatres-4] found 2701 quaternary clauses 43% in total
c [quatres-4-1] removed 3 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 59 single-self-subsuming ternary resolvents
c [quatres-4-2] added 120 quaternary resolvents
c [ternres-4] limit 13973853 with penalty 0 = 0 + 0
c [ternres-4] all 1148 free variables schedulable
c [ternres-4] 323 ternary resolvents (39 bin, 284 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 1 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 52 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 1147 variables 100%
c [elim-5] limit of 139738535 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 17 variables 1% in round 1 in 755489 steps
c [elim-5-1] backward subsumption/strengthening limit 755400
c [elim-5-1-1] backward checking 87 touched variables 8%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 7 and strengthened 13 clauses in 30987 steps
c [elim-5-1] rescheduled 25 variables 2% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 31166 steps
c [elim-5-2] backward subsumption/strengthening limit 31100
c [elim-5-2-1] backward checking 9 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 6446 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 18 = 2% variables out of 1147 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 41921560 penalty 0 = 0 + 0
c [sweep-5-1] 25 pos 51.0% + 24 neg 49.0% = 49 sched 4.3% ret 1080
c [sweep-5-1] 610651 steps 29 queries 7.86 avg class size
c [sweep-5-1] 825 decisions 26 SAT calls 61.08 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-18] removed 4 variables
c [sweep-5-1] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-5-2] 520 pos 46.2% + 605 neg 53.8% = 1125 sched 100.0% ret 0
c [sweep-5-2] 3446879 steps 122 queries 16.66 avg class size
c [sweep-5-2] 4756 decisions 133 SAT calls 139.44 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-19] removed 34 variables
c [sweep-5-2] removed 34 vars (0 failed, 31 eqs, 4 impls)
c [sweep-5-3] 506 pos 46.4% + 585 neg 53.6% = 1091 sched 100.0% ret 0
c [sweep-5-3] 3282332 steps 108 queries 25.61 avg class size
c [sweep-5-3] 4150 decisions 116 SAT calls 150.30 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-20] removed 17 variables
c [sweep-5-3] removed 17 vars (0 failed, 18 eqs, 3 impls)
c [sweep-5] removed 55 vars in TOTAL (3 rounds, 256 queries)
c [score-dist-7] active 1074 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 518, different 14 (3%)
c [score-dist-7] median active exp 516, avg 515.5
c [simplification-7] removed 74 variables 6.4% (1074 remain 19%)
c [simplification-7] removed 167 irredundant clauses 2.6% (6240 remain 38%)
c [simplification-7] maximum reduction of 6% = max (6%, 3%)
c [simplification-7] large reduction 6% >= 5% limit
c [simplification-7] next conflict interval 2165 = min (216576/100, 63997)
c [simplification-7] penalized conflict interval 2165 = 1 * 2165
c [simplification-7] hard conflict limit 228741 (soft 218741 + delta 10000)
c [simplification-7] new conflict limit 218741 (hard 228741)
c 
c [simplification-8] limit 218741 conflicts (hard 228741) hit after 218741 conflicts
c [quatres-5] found 2725 quaternary clauses 44% in total
c [quatres-5-1] removed 9 duplicate quaternary clauses
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 51 single-self-subsuming ternary resolvents
c [quatres-5-2] added 81 quaternary resolvents
c [ternres-5] limit 14152885 with penalty 0 = 0 + 0
c [ternres-5] all 1074 free variables schedulable
c [ternres-5] 218 ternary resolvents (38 bin, 180 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 1 variables
c [simpleprobe-3] all 1073 free variables schedulable
c [simpleprobe-3] limit 28305770 penalty 1 = 1 + 0
c [decomp-22] removed 2 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 2 variables, found 12 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 48 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 1071 variables 100%
c [block-3] limit of 35382213 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 1071 variables 100%
c [elim-6] limit of 283057706 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 30 variables 3% in round 1 in 751037 steps
c [elim-6-1] backward subsumption/strengthening limit 751000
c [elim-6-1-1] backward checking 140 touched variables 13%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 4 clauses in 43911 steps
c [elim-6-1] rescheduled 8 variables 1% by backward subsumption
c [elim-6-2] eliminated 2 variables 0% in round 2 in 2364 steps
c [elim-6-2] backward subsumption/strengthening limit 2300
c [elim-6-2-1] backward checking 9 touched variables 1%
c [elim-6-2-1] incomplete backward checking 7 remain 78%
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 2334 steps
c [elim-6-2] fully rescheduled 1039 variables 97%
c [elim-6-3] eliminated 2 variables 0% in round 3 in 725368 steps
c [elim-6-3] backward subsumption/strengthening limit 725300
c [elim-6-3-1] backward checking 12 touched variables 1%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 7466 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 34 = 3% variables out of 1071 scheduled
c [bca-3] limit of 10000000 steps and 12304 added (scaled 2)
c [bca-3] 153 out of 2076 literals actually usable 7%
c [bca-3] added 18 blocked clauses in 15597 steps
c [sweep-6] limit 4245865 penalty 0 = 0 + 0
c [sweep-6-1] 465 pos 44.8% + 572 neg 55.2% = 1037 sched 100.0% ret 0
c [sweep-6-1] 1287054 steps 108 queries 24.95 avg class size
c [sweep-6-1] 3863 decisions 111 SAT calls 75.27 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-23] removed 13 variables
c [sweep-6-1] removed 13 vars (0 failed, 12 eqs, 1 impls)
c [sweep-6-2] 460 pos 44.9% + 564 neg 55.1% = 1024 sched 100.0% ret 0
c [sweep-6-2] 1668822 steps 116 queries 23.73 avg class size
c [sweep-6-2] 4437 decisions 117 SAT calls 93.45 avg env size
c [sweep-6-2] fully completed sweeping round
c [decomp-24] removed 25 variables
c [sweep-6-2] removed 25 vars (0 failed, 24 eqs, 2 impls)
c [sweep-6-3] 450 pos 45.0% + 549 neg 55.0% = 999 sched 100.0% ret 0
c [sweep-6-3] 1297401 steps 89 queries 28.39 avg class size
c [sweep-6-3] 3058 decisions 87 SAT calls 96.77 avg env size
c [sweep-6-3] 38 variables remain 4% (961 retained 96%)
c [decomp-25] removed 17 variables
c [sweep-6-3] removed 17 vars (0 failed, 15 eqs, 4 impls)
c [sweep-6] removed 55 vars in TOTAL (3 rounds, 310 queries)
c [score-dist-8] active 982 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 518, different 14 (3%)
c [score-dist-8] median active exp 516, avg 515.6
c [simplification-8] removed 92 variables 8.6% (982 remain 17%)
c [simplification-8] removed 364 irredundant clauses 5.8% (5876 remain 36%)
c [simplification-8] maximum reduction of 9% = max (9%, 6%)
c [simplification-8] large reduction 9% >= 5% limit
c [simplification-8] next conflict interval 2187 = min (218741/100, 63997)
c [simplification-8] penalized conflict interval 2187 = 1 * 2187
c [simplification-8] hard conflict limit 230928 (soft 220928 + delta 10000)
c [simplification-8] new conflict limit 220928 (hard 230928)
c 
c [simplification-9] limit 220928 conflicts (hard 230928) hit after 220928 conflicts
c [quatres-6] found 2732 quaternary clauses 49% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 56 single-self-subsuming ternary resolvents
c [quatres-6-2] added 46 quaternary resolvents
c [ternres-6] limit 14248417 with penalty 0 = 0 + 0
c [ternres-6] all 982 free variables schedulable
c [ternres-6] 223 ternary resolvents (39 bin, 184 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 712420 penalty 2 = 2 + 0
c [gauss-3] extracted 1776 xors of average arity 3.7
c [gauss-3] connected 6516 occurrences of 544 variables (average 12.0)
c [gauss-3] limit 712420 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 1 variables
c [treelook-3] limit 1424841 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 1962 literals 100%
c [treelook-3] scheduling used 126445 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1424841 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 153862 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 1 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 47 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 178105222 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 2 clauses out of 33 (6%) of length 6
c [cce-4-1] eliminated 25 clauses out of 380 (7%) of length 5
c [cce-4-1] eliminated 210 clauses out of 2079 (10%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 237 large clauses in 318661 steps
c [cce-4-1] allowing another 159330 steps for small clauses
c [cce-4-1] scheduling 1774 clauses = 598 binary + 1176 ternary
c [cce-4-1] tried to eliminate 1774 small clauses 100%
c [cce-4-1] eliminated 11 binary clauses 2%
c [cce-4-1] eliminated 33 ternary clauses 3%
c [cce-4-1] eliminated 44 small clauses 2%
c [cce-4-1] eliminated 44 small clauses in 342988 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 281 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 143965 steps for small clauses
c [cce-4-2] scheduling 1730 clauses = 587 binary + 1143 ternary
c [cce-4-2] tried to eliminate 1730 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 281 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 981 variables 100%
c [elim-7] limit of 284968357 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 30 variables 3% in round 1 in 653133 steps
c [elim-7-1] backward subsumption/strengthening limit 653100
c [elim-7-1-1] backward checking 120 touched variables 12%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 3 and strengthened 8 clauses in 32003 steps
c [elim-7-1] rescheduled 19 variables 2% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 26920 steps
c [elim-7-2] backward subsumption/strengthening limit 26900
c [elim-7-2-1] backward checking 21 touched variables 2%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 3 and strengthened 4 clauses in 11704 steps
c [elim-7-2] rescheduled 12 variables 1% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 17782 steps
c [elim-7-3] backward subsumption/strengthening limit 17700
c [elim-7-3-1] backward checking 14 touched variables 1%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 8202 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 36 = 4% variables out of 981 scheduled
c [sweep-7] limit 4274525 penalty 0 = 0 + 0
c [sweep-7-1] 15 pos 40.5% + 22 neg 59.5% = 37 sched 3.9% ret 908
c [sweep-7-1] 77205 steps 21 queries 5.62 avg class size
c [sweep-7-1] 434 decisions 17 SAT calls 72.06 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-28] removed 2 variables
c [sweep-7-1] removed 2 vars (0 failed, 4 eqs, 1 impls)
c [sweep-7-2] 398 pos 42.2% + 545 neg 57.8% = 943 sched 100.0% ret 0
c [sweep-7-2] 1192461 steps 98 queries 18.42 avg class size
c [sweep-7-2] 3142 decisions 95 SAT calls 86.48 avg env size
c [sweep-7-2] fully completed sweeping round
c [decomp-29] removed 9 variables
c [sweep-7-2] removed 9 vars (0 failed, 11 eqs, 6 impls)
c [sweep-7-3] 392 pos 42.0% + 542 neg 58.0% = 934 sched 100.0% ret 0
c [sweep-7-3] 1051760 steps 86 queries 18.17 avg class size
c [sweep-7-3] 2754 decisions 79 SAT calls 82.24 avg env size
c [sweep-7-3] fully completed sweeping round
c [decomp-30] removed 8 variables
c [sweep-7-3] removed 8 vars (0 failed, 9 eqs, 3 impls)
c [sweep-7] removed 19 vars in TOTAL (3 rounds, 202 queries)
c [score-dist-9] active 926 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 518, different 13 (3%)
c [score-dist-9] median active exp 516, avg 515.7
c [simplification-9] removed 56 variables 5.7% (926 remain 16%)
c [simplification-9] removed 546 irredundant clauses 9.3% (5330 remain 32%)
c [simplification-9] maximum reduction of 9% = max (6%, 9%)
c [simplification-9] large reduction 9% >= 5% limit
c [simplification-9] next conflict interval 2209 = min (220928/100, 63997)
c [simplification-9] penalized conflict interval 2209 = 1 * 2209
c [simplification-9] hard conflict limit 233137 (soft 223137 + delta 10000)
c [simplification-9] new conflict limit 223137 (hard 233137)
c 
c [simplification-10] limit 223137 conflicts (hard 233137) hit after 223139 conflicts
c [quatres-7] found 2482 quaternary clauses 48% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 22 single-self-subsuming ternary resolvents
c [quatres-7-2] added 42 quaternary resolvents
c [ternres-7] limit 14347792 with penalty 0 = 0 + 0
c [ternres-7] all 926 free variables schedulable
c [ternres-7] 171 ternary resolvents (40 bin, 131 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 896737 penalty 3 = 3 + 0
c [card-4] found 5 at-most-one constraints of average size 3.8
c [card-4] found 17 at-most-two constraints of average size 4.0
c [card-4] using previous limit 896737 for elimination
c [card-4] 21 out of 22 constraints (95%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 358694 with penalty 3 = 3 + 0
c [unhide-4-7] 0 units, 0 failed, 356 tauts, 0 hbrs, 9620 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 926 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5739117040 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 12 variables 1% in round 1 in 629999 steps
c [elim-8-1] backward subsumption/strengthening limit 629900
c [elim-8-1-1] backward checking 92 touched variables 10%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 25390 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 12 = 1% variables out of 926 scheduled
c [bca-4] limit of 10000000 steps and 10921 added (scaled 2)
c [bca-4] 105 out of 1830 literals actually usable 6%
c [bca-4] added 3 blocked clauses in 12108 steps
c [sweep-8] limit 4304337 penalty 0 = 0 + 0
c [sweep-8-1] 400 pos 43.8% + 514 neg 56.2% = 914 sched 100.0% ret 0
c [sweep-8-1] 710841 steps 96 queries 18.92 avg class size
c [sweep-8-1] 2544 decisions 95 SAT calls 74.92 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-32] removed 12 variables
c [sweep-8-1] removed 12 vars (0 failed, 15 eqs, 1 impls)
c [sweep-8-2] 395 pos 43.8% + 507 neg 56.2% = 902 sched 100.0% ret 0
c [sweep-8-2] 880658 steps 92 queries 21.21 avg class size
c [sweep-8-2] 2652 decisions 85 SAT calls 75.69 avg env size
c [sweep-8-2] fully completed sweeping round
c [decomp-33] removed 11 variables
c [sweep-8-2] removed 11 vars (0 failed, 14 eqs, 5 impls)
c [sweep-8-3] 388 pos 43.5% + 503 neg 56.5% = 891 sched 100.0% ret 0
c [sweep-8-3] 783038 steps 94 queries 21.57 avg class size
c [sweep-8-3] 2781 decisions 90 SAT calls 70.70 avg env size
c [sweep-8-3] fully completed sweeping round
c [decomp-34] removed 8 variables
c [sweep-8-3] removed 8 vars (0 failed, 10 eqs, 4 impls)
c [sweep-8] removed 31 vars in TOTAL (3 rounds, 279 queries)
c [score-dist-10] active 883 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 518, different 13 (3%)
c [score-dist-10] median active exp 516, avg 515.7
c [simplification-10] removed 43 variables 4.6% (883 remain 16%)
c [simplification-10] removed 136 irredundant clauses 2.6% (5194 remain 31%)
c [simplification-10] maximum reduction of 5% = max (5%, 3%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2231 = min (223139/100, 63997)
c [simplification-10] penalized conflict interval 2231 = 1 * 2231
c [simplification-10] hard conflict limit 235370 (soft 225370 + delta 10000)
c [simplification-10] new conflict limit 225370 (hard 235370)
c 
c [simplification-11] limit 225370 conflicts (hard 235370) hit after 225370 conflicts
c [quatres-8] found 2513 quaternary clauses 49% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 33 single-self-subsuming ternary resolvents
c [quatres-8-2] added 68 quaternary resolvents
c [ternres-8] limit 14437950 with penalty 0 = 0 + 0
c [ternres-8] all 883 free variables schedulable
c [ternres-8] 319 ternary resolvents (33 bin, 286 trn)
c [ternres-8] fully completed ternary resolution
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 41 transitive binary clauses
c [transred-8] found 1 units
c [cce-5] limit of 36094877 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 35 (11%) of length 6
c [cce-5-1] eliminated 14 clauses out of 271 (5%) of length 5
c [cce-5-1] eliminated 71 clauses out of 1816 (4%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 89 large clauses in 388032 steps
c [cce-5-1] allowing another 194016 steps for small clauses
c [cce-5-1] scheduling 1630 clauses = 545 binary + 1085 ternary
c [cce-5-1] tried to eliminate 1630 small clauses 100%
c [cce-5-1] eliminated 12 binary clauses 2%
c [cce-5-1] eliminated 19 ternary clauses 2%
c [cce-5-1] eliminated 31 small clauses 2%
c [cce-5-1] eliminated 37 small clauses in 411092 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 126 covered clauses in round 1
c [cce-5-2] eliminated 2 clauses out of 1745 (0%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 2 large clauses in 374566 steps
c [cce-5-2] allowing another 187283 steps for small clauses
c [cce-5-2] scheduling 1599 clauses = 533 binary + 1066 ternary
c [cce-5-2] tried to eliminate 1599 small clauses 100%
c [cce-5-2] eliminated 1 ternary clauses 0%
c [cce-5-2] eliminated 1 small clauses 0%
c [cce-5-2] eliminated 1 small clauses in 396250 steps
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 3 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 186003 steps for small clauses
c [cce-5-3] scheduling 1598 clauses = 533 binary + 1065 ternary
c [cce-5-3] tried to eliminate 1598 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 129 covered clauses in TOTAL during 3 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 882 variables 100%
c [elim-9] limit of 288759019 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 16 variables 2% in round 1 in 595834 steps
c [elim-9-1] backward subsumption/strengthening limit 595800
c [elim-9-1-1] backward checking 92 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 25019 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 16 = 2% variables out of 882 scheduled
c [bca-5] limit of 10000000 steps and 10408 added (scaled 2)
c [bca-5] 100 out of 1734 literals actually usable 6%
c [bca-5] added 0 blocked clauses in 11243 steps
c [sweep-9] limit 4331385 penalty 0 = 0 + 0
c [sweep-9-1] 400 pos 46.2% + 466 neg 53.8% = 866 sched 100.0% ret 0
c [sweep-9-1] 762934 steps 93 queries 20.46 avg class size
c [sweep-9-1] 2290 decisions 85 SAT calls 70.73 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-36] removed 8 variables
c [sweep-9-1] removed 8 vars (0 failed, 12 eqs, 5 impls)
c [sweep-9-2] 397 pos 46.3% + 461 neg 53.7% = 858 sched 100.0% ret 0
c [sweep-9-2] 827258 steps 93 queries 21.90 avg class size
c [sweep-9-2] 2788 decisions 86 SAT calls 82.52 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-37] removed 6 variables
c [sweep-9-2] removed 6 vars (0 failed, 10 eqs, 2 impls)
c [sweep-9-3] 393 pos 46.1% + 459 neg 53.9% = 852 sched 100.0% ret 0
c [sweep-9-3] 535685 steps 102 queries 20.87 avg class size
c [sweep-9-3] 2046 decisions 96 SAT calls 71.82 avg env size
c [sweep-9-3] fully completed sweeping round
c [decomp-38] removed 11 variables
c [sweep-9-3] removed 11 vars (0 failed, 18 eqs, 5 impls)
c [sweep-9] removed 25 vars in TOTAL (3 rounds, 285 queries)
c [score-dist-11] active 841 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 518, different 13 (3%)
c [score-dist-11] median active exp 516, avg 515.8
c [simplification-11] removed 42 variables 4.8% (841 remain 15%)
c [simplification-11] removed 255 irredundant clauses 4.9% (4939 remain 30%)
c [simplification-11] maximum reduction of 5% = max (5%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2253 = min (225370/100, 63997)
c [simplification-11] penalized conflict interval 2253 = 1 * 2253
c [simplification-11] hard conflict limit 237623 (soft 227623 + delta 10000)
c [simplification-11] new conflict limit 227623 (hard 237623)
c 
c [simplification-12] limit 227623 conflicts (hard 237623) hit after 227624 conflicts
c [quatres-9] found 2459 quaternary clauses 51% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 14 single-self-subsuming ternary resolvents
c [quatres-9-2] added 50 quaternary resolvents
c [ternres-9] limit 14525300 with penalty 0 = 0 + 0
c [ternres-9] all 841 free variables schedulable
c [ternres-9] 153 ternary resolvents (38 bin, 115 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-39] removed 1 variables
c [basicprobe-3] limit 18156625 penalty 2 = 2 + 0
c [basicprobe-3-0] 450 sched 54%, 1 failed, 0 lifted, 3 hbrs
c [decomp-40] removed 1 variables
c [basicprobe-3-1] 448 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 1 variables, found 3 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 45 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 839 variables 100%
c [block-4] limit of 18156625 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-6] limit of 72626501 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 34 clauses out of 1736 (2%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 34 large clauses in 249230 steps
c [cce-6-1] allowing another 124615 steps for small clauses
c [cce-6-1] scheduling 1846 clauses = 511 binary + 1335 ternary
c [cce-6-1] tried to eliminate 1846 small clauses 100%
c [cce-6-1] eliminated 1 binary clauses 0%
c [cce-6-1] eliminated 133 ternary clauses 10%
c [cce-6-1] eliminated 134 small clauses 7%
c [cce-6-1] eliminated 134 small clauses in 328405 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 168 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 120905 steps for small clauses
c [cce-6-2] scheduling 1712 clauses = 510 binary + 1202 ternary
c [cce-6-2] tried to eliminate 1712 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 168 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 839 variables 100%
c [elim-10] limit of 290506005 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 7 variables 1% in round 1 in 563523 steps
c [elim-10-1] backward subsumption/strengthening limit 563500
c [elim-10-1-1] backward checking 43 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 13537 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 7 = 1% variables out of 839 scheduled
c [elim-10] 7 < 1/100 * 839 = 8 considered unsuccessful
c [sweep-10] limit 4357590 penalty 0 = 0 + 0
c [sweep-10-1] 354 pos 42.5% + 478 neg 57.5% = 832 sched 100.0% ret 0
c [sweep-10-1] 999227 steps 105 queries 23.27 avg class size
c [sweep-10-1] 2661 decisions 97 SAT calls 64.07 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-41] removed 11 variables
c [sweep-10-1] removed 11 vars (0 failed, 17 eqs, 0 impls)
c [sweep-10-2] 347 pos 42.3% + 474 neg 57.7% = 821 sched 100.0% ret 0
c [sweep-10-2] 854369 steps 103 queries 19.55 avg class size
c [sweep-10-2] 2535 decisions 96 SAT calls 74.42 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-42] removed 9 variables
c [sweep-10-2] removed 9 vars (0 failed, 16 eqs, 2 impls)
c [sweep-10-3] 344 pos 42.4% + 468 neg 57.6% = 812 sched 100.0% ret 0
c [sweep-10-3] 791951 steps 100 queries 15.14 avg class size
c [sweep-10-3] 2287 decisions 91 SAT calls 70.86 avg env size
c [sweep-10-3] fully completed sweeping round
c [decomp-43] removed 9 variables
c [sweep-10-3] removed 9 vars (0 failed, 17 eqs, 6 impls)
c [sweep-10] removed 29 vars in TOTAL (3 rounds, 305 queries)
c [score-dist-12] active 803 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 518, different 13 (3%)
c [score-dist-12] median active exp 516, avg 515.8
c [simplification-12] removed 38 variables 4.5% (803 remain 14%)
c [simplification-12] removed 242 irredundant clauses 4.9% (4697 remain 28%)
c [simplification-12] maximum reduction of 5% = max (5%, 5%)
c [simplification-12] large reduction 5% >= 5% limit
c [simplification-12] next conflict interval 2276 = min (227624/100, 63997)
c [simplification-12] penalized conflict interval 2276 = 1 * 2276
c [simplification-12] hard conflict limit 239900 (soft 229900 + delta 10000)
c [simplification-12] new conflict limit 229900 (hard 239900)
c 
c [simplification-13] limit 229900 conflicts (hard 239900) hit after 229901 conflicts
c [quatres-10] found 2459 quaternary clauses 50% in total
c [quatres-10-1] removed 8 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 9 single-self-subsuming ternary resolvents
c [quatres-10-2] added 14 quaternary resolvents
c [ternres-10] limit 14612789 with penalty 0 = 0 + 0
c [ternres-10] all 803 free variables schedulable
c [ternres-10] 159 ternary resolvents (29 bin, 130 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 365319 penalty 3 = 3 + 0
c [gauss-4] extracted 1352 xors of average arity 3.5
c [gauss-4] connected 4748 occurrences of 353 variables (average 13.5)
c [gauss-4] limit 365319 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-44] removed 1 variables
c [simpleprobe-4] all 802 free variables schedulable
c [simpleprobe-4] limit 58451158 penalty 0 = 0 + 0
c [decomp-45] removed 8 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 8 variables, found 14 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 45 transitive binary clauses
c [cce-7] limit of 73063947 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 16 clauses out of 265 (6%) of length 5
c [cce-7-1] eliminated 107 clauses out of 1691 (6%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 123 large clauses in 337842 steps
c [cce-7-1] allowing another 168921 steps for small clauses
c [cce-7-1] scheduling 1463 clauses = 499 binary + 964 ternary
c [cce-7-1] tried to eliminate 1463 small clauses 100%
c [cce-7-1] eliminated 1 binary clauses 0%
c [cce-7-1] eliminated 13 ternary clauses 1%
c [cce-7-1] eliminated 14 small clauses 1%
c [cce-7-1] eliminated 14 small clauses in 356130 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 137 covered clauses in round 1
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] allowing another 162849 steps for small clauses
c [cce-7-2] scheduling 1449 clauses = 498 binary + 951 ternary
c [cce-7-2] tried to eliminate 1449 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 137 covered clauses in TOTAL during 2 rounds
c [bca-6] limit of 10000000 steps and 9540 added (scaled 2)
c [bca-6] 99 out of 1590 literals actually usable 6%
c [bca-6] not enough literals usable
c [bca-6] added 0 blocked clauses in 13958 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 43838360 penalty 0 = 0 + 0
c [sweep-11-1] 332 pos 41.8% + 462 neg 58.2% = 794 sched 100.0% ret 0
c [sweep-11-1] 1263018 steps 87 queries 24.59 avg class size
c [sweep-11-1] 2389 decisions 86 SAT calls 85.65 avg env size
c [sweep-11-1] fully completed sweeping round
c [sweep-11-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-11-2] 332 pos 41.8% + 462 neg 58.2% = 794 sched 100.0% ret 0
c [sweep-11-2] 1464190 steps 86 queries 19.34 avg class size
c [sweep-11-2] 2438 decisions 85 SAT calls 80.22 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-47] removed 8 variables
c [sweep-11-2] removed 8 vars (0 failed, 9 eqs, 1 impls)
c [sweep-11-3] 329 pos 41.9% + 457 neg 58.1% = 786 sched 100.0% ret 0
c [sweep-11-3] 1395315 steps 80 queries 24.32 avg class size
c [sweep-11-3] 2115 decisions 77 SAT calls 81.43 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-48] removed 1 variables
c [sweep-11-3] removed 1 vars (0 failed, 2 eqs, 3 impls)
c [sweep-11] removed 9 vars in TOTAL (3 rounds, 250 queries)
c [score-dist-13] active 785 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 518, different 13 (3%)
c [score-dist-13] median active exp 516, avg 515.8
c [simplification-13] removed 18 variables 2.2% (785 remain 14%)
c [simplification-13] removed 186 irredundant clauses 4.0% (4511 remain 27%)
c [simplification-13] maximum reduction of 4% = max (2%, 4%)
c [simplification-13] geometric conflict interval increment 12799 = 63997 / 5
c [simplification-13] new conflict interval 76796
c [simplification-13] penalized conflict interval 76796 = 1 * 76796
c [simplification-13] hard conflict limit 345095 (soft 306697 + delta 38398)
c [simplification-13] new conflict limit 306697 (hard 345095)
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 -   44.7     785     4511    274355   29829   1801   316   18    28   10  66%   1008  -14   18   20   91%
c -   48.9     785     4511    305214   31102   1803   316   19    26   10  73%   1014  -10   20   20  101%
c -   52.9     785     4511    336130   31628   1805   316   16    23   10  70%   1018   -9   16   19   83%
c 
c [simplification-14] limit 306697 conflicts (hard 345095) hit after 345096 conflicts
c [quatres-11] found 2370 quaternary clauses 44% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 8 single-self-subsuming ternary resolvents
c [quatres-11-2] added 21 quaternary resolvents
c [ternres-11] limit 24680611 with penalty 0 = 0 + 0
c [ternres-11] all 785 free variables schedulable
c [ternres-11] 53 ternary resolvents (32 bin, 21 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 35 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1234030590 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 241 (1%) of length 5
c [cce-8-1] eliminated 20 clauses out of 1579 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 22 large clauses in 228226 steps
c [cce-8-1] allowing another 114113 steps for small clauses
c [cce-8-1] scheduling 1442 clauses = 498 binary + 944 ternary
c [cce-8-1] tried to eliminate 1442 small clauses 100%
c [cce-8-1] eliminated 2 ternary clauses 0%
c [cce-8-1] eliminated 2 small clauses 0%
c [cce-8-1] eliminated 2 small clauses in 270388 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 24 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 113758 steps for small clauses
c [cce-8-2] scheduling 1441 clauses = 498 binary + 943 ternary
c [cce-8-2] tried to eliminate 1441 small clauses 100%
c [cce-8-2] eliminated 1 ternary clauses 0%
c [cce-8-2] eliminated 1 small clauses 0%
c [cce-8-2] eliminated 1 small clauses in 270195 steps
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 1 covered clauses in round 2
c [cce-8-3] completed large round (ATE)
c [cce-8-3] allowing another 113723 steps for small clauses
c [cce-8-3] scheduling 1440 clauses = 498 binary + 942 ternary
c [cce-8-3] tried to eliminate 1440 small clauses 100%
c [cce-8-3] completed small round (ATE)
c [cce-8-3] eliminated 0 covered clauses in round 3
c [cce-8] eliminated 25 covered clauses in TOTAL during 3 rounds
c [cce-8] 25 < 1/100 * 4503 = 45 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 785 variables 100%
c [elim-11] limit of 246806119 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 20 variables 3% in round 1 in 532288 steps
c [elim-11-1] backward subsumption/strengthening limit 532200
c [elim-11-1-1] backward checking 111 touched variables 14%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 4 clauses in 21999 steps
c [elim-11-1] rescheduled 10 variables 1% by backward subsumption
c [elim-11-2] eliminated 6 variables 1% in round 2 in 4837 steps
c [elim-11-2] backward subsumption/strengthening limit 4800
c [elim-11-2-1] backward checking 18 touched variables 2%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 4674 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 26 = 3% variables out of 785 scheduled
c [sweep-12] limit 7404183 penalty 0 = 0 + 0
c [sweep-12-1] 308 pos 40.6% + 451 neg 59.4% = 759 sched 100.0% ret 0
c [sweep-12-1] 809975 steps 82 queries 19.70 avg class size
c [sweep-12-1] 1528 decisions 82 SAT calls 55.66 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-50] removed 2 variables
c [sweep-12-1] removed 2 vars (0 failed, 3 eqs, 0 impls)
c [sweep-12-2] 307 pos 40.6% + 450 neg 59.4% = 757 sched 100.0% ret 0
c [sweep-12-2] 569037 steps 79 queries 22.18 avg class size
c [sweep-12-2] 1608 decisions 78 SAT calls 60.47 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-51] removed 2 variables
c [sweep-12-2] removed 2 vars (0 failed, 3 eqs, 0 impls)
c [sweep-12-3] 306 pos 40.5% + 449 neg 59.5% = 755 sched 100.0% ret 0
c [sweep-12-3] 1133788 steps 79 queries 28.43 avg class size
c [sweep-12-3] 1778 decisions 77 SAT calls 62.65 avg env size
c [sweep-12-3] fully completed sweeping round
c [sweep-12-3] removed 0 vars (0 failed, 1 eqs, 1 impls)
c [sweep-12] removed 4 vars in TOTAL (3 rounds, 237 queries)
c [score-dist-14] active 755 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-14] max exp 519, different 14 (3%)
c [score-dist-14] median active exp 516, avg 516.1
c [simplification-14] removed 30 variables 3.8% (755 remain 13%)
c [simplification-14] removed 117 irredundant clauses 2.6% (4394 remain 27%)
c [simplification-14] maximum reduction of 4% = max (4%, 3%)
c [simplification-14] geometric conflict interval increment 15359 = 76796 / 5
c [simplification-14] new conflict interval 92155
c [simplification-14] penalized conflict interval 92155 = 1 * 92155
c [simplification-14] hard conflict limit 483328 (soft 437251 + delta 46077)
c [simplification-14] new conflict limit 437251 (hard 483328)
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 -   59.3     755     4392    392684   31428   1800   301   17    49    9  34%   1021    8   17   18   94%
c -   63.5     755     4392    427274   33117   1803   301   17    51    9  32%   1022    7   16   17   97%
c 
c [simplification-15] limit 437251 conflicts (hard 483328) hit after 437252 conflicts
c [quatres-12] found 2403 quaternary clauses 35% in total
c [quatres-12-2] added 10 single-self-subsuming ternary resolvents
c [quatres-12-2] added 8 quaternary resolvents
c [ternres-12] limit 30443932 with penalty 0 = 0 + 0
c [ternres-12] all 755 free variables schedulable
c [ternres-12] 74 ternary resolvents (30 bin, 44 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 951372 penalty 4 = 4 + 0
c [card-5] found 1 at-most-one constraints of average size 4.0
c [card-5] found 23 at-most-two constraints of average size 4.0
c [card-5] using previous limit 951372 for elimination
c [card-5] 24 out of 24 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 1522196 penalty 2 = 2 + 0
c [gauss-5] extracted 1152 xors of average arity 3.5
c [gauss-5] connected 3988 occurrences of 276 variables (average 14.4)
c [gauss-5] limit 1522196 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 1522196 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 1510 literals 100%
c [treelook-4] scheduling used 161699 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1522196 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 124988 steps
c [treelook-4] fully completed tree based probing
c [treelook-4] removed 0 variables, found 1 hbrs
c [unhide-5] limit 380549 with penalty 4 = 4 + 0
c [unhide-5-8] 0 units, 0 failed, 171 tauts, 0 hbrs, 14499 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 9 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 755 variables 100%
c [elim-12] limit of 608878659 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 9 variables 1% in round 1 in 529548 steps
c [elim-12-1] backward subsumption/strengthening limit 529500
c [elim-12-1-1] backward checking 33 touched variables 4%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 6094 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 9 = 1% variables out of 755 scheduled
c [sweep-13] limit 9133179 penalty 0 = 0 + 0
c [sweep-13-1] 320 pos 42.9% + 426 neg 57.1% = 746 sched 100.0% ret 0
c [sweep-13-1] 2533545 steps 83 queries 22.93 avg class size
c [sweep-13-1] 3195 decisions 82 SAT calls 121.40 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-55] removed 2 variables
c [sweep-13-1] removed 2 vars (0 failed, 3 eqs, 0 impls)
c [sweep-13-2] 318 pos 42.7% + 426 neg 57.3% = 744 sched 100.0% ret 0
c [sweep-13-2] 1903829 steps 77 queries 25.55 avg class size
c [sweep-13-2] 2407 decisions 74 SAT calls 111.39 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-56] removed 3 variables
c [sweep-13-2] removed 3 vars (0 failed, 4 eqs, 0 impls)
c [sweep-13-3] 316 pos 42.6% + 425 neg 57.4% = 741 sched 100.0% ret 0
c [sweep-13-3] 3128604 steps 65 queries 28.17 avg class size
c [sweep-13-3] 2573 decisions 61 SAT calls 114.72 avg env size
c [sweep-13-3] fully completed sweeping round
c [decomp-57] removed 5 variables
c [sweep-13-3] removed 5 vars (0 failed, 5 eqs, 0 impls)
c [sweep-13] removed 10 vars in TOTAL (3 rounds, 222 queries)
c [score-dist-15] active 736 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-15] max exp 520, different 12 (2%)
c [score-dist-15] median active exp 517, avg 516.6
c [simplification-15] removed 19 variables 2.5% (736 remain 13%)
c [simplification-15] removed 71 irredundant clauses 1.6% (4321 remain 26%)
c [simplification-15] maximum reduction of 3% = max (3%, 2%)
c [simplification-15] geometric conflict interval increment 23038 = 92155 / 4
c [simplification-15] new conflict interval 115193
c [simplification-15] penalized conflict interval 115193 = 1 * 115193
c [simplification-15] hard conflict limit 610041 (soft 552445 + delta 57596)
c [simplification-15] new conflict limit 552445 (hard 610041)
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 -   68.4     736     4321    465121   33577   1718   282   14    53    9  26%   1023    6   14   16   91%
c -   72.6     736     4321    503573   34104   1724   283   15    39    8  38%   1024   -9   17   15  114%
c -   76.6     736     4321    543287   35153   1729   283   11    22   11  52%   1024  -18   10   14   74%
c -   80.8     736     4321    584626   35964   1734   283   11    16   11  67%   1024  -14   12   13   98%
c 
c [simplification-16] limit 552445 conflicts (hard 610041) hit after 610041 conflicts
c [quatres-13] found 2517 quaternary clauses 26% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 17 single-self-subsuming ternary resolvents
c [quatres-13-2] added 21 quaternary resolvents
c [ternres-13] limit 41999907 with penalty 0 = 0 + 0
c [ternres-13] all 736 free variables schedulable
c [ternres-13] 171 ternary resolvents (28 bin, 143 trn)
c [ternres-13] fully completed ternary resolution
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 29 transitive binary clauses
c [cce-9] limit of 104999768 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 19 clauses out of 239 (8%) of length 5
c [cce-9-1] eliminated 37 clauses out of 1580 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 56 large clauses in 285900 steps
c [cce-9-1] allowing another 142950 steps for small clauses
c [cce-9-1] scheduling 1582 clauses = 457 binary + 1125 ternary
c [cce-9-1] tried to eliminate 1582 small clauses 100%
c [cce-9-1] eliminated 2 binary clauses 0%
c [cce-9-1] eliminated 69 ternary clauses 6%
c [cce-9-1] eliminated 71 small clauses 4%
c [cce-9-1] eliminated 71 small clauses in 355274 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 127 covered clauses in round 1
c [cce-9-2] eliminated 4 clauses out of 6 (67%) of length 7
c [cce-9-2] eliminated 1 clauses out of 25 (4%) of length 6
c [cce-9-2] eliminated 2 clauses out of 220 (1%) of length 5
c [cce-9-2] eliminated 1 clauses out of 1543 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 8 large clauses in 278487 steps
c [cce-9-2] allowing another 139243 steps for small clauses
c [cce-9-2] scheduling 1511 clauses = 455 binary + 1056 ternary
c [cce-9-2] tried to eliminate 1511 small clauses 100%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 2 small clauses 0%
c [cce-9-2] eliminated 2 small clauses in 336638 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 10 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 24 (4%) of length 6
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 1 large clauses in 273032 steps
c [cce-9-3] allowing another 136516 steps for small clauses
c [cce-9-3] scheduling 1509 clauses = 455 binary + 1054 ternary
c [cce-9-3] tried to eliminate 1509 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 1 covered clauses in round 3
c [cce-9] eliminated 138 covered clauses in TOTAL during 3 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 736 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 20 variables 3% in round 1 in 494443 steps
c [elim-13-1] backward subsumption/strengthening limit 494400
c [elim-13-1-1] backward checking 73 touched variables 10%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 3 clauses in 17591 steps
c [elim-13-1] rescheduled 7 variables 1% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 18320 steps
c [elim-13-2] backward subsumption/strengthening limit 18300
c [elim-13-2-1] backward checking 11 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 1 and strengthened 6 clauses in 10495 steps
c [elim-13-2] rescheduled 9 variables 1% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 17962 steps
c [elim-13-3] backward subsumption/strengthening limit 17900
c [elim-13-3-1] backward checking 13 touched variables 2%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 0 and strengthened 1 clauses in 11073 steps
c [elim-13] incomplete 7 not tried 1% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 23 = 3% variables out of 736 scheduled
c [bca-7] limit of 10000000 steps and 8730 added (scaled 2)
c [bca-7] 46 out of 1428 literals actually usable 3%
c [bca-7] not enough literals usable
c [bca-7] added 0 blocked clauses in 49920 steps
c [sweep-14] limit 12599972 penalty 0 = 0 + 0
c [sweep-14-1] 332 pos 46.6% + 381 neg 53.4% = 713 sched 100.0% ret 0
c [sweep-14-1] 1573127 steps 62 queries 19.32 avg class size
c [sweep-14-1] 1545 decisions 60 SAT calls 82.97 avg env size
c [sweep-14-1] fully completed sweeping round
c [sweep-14-1] removed 0 vars (0 failed, 1 eqs, 1 impls)
c [sweep-14-2] 332 pos 46.6% + 381 neg 53.4% = 713 sched 100.0% ret 0
c [sweep-14-2] 1604446 steps 63 queries 20.89 avg class size
c [sweep-14-2] 1781 decisions 62 SAT calls 83.81 avg env size
c [sweep-14-2] fully completed sweeping round
c [decomp-60] removed 1 variables
c [sweep-14-2] removed 1 vars (0 failed, 2 eqs, 0 impls)
c [sweep-14-3] 332 pos 46.6% + 380 neg 53.4% = 712 sched 100.0% ret 0
c [sweep-14-3] 1499461 steps 64 queries 22.30 avg class size
c [sweep-14-3] 1634 decisions 63 SAT calls 84.62 avg env size
c [sweep-14-3] fully completed sweeping round
c [sweep-14-3] removed 0 vars (0 failed, 1 eqs, 1 impls)
c [sweep-14] removed 1 vars in TOTAL (3 rounds, 186 queries)
c [score-dist-16] active 712 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-16] max exp 520, different 12 (2%)
c [score-dist-16] median active exp 517, avg 516.9
c [simplification-16] removed 24 variables 3.3% (712 remain 13%)
c [simplification-16] removed 211 irredundant clauses 4.9% (4110 remain 25%)
c [simplification-16] maximum reduction of 5% = max (3%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 6100 = min (610041/100, 115193)
c [simplification-16] penalized conflict interval 6100 = 1 * 6100
c [simplification-16] hard conflict limit 626141 (soft 616141 + delta 10000)
c [simplification-16] new conflict limit 616141 (hard 626141)
c 
c [simplification-17] limit 616141 conflicts (hard 626141) hit after 626141 conflicts
c [quatres-14] found 2469 quaternary clauses 26% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 2 single-self-subsuming ternary resolvents
c [quatres-14-2] added 16 quaternary resolvents
c [ternres-14] limit 43134378 with penalty 0 = 0 + 0
c [ternres-14] all 712 free variables schedulable
c [ternres-14] 76 ternary resolvents (27 bin, 49 trn)
c [ternres-14] fully completed ternary resolution
c [basicprobe-4] limit 107835946 penalty 1 = 1 + 0
c [basicprobe-4-0] 379 sched 53%, 1 failed, 0 lifted, 1 hbrs
c [decomp-63] removed 1 variables
c [basicprobe-4-1] 379 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-1] fully completed probing
c [basicprobe-4-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-4-1] removed 1 variables, found 1 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 29 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 711 variables 100%
c [block-5] limit of 26958986 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 4 blocked clauses
c [block-5] 4 < 1/100 * 4098 = 40 considered unsuccessful
c [cce-10] limit of 215671893 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 9 clauses out of 227 (4%) of length 5
c [cce-10-1] eliminated 5 clauses out of 1541 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 14 large clauses in 218388 steps
c [cce-10-1] allowing another 109194 steps for small clauses
c [cce-10-1] scheduling 1309 clauses = 440 binary + 869 ternary
c [cce-10-1] tried to eliminate 1309 small clauses 100%
c [cce-10-1] eliminated 2 binary clauses 0%
c [cce-10-1] eliminated 2 ternary clauses 0%
c [cce-10-1] eliminated 4 small clauses 0%
c [cce-10-1] eliminated 4 small clauses in 251139 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 18 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 108568 steps for small clauses
c [cce-10-2] scheduling 1305 clauses = 438 binary + 867 ternary
c [cce-10-2] tried to eliminate 1305 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 18 covered clauses in TOTAL during 2 rounds
c [cce-10] 18 < 1/100 * 4094 = 40 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 711 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 8 variables 1% in round 1 in 485532 steps
c [elim-14-1] backward subsumption/strengthening limit 485500
c [elim-14-1-1] backward checking 46 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 5 and strengthened 0 clauses in 12417 steps
c [elim-14-1] rescheduled 11 variables 2% by backward subsumption
c [elim-14-2] eliminated 3 variables 0% in round 2 in 22073 steps
c [elim-14-2] backward subsumption/strengthening limit 22000
c [elim-14-2-1] backward checking 8 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 3595 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 11 = 2% variables out of 711 scheduled
c [sweep-15] limit 12940313 penalty 0 = 0 + 0
c [sweep-15-1] 318 pos 45.4% + 382 neg 54.6% = 700 sched 100.0% ret 0
c [sweep-15-1] 3528863 steps 71 queries 22.24 avg class size
c [sweep-15-1] 1919 decisions 69 SAT calls 89.03 avg env size
c [sweep-15-1] fully completed sweeping round
c [sweep-15-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15-2] 318 pos 45.4% + 382 neg 54.6% = 700 sched 100.0% ret 0
c [sweep-15-2] 2678503 steps 69 queries 24.04 avg class size
c [sweep-15-2] 1912 decisions 67 SAT calls 87.10 avg env size
c [sweep-15-2] fully completed sweeping round
c [sweep-15-2] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15-3] 318 pos 45.4% + 382 neg 54.6% = 700 sched 100.0% ret 0
c [sweep-15-3] 1674997 steps 59 queries 23.42 avg class size
c [sweep-15-3] 1499 decisions 57 SAT calls 87.88 avg env size
c [sweep-15-3] fully completed sweeping round
c [sweep-15-3] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15] removed 0 vars in TOTAL (3 rounds, 196 queries)
c [score-dist-17] active 700 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-17] max exp 520, different 12 (2%)
c [score-dist-17] median active exp 517, avg 517.0
c [simplification-17] removed 12 variables 1.7% (700 remain 12%)
c [simplification-17] removed 75 irredundant clauses 1.8% (4035 remain 24%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 38397 = 115193 / 3
c [simplification-17] new conflict interval 153590
c [simplification-17] penalized conflict interval 153590 = 1 * 153590
c [simplification-17] hard conflict limit 856526 (soft 779731 + delta 76795)
c [simplification-17] new conflict limit 779731 (hard 856526)
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 -   86.6     700     4035    640915   36726   1890   272    8     9   11  90%   1024  -11    7   11   63%
c i   88.4     699     4035    665729   52396   1955   286    6     7   13  91%   1024   -9    4   10   44%
c i   89.0     698     4035    674835   57914   2005   298    9    45   11  20%  -8171   27    8   10   81%
c i   90.9     696     4035    698470   70625   2073   311    6     7   15  90%  -5489  -10    4    9   48%
c -   91.7     696     4035    707601   39502   2100   314    7     7   10  90%  -4968   -9    6    9   68%
c i   91.8     695     4035    708518   39868   2135   322    6     7   12  90%  -4885   -9    4    9   51%
c i   92.1     694     4035    712822   41789   2186   332    6     7   12  90%  -4656   -8    4    8   51%
c i   92.2     693     4035    715018   42865   2220   342    6     6   12  90%  -4529   -8    4    8   52%
c i   92.3     690     4035    716143   43308   2249   351    6     6   12  90%  -4463   -8    4    8   53%
c i   92.3     686     4035    716687   43532   2272   360    5     6   12  90%  -4430   -9    4    8   49%
c i   92.3     680     4035    717057   43687   2297   367    5     6   12  90%  -4408   -9    4    8   48%
c i   92.3     672     4035    717136   43699   2307   372    5     6   12  90%  -4403   -9    4    8   45%
c i   92.3     670     4035    717170   43705   2314   377    5     6   12  90%  -4401   -9    4    8   43%
c i   92.3     665     4035    717191   43707   2320   380    5     6   12  90%  -4400   -9    3    8   42%
c i   92.3     663     4035    717203   43710   2324   382    5     6   12  90%  -4399   -9    3    8   41%
c i   92.3     656     4035    717206   43710   2323   384    5     6   12  90%  -4399   -9    3    8   41%
c i   92.3     645     4035    717207   43710   2323   384    5     6   12  90%  -4399   -9    3    8   41%
c 0   92.3     641     4035    717207   43710   2323   384    5     6   12  90%  -4399   -9    3    8   41%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 7 count, 21 added (0 skipped), 169052 steps
c bkwd: tried 11522 clauses, 22972 lits, 1.99 lits/clause
c bkwd: checked 243235 occs, 21.11 occs/clause, 10.59 occs/lit
c bkwd: subsumed 1 binary, 11 ternary, 14 large
c bkwd: strengthened 7 binary, 2 ternary (100% self), 85 large (0% self)
c blkd: 5 bces, 68 removed, 159076 resolutions, 377782 steps
c blkd: 72 blocking literals 1%, 0 pure
c bump: 731071 bumped seen, 61205573 lits 83.7 on average
c card: 5 count, 0 units, 0 am1, 35809324 steps
c card: 9 rescheduled, 54 eliminated, 171470 resolved, 3422 subsumed
c card: 7 at-most-one constraints found, average size 3.71
c card: 7 at-most-one constraints used 100%, average size 3.71
c card: 47 at-most-two constraints found, average size 4.00
c card: 46 at-most-two constraints used 98%, average size 4.00
c cces: 10 cces, 1062 eliminated, 997 ate 94%, 65 abce 6%
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: 55062 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 83 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 66 decompositions, 656 equivalent 12%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2114625 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 4243 eliminated 75%, 3 pure 0%
c elms: 39 rounds, 2.8 rounds/bve
c elms: 4179 small 98%, 61 large 1%
c elms: 17232 tried small, 4179 succeeded 24%, 13053 failed 76%
c elms: 653 subsumed, 889 strengthened, 27 blocked
c elms: 581160 copies, 704009 resolutions, 1187945 ipos
c elms: 8187 subchks, 15127 strchks
c gaus: 5 extractions, 8552 extracted, 3.6 size, 4 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 2893864 steps, 1446932 extr 50%, 306890 elim 11%
c glue: 15.9 orig avg, 15.9 real avg, 3.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1222 = 947 simple 77% + 275 trn 23% + 0 lrg 0%, 10 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 731071 clauses, 29.4 length
c lrnd: 21484461 lits = 34952954 orig - 13468493 removed 39%
c lrnd: 139279 uips 19%, 379070 flips 52%
c mins: 728506 mins 100%, 36 bin 0%, 2529 size 0%
c mins: 21702194 poisoned searches, 3369403 hits, 16% hit rate
c mins: 52544900 used twice searches, 6549608 hits, 12% hit rate
c move: moved 498, 71 bin 14%, 427 trn 86%
c otfs: 3144 driving 22%, 10906 restarting 78%
c otfs: str 14050, 13972 red 99%, 78 irr 1%
c otfs: str 14050, 0 bin 0%, 509 trn 4%, 13541 lrg 96%
c otfs: sub 495, 478 red 97%, 17 irr 3%
c otfs: sub 495, 0 bin 0%, 25 trn 5%, 470 lrg 95%
c phas: 1 computed, 1243 set, 242 pos (19%), 1001 neg (81%)
c prbs: 4 basic, 7295 probed, 2 failed, 0 lifted
c prbs: 4 simple, 19154 probed, 6 failed, 692 eqs
c prbs: 4 treelook, 8002 probed, 0 failed, 0 lifted
c prom: 48665 locked 7% out of 654343 tried
c prps: 86062868 props, 40 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 713 quat, 467 self1, 15 self2, 271 dup
c queu: 3 sorted, 2114625 next (84198 steps 0.04)
c queu: 61212838 enq (95566882 steps 1.56), 61205573 deq 100%
c redc: 1656 clauses 3%, 64039 tried 9%, 0 sat 0%
c redc: 1835 lits 0%, 619350 tried 2%, 0 sat 0%
c redc: 48 times jump level reduced, 2.9 levels on average
c reds: 16 count, 44825.4 conflicts per reduce
c reds: 0 memlim 0%, 16 arith 100%
c reds: 460049 collected 94%, 30225 retired 6%
c rmbd: 51 removed, 50 red 98%
c rsts: 7811 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 17 count, 17 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 731071 count (408187 tried 0.6), 97710 sub out of 728974 (13.4%)
c swps: 15 count, 38 rounds, 2971 queries (78.2/round)
c swps: 2936 sat calls, 310 unsat (5.8% success rate)
c swps: 90792 decisions 30.9, 17008 conflicts 5.8
c swps; 22.7 avg class size, 89.4 avg environment size
c swps: 0 failed, 91 impls, 344 equivs
c swp0: 976 type 0 queries, 237 unsat (24.3%), 897 sat (91.9%)
c swp1: 1995 type 1 queries, 716 unsat (35.9%), 1730 sat (86.7%)
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: 5691726 calls to obtain time
c tops: 98 fixed 2%, 15 its, 47813.80 confs/it
c trds: 14 transitive reductions, 505 removed, 1 failed
c trds: 26399 nodes, 12991 edges, 143847 steps
c trim: 475955 words, 1.8 MB
c trnr: 14 count, 486 bin, 2381 trn, 11191827 steps
c unhd: 5 count, 8 rounds, 2379710 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 793 tauts, 47 bin 6%, 648 trn 82%, 43 lrg 5%
c unhd: 793 tauts, 55 stamp 7%, 771 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 68178 str, 0 bin 0%, 63 trn 0%, 68115 lrg 100%, 67965 red 100%
c vars: 641 remaining 11% and 4997 removed 89% out of 5638
c vars: 98 fixed 2%, 4243 eliminated 75%, 656 equivalent 12%
c vsts: 5023076642 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 58.8 search visits per propagation, 6928.9 per conflict
c wchs: 821413999 pushed, 1052112 enlarged, 176 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         729687        460049         30225      12509458       5763462        341047
c 
c  0 0         21155   3       555   0         0   0   6875846  55   2392440  42    110490  32     0.4
c  1 5         18512   3      2955   1      1722   6   1473300  12<   608072  11     25626   8     0.3
c  2 6         95185  13     35505   8      6499  22   1795502  14    975449  17<    56523  17<    2.2
c  3 9        173855  24    117328  26      8605  28<  1343112  11    958570  17     87947  26     3.2
c  4 14       219131  30<   171630  37<     7724  26    708380   6    587101  10     54439  16     4.8
c  5 21       172230  24    114308  25      4800  16    272915   2    210657   4      5646   2     4.3
c  6 30        29541   4     17725   4       869   3     40231   0     31085   1       371   0     1.7
c  7 41           78   0        43   0         6   0       172   0        88   0         5   0     0.0
c 
c avg                  3.6           3.9           3.3           1.1           1.6           1.9
c std                  1.3           1.0           1.2           1.4           1.6           1.6
c 
c    6.398   7% bump
c    2.785   3% sweep
c    1.372   1% decide
c    1.254   1% elim
c    0.609   1% cce
c    0.477   1% card
c 
c    1.313 < 1% rest (below)
c 
c    0.433   0% unhide
c    0.374   0% probe
c    0.126   0% quatres
c    0.112   0% gauss
c    0.100   0% block
c    0.077   0% ternres
c    0.071   0% bca
c    0.019   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.260   0% preprocessing     4%
c    6.716   7% inprocessing     96%
c ==================================
c    6.976   8% simplifying
c   85.369  92% search
c ==================================
c   92.346 100% all
c 
c        717207 conflicts,        7766.5 confs/sec
c           816 ternaries,         878.9 confs/ternary
c           107 binaries,         6702.9 confs/binary
c            15 iterations,      47813.8 confs/iteration
c 
c            16 reductions,          0.2 redus/sec,  44825.4 confs/reduction
c          7811 restarts,           84.6 rests/sec,     91.8 confs/restart
c       2114625 decisions,       22899.0 decis/sec,      2.9 decis/conflict
c      86062868 propagations,   931963.2 props/sec,     40.7 props/decision
c 
c 92.3 seconds, 20.3 MB
c launch: done
