c launch: /data/cnf/sc2014/app/6s168-opt.cnf.bz2
c host: atom21
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=0
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] STATIC (--score=0)
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 1 variables
c [simpleprobe-2] all 1242 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 268 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 2484 literals 100%
c [treelook-1] scheduling used 36285 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 156975 steps
c [treelook-1] fully completed tree based probing
c [treelook-1] removed 0 variables, found 173 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 689 sched 55%, 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 1242 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 2 variables 0% in round 1 in 703167 steps
c [elim-2-1] backward subsumption/strengthening limit 703100
c [elim-2-1-1] backward checking 11 touched variables 1%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 1 clauses in 4216 steps
c [elim-2-1] rescheduled 4 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 2349 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 2 = 0% variables out of 1242 scheduled
c [elim-2] 2 < 1/100 * 1242 = 12 considered unsuccessful
c [sort-queue-2] sorted 1240 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 1240 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 3 variables 0.2% (1240 remain 22%)
c [simplification-2] removed 16 irredundant clauses 0.2% (6749 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 21001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] no at-most-two constraint found
c [decomp-6] removed 2 variables
c [unhide-2] limit 51185 with penalty 1 = 1 + 0
c [unhide-2-3] 0 units, 0 failed, 25 tauts, 0 hbrs, 25585 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 15 clauses out of 2369 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 15 large clauses in 349944 steps
c [cce-1-1] allowing another 174972 steps for small clauses
c [cce-1-1] scheduling 2672 clauses = 707 binary + 1965 ternary
c [cce-1-1] tried to eliminate 2672 small clauses 100%
c [cce-1-1] eliminated 18 binary clauses 3%
c [cce-1-1] eliminated 38 ternary clauses 2%
c [cce-1-1] eliminated 56 small clauses 2%
c [cce-1-1] eliminated 56 small clauses in 472688 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 71 covered clauses in round 1
c [cce-1-2] eliminated 1 clauses out of 2354 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 1 large clauses in 356725 steps
c [cce-1-2] allowing another 178362 steps for small clauses
c [cce-1-2] scheduling 2616 clauses = 689 binary + 1927 ternary
c [cce-1-2] tried to eliminate 2616 small clauses 100%
c [cce-1-2] eliminated 4 binary clauses 1%
c [cce-1-2] eliminated 2 ternary clauses 0%
c [cce-1-2] eliminated 6 small clauses 0%
c [cce-1-2] eliminated 6 small clauses in 479602 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 7 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 336167 steps for small clauses
c [cce-1-3] scheduling 2610 clauses = 685 binary + 1925 ternary
c [cce-1-3] tried to eliminate 2610 small clauses 100%
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 0 covered clauses in round 3
c [cce-1] eliminated 78 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 13698 added (scaled 2)
c [bca-1] 5 out of 2478 literals actually usable 0%
c [bca-1] not enough literals usable
c [bca-1] added 0 blocked clauses in 19980 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 529 pos 42.7% + 709 neg 57.3% = 1238 sched 100.0% ret 0
c [sweep-1-1] 1013450 steps 50 queries 58.38 avg class size
c [sweep-1-1] 2985 decisions 50 SAT calls 209.92 avg env size
c [sweep-1-1] 309 variables remain 25% (929 retained 75%)
c [decomp-7] removed 6 variables
c [sweep-1-1] removed 6 vars (0 failed, 5 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 6 vars in TOTAL (1 rounds, 49 queries)
c [sort-queue-3] sorted 1232 enqueued variables after 21001 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 1232 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 8 variables 0.6% (1232 remain 22%)
c [simplification-3] removed 159 irredundant clauses 2.4% (6590 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 61000 (soft 47667 + delta 13333)
c [simplification-3] new conflict limit 47667 (hard 61000)
c 
c [simplification-4] limit 47667 conflicts (hard 61000) hit after 47667 conflicts
c [quatres-1] found 3105 quaternary clauses 50% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 124 single-self-subsuming ternary resolvents
c [quatres-1-2] added 119 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 1232 free variables schedulable
c [ternres-1] 809 ternary resolvents (50 bin, 759 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2189 xors of average arity 3.7
c [gauss-1] connected 8059 occurrences of 693 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 4 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 2018 literals 82%
c [treelook-2] scheduling used 150060 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150016 steps
c [treelook-2] 78 literals remain 3%
c [treelook-2] 77 variables remain to probed next time 6%
c [decomp-9] removed 1 variables
c [treelook-2] removed 2 variables, found 12 hbrs
c [transred-1] limit 1939655 with penalty 0 = 0 + 0
c [transred-1] removed 85 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 8 clauses out of 302 (3%) of length 5
c [cce-2-1] eliminated 10 clauses out of 2356 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 18 large clauses in 332523 steps
c [cce-2-1] allowing another 166261 steps for small clauses
c [cce-2-1] scheduling 1972 clauses = 681 binary + 1291 ternary
c [cce-2-1] tried to eliminate 1972 small clauses 100%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 15 ternary clauses 1%
c [cce-2-1] eliminated 16 small clauses 1%
c [cce-2-1] eliminated 16 small clauses in 364456 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 34 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 164585 steps for small clauses
c [cce-2-2] scheduling 1956 clauses = 680 binary + 1276 ternary
c [cce-2-2] tried to eliminate 1956 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 34 covered clauses in TOTAL during 2 rounds
c [cce-2] 34 < 1/100 * 6582 = 65 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1226 variables 100%
c [elim-3] limit of 19396557 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 26 variables 2% in round 1 in 772321 steps
c [elim-3-1] backward subsumption/strengthening limit 772300
c [elim-3-1-1] backward checking 100 touched variables 8%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 2 clauses in 25497 steps
c [elim-3-1] rescheduled 5 variables 0% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 1538 steps
c [elim-3-2] backward subsumption/strengthening limit 1500
c [elim-3-2-1] backward checking 10 touched variables 1%
c [elim-3-2-1] incomplete backward checking 7 remain 70%
c [elim-3-2] subsumed 0 and strengthened 3 clauses in 1528 steps
c [elim-3-2] rescheduled 4 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 3709 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 29 = 2% variables out of 1226 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 136 pos 45.6% + 162 neg 54.4% = 298 sched 24.9% ret 899
c [sweep-2-1] 1015784 steps 61 queries 10.03 avg class size
c [sweep-2-1] 2820 decisions 59 SAT calls 148.49 avg env size
c [sweep-2-1] 6 variables remain 1% (1191 retained 99%)
c [decomp-10] removed 19 variables
c [sweep-2-1] removed 19 vars (0 failed, 20 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 19 vars in TOTAL (1 rounds, 60 queries)
c [sort-queue-4] sorted 1178 enqueued variables after 47667 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 1178 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 54 variables 4.4% (1178 remain 21%)
c [simplification-4] removed 142 irredundant clauses 2.2% (6448 remain 39%)
c [simplification-4] maximum reduction of 4% = max (4%, 2%)
c [simplification-4] geometric conflict interval increment 5333 = 26666 / 5
c [simplification-4] new conflict interval 31999
c [simplification-4] penalized conflict interval 31999 = 1 * 31999
c [simplification-4] hard conflict limit 95665 (soft 79666 + delta 15999)
c [simplification-4] new conflict limit 79666 (hard 95665)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.9    1177     6445     60829   49021   1745   469   14    87   15  17%    613   37   16    9  184%
c -   11.3    1176     6445     66626   18295   1806   477   14    86    7  17%   -233   33   15    9  168%
c 
c [simplification-5] limit 79666 conflicts (hard 95665) hit after 80226 conflicts
c [quatres-2] found 3252 quaternary clauses 40% in total
c [quatres-2-1] removed 12 duplicate quaternary clauses
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 65 single-self-subsuming ternary resolvents
c [quatres-2-2] added 89 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 1176 free variables schedulable
c [ternres-2] 181 ternary resolvents (37 bin, 144 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-11] removed 11 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 51 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1167 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 8 blocked clauses
c [block-2] 8 < 1/100 * 6428 = 64 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 1167 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1503911720 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 13 variables 1% in round 1 in 732404 steps
c [elim-4-1] backward subsumption/strengthening limit 732400
c [elim-4-1-1] backward checking 62 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 24452 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 13 = 1% variables out of 1167 scheduled
c [bca-2] limit of 10000000 steps and 13162 added (scaled 2)
c [bca-2] 0 out of 2310 literals actually usable 0%
c [bca-2] not enough literals usable
c [bca-2] added 0 blocked clauses in 28648 steps
c [sweep-3] limit 1127933 penalty 0 = 0 + 0
c [sweep-3-1] 2 pos 40.0% + 3 neg 60.0% = 5 sched 0.4% ret 1149
c [sweep-3-1] 44275 steps 5 queries 2.80 avg class size
c [sweep-3-1] 141 decisions 4 SAT calls 173.25 avg env size
c [sweep-3-1] fully completed sweeping round
c [decomp-12] removed 2 variables
c [sweep-3-1] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-3-2] 459 pos 39.8% + 693 neg 60.2% = 1152 sched 100.0% ret 0
c [sweep-3-2] 1120262 steps 39 queries 38.33 avg class size
c [sweep-3-2] 2940 decisions 40 SAT calls 251.90 avg env size
c [sweep-3-2] 271 variables remain 24% (881 retained 76%)
c [decomp-13] removed 4 variables
c [sweep-3-2] removed 4 vars (0 failed, 4 eqs, 1 impls)
c [sweep-3] removed 6 vars in TOTAL (2 rounds, 42 queries)
c [sort-queue-5] sorted 1148 enqueued variables after 80226 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 1148 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 28 variables 2.4% (1148 remain 20%)
c [simplification-5] removed 114 irredundant clauses 1.8% (6331 remain 38%)
c [simplification-5] maximum reduction of 2% = max (2%, 2%)
c [simplification-5] geometric conflict interval increment 10666 = 31999 / 3
c [simplification-5] new conflict interval 42665
c [simplification-5] penalized conflict interval 42665 = 1 * 42665
c [simplification-5] hard conflict limit 144223 (soft 122891 + delta 21332)
c [simplification-5] new conflict limit 122891 (hard 144223)
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 -   18.6    1148     6331    110213   22569   2127   453   14    87    8  16%    376   18   15   11  130%
c 
c [simplification-6] limit 122891 conflicts (hard 144223) hit after 122891 conflicts
c [quatres-3] found 3578 quaternary clauses 34% in total
c [quatres-3-1] removed 5 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 57 single-self-subsuming ternary resolvents
c [quatres-3-2] added 125 quaternary resolvents
c [ternres-3] limit 6024476 with penalty 0 = 0 + 0
c [ternres-3] all 1148 free variables schedulable
c [ternres-3] 321 ternary resolvents (43 bin, 278 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 753059 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] found 13 at-most-two constraints of average size 4.0
c [card-3] using previous limit 753059 for elimination
c [card-3] 14 out of 14 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 1 at-most-one constraints, 0 used 0%
c [card-3] exported 0 binary clauses, 0.0 per/constraint
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2121 xors of average arity 3.7
c [gauss-2] connected 7755 occurrences of 660 variables (average 11.8)
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-14] removed 10 variables
c [basicprobe-2] limit 15061190 penalty 1 = 1 + 0
c [basicprobe-2-0] 635 sched 56%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-1] 637 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 [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-3] limit 301223 with penalty 2 = 2 + 0
c [unhide-3-4] 0 units, 0 failed, 149 tauts, 0 hbrs, 10414 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 34 transitive binary clauses
c [cce-3] limit of 15061190 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 6 clauses out of 35 (17%) of length 6
c [cce-3-1] eliminated 30 clauses out of 300 (10%) of length 5
c [cce-3-1] eliminated 76 clauses out of 2262 (3%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 112 large clauses in 531576 steps
c [cce-3-1] allowing another 265788 steps for small clauses
c [cce-3-1] scheduling 1897 clauses = 652 binary + 1245 ternary
c [cce-3-1] tried to eliminate 1897 small clauses 100%
c [cce-3-1] eliminated 7 binary clauses 1%
c [cce-3-1] eliminated 15 ternary clauses 1%
c [cce-3-1] eliminated 22 small clauses 1%
c [cce-3-1] eliminated 22 small clauses in 500134 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 134 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 264985 steps for small clauses
c [cce-3-2] scheduling 1875 clauses = 645 binary + 1230 ternary
c [cce-3-2] tried to eliminate 1875 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 134 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 1138 variables 100%
c [elim-5] limit of 120489521 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 10 variables 1% in round 1 in 701229 steps
c [elim-5-1] backward subsumption/strengthening limit 701200
c [elim-5-1-1] backward checking 48 touched variables 4%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 13872 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 10 = 1% variables out of 1138 scheduled
c [elim-5] 10 < 1/100 * 1138 = 11 considered unsuccessful
c [sweep-4] limit 1807342 penalty 0 = 0 + 0
c [sweep-4-1] 87 pos 33.3% + 174 neg 66.7% = 261 sched 23.1% ret 867
c [sweep-4-1] 1366117 steps 64 queries 7.56 avg class size
c [sweep-4-1] 2880 decisions 53 SAT calls 189.23 avg env size
c [sweep-4-1] fully completed sweeping round
c [decomp-16] removed 17 variables
c [sweep-4-1] removed 17 vars (0 failed, 18 eqs, 9 impls)
c [sweep-4-2] 374 pos 33.7% + 737 neg 66.3% = 1111 sched 100.0% ret 0
c [sweep-4-2] 447019 steps 17 queries 114.06 avg class size
c [sweep-4-2] 1281 decisions 16 SAT calls 316.00 avg env size
c [sweep-4-2] 746 variables remain 67% (365 retained 33%)
c [decomp-17] removed 1 variables
c [sweep-4-2] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 18 vars in TOTAL (2 rounds, 79 queries)
c [sort-queue-6] sorted 1110 enqueued variables after 122891 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 1110 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 38 variables 3.3% (1110 remain 20%)
c [simplification-6] removed 200 irredundant clauses 3.2% (6131 remain 37%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 10666 = 42665 / 4
c [simplification-6] new conflict interval 53331
c [simplification-6] penalized conflict interval 53331 = 1 * 53331
c [simplification-6] hard conflict limit 202887 (soft 176222 + delta 26665)
c [simplification-6] new conflict limit 176222 (hard 202887)
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 -   24.6    1110     6131    151950   28190   2167   434   14    83    8  17%    681    6   15   13  119%
c 
c [simplification-7] limit 176222 conflicts (hard 202887) hit after 178555 conflicts
c [quatres-4] found 3987 quaternary clauses 27% in total
c [quatres-4-1] removed 6 duplicate quaternary clauses
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 44 single-self-subsuming ternary resolvents
c [quatres-4-2] added 69 quaternary resolvents
c [ternres-4] limit 8436696 with penalty 0 = 0 + 0
c [ternres-4] all 1110 free variables schedulable
c [ternres-4] 380 ternary resolvents (36 bin, 344 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-18] removed 10 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 45 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 421834820 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 4 clauses out of 279 (1%) of length 5
c [cce-4-1] eliminated 69 clauses out of 2160 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 73 large clauses in 273318 steps
c [cce-4-1] allowing another 136659 steps for small clauses
c [cce-4-1] scheduling 2396 clauses = 635 binary + 1761 ternary
c [cce-4-1] tried to eliminate 2396 small clauses 100%
c [cce-4-1] eliminated 4 binary clauses 1%
c [cce-4-1] eliminated 81 ternary clauses 5%
c [cce-4-1] eliminated 85 small clauses 4%
c [cce-4-1] eliminated 85 small clauses in 371739 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 158 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 131969 steps for small clauses
c [cce-4-2] scheduling 2311 clauses = 631 binary + 1680 ternary
c [cce-4-2] tried to eliminate 2311 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 158 covered clauses in TOTAL during 2 rounds
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 25310080 penalty 0 = 0 + 0
c [sweep-5-1] 275 pos 37.1% + 466 neg 62.9% = 741 sched 67.4% ret 359
c [sweep-5-1] 3520546 steps 94 queries 13.14 avg class size
c [sweep-5-1] 5699 decisions 91 SAT calls 298.76 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-19] removed 30 variables
c [sweep-5-1] removed 30 vars (0 failed, 26 eqs, 9 impls)
c [sweep-5-2] 405 pos 37.9% + 665 neg 62.1% = 1070 sched 100.0% ret 0
c [sweep-5-2] 3970871 steps 104 queries 17.04 avg class size
c [sweep-5-2] 5842 decisions 97 SAT calls 308.25 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-20] removed 28 variables
c [sweep-5-2] removed 28 vars (0 failed, 32 eqs, 11 impls)
c [sweep-5-3] 396 pos 38.0% + 646 neg 62.0% = 1042 sched 100.0% ret 0
c [sweep-5-3] 3267063 steps 89 queries 19.91 avg class size
c [sweep-5-3] 5131 decisions 86 SAT calls 323.03 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-21] removed 18 variables
c [sweep-5-3] removed 18 vars (0 failed, 16 eqs, 7 impls)
c [sweep-5] removed 76 vars in TOTAL (3 rounds, 284 queries)
c [sort-queue-7] sorted 1024 enqueued variables after 178555 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 1024 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 86 variables 7.7% (1024 remain 18%)
c [simplification-7] removed 175 irredundant clauses 2.9% (5956 remain 36%)
c [simplification-7] maximum reduction of 8% = max (8%, 3%)
c [simplification-7] large reduction 8% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 190555 (soft 180555 + delta 10000)
c [simplification-7] new conflict limit 180555 (hard 190555)
c 
c [simplification-8] limit 180555 conflicts (hard 190555) hit after 183081 conflicts
c [quatres-5] found 3885 quaternary clauses 26% in total
c [quatres-5-1] removed 17 duplicate quaternary clauses
c [quatres-5-2] added 37 single-self-subsuming ternary resolvents
c [quatres-5-2] added 59 quaternary resolvents
c [ternres-5] limit 8641714 with penalty 0 = 0 + 0
c [ternres-5] all 1024 free variables schedulable
c [ternres-5] 238 ternary resolvents (40 bin, 198 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-22] removed 3 variables
c [simpleprobe-3] all 1021 free variables schedulable
c [simpleprobe-3] limit 17283429 penalty 1 = 1 + 0
c [decomp-23] removed 4 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 4 variables, found 10 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 1017 variables 100%
c [block-3] limit of 21604287 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 3 blocked clauses
c [block-3] 3 < 1/100 * 5861 = 58 considered unsuccessful
c [cce-5] limit of 43208574 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 29 clauses out of 271 (11%) of length 5
c [cce-5-1] eliminated 185 clauses out of 2007 (9%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 214 large clauses in 476535 steps
c [cce-5-1] allowing another 238267 steps for small clauses
c [cce-5-1] scheduling 1836 clauses = 633 binary + 1203 ternary
c [cce-5-1] tried to eliminate 1836 small clauses 100%
c [cce-5-1] eliminated 1 binary clauses 0%
c [cce-5-1] eliminated 13 ternary clauses 1%
c [cce-5-1] eliminated 14 small clauses 1%
c [cce-5-1] eliminated 14 small clauses in 459139 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 228 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 221911 steps for small clauses
c [cce-5-2] scheduling 1822 clauses = 632 binary + 1190 ternary
c [cce-5-2] tried to eliminate 1822 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 228 covered clauses in TOTAL during 2 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 1017 variables 100%
c [elim-6] limit of 86417149 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 49 variables 5% in round 1 in 652058 steps
c [elim-6-1] backward subsumption/strengthening limit 652000
c [elim-6-1-1] backward checking 207 touched variables 20%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 2 clauses in 52391 steps
c [elim-6-1] rescheduled 9 variables 1% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 19301 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 50 = 5% variables out of 1017 scheduled
c [bca-3] limit of 10000000 steps and 11308 added (scaled 2)
c [bca-3] 0 out of 1936 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 42090 steps
c [sweep-6] limit 2592514 penalty 0 = 0 + 0
c [sweep-6-1] 353 pos 36.5% + 614 neg 63.5% = 967 sched 100.0% ret 0
c [sweep-6-1] 2621300 steps 95 queries 20.05 avg class size
c [sweep-6-1] 4965 decisions 96 SAT calls 200.73 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-24] removed 21 variables
c [sweep-6-1] removed 21 vars (0 failed, 17 eqs, 4 impls)
c [sweep-6] removed 21 vars in TOTAL (1 rounds, 94 queries)
c [sort-queue-8] sorted 946 enqueued variables after 183081 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 946 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 78 variables 7.6% (946 remain 17%)
c [simplification-8] removed 569 irredundant clauses 9.6% (5386 remain 33%)
c [simplification-8] maximum reduction of 10% = max (8%, 10%)
c [simplification-8] large reduction 10% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 195081 (soft 185081 + delta 10000)
c [simplification-8] new conflict limit 185081 (hard 195081)
c 
c [simplification-9] limit 185081 conflicts (hard 195081) hit after 185081 conflicts
c [quatres-6] found 3572 quaternary clauses 29% in total
c [quatres-6-1] removed 5 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 42 single-self-subsuming ternary resolvents
c [quatres-6-2] added 78 quaternary resolvents
c [ternres-6] limit 8711701 with penalty 0 = 0 + 0
c [ternres-6] all 946 free variables schedulable
c [ternres-6] 157 ternary resolvents (32 bin, 125 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1593 xors of average arity 3.6
c [gauss-3] connected 5735 occurrences of 455 variables (average 12.6)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-25] removed 4 variables
c [treelook-3] limit 871170 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 163 literals 9%
c [treelook-3] scheduling used 76979 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 871170 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 32564 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 44 transitive binary clauses
c [cce-6] limit of 43558508 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 29 (7%) of length 6
c [cce-6-1] eliminated 2 clauses out of 291 (1%) of length 5
c [cce-6-1] eliminated 51 clauses out of 1850 (3%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 55 large clauses in 257647 steps
c [cce-6-1] allowing another 128823 steps for small clauses
c [cce-6-1] scheduling 2094 clauses = 551 binary + 1543 ternary
c [cce-6-1] tried to eliminate 2094 small clauses 100%
c [cce-6-1] eliminated 122 ternary clauses 8%
c [cce-6-1] eliminated 122 small clauses 6%
c [cce-6-1] eliminated 122 small clauses in 355384 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 177 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 124517 steps for small clauses
c [cce-6-2] scheduling 1972 clauses = 551 binary + 1421 ternary
c [cce-6-2] tried to eliminate 1972 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 177 covered clauses in TOTAL during 2 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 942 variables 100%
c [elim-7] limit of 174234034 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 12 variables 1% in round 1 in 604748 steps
c [elim-7-1] backward subsumption/strengthening limit 604700
c [elim-7-1-1] backward checking 83 touched variables 9%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 2 clauses in 25563 steps
c [elim-7-1] rescheduled 5 variables 1% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 14124 steps
c [elim-7-2] backward subsumption/strengthening limit 14100
c [elim-7-2-1] backward checking 10 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 0 clauses in 4166 steps
c [elim-7-2] rescheduled 4 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 15005 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 15 = 2% variables out of 942 scheduled
c [sweep-7] limit 2613510 penalty 0 = 0 + 0
c [sweep-7-1] 316 pos 34.1% + 611 neg 65.9% = 927 sched 100.0% ret 0
c [sweep-7-1] 2021127 steps 87 queries 28.00 avg class size
c [sweep-7-1] 4677 decisions 87 SAT calls 208.20 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-27] removed 18 variables
c [sweep-7-1] removed 18 vars (0 failed, 14 eqs, 7 impls)
c [sweep-7-2] 307 pos 33.8% + 602 neg 66.2% = 909 sched 100.0% ret 0
c [sweep-7-2] 601776 steps 20 queries 81.20 avg class size
c [sweep-7-2] 1250 decisions 20 SAT calls 201.35 avg env size
c [sweep-7-2] 612 variables remain 67% (295 retained 33%)
c [decomp-28] removed 3 variables
c [sweep-7-2] removed 3 vars (0 failed, 1 eqs, 0 impls)
c [sweep-7] removed 21 vars in TOTAL (2 rounds, 105 queries)
c [sort-queue-9] sorted 906 enqueued variables after 185081 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 906 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 40 variables 4.2% (906 remain 16%)
c [simplification-9] removed 293 irredundant clauses 5.4% (5092 remain 31%)
c [simplification-9] maximum reduction of 5% = max (4%, 5%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 197081 (soft 187081 + delta 10000)
c [simplification-9] new conflict limit 187081 (hard 197081)
c 
c [simplification-10] limit 187081 conflicts (hard 197081) hit after 197081 conflicts
c [quatres-7] found 3616 quaternary clauses 29% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-1] added 3 double-self-subsuming ternary resolvents
c [quatres-7-2] added 43 single-self-subsuming ternary resolvents
c [quatres-7-2] added 89 quaternary resolvents
c [ternres-7] limit 9148912 with penalty 0 = 0 + 0
c [ternres-7] all 906 free variables schedulable
c [ternres-7] 229 ternary resolvents (40 bin, 189 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 571807 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] found 66 at-most-two constraints of average size 4.0
c [card-4] using previous limit 571807 for elimination
c [card-4] 62 out of 67 constraints (93%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-29] removed 6 variables
c [unhide-4] limit 228722 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 482 tauts, 0 hbrs, 48979 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 22 transitive binary clauses
c [cce-7] limit of 45744564 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 23 clauses out of 244 (9%) of length 5
c [cce-7-1] eliminated 57 clauses out of 1762 (3%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 80 large clauses in 395389 steps
c [cce-7-1] allowing another 197694 steps for small clauses
c [cce-7-1] scheduling 1626 clauses = 565 binary + 1061 ternary
c [cce-7-1] tried to eliminate 1626 small clauses 100%
c [cce-7-1] eliminated 13 binary clauses 2%
c [cce-7-1] eliminated 26 ternary clauses 2%
c [cce-7-1] eliminated 39 small clauses 2%
c [cce-7-1] eliminated 39 small clauses in 407110 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 119 covered clauses in round 1
c [cce-7-2] eliminated 2 clauses out of 2 (100%) of length 8
c [cce-7-2] eliminated 1 clauses out of 24 (4%) of length 7
c [cce-7-2] eliminated 2 clauses out of 27 (7%) of length 6
c [cce-7-2] eliminated 1 clauses out of 1705 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 6 large clauses in 382365 steps
c [cce-7-2] allowing another 191182 steps for small clauses
c [cce-7-2] scheduling 1587 clauses = 552 binary + 1035 ternary
c [cce-7-2] tried to eliminate 1587 small clauses 100%
c [cce-7-2] eliminated 1 ternary clauses 0%
c [cce-7-2] eliminated 1 small clauses 0%
c [cce-7-2] eliminated 1 small clauses in 393239 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 7 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 186739 steps for small clauses
c [cce-7-3] scheduling 1586 clauses = 552 binary + 1034 ternary
c [cce-7-3] tried to eliminate 1586 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 126 covered clauses in TOTAL during 3 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 900 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3659565120 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 15 variables 2% in round 1 in 565749 steps
c [elim-8-1] backward subsumption/strengthening limit 565700
c [elim-8-1-1] backward checking 67 touched variables 7%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 21996 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 15 = 2% variables out of 900 scheduled
c [sweep-8] limit 2744673 penalty 0 = 0 + 0
c [sweep-8-1] 198 pos 33.1% + 401 neg 66.9% = 599 sched 67.7% ret 286
c [sweep-8-1] 1836425 steps 78 queries 14.53 avg class size
c [sweep-8-1] 3531 decisions 72 SAT calls 238.85 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-30] removed 21 variables
c [sweep-8-1] removed 21 vars (0 failed, 18 eqs, 6 impls)
c [sweep-8-2] 304 pos 35.2% + 560 neg 64.8% = 864 sched 100.0% ret 0
c [sweep-8-2] 1007484 steps 23 queries 60.35 avg class size
c [sweep-8-2] 1459 decisions 22 SAT calls 288.86 avg env size
c [sweep-8-2] 436 variables remain 50% (428 retained 50%)
c [sweep-8-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 21 vars in TOTAL (2 rounds, 99 queries)
c [sort-queue-10] sorted 864 enqueued variables after 197081 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 864 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 42 variables 4.6% (864 remain 15%)
c [simplification-10] removed 233 irredundant clauses 4.6% (4859 remain 29%)
c [simplification-10] maximum reduction of 5% = max (5%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 209081 (soft 199081 + delta 10000)
c [simplification-10] new conflict limit 199081 (hard 209081)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.9     863     4859    202859   55034   2247   340   14    71   14  20%    866   -5   15   13  112%
c i   31.9     862     4859    202865   55035   2247   341   14    71   14  20%    853   -5   15   13  110%
c 
c [simplification-11] limit 199082 conflicts (hard 209081) hit after 209082 conflicts
c [quatres-8] found 3585 quaternary clauses 29% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 25 single-self-subsuming ternary resolvents
c [quatres-8-2] added 35 quaternary resolvents
c [ternres-8] limit 9710694 with penalty 0 = 0 + 0
c [ternres-8] all 862 free variables schedulable
c [ternres-8] 293 ternary resolvents (40 bin, 253 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 1421 xors of average arity 3.6
c [gauss-4] connected 5051 occurrences of 380 variables (average 13.3)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 2 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 44 transitive binary clauses
c [transred-8] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 485534730 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 34 clauses out of 1674 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 34 large clauses in 218833 steps
c [cce-8-1] allowing another 109416 steps for small clauses
c [cce-8-1] scheduling 1832 clauses = 530 binary + 1302 ternary
c [cce-8-1] tried to eliminate 1832 small clauses 100%
c [cce-8-1] eliminated 51 ternary clauses 4%
c [cce-8-1] eliminated 51 small clauses 3%
c [cce-8-1] eliminated 60 small clauses in 310089 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 94 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 107762 steps for small clauses
c [cce-8-2] scheduling 1781 clauses = 530 binary + 1251 ternary
c [cce-8-2] tried to eliminate 1781 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 94 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 859 variables 100%
c [elim-9] limit of 194213894 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 18 variables 2% in round 1 in 539459 steps
c [elim-9-1] backward subsumption/strengthening limit 539400
c [elim-9-1-1] backward checking 68 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 2 clauses in 18117 steps
c [elim-9-1] rescheduled 6 variables 1% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 9218 steps
c [elim-9-2] backward subsumption/strengthening limit 9200
c [elim-9-2-1] backward checking 8 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 6393 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 19 = 2% variables out of 859 scheduled
c [sweep-9] limit 2913208 penalty 0 = 0 + 0
c [sweep-9-1] 166 pos 39.6% + 253 neg 60.4% = 419 sched 49.9% ret 421
c [sweep-9-1] 2118858 steps 54 queries 15.24 avg class size
c [sweep-9-1] 2954 decisions 52 SAT calls 242.29 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-33] removed 2 variables
c [sweep-9-1] removed 2 vars (0 failed, 4 eqs, 1 impls)
c [sweep-9-2] 331 pos 39.5% + 507 neg 60.5% = 838 sched 100.0% ret 0
c [sweep-9-2] 835786 steps 17 queries 82.18 avg class size
c [sweep-9-2] 1340 decisions 16 SAT calls 336.94 avg env size
c [sweep-9-2] 560 variables remain 67% (278 retained 33%)
c [decomp-34] removed 2 variables
c [sweep-9-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9] removed 4 vars in TOTAL (2 rounds, 69 queries)
c [sort-queue-11] sorted 836 enqueued variables after 209082 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 836 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 26 variables 3.0% (836 remain 15%)
c [simplification-11] removed 220 irredundant clauses 4.5% (4639 remain 28%)
c [simplification-11] maximum reduction of 5% = max (3%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2090 = min (209082/100, 53331)
c [simplification-11] penalized conflict interval 2090 = 1 * 2090
c [simplification-11] hard conflict limit 221172 (soft 211172 + delta 10000)
c [simplification-11] new conflict limit 211172 (hard 221172)
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 -   33.9     836     4639    215540   32138   2501   332   14    66    5  22%   -964  -10   15   13  110%
c 
c [simplification-12] limit 211172 conflicts (hard 221172) hit after 221173 conflicts
c [quatres-9] found 3565 quaternary clauses 28% in total
c [quatres-9-1] removed 4 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 32 quaternary resolvents
c [ternres-9] limit 10211134 with penalty 0 = 0 + 0
c [ternres-9] all 836 free variables schedulable
c [ternres-9] 135 ternary resolvents (33 bin, 102 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-35] removed 4 variables
c [basicprobe-3] limit 12763917 penalty 2 = 2 + 0
c [basicprobe-3-0] 448 sched 54%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-1] 447 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 3 hbrs
c [bate-2] eliminated 3 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 42 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 832 variables 100%
c [block-4] limit of 12763917 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 3 blocked clauses
c [block-4] 3 < 1/100 * 4633 = 46 considered unsuccessful
c [cce-9] limit of 51055671 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 24 (4%) of length 7
c [cce-9-1] eliminated 2 clauses out of 215 (1%) of length 5
c [cce-9-1] eliminated 17 clauses out of 1650 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 20 large clauses in 312901 steps
c [cce-9-1] allowing another 156450 steps for small clauses
c [cce-9-1] scheduling 1711 clauses = 511 binary + 1200 ternary
c [cce-9-1] tried to eliminate 1711 small clauses 100%
c [cce-9-1] eliminated 2 binary clauses 0%
c [cce-9-1] eliminated 5 ternary clauses 0%
c [cce-9-1] eliminated 7 small clauses 0%
c [cce-9-1] eliminated 7 small clauses in 378012 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 27 covered clauses in round 1
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] allowing another 154723 steps for small clauses
c [cce-9-2] scheduling 1704 clauses = 509 binary + 1195 ternary
c [cce-9-2] tried to eliminate 1704 small clauses 100%
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 0 covered clauses in round 2
c [cce-9] eliminated 27 covered clauses in TOTAL during 2 rounds
c [cce-9] 27 < 1/100 * 4630 = 46 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 832 variables 100%
c [elim-10] limit of 204222684 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 5 variables 1% in round 1 in 528533 steps
c [elim-10-1] backward subsumption/strengthening limit 528500
c [elim-10-1-1] backward checking 44 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 1 clauses in 16267 steps
c [elim-10-1] rescheduled 4 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 13609 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 5 = 1% variables out of 832 scheduled
c [elim-10] 5 < 1/100 * 832 = 8 considered unsuccessful
c [bca-4] limit of 10000000 steps and 9656 added (scaled 2)
c [bca-4] 0 out of 1656 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 35921 steps
c [sweep-10] limit 3063340 penalty 0 = 0 + 0
c [sweep-10-1] 201 pos 36.3% + 353 neg 63.7% = 554 sched 67.0% ret 273
c [sweep-10-1] 1366801 steps 72 queries 11.60 avg class size
c [sweep-10-1] 2430 decisions 71 SAT calls 159.48 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-37] removed 6 variables
c [sweep-10-1] removed 6 vars (0 failed, 8 eqs, 2 impls)
c [sweep-10-2] 294 pos 35.8% + 527 neg 64.2% = 821 sched 100.0% ret 0
c [sweep-10-2] 1729899 steps 73 queries 21.26 avg class size
c [sweep-10-2] 3202 decisions 74 SAT calls 194.59 avg env size
c [sweep-10-2] 58 variables remain 7% (763 retained 93%)
c [decomp-38] removed 14 variables
c [sweep-10-2] removed 14 vars (0 failed, 11 eqs, 3 impls)
c [sweep-10] removed 20 vars in TOTAL (2 rounds, 143 queries)
c [sort-queue-12] sorted 807 enqueued variables after 221173 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 807 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 29 variables 3.5% (807 remain 14%)
c [simplification-12] removed 69 irredundant clauses 1.5% (4570 remain 28%)
c [simplification-12] maximum reduction of 3% = max (3%, 1%)
c [simplification-12] geometric conflict interval increment 13332 = 53331 / 4
c [simplification-12] new conflict interval 66663
c [simplification-12] penalized conflict interval 66663 = 1 * 66663
c [simplification-12] hard conflict limit 321167 (soft 287836 + delta 33331)
c [simplification-12] new conflict limit 287836 (hard 321167)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   34.7     806     4570    221725   36872   2447   310   15    70    7  21%   -785   -4   16   14  115%
c -   37.5     806     4570    251898   35481   2533   326   13    60    6  22%   -306  -11   11   14   78%
c -   40.5     806     4570    285956   37081   2605   338   15    73    6  20%    233    3   14   14   98%
c 
c [simplification-13] limit 287836 conflicts (hard 321167) hit after 289206 conflicts
c [quatres-10] found 3868 quaternary clauses 25% in total
c [quatres-10-1] removed 6 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 32 single-self-subsuming ternary resolvents
c [quatres-10-2] added 71 quaternary resolvents
c [ternres-10] limit 12939371 with penalty 0 = 0 + 0
c [ternres-10] all 806 free variables schedulable
c [ternres-10] 198 ternary resolvents (30 bin, 168 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-39] removed 13 variables
c [simpleprobe-4] all 794 free variables schedulable
c [simpleprobe-4] limit 51757484 penalty 0 = 0 + 0
c [decomp-40] removed 3 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 3 variables, found 12 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 53 transitive binary clauses
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 38818110 penalty 0 = 0 + 0
c [sweep-11-1] 18 pos 34.6% + 34 neg 65.4% = 52 sched 6.6% ret 739
c [sweep-11-1] 579004 steps 26 queries 6.31 avg class size
c [sweep-11-1] 870 decisions 24 SAT calls 165.62 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-41] removed 2 variables
c [sweep-11-1] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-11-2] 329 pos 41.7% + 460 neg 58.3% = 789 sched 100.0% ret 0
c [sweep-11-2] 1687139 steps 70 queries 17.64 avg class size
c [sweep-11-2] 2468 decisions 67 SAT calls 162.30 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-42] removed 15 variables
c [sweep-11-2] removed 15 vars (0 failed, 14 eqs, 5 impls)
c [sweep-11-3] 321 pos 41.5% + 453 neg 58.5% = 774 sched 100.0% ret 0
c [sweep-11-3] 1397836 steps 59 queries 20.44 avg class size
c [sweep-11-3] 2213 decisions 57 SAT calls 147.98 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-43] removed 4 variables
c [sweep-11-3] removed 4 vars (0 failed, 4 eqs, 1 impls)
c [sweep-11] removed 21 vars in TOTAL (3 rounds, 152 queries)
c [sort-queue-13] sorted 770 enqueued variables after 289206 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 770 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 36 variables 4.5% (770 remain 14%)
c [simplification-13] removed 43 irredundant clauses 0.9% (4527 remain 27%)
c [simplification-13] maximum reduction of 4% = max (4%, 1%)
c [simplification-13] geometric conflict interval increment 13332 = 66663 / 5
c [simplification-13] new conflict interval 79995
c [simplification-13] penalized conflict interval 79995 = 1 * 79995
c [simplification-13] hard conflict limit 409198 (soft 369201 + delta 39997)
c [simplification-13] new conflict limit 369201 (hard 409198)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   43.4     769     4523    311733   61551   2625   295   15    75   11  20%    490    4   16   14  112%
c -   44.5     769     4523    321348   36871   2648   296   14    66    6  21%   -671   -4   12   14   84%
c -   48.4     769     4522    359197   40431   2698   309   15    62    9  24%     73   -6   14   14  101%
c i   49.6     768     4522    373177   54139   2720   310   15    63   13  24%    256   -4   16   14  115%
c -   52.4     765     4522    396233   42869   2767   314   13    49    6  26%   -203  -15   15   14  105%
c 
c [simplification-14] limit 369201 conflicts (hard 409198) hit after 409199 conflicts
c [quatres-11] found 4123 quaternary clauses 21% in total
c [quatres-11-1] removed 14 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 25 single-self-subsuming ternary resolvents
c [quatres-11-2] added 48 quaternary resolvents
c [ternres-11] limit 18622509 with penalty 0 = 0 + 0
c [ternres-11] all 765 free variables schedulable
c [ternres-11] 210 ternary resolvents (35 bin, 175 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-5] limit 931125 penalty 2 = 2 + 0
c [gauss-5] extracted 1495 xors of average arity 3.5
c [gauss-5] connected 5211 occurrences of 358 variables (average 14.6)
c [gauss-5] limit 931125 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-44] removed 5 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 42 transitive binary clauses
c [cce-10] limit of 46556274 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 1 clauses out of 18 (6%) of length 6
c [cce-10-1] eliminated 20 clauses out of 149 (13%) of length 5
c [cce-10-1] eliminated 125 clauses out of 1619 (8%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 146 large clauses in 194037 steps
c [cce-10-1] allowing another 97018 steps for small clauses
c [cce-10-1] scheduling 1693 clauses = 505 binary + 1188 ternary
c [cce-10-1] tried to eliminate 1693 small clauses 100%
c [cce-10-1] eliminated 1 binary clauses 0%
c [cce-10-1] eliminated 55 ternary clauses 5%
c [cce-10-1] eliminated 56 small clauses 3%
c [cce-10-1] eliminated 56 small clauses in 281578 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 202 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 92166 steps for small clauses
c [cce-10-2] scheduling 1637 clauses = 504 binary + 1133 ternary
c [cce-10-2] tried to eliminate 1637 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 202 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 760 variables 100%
c [elim-11] limit of 186225096 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 32 variables 4% in round 1 in 480991 steps
c [elim-11-1] backward subsumption/strengthening limit 480900
c [elim-11-1-1] backward checking 131 touched variables 17%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 2 clauses in 27874 steps
c [elim-11-1] rescheduled 4 variables 1% by backward subsumption
c [elim-11-2] eliminated 4 variables 1% in round 2 in 748 steps
c [elim-11-2] backward subsumption/strengthening limit 700
c [elim-11-2-1] backward checking 11 touched variables 1%
c [elim-11-2-1] incomplete backward checking 5 remain 45%
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 721 steps
c [elim-11-2] fully rescheduled 724 variables 95%
c [elim-11-3] eliminated 3 variables 0% in round 3 in 473729 steps
c [elim-11-3] backward subsumption/strengthening limit 473700
c [elim-11-3-1] backward checking 25 touched variables 3%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 9332 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 39 = 5% variables out of 760 scheduled
c [sweep-12] limit 5586752 penalty 0 = 0 + 0
c [sweep-12-1] 253 pos 35.1% + 468 neg 64.9% = 721 sched 100.0% ret 0
c [sweep-12-1] 2746400 steps 64 queries 24.77 avg class size
c [sweep-12-1] 2602 decisions 61 SAT calls 146.95 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-45] removed 5 variables
c [sweep-12-1] removed 5 vars (0 failed, 4 eqs, 3 impls)
c [sweep-12-2] 249 pos 34.8% + 467 neg 65.2% = 716 sched 100.0% ret 0
c [sweep-12-2] 2887059 steps 50 queries 23.90 avg class size
c [sweep-12-2] 2509 decisions 50 SAT calls 160.52 avg env size
c [sweep-12-2] 37 variables remain 5% (679 retained 95%)
c [decomp-46] removed 2 variables
c [sweep-12-2] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-12] removed 7 vars in TOTAL (2 rounds, 112 queries)
c [sort-queue-14] sorted 714 enqueued variables after 409199 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 714 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 51 variables 6.7% (714 remain 13%)
c [simplification-14] removed 443 irredundant clauses 9.8% (4079 remain 25%)
c [simplification-14] maximum reduction of 10% = max (7%, 10%)
c [simplification-14] large reduction 10% >= 5% limit
c [simplification-14] next conflict interval 4091 = min (409199/100, 79995)
c [simplification-14] penalized conflict interval 4091 = 1 * 4091
c [simplification-14] hard conflict limit 423290 (soft 413290 + delta 10000)
c [simplification-14] new conflict limit 413290 (hard 423290)
c 
c [simplification-15] limit 413290 conflicts (hard 423290) hit after 423293 conflicts
c [quatres-12] found 3897 quaternary clauses 22% in total
c [quatres-12-1] removed 11 duplicate quaternary clauses
c [quatres-12-2] added 19 single-self-subsuming ternary resolvents
c [quatres-12-2] added 21 quaternary resolvents
c [ternres-12] limit 19376605 with penalty 0 = 0 + 0
c [ternres-12] all 714 free variables schedulable
c [ternres-12] 104 ternary resolvents (32 bin, 72 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 605518 penalty 4 = 4 + 0
c [card-5] no at-most-one constraint found
c [card-5] found 97 at-most-two constraints of average size 4.0
c [card-5] using previous limit 605518 for elimination
c [card-5] 91 out of 97 constraints (94%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [treelook-4] limit 968830 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 1428 literals 100%
c [treelook-4] scheduling used 197089 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 968830 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 135950 steps
c [treelook-4] fully completed tree based probing
c [unhide-5] limit 242207 with penalty 4 = 4 + 0
c [unhide-5-6] 0 units, 0 failed, 239 tauts, 0 hbrs, 20041 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 16 transitive binary clauses
c [cce-11] limit of 96883026 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 7
c [cce-11-1] eliminated 10 clauses out of 21 (48%) of length 6
c [cce-11-1] eliminated 23 clauses out of 160 (14%) of length 5
c [cce-11-1] eliminated 54 clauses out of 1471 (4%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 88 large clauses in 237417 steps
c [cce-11-1] allowing another 118708 steps for small clauses
c [cce-11-1] scheduling 1426 clauses = 456 binary + 970 ternary
c [cce-11-1] tried to eliminate 1426 small clauses 100%
c [cce-11-1] eliminated 4 binary clauses 1%
c [cce-11-1] eliminated 48 ternary clauses 5%
c [cce-11-1] eliminated 52 small clauses 4%
c [cce-11-1] eliminated 52 small clauses in 301087 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 140 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 11 (9%) of length 6
c [cce-11-2] eliminated 18 clauses out of 1417 (1%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 19 large clauses in 228077 steps
c [cce-11-2] allowing another 114038 steps for small clauses
c [cce-11-2] scheduling 1374 clauses = 452 binary + 922 ternary
c [cce-11-2] tried to eliminate 1374 small clauses 100%
c [cce-11-2] eliminated 1 binary clauses 0%
c [cce-11-2] eliminated 1 small clauses 0%
c [cce-11-2] eliminated 1 small clauses in 285760 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 20 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 113000 steps for small clauses
c [cce-11-3] scheduling 1373 clauses = 451 binary + 922 ternary
c [cce-11-3] tried to eliminate 1373 small clauses 100%
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 0 covered clauses in round 3
c [cce-11] eliminated 160 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 714 variables 100%
c [elim-12] limit of 387532105 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 83 variables 12% in round 1 in 415505 steps
c [elim-12-1] backward subsumption/strengthening limit 415500
c [elim-12-1-1] backward checking 97 touched variables 14%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 16787 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 83 = 12% variables out of 714 scheduled
c [sweep-13] limit 5812981 penalty 0 = 0 + 0
c [sweep-13-1] 4 pos 14.3% + 24 neg 85.7% = 28 sched 4.4% ret 603
c [sweep-13-1] 962991 steps 17 queries 4.47 avg class size
c [sweep-13-1] 559 decisions 16 SAT calls 124.62 avg env size
c [sweep-13-1] fully completed sweeping round
c [sweep-13-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13-2] 223 pos 35.3% + 408 neg 64.7% = 631 sched 100.0% ret 0
c [sweep-13-2] 5038650 steps 37 queries 33.38 avg class size
c [sweep-13-2] 2327 decisions 35 SAT calls 175.74 avg env size
c [sweep-13-2] 114 variables remain 18% (517 retained 82%)
c [decomp-49] removed 2 variables
c [sweep-13-2] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-13] removed 2 vars in TOTAL (2 rounds, 52 queries)
c [sort-queue-15] sorted 629 enqueued variables after 423293 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 629 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 85 variables 11.9% (629 remain 11%)
c [simplification-15] removed 526 irredundant clauses 12.9% (3553 remain 22%)
c [simplification-15] maximum reduction of 13% = max (12%, 13%)
c [simplification-15] large reduction 13% >= 5% limit
c [simplification-15] next conflict interval 4232 = min (423293/100, 79995)
c [simplification-15] penalized conflict interval 4232 = 1 * 4232
c [simplification-15] hard conflict limit 437525 (soft 427525 + delta 10000)
c [simplification-15] new conflict limit 427525 (hard 437525)
c 
c [simplification-16] limit 427525 conflicts (hard 437525) hit after 437529 conflicts
c [quatres-13] found 3411 quaternary clauses 22% in total
c [quatres-13-1] removed 6 duplicate quaternary clauses
c [quatres-13-2] added 12 single-self-subsuming ternary resolvents
c [quatres-13-2] added 18 quaternary resolvents
c [ternres-13] limit 20299268 with penalty 0 = 0 + 0
c [ternres-13] all 629 free variables schedulable
c [ternres-13] 160 ternary resolvents (24 bin, 136 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-6] limit 2029926 penalty 1 = 1 + 0
c [gauss-6] extracted 995 xors of average arity 3.4
c [gauss-6] connected 3381 occurrences of 210 variables (average 16.1)
c [gauss-6] limit 2029926 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 26 transitive binary clauses
c [cce-12] limit of 101496341 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 4 clauses out of 7 (57%) of length 7
c [cce-12-1] eliminated 4 clauses out of 13 (31%) of length 6
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 8 large clauses in 170977 steps
c [cce-12-1] allowing another 85488 steps for small clauses
c [cce-12-1] scheduling 1276 clauses = 404 binary + 872 ternary
c [cce-12-1] tried to eliminate 1276 small clauses 100%
c [cce-12-1] eliminated 6 ternary clauses 1%
c [cce-12-1] eliminated 6 small clauses 0%
c [cce-12-1] eliminated 6 small clauses in 231137 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 14 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 84982 steps for small clauses
c [cce-12-2] scheduling 1270 clauses = 404 binary + 866 ternary
c [cce-12-2] tried to eliminate 1270 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 14 covered clauses in TOTAL during 2 rounds
c [cce-12] 14 < 1/100 * 3551 = 35 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 629 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 31 variables 5% in round 1 in 400970 steps
c [elim-13-1] backward subsumption/strengthening limit 400900
c [elim-13-1-1] backward checking 71 touched variables 11%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 6 clauses in 13042 steps
c [elim-13-1] rescheduled 9 variables 1% by backward subsumption
c [elim-13-2] eliminated 4 variables 1% in round 2 in 3492 steps
c [elim-13-2] backward subsumption/strengthening limit 3400
c [elim-13-2-1] backward checking 21 touched variables 3%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 3401 steps
c [elim-13-2] fully rescheduled 594 variables 94%
c [elim-13-3] eliminated 15 variables 2% in round 3 in 384866 steps
c [elim-13-3] backward subsumption/strengthening limit 384800
c [elim-13-3-1] backward checking 55 touched variables 9%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 0 and strengthened 0 clauses in 10756 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 50 = 8% variables out of 629 scheduled
c [sweep-14] limit 6089780 penalty 0 = 0 + 0
c [sweep-14-1] 23 pos 24.0% + 73 neg 76.0% = 96 sched 16.6% ret 483
c [sweep-14-1] 2462070 steps 30 queries 7.20 avg class size
c [sweep-14-1] 1087 decisions 27 SAT calls 123.00 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-51] removed 2 variables
c [sweep-14-1] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-14-2] 172 pos 29.8% + 405 neg 70.2% = 577 sched 100.0% ret 0
c [sweep-14-2] 4055548 steps 11 queries 85.00 avg class size
c [sweep-14-2] 1155 decisions 10 SAT calls 314.00 avg env size
c [sweep-14-2] 370 variables remain 64% (207 retained 36%)
c [sweep-14-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 2 vars in TOTAL (2 rounds, 39 queries)
c [sort-queue-16] sorted 577 enqueued variables after 437529 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 577 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 52 variables 8.3% (577 remain 10%)
c [simplification-16] removed 288 irredundant clauses 8.1% (3265 remain 20%)
c [simplification-16] maximum reduction of 8% = max (8%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 4375 = min (437529/100, 79995)
c [simplification-16] penalized conflict interval 4375 = 1 * 4375
c [simplification-16] hard conflict limit 451904 (soft 441904 + delta 10000)
c [simplification-16] new conflict limit 441904 (hard 451904)
c 
c [simplification-17] limit 441904 conflicts (hard 451904) hit after 451905 conflicts
c [quatres-14] found 3119 quaternary clauses 22% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 14 quaternary resolvents
c [ternres-14] limit 21165283 with penalty 0 = 0 + 0
c [ternres-14] all 577 free variables schedulable
c [ternres-14] 36 ternary resolvents (20 bin, 16 trn)
c [ternres-14] fully completed ternary resolution
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 25 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 577 variables 100%
c [block-5] limit of 13228302 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 22 blocked clauses
c [block-5] 22 < 1/100 * 3256 = 32 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 575 variables 100%
c [elim-14] limit of 423305676 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 14 variables 2% in round 1 in 374710 steps
c [elim-14-1] backward subsumption/strengthening limit 374700
c [elim-14-1-1] backward checking 49 touched variables 9%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 1 clauses in 11177 steps
c [elim-14-1] rescheduled 5 variables 1% by backward subsumption
c [elim-14-2] eliminated 5 variables 1% in round 2 in 492 steps
c [elim-14-2] backward subsumption/strengthening limit 400
c [elim-14-2-1] backward checking 11 touched variables 2%
c [elim-14-2-1] incomplete backward checking 5 remain 45%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 401 steps
c [elim-14-2] fully rescheduled 556 variables 97%
c [elim-14-3] eliminated 12 variables 2% in round 3 in 359947 steps
c [elim-14-3] backward subsumption/strengthening limit 359900
c [elim-14-3-1] backward checking 37 touched variables 6%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 6 and strengthened 0 clauses in 5928 steps
c [elim-14] incomplete 7 not tried 1% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 31 = 5% variables out of 575 scheduled
c [bca-5] limit of 10000000 steps and 6646 added (scaled 2)
c [bca-5] 1 out of 1090 literals actually usable 0%
c [bca-5] not enough literals usable
c [bca-5] added 0 blocked clauses in 63204 steps
c [sweep-15] limit 6349585 penalty 0 = 0 + 0
c [sweep-15-1] 107 pos 31.7% + 231 neg 68.3% = 338 sched 62.1% ret 206
c [sweep-15-1] 7044855 steps 31 queries 25.19 avg class size
c [sweep-15-1] 1893 decisions 30 SAT calls 170.03 avg env size
c [sweep-15-1] 70 variables remain 13% (474 retained 87%)
c [sweep-15-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] removed 0 vars in TOTAL (1 rounds, 30 queries)
c [sort-queue-17] sorted 544 enqueued variables after 451905 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 544 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 33 variables 5.7% (544 remain 10%)
c [simplification-17] removed 192 irredundant clauses 5.9% (3073 remain 19%)
c [simplification-17] maximum reduction of 6% = max (6%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 4519 = min (451905/100, 79995)
c [simplification-17] penalized conflict interval 4519 = 1 * 4519
c [simplification-17] hard conflict limit 466424 (soft 456424 + delta 10000)
c [simplification-17] new conflict limit 456424 (hard 466424)
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 -   61.8     544     3073    459670   37496   2123   207   10    27    6  38%    558  -24    8   13   61%
c 
c [simplification-18] limit 456424 conflicts (hard 466424) hit after 466424 conflicts
c [quatres-15] found 2966 quaternary clauses 21% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 4 single-self-subsuming ternary resolvents
c [quatres-15-2] added 12 quaternary resolvents
c [ternres-15] limit 22082204 with penalty 0 = 0 + 0
c [ternres-15] all 544 free variables schedulable
c [ternres-15] 42 ternary resolvents (20 bin, 22 trn)
c [ternres-15] fully completed ternary resolution
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 21 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 552055105 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 11 clauses out of 11 (100%) of length 9
c [cce-13-1] eliminated 3 clauses out of 5 (60%) of length 8
c [cce-13-1] eliminated 4 clauses out of 6 (67%) of length 7
c [cce-13-1] eliminated 3 clauses out of 9 (33%) of length 6
c [cce-13-1] eliminated 9 clauses out of 122 (7%) of length 5
c [cce-13-1] eliminated 46 clauses out of 1108 (4%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 76 large clauses in 198056 steps
c [cce-13-1] allowing another 99028 steps for small clauses
c [cce-13-1] scheduling 1045 clauses = 348 binary + 697 ternary
c [cce-13-1] tried to eliminate 1045 small clauses 100%
c [cce-13-1] eliminated 6 binary clauses 2%
c [cce-13-1] eliminated 28 ternary clauses 4%
c [cce-13-1] eliminated 34 small clauses 3%
c [cce-13-1] eliminated 34 small clauses in 229832 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 110 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-13-2] eliminated 1 clauses out of 6 (17%) of length 6
c [cce-13-2] eliminated 7 clauses out of 113 (6%) of length 5
c [cce-13-2] eliminated 6 clauses out of 1062 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 15 large clauses in 178130 steps
c [cce-13-2] allowing another 89065 steps for small clauses
c [cce-13-2] scheduling 1011 clauses = 342 binary + 669 ternary
c [cce-13-2] tried to eliminate 1011 small clauses 100%
c [cce-13-2] eliminated 1 binary clauses 0%
c [cce-13-2] eliminated 7 ternary clauses 1%
c [cce-13-2] eliminated 8 small clauses 1%
c [cce-13-2] eliminated 8 small clauses in 217109 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 23 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 106 (1%) of length 5
c [cce-13-3] eliminated 1 clauses out of 1056 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 2 large clauses in 172923 steps
c [cce-13-3] allowing another 86461 steps for small clauses
c [cce-13-3] scheduling 1003 clauses = 341 binary + 662 ternary
c [cce-13-3] tried to eliminate 1003 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 2 covered clauses in round 3
c [cce-13] eliminated 135 covered clauses in TOTAL during 3 rounds
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 544 variables 100%
c [elim-15] limit of 441644086 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 68 variables 12% in round 1 in 306730 steps
c [elim-15-1] backward subsumption/strengthening limit 306700
c [elim-15-1-1] backward checking 97 touched variables 18%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 0 clauses in 9559 steps
c [elim-15-1] rescheduled 11 variables 2% by backward subsumption
c [elim-15-2] eliminated 8 variables 1% in round 2 in 4528 steps
c [elim-15-2] backward subsumption/strengthening limit 4500
c [elim-15-2-1] backward checking 16 touched variables 3%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 3 and strengthened 0 clauses in 4501 steps
c [elim-15-2] rescheduled 10 variables 2% by backward subsumption
c [elim-15-3] eliminated 5 variables 1% in round 3 in 8768 steps
c [elim-15-3] backward subsumption/strengthening limit 8700
c [elim-15-3-1] backward checking 27 touched variables 5%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 3 and strengthened 5 clauses in 8701 steps
c [elim-15] incomplete 11 not tried 2% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 81 = 15% variables out of 544 scheduled
c [sort-queue-18] sorted 463 enqueued variables after 466424 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 463 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 81 variables 14.9% (463 remain 8%)
c [simplification-18] removed 523 irredundant clauses 17.0% (2550 remain 15%)
c [simplification-18] maximum reduction of 17% = max (15%, 17%)
c [simplification-18] large reduction 17% >= 5% limit
c [simplification-18] next conflict interval 4664 = min (466424/100, 79995)
c [simplification-18] penalized conflict interval 4664 = 1 * 4664
c [simplification-18] hard conflict limit 481088 (soft 471088 + delta 10000)
c [simplification-18] new conflict limit 471088 (hard 481088)
c 
c [simplification-19] limit 471088 conflicts (hard 481088) hit after 481092 conflicts
c [quatres-16] found 2568 quaternary clauses 20% in total
c [quatres-16-1] removed 3 duplicate quaternary clauses
c [quatres-16-2] added 2 single-self-subsuming ternary resolvents
c [quatres-16-2] added 8 quaternary resolvents
c [ternres-16] limit 23040930 with penalty 0 = 0 + 0
c [ternres-16] all 463 free variables schedulable
c [ternres-16] 36 ternary resolvents (18 bin, 18 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-7] limit 1152046 penalty 2 = 2 + 0
c [gauss-7] extracted 746 xors of average arity 3.4
c [gauss-7] connected 2534 occurrences of 149 variables (average 17.0)
c [gauss-7] limit 1152046 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [basicprobe-4] limit 14400581 penalty 3 = 3 + 0
c [basicprobe-4-0] 255 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-0] fully completed probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 22 transitive binary clauses
c [cce-14] limit of 115204654 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 1 large clauses in 119159 steps
c [cce-14-1] allowing another 59579 steps for small clauses
c [cce-14-1] scheduling 952 clauses = 295 binary + 657 ternary
c [cce-14-1] tried to eliminate 952 small clauses 100%
c [cce-14-1] eliminated 1 binary clauses 0%
c [cce-14-1] eliminated 6 ternary clauses 1%
c [cce-14-1] eliminated 7 small clauses 1%
c [cce-14-1] eliminated 7 small clauses in 162747 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 8 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 59520 steps for small clauses
c [cce-14-2] scheduling 945 clauses = 294 binary + 651 ternary
c [cce-14-2] tried to eliminate 945 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 8 covered clauses in TOTAL during 2 rounds
c [cce-14] 8 < 1/100 * 2549 = 25 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 463 variables 100%
c [elim-16] limit of 460818617 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 48 variables 10% in round 1 in 271581 steps
c [elim-16-1] backward subsumption/strengthening limit 271500
c [elim-16-1-1] backward checking 76 touched variables 16%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 4 clauses in 6576 steps
c [elim-16-1] rescheduled 14 variables 3% by backward subsumption
c [elim-16-2] eliminated 4 variables 1% in round 2 in 7861 steps
c [elim-16-2] backward subsumption/strengthening limit 7800
c [elim-16-2-1] backward checking 20 touched variables 4%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 4684 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 52 = 11% variables out of 463 scheduled
c [sweep-16] limit 3456139 penalty 1 = 1 + 0
c [sweep-16-1] 14 pos 35.9% + 25 neg 64.1% = 39 sched 9.5% ret 372
c [sweep-16-1] 2996528 steps 14 queries 6.14 avg class size
c [sweep-16-1] 964 decisions 13 SAT calls 184.46 avg env size
c [sweep-16-1] fully completed sweeping round
c [sweep-16-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16-2] 167 pos 40.6% + 244 neg 59.4% = 411 sched 100.0% ret 0
c [sweep-16-2] 869127 steps 2 queries 205.50 avg class size
c [sweep-16-2] 150 decisions 1 SAT calls 280.00 avg env size
c [sweep-16-2] 411 variables remain 100% (0 retained 0%)
c [sweep-16-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-16] removed 0 vars in TOTAL (2 rounds, 14 queries)
c [sort-queue-19] sorted 411 enqueued variables after 481092 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 411 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 52 variables 11.2% (411 remain 7%)
c [simplification-19] removed 259 irredundant clauses 10.2% (2291 remain 14%)
c [simplification-19] maximum reduction of 11% = max (11%, 10%)
c [simplification-19] large reduction 11% >= 5% limit
c [simplification-19] next conflict interval 4810 = min (481092/100, 79995)
c [simplification-19] penalized conflict interval 4810 = 1 * 4810
c [simplification-19] hard conflict limit 495902 (soft 485902 + delta 10000)
c [simplification-19] new conflict limit 485902 (hard 495902)
c 
c [simplification-20] limit 485902 conflicts (hard 495902) hit after 495903 conflicts
c [quatres-17] found 2369 quaternary clauses 18% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 5 single-self-subsuming ternary resolvents
c [quatres-17-2] added 27 quaternary resolvents
c [ternres-17] limit 24299527 with penalty 0 = 0 + 0
c [ternres-17] all 411 free variables schedulable
c [ternres-17] 36 ternary resolvents (14 bin, 22 trn)
c [ternres-17] fully completed ternary resolution
c [simpleprobe-5] all 411 free variables schedulable
c [simpleprobe-5] limit 97198111 penalty 0 = 0 + 0
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 0 variables, found 8 hbrs, 0 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 23 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 411 variables 100%
c [elim-17] limit of 485990559 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 17 variables 4% in round 1 in 249805 steps
c [elim-17-1] backward subsumption/strengthening limit 249800
c [elim-17-1-1] backward checking 31 touched variables 8%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 7 and strengthened 0 clauses in 3561 steps
c [elim-17-1] rescheduled 9 variables 2% by backward subsumption
c [elim-17-2] eliminated 3 variables 1% in round 2 in 2713 steps
c [elim-17-2] backward subsumption/strengthening limit 2700
c [elim-17-2-1] backward checking 18 touched variables 4%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 4 and strengthened 3 clauses in 2701 steps
c [elim-17-2] rescheduled 6 variables 1% by backward subsumption
c [elim-17-3] eliminated 5 variables 1% in round 3 in 1433 steps
c [elim-17-3] backward subsumption/strengthening limit 1400
c [elim-17-3-1] backward checking 14 touched variables 3%
c [elim-17-3-1] incomplete backward checking 12 remain 86%
c [elim-17-3] subsumed 11 and strengthened 10 clauses in 1416 steps
c [elim-17] incomplete 11 not tried 3% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 25 = 6% variables out of 411 scheduled
c [sort-queue-20] sorted 386 enqueued variables after 495903 conflicts
c [score-dist-20] active 0 (0%), one 0 (0%), zero 386 (100%)
c [score-dist-20] max exp 0, different 1 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 25 variables 6.1% (386 remain 7%)
c [simplification-20] removed 164 irredundant clauses 7.2% (2127 remain 13%)
c [simplification-20] maximum reduction of 7% = max (6%, 7%)
c [simplification-20] large reduction 7% >= 5% limit
c [simplification-20] next conflict interval 4959 = min (495903/100, 79995)
c [simplification-20] penalized conflict interval 4959 = 1 * 4959
c [simplification-20] hard conflict limit 510862 (soft 500862 + delta 10000)
c [simplification-20] new conflict limit 500862 (hard 510862)
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 -   67.8     386     2127    498818   38627   1611   153   13    34    6  37%    768   -9   12   13   91%
c 
c [simplification-21] limit 500862 conflicts (hard 510862) hit after 510862 conflicts
c [quatres-18] found 2283 quaternary clauses 17% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-1] added 2 double-self-subsuming ternary resolvents
c [quatres-18-2] added 3 single-self-subsuming ternary resolvents
c [quatres-18-2] added 16 quaternary resolvents
c [ternres-18] limit 25464927 with penalty 0 = 0 + 0
c [ternres-18] all 386 free variables schedulable
c [ternres-18] 25 ternary resolvents (15 bin, 10 trn)
c [ternres-18] fully completed ternary resolution
c [card-6] limit 795778 penalty 4 = 4 + 0
c [card-6] no at-most-one constraint found
c [card-6] found 53 at-most-two constraints of average size 4.0
c [card-6] using previous limit 795778 for elimination
c [card-6] 50 out of 53 constraints (94%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [gauss-8] limit 2546492 penalty 1 = 1 + 0
c [gauss-8] extracted 755 xors of average arity 3.4
c [gauss-8] connected 2537 occurrences of 139 variables (average 18.3)
c [gauss-8] limit 2546492 penalty 1 = 1 + 0
c [gauss-8] proved unsatisfiability
c [simplification-21] removed 0 variables 0.0% (386 remain 7%)
c [simplification-21] removed 0 irredundant clauses 0.0% (2127 remain 13%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 79995
c [simplification-21] new conflict interval 159990
c [simplification-21] penalized conflict interval 159990 = 1 * 159990
c [simplification-21] hard conflict limit 750847 (soft 670852 + delta 79995)
c [simplification-21] new conflict limit 670852 (hard 750847)
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   69.7     386     2127    510862   50207   1636   168   14    30    5  46%    811  -11   14   13  108%
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: 5 basic ate = 5 trn 100% + 0 lrg 0% in 2 updates
c bcas: 5 count, 0 added (0 skipped), 189843 steps
c bkwd: tried 12667 clauses, 25232 lits, 1.99 lits/clause
c bkwd: checked 262793 occs, 20.75 occs/clause, 10.42 occs/lit
c bkwd: subsumed 0 binary, 12 ternary, 42 large
c bkwd: strengthened 7 binary, 2 ternary (100% self), 82 large (0% self)
c blkd: 5 bces, 100 removed, 151407 resolutions, 357822 steps
c blkd: 160 blocking literals 1%, 2 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 6 count, 0 units, 0 am1, 3794412 steps
c card: 1 rescheduled, 6 eliminated, 7316 resolved, 1734 subsumed
c card: 2 at-most-one constraints found, average size 3.00
c card: 2 at-most-one constraints used 100%, average size 3.00
c card: 229 at-most-two constraints found, average size 4.00
c card: 215 at-most-two constraints used 94%, average size 4.00
c cces: 14 cces, 1566 eliminated, 1343 ate 86%, 223 abce 14%
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: 100 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 60 decompositions, 654 equivalent 12%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2627311 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 4546 eliminated 81%, 23 pure 1%
c elms: 50 rounds, 2.9 rounds/bve
c elms: 4447 small 98%, 74 large 2%
c elms: 18570 tried small, 4447 succeeded 24%, 14123 failed 76%
c elms: 666 subsumed, 879 strengthened, 59 blocked
c elms: 619077 copies, 748637 resolutions, 1242646 ipos
c elms: 10126 subchks, 16309 strchks
c gaus: 8 extractions, 11315 extracted, 3.6 size, 4 max
c gaus: exported 0 units, 0 binary and 4 ternary equations
c gaus: 0 gc, 4734492 steps, 2367246 extr 50%, 351523 elim 7%
c glue: 13.6 orig avg, 13.6 real avg, 3.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1215 = 963 simple 79% + 252 trn 21% + 0 lrg 0%, 17 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 524238 clauses, 30.7 length
c lrnd: 16068721 lits = 20294835 orig - 4226114 removed 21%
c lrnd: 192342 uips 37%, 212851 flips 41%
c mins: 512968 mins 98%, 67 bin 0%, 11203 size 2%
c mins: 18940206 poisoned searches, 2588013 hits, 14% hit rate
c mins: 36068975 used twice searches, 3996322 hits, 11% hit rate
c move: moved 653, 81 bin 12%, 572 trn 88%
c otfs: 2179 driving 27%, 5943 restarting 73%
c otfs: str 8122, 8015 red 99%, 107 irr 1%
c otfs: str 8122, 0 bin 0%, 516 trn 6%, 7606 lrg 94%
c otfs: sub 206, 194 red 94%, 12 irr 6%
c otfs: sub 206, 0 bin 0%, 51 trn 25%, 155 lrg 75%
c phas: 1 computed, 1243 set, 242 pos (19%), 1001 neg (81%)
c prbs: 4 basic, 6222 probed, 0 failed, 0 lifted
c prbs: 5 simple, 19878 probed, 6 failed, 686 eqs
c prbs: 4 treelook, 6009 probed, 1 failed, 0 lifted
c prom: 64978 locked 10% out of 621663 tried
c prps: 48546451 props, 18 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 18 count, 930 quat, 554 self1, 21 self2, 333 dup
c queu: 20 sorted, 2627311 next (0 steps 0.00)
c queu: 22666 enq (22645 steps 1.00), 0 deq 0%
c redc: 4719 clauses 6%, 78132 tried 15%, 3 sat 0%
c redc: 5210 lits 1%, 844641 tried 4%, 3 sat 0%
c redc: 130 times jump level reduced, 6.5 levels on average
c reds: 11 count, 46442.0 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 302512 collected 82%, 65703 retired 18%
c rmbd: 23 removed, 21 red 91%
c rsts: 14129 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: 21 count, 21 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 524238 count (240040 tried 0.5), 10783 sub out of 521208 (2.1%)
c swps: 16 count, 30 rounds, 1423 queries (47.4/round)
c swps: 1397 sat calls, 203 unsat (11.1% success rate)
c swps: 74324 decisions 53.2, 15555 conflicts 11.1
c swps; 24.2 avg class size, 215.7 avg environment size
c swps: 0 failed, 82 impls, 225 equivs
c swp0: 465 type 0 queries, 124 unsat (26.7%), 418 sat (89.9%)
c swp1: 958 type 1 queries, 453 unsat (47.3%), 780 sat (81.4%)
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: 5254997 calls to obtain time
c tops: 52 fixed 1%, 6 its, 85143.67 confs/it
c trds: 17 transitive reductions, 643 removed, 1 failed
c trds: 28105 nodes, 13548 edges, 132603 steps
c trim: 70028 words, 0.3 MB
c trnr: 18 count, 559 bin, 3031 trn, 26258298 steps
c unhd: 5 count, 6 rounds, 2408293 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: 895 tauts, 47 bin 5%, 627 trn 70%, 170 lrg 19%
c unhd: 895 tauts, 51 stamp 6%, 894 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 105019 str, 0 bin 0%, 80 trn 0%, 104939 lrg 100%, 104841 red 100%
c vars: 386 remaining 7% and 5252 removed 93% out of 5638
c vars: 52 fixed 1%, 4546 eliminated 81%, 654 equivalent 12%
c vsts: 2608841179 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 53.7 search visits per propagation, 4984.7 per conflict
c wchs: 1086342451 pushed, 1350059 enlarged, 263 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         522138        302512         65703       9121277       3366378        268779
c 
c  0 0         35375   7      1310   0         0   0   5814874  64   1706941  51    102917  38     0.6
c  1 5         23472   4      4707   2      3283   5   1228545  13<   453182  13<    38865  14<    0.4
c  2 6         88247  17     40219  13     12352  19   1267340  14    630421  19     76230  28     1.1
c  3 9        151212  29<   106219  35     17418  27    461015   5    326178  10     36533  14     1.8
c  4 14       136208  26     98993  33<    17277  26<   222743   2    164396   5      9996   4     2.4
c  5 21        66745  13     40935  14     10451  16     97818   1     68180   2      3071   1     1.5
c  6 30        16346   3      8130   3      3626   6     22848   0     13858   0       861   0     0.5
c  7 41         3627   1      1651   1       985   1      4900   0      2661   0       247   0     0.2
c  8 54          776   0       302   0       259   0      1029   0       494   0        51   0     0.1
c  9 69          117   0        45   0        46   0       150   0        64   0         6   0     0.0
c 10 86           13   0         1   0         6   0        15   0         3   0         2   0     0.0
c 
c avg                  3.2           3.5           3.5           0.7           1.1           1.4
c std                  1.5           1.1           1.4           1.2           1.4           1.3
c 
c    2.969   4% sweep
c    1.548   2% decide
c    1.371   2% elim
c    0.897   1% cce
c    0.403   1% unhide
c    0.374   1% probe
c 
c    0.908 < 1% rest (below)
c 
c    0.326   0% quatres
c    0.232   0% gauss
c    0.159   0% ternres
c    0.093   0% block
c    0.058   0% card
c    0.022   0% transred
c    0.018   0% bca
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.258   0% preprocessing     3%
c    7.424  11% inprocessing     97%
c ==================================
c    7.681  11% simplifying
c   61.987  89% search
c ==================================
c   69.668 100% all
c 
c        510862 conflicts,        7332.8 confs/sec
c          2177 ternaries,         234.7 confs/ternary
c            70 binaries,         7298.0 confs/binary
c             6 iterations,      85143.7 confs/iteration
c 
c            11 reductions,          0.2 redus/sec,  46442.0 confs/reduction
c         14129 restarts,          202.8 rests/sec,     36.2 confs/restart
c       2627311 decisions,       37711.7 decis/sec,      5.1 decis/conflict
c      48546451 propagations,   696822.7 props/sec,     18.5 props/decision
c 
c 69.7 seconds, 21.0 MB
c launch: done
