c launch: /data/cnf/sc2014/app/dated-10-11-u.cnf.bz2
c host: atom04
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/dated-10-11-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-11-u.cnf.bz2
c no embedded options
c found 'p cnf 141860 629461' header
c read 141860 variables, 629461 clauses, 1429872 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 135830 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  135830   617431         0       0      0     0    0     0   31   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] found 9985 at-most-one constraints of average size 5.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9985 out of 9985 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 73366 variables
c [simpleprobe-1] all 68494 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 45584 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 45584 variables, found 5600 hbrs, 920 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 625 failed, 4664 tauts, 0 hbrs, 352 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 22330 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 7935 variables 36% in round 1 in 8218579 steps
c [elim-1-1] backward subsumption/strengthening limit 8218500
c [elim-1-1-1] backward checking 14493 touched variables 65%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 73 and strengthened 236 clauses in 1854079 steps
c [elim-1-1] rescheduled 580 variables 3% by backward subsumption
c [elim-1-2] eliminated 167 variables 1% in round 2 in 305123 steps
c [elim-1-2] backward subsumption/strengthening limit 305100
c [elim-1-2-1] backward checking 563 touched variables 3%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 51 and strengthened 44 clauses in 220620 steps
c [elim-1-2] rescheduled 160 variables 1% by backward subsumption
c [elim-1-3] eliminated 44 variables 0% in round 3 in 91627 steps
c [elim-1-3] backward subsumption/strengthening limit 91600
c [elim-1-3-1] backward checking 183 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 36 and strengthened 16 clauses in 91601 steps
c [elim-1] incomplete 101 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 8230 = 37% variables out of 22330 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 98493 negative 99.1% of 99405 except 912 0.9%
c [phase-count-1] 81651 positive 82.1% of 99405 except 17754 17.9%
c [phase-count-1] less non-negative clauses 912 than limit 9900 (10.0%)
c [phase-count-1] non-pos/non-neg = 17754/912 = 19.47 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 14100 negative 100%
c [sort-queue-1] sorted 14100 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 14100 (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 90208 variables 86.5% (14100 remain 10%)
c [simplification-1] removed 518026 irredundant clauses 83.9% (99405 remain 16%)
c [simplification-1] maximum reduction of 86% = max (86%, 84%)
c [simplification-1] large reduction 86% >= 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  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    1.3   14099    99405        12      10      1  3305    0     2   11   1%      0    2    0    0 25039%
c i    1.3   14096    99405        51      43      3  3305    0     2   11   3%      0    2    1    0 23041%
c i    1.3   14093    99405        58      44      6  3307    0     2   11   3%      0    2    1    0 22491%
c i    1.3   14089    99405       143     117      9  3311    0     4   11   6%      0    4    3    0 20287%
c i    1.3   14086    99405       202     166     12  3312    0     4   11   9%      0    4    5    0 19400%
c i    1.4   14082    99405       481     420     20  3320    1     9   12  17%      1    9   13    0 13539%
c i    1.4   14079    99405       519     442     21  3320    1     9   12  17%      1    9   12    0 12160%
c i    1.5   14078    99405       539     461     21  3320    2     9   12  17%      1    9   12    0 11889%
c i    1.5   14075    99405       752     646     30  3334    3    13   12  22%      1   13   19    0 10273%
c i    1.5   14072    99405       753     646     30  3334    3    13   12  22%      1   13   19    0 10233%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 53 variables
c [simpleprobe-2] all 14047 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 571 variables
c [simpleprobe-2] 3762 variables remain 28% (9714 retained 72%)
c [simpleprobe-2] removed 571 variables, found 2378 hbrs, 236 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26952 literals 100%
c [treelook-1] scheduling used 293913 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302595 steps
c [treelook-1] 26885 literals remain 100%
c [treelook-1] 13457 variables remain to probed next time 100%
c [decomp-5] removed 16 variables
c [treelook-1] removed 35 variables, found 2339 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1786 probes remain 13% after last round
c [basicprobe-1-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 54 variables, found 4893 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 254 failed, 2250 tauts, 0 hbrs, 2589 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 13237 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 540 variables 4% in round 1 in 6646553 steps
c [elim-2-1] backward subsumption/strengthening limit 6646500
c [elim-2-1-1] backward checking 2497 touched variables 19%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 36 and strengthened 19 clauses in 493525 steps
c [elim-2-1] rescheduled 105 variables 1% by backward subsumption
c [elim-2-2] eliminated 18 variables 0% in round 2 in 71735 steps
c [elim-2-2] backward subsumption/strengthening limit 71700
c [elim-2-2-1] backward checking 90 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 13 and strengthened 1 clauses in 35221 steps
c [elim-2-2] rescheduled 27 variables 0% by backward subsumption
c [elim-2-3] eliminated 12 variables 0% in round 3 in 14107 steps
c [elim-2-3] backward subsumption/strengthening limit 14100
c [elim-2-3-1] backward checking 42 touched variables 0%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 14 and strengthened 1 clauses in 14101 steps
c [elim-2] incomplete 23 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 608 = 5% variables out of 13237 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 88444 negative 99.1% of 89242 except 798 0.9%
c [phase-count-2] 72055 positive 80.7% of 89242 except 17187 19.3%
c [phase-count-2] less non-negative clauses 798 than limit 8900 (10.0%)
c [phase-count-2] non-pos/non-neg = 17187/798 = 21.54 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 120 negative 100%
c [sort-queue-2] sorted 6274 enqueued variables after 753 conflicts
c [score-dist-2] active 6355 (50%), one 0 (0%), zero 6274 (50%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 510, avg 509.9
c [simplification-2] removed 1440 variables 10.2% (12629 remain 9%)
c [simplification-2] removed 10163 irredundant clauses 10.2% (89242 remain 14%)
c [simplification-2] maximum reduction of 10% = max (10%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1011 (hard 11000)
c [simplification-2] new iteration interval 100
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    2.2   12628    89242       845     685     30  6023    3    14   11  21%      1   14   17    0 8148%
c 
c [simplification-3] limit 1011 conflicts (hard 11000) hit after 1011 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5458 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5458 out of 5458 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 93 at-most-one constraints, 93 used 100%
c [card-2] exported 3194 binary clauses, 34.3 per/constraint
c [decomp-6] removed 12 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 25234 literals 100%
c [treelook-2] scheduling used 290204 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 302213 steps
c [treelook-2] 25212 literals remain 100%
c [treelook-2] 12610 variables remain to probed next time 100%
c [decomp-7] removed 1 variables
c [treelook-2] removed 8 variables, found 2664 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 120 failed, 3130 tauts, 0 hbrs, 1179 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 12524 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 272 variables 2% in round 1 in 6181916 steps
c [elim-3-1] backward subsumption/strengthening limit 6181900
c [elim-3-1-1] backward checking 1549 touched variables 12%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 3 and strengthened 2 clauses in 287434 steps
c [elim-3-1] rescheduled 22 variables 0% by backward subsumption
c [elim-3-2] eliminated 9 variables 0% in round 2 in 8785 steps
c [elim-3-2] backward subsumption/strengthening limit 8700
c [elim-3-2-1] backward checking 36 touched variables 0%
c [elim-3-2-1] incomplete backward checking 0 remain 0%
c [elim-3-2] subsumed 21 and strengthened 0 clauses in 8701 steps
c [elim-3-2] rescheduled 21 variables 0% by backward subsumption
c [elim-3-3] eliminated 6 variables 0% in round 3 in 13048 steps
c [elim-3-3] backward subsumption/strengthening limit 13000
c [elim-3-3-1] backward checking 28 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 9 and strengthened 0 clauses in 13001 steps
c [elim-3] incomplete 13 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 303 = 2% variables out of 12524 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 83762 negative 99.1% of 84521 except 759 0.9%
c [phase-count-3] 68997 positive 81.6% of 84521 except 15524 18.4%
c [phase-count-3] less non-negative clauses 759 than limit 8400 (10.0%)
c [phase-count-3] non-pos/non-neg = 15524/759 = 20.45 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 3 negative 100%
c [sort-queue-3] sorted 5816 enqueued variables after 1011 conflicts
c [score-dist-3] active 6405 (52%), one 0 (0%), zero 5816 (48%)
c [score-dist-3] max exp 511, different 11 (2%)
c [score-dist-3] median active exp 511, avg 510.1
c [simplification-3] removed 407 variables 3.2% (12221 remain 9%)
c [simplification-3] removed 4721 irredundant clauses 5.3% (84521 remain 14%)
c [simplification-3] maximum reduction of 5% = max (3%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13011 (soft 3011 + delta 10000)
c [simplification-3] new conflict limit 3011 (hard 13011)
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    2.7   12220    84521      1117     909     30 10251    6    22   12  26%      1   21   35    0 9176%
c i    2.7   12217    84521      1119     910     30 10251    6    22   12  26%      1   21   35    0 9106%
c i    2.7   12214    84521      1120     910     30 10251    6    22   12  26%      1   21   35    0 9070%
c i    2.7   12213    84521      1122     910     30 10252    6    22   12  26%      1   21   34    0 9001%
c i    2.8   11611    84521      1289    1065     32 10257    6    25   12  25%      1   24   28    0 6490%
c i    2.8   10906    84521      1375    1143     32 10259    7    26   12  25%      1   26   27    0 5770%
c i    2.8   10903    84521      1381    1147     33 10259    7    26   12  25%      1   26   27    0 5718%
c i    3.1   10900    84521      2177    1863     40 10276   12    40   13  29%      4   40   34    1 3868%
c i    3.1   10894    84521      2178    1863     40 10276   12    40   13  29%      4   40   34    1 3853%
c i    3.1   10890    84521      2179    1863     40 10276   12    40   13  29%      4   40   34    1 3838%
c i    3.1   10885    84521      2182    1864     40 10276   12    40   13  29%      4   40   34    1 3810%
c i    3.2   10883    84521      2631    2294     40 10276   14    46   13  30%      4   45   30    1 2773%
c i    3.3   10733    84521      2825    2463     40 10277   15    48   13  31%      4   47   34    1 2862%
c i    3.3   10732    84521      2826    2463     40 10277   15    48   13  31%      4   47   34    1 2851%
c i    3.4   10721    84521      3005    2622     42 10280   16    50   13  32%      3   49   35    1 2716%
c 
c [simplification-4] limit 3065 conflicts (hard 13011) hit after 3065 conflicts
c [decomp-8] removed 1741 variables
c [basicprobe-2] limit 1749151 penalty 0 = 0 + 0
c [basicprobe-2-0] 1273 probes remain 12% after last round
c [basicprobe-2-0] 35 units = 32 failed (91%) + 3 lifted (9%)
c [basicprobe-2-0] removed 51 variables, found 8454 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 3 units, 219 failed, 2287 tauts, 0 hbrs, 5148 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 10187 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 722 variables 7% in round 1 in 4600610 steps
c [elim-4-1] backward subsumption/strengthening limit 4600600
c [elim-4-1-1] backward checking 2410 touched variables 24%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 18 and strengthened 6 clauses in 382367 steps
c [elim-4-1] rescheduled 83 variables 1% by backward subsumption
c [elim-4-2] eliminated 13 variables 0% in round 2 in 42290 steps
c [elim-4-2] backward subsumption/strengthening limit 42200
c [elim-4-2-1] backward checking 56 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 2 clauses in 25311 steps
c [elim-4-2] rescheduled 8 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 5980 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 769 = 8% variables out of 10187 scheduled
c [sort-queue-4] sorted 3863 enqueued variables after 3065 conflicts
c [score-dist-4] active 5555 (59%), one 0 (0%), zero 3863 (41%)
c [score-dist-4] max exp 513, different 9 (2%)
c [score-dist-4] median active exp 513, avg 512.7
c [simplification-4] removed 1302 variables 12.1% (9418 remain 7%)
c [simplification-4] removed 19989 irredundant clauses 23.6% (64532 remain 10%)
c [simplification-4] maximum reduction of 24% = max (12%, 24%)
c [simplification-4] large reduction 24% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15065 (soft 5065 + delta 10000)
c [simplification-4] new conflict limit 5065 (hard 15065)
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    4.0    9417    64532      3536    2719     34 10592   18    56   12  32%      4   54   35    2 2235%
c i    4.0    9414    64532      3592    2763     34 10595   18    55   12  33%      3   54   32    2 2017%
c i    4.0    9413    64532      3624    2792     34 10595   18    55   12  33%      3   54   32    2 1993%
c 
c [simplification-5] limit 5065 conflicts (hard 15065) hit after 5067 conflicts
c [quatres-1] found 4021 quaternary clauses 68% in total
c [quatres-1-2] added 5 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 9413 free variables schedulable
c [ternres-1] 185 ternary resolvents (1 bin, 184 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 194 xors of average arity 3.0
c [gauss-1] connected 583 occurrences of 285 variables (average 2.0)
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-9] removed 19 variables
c [simpleprobe-3] 2336 schedulable variables 25%
c [simpleprobe-3] limit 2207794 penalty 0 = 0 + 0
c [decomp-10] removed 122 variables
c [simpleprobe-3] 264 variables remain 3% (9008 retained 97%)
c [simpleprobe-3] removed 122 variables, found 4177 hbrs, 48 units
c [unhide-5] limit 110389 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 68 failed, 3363 tauts, 0 hbrs, 5537 literals
c [transred-1] limit 551948 with penalty 0 = 0 + 0
c [transred-1] removed 180 transitive binary clauses
c [transred-1] found 6 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 9193 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 438 blocked clauses
c [block-1] 438 < 1/100 * 61014 = 610 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 33 (12%) of length 7
c [cce-1-1] eliminated 35 clauses out of 345 (10%) of length 6
c [cce-1-1] eliminated 112 clauses out of 909 (12%) of length 5
c [cce-1-1] eliminated 1291 clauses out of 3690 (35%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1442 large clauses in 15623951 steps
c [cce-1-1] allowing another 7811975 steps for small clauses
c [cce-1-1] scheduling 44103 clauses = 34421 binary + 9682 ternary
c [cce-1-1] tried to eliminate 2394 small clauses 5%
c [cce-1-1] eliminated 691 binary clauses 2%
c [cce-1-1] eliminated 101 ternary clauses 1%
c [cce-1-1] eliminated 792 small clauses 2%
c [cce-1-1] eliminated 792 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2234 covered clauses in round 1
c [cce-1] eliminated 2234 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 9192 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 596 variables 6% in round 1 in 3859830 steps
c [elim-5-1] backward subsumption/strengthening limit 3859800
c [elim-5-1-1] backward checking 2482 touched variables 27%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 9 and strengthened 8 clauses in 403010 steps
c [elim-5-1] rescheduled 41 variables 0% by backward subsumption
c [elim-5-2] eliminated 2 variables 0% in round 2 in 19794 steps
c [elim-5-2] backward subsumption/strengthening limit 19700
c [elim-5-2-1] backward checking 29 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 13462 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 598 = 7% variables out of 9192 scheduled
c [bca-1] limit of 10000000 steps and 113594 added (scaled 2)
c [bca-1] 13865 out of 17190 literals actually usable 81%
c [bca-1] added 20 blocked clauses in 31883 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1384 pos 16.1% + 7210 neg 83.9% = 8594 sched 100.0% ret 0
c [sweep-1-1] 1026392 steps 34 queries 631.62 avg class size
c [sweep-1-1] 310 decisions 25 SAT calls 74.24 avg env size
c [sweep-1-1] 7837 variables remain 91% (742 retained 9%)
c [decomp-11] removed 36 variables
c [sweep-1-1] removed 36 vars (0 failed, 9 eqs, 13 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 36 vars in TOTAL (1 rounds, 33 queries)
c [sort-queue-5] sorted 3096 enqueued variables after 5067 conflicts
c [score-dist-5] active 5462 (64%), one 0 (0%), zero 3096 (36%)
c [score-dist-5] max exp 514, different 9 (2%)
c [score-dist-5] median active exp 514, avg 513.8
c [simplification-5] removed 855 variables 9.1% (8558 remain 6%)
c [simplification-5] removed 8178 irredundant clauses 12.7% (56354 remain 9%)
c [simplification-5] maximum reduction of 13% = max (9%, 13%)
c [simplification-5] large reduction 13% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17067 (soft 7067 + delta 10000)
c [simplification-5] new conflict limit 7067 (hard 17067)
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    6.0    8557    56354      5068    3303    334 14783   26    70   12  37%     11   67   41    3 1630%
c i    6.0    8234    56354      5094    3324    335 14783   26    70   12  37%     11   67   39    3 1521%
c i    6.2    8091    56354      5943    4094    350 14792   28    74   13  38%      9   70   42    3 1417%
c i    6.3    8090    56354      6058    4205    351 14792   28    75   13  38%      8   71   38    3 1248%
c i    6.4    8087    56354      6295    4421    353 14793   29    75   13  38%      7   71   32    3 1025%
c i    6.4    8086    56354      6314    4438    353 14793   29    75   13  38%      6   71   35    3 1104%
c i    6.4    8084    56354      6315    4438    353 14793   29    75   13  38%      6   71   35    3 1100%
c i    6.4    8082    56354      6316    4438    353 14793   29    75   13  38%      6   71   35    3 1095%
c i    6.4    8081    56354      6340    4456    355 14794   29    76   13  38%      6   71   37    3 1158%
c i    6.4    8080    56354      6345    4460    355 14794   29    76   13  38%      6   71   37    3 1158%
c i    6.4    8075    56354      6527    4620    359 14797   29    78   13  37%      5   73   33    3 1013%
c i    6.4    8074    56354      6581    4647    363 14802   29    77   13  37%      5   73   28    3  864%
c i    6.4    8073    56354      6585    4650    363 14802   29    77   13  37%      5   73   28    3  856%
c i    6.4    8072    56354      6587    4650    363 14802   29    77   13  37%      5   73   28    3  853%
c i    6.5    8070    56354      6667    4722    363 14806   29    78   13  37%      5   73   32    3  965%
c i    6.5    8067    56354      6671    4723    364 14806   29    78   13  37%      5   73   32    3  955%
c i    6.5    8065    56354      6914    4954    365 14809   29    78   13  37%      4   73   32    3  933%
c 
c [simplification-6] limit 7098 conflicts (hard 17067) hit after 7098 conflicts
c [quatres-2] found 2125 quaternary clauses 61% in total
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 8065 free variables schedulable
c [ternres-2] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2490 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2490 out of 2490 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 591 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15934 literals 100%
c [treelook-3] scheduling used 196577 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 308525 steps
c [treelook-3] 15868 literals remain 100%
c [treelook-3] 7943 variables remain to probed next time 100%
c [decomp-13] removed 6 variables
c [treelook-3] removed 30 variables, found 3634 hbrs
c [unhide-6] limit 145190 with penalty 0 = 0 + 0
c [unhide-6-6] 5 units, 197 failed, 3016 tauts, 0 hbrs, 11165 literals
c [transred-2] limit 725952 with penalty 0 = 0 + 0
c [transred-2] removed 248 transitive binary clauses
c [transred-2] found 4 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-2-1] eliminated 3 clauses out of 33 (9%) of length 7
c [cce-2-1] eliminated 7 clauses out of 227 (3%) of length 6
c [cce-2-1] eliminated 23 clauses out of 686 (3%) of length 5
c [cce-2-1] eliminated 236 clauses out of 2133 (11%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 270 large clauses in 10785267 steps
c [cce-2-1] allowing another 5392633 steps for small clauses
c [cce-2-1] scheduling 38094 clauses = 29087 binary + 9007 ternary
c [cce-2-1] tried to eliminate 3192 small clauses 8%
c [cce-2-1] eliminated 892 binary clauses 3%
c [cce-2-1] eliminated 141 ternary clauses 2%
c [cce-2-1] eliminated 1033 small clauses 3%
c [cce-2-1] eliminated 2315 small clauses in 30000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2585 covered clauses in round 1
c [cce-2] eliminated 2585 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 7793 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 583 variables 7% in round 1 in 3144825 steps
c [elim-6-1] backward subsumption/strengthening limit 3144800
c [elim-6-1-1] backward checking 2187 touched variables 28%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 5 and strengthened 18 clauses in 330849 steps
c [elim-6-1] rescheduled 83 variables 1% by backward subsumption
c [elim-6-2] eliminated 9 variables 0% in round 2 in 50849 steps
c [elim-6-2] backward subsumption/strengthening limit 50800
c [elim-6-2-1] backward checking 37 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 7 and strengthened 6 clauses in 13932 steps
c [elim-6-2] rescheduled 19 variables 0% by backward subsumption
c [elim-6-3] eliminated 4 variables 0% in round 3 in 11809 steps
c [elim-6-3] backward subsumption/strengthening limit 11800
c [elim-6-3-1] backward checking 13 touched variables 0%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 4 and strengthened 1 clauses in 10444 steps
c [elim-6] incomplete 13 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 620 = 8% variables out of 7793 scheduled
c [bca-2] limit of 10000000 steps and 93992 added (scaled 2)
c [bca-2] 11168 out of 14348 literals actually usable 78%
c [bca-2] added 13 blocked clauses in 26951 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1139 pos 17.1% + 5508 neg 82.9% = 6647 sched 92.7% ret 526
c [sweep-2-1] 1053899 steps 29 queries 695.52 avg class size
c [sweep-2-1] 417 decisions 26 SAT calls 81.54 avg env size
c [sweep-2-1] 6079 variables remain 85% (1070 retained 15%)
c [decomp-14] removed 33 variables
c [sweep-2-1] removed 33 vars (0 failed, 4 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 33 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-6] sorted 2442 enqueued variables after 7098 conflicts
c [score-dist-6] active 4698 (66%), one 0 (0%), zero 2442 (34%)
c [score-dist-6] max exp 514, different 9 (2%)
c [score-dist-6] median active exp 514, avg 513.9
c [simplification-6] removed 925 variables 11.5% (7140 remain 5%)
c [simplification-6] removed 9873 irredundant clauses 17.5% (46481 remain 8%)
c [simplification-6] maximum reduction of 18% = max (11%, 18%)
c [simplification-6] large reduction 18% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 19098 (soft 9098 + delta 10000)
c [simplification-6] new conflict limit 9098 (hard 19098)
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    7.9    7139    46481      7154    3983    384 12850   30    80   12  38%      3   75   42    4 1169%
c i    7.9    7136    46481      7410    4229    385 12853   30    79   12  38%      3   73   31    4  838%
c i    8.1    7131    46481      7925    4711    387 12854   31    82   12  38%      3   76   41    4 1046%
c i    8.1    7127    46481      7963    4747    387 12854   31    82   12  38%      3   76   42    4 1049%
c i    8.1    7126    46481      7973    4753    388 12855   31    82   12  38%      3   76   41    4 1022%
c i    8.1    7125    46481      7974    4753    388 12855   31    82   12  38%      3   76   40    4 1018%
c i    8.1    7123    46481      7975    4753    388 12855   31    82   12  38%      3   76   40    4 1014%
c i    8.4    7122    46481      8966    5671    391 12858   36    88   13  41%      6   81   53    5 1127%
c 
c [simplification-7] limit 9119 conflicts (hard 19098) hit after 9121 conflicts
c [quatres-3] found 2020 quaternary clauses 57% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-2] added 15 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7122 free variables schedulable
c [ternres-3] 87 ternary resolvents (0 bin, 87 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 46 xors of average arity 2.8
c [gauss-2] connected 130 occurrences of 57 variables (average 2.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 9 variables
c [basicprobe-3] limit 4428085 penalty 0 = 0 + 0
c [basicprobe-3-0] 858 probes remain 13% after last round
c [basicprobe-3-0] 127 units = 119 failed (94%) + 8 lifted (6%)
c [basicprobe-3-0] removed 391 variables, found 12486 hbrs
c [bate-1] eliminated 48 asymmetric tautologies during probing
c [unhide-7] limit 177123 with penalty 0 = 0 + 0
c [unhide-7-7] 2 units, 124 failed, 1490 tauts, 0 hbrs, 10275 literals
c [transred-3] limit 885617 with penalty 0 = 0 + 0
c [transred-3] removed 446 transitive binary clauses
c [transred-3] found 16 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 6595 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 152 blocked clauses
c [block-2] 152 < 1/100 * 40469 = 404 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 9
c [cce-3-1] eliminated 1 clauses out of 30 (3%) of length 7
c [cce-3-1] eliminated 3 clauses out of 180 (2%) of length 6
c [cce-3-1] eliminated 22 clauses out of 565 (4%) of length 5
c [cce-3-1] eliminated 151 clauses out of 1682 (9%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 178 large clauses in 6707732 steps
c [cce-3-1] allowing another 3353866 steps for small clauses
c [cce-3-1] scheduling 30301 clauses = 23791 binary + 6510 ternary
c [cce-3-1] tried to eliminate 4320 small clauses 14%
c [cce-3-1] eliminated 1186 binary clauses 5%
c [cce-3-1] eliminated 199 ternary clauses 3%
c [cce-3-1] eliminated 1385 small clauses 5%
c [cce-3-1] eliminated 1385 small clauses in 30000004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1563 covered clauses in round 1
c [cce-3] eliminated 1563 covered clauses in TOTAL during 1 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 6592 variables 100%
c [elim-7] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 652 variables 10% in round 1 in 2388617 steps
c [elim-7-1] backward subsumption/strengthening limit 2388600
c [elim-7-1-1] backward checking 2333 touched variables 35%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 9 clauses in 309175 steps
c [elim-7-1] rescheduled 39 variables 1% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 18998 steps
c [elim-7-2] backward subsumption/strengthening limit 18900
c [elim-7-2-1] backward checking 26 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 3 and strengthened 0 clauses in 10596 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3118 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 654 = 10% variables out of 6592 scheduled
c [bca-3] limit of 10000000 steps and 74192 added (scaled 2)
c [bca-3] 9118 out of 11878 literals actually usable 77%
c [bca-3] added 8 blocked clauses in 22388 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 958 pos 18.8% + 4136 neg 81.2% = 5094 sched 85.8% ret 844
c [sweep-3-1] 1138689 steps 27 queries 364.30 avg class size
c [sweep-3-1] 462 decisions 24 SAT calls 79.33 avg env size
c [sweep-3-1] 4403 variables remain 74% (1513 retained 26%)
c [decomp-16] removed 40 variables
c [sweep-3-1] removed 40 vars (0 failed, 6 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 40 vars in TOTAL (1 rounds, 26 queries)
c [sort-queue-7] sorted 1852 enqueued variables after 9121 conflicts
c [score-dist-7] active 4046 (69%), one 0 (0%), zero 1852 (31%)
c [score-dist-7] max exp 515, different 9 (2%)
c [score-dist-7] median active exp 515, avg 514.7
c [simplification-7] removed 1224 variables 17.2% (5898 remain 4%)
c [simplification-7] removed 9878 irredundant clauses 21.3% (36603 remain 6%)
c [simplification-7] maximum reduction of 21% = max (17%, 21%)
c [simplification-7] large reduction 21% >= 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 21121 (soft 11121 + delta 10000)
c [simplification-7] new conflict limit 11121 (hard 21121)
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    5897    36603      9207    3676    426 17260   37    91   12  41%      5   83   56    5 1145%
c i   10.0    5896    36603      9801    4207    434 17264   38    92   12  42%      5   83   46    5  872%
c i   10.0    5895    36603      9859    4263    435 17264   38    92   12  42%      5   84   47    5  884%
c i   10.0    5894    36603      9933    4334    435 17265   39    93   12  42%      4   84   48    5  897%
c i   10.2    5893    36603     10401    4782    439 17268   38    93   12  41%      4   84   37    6  668%
c i   10.2    5889    36603     10402    4782    439 17268   38    93   12  41%      4   84   37    6  665%
c i   10.2    5887    36603     10403    4782    439 17268   38    93   12  41%      4   84   37    6  663%
c i   10.2    5886    36603     10472    4849    439 17268   38    93   12  41%      4   83   34    6  609%
c 
c [simplification-8] limit 11141 conflicts (hard 21121) hit after 11141 conflicts
c [quatres-4] found 1685 quaternary clauses 57% in total
c [quatres-4-2] added 5 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5886 free variables schedulable
c [ternres-4] 107 ternary resolvents (1 bin, 106 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 14 variables
c [simpleprobe-4] 190 schedulable variables 3%
c [simpleprobe-4] limit 4058862 penalty 0 = 0 + 0
c [decomp-18] removed 86 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 86 variables, found 1825 hbrs, 38 units
c [unhide-8] limit 202943 with penalty 0 = 0 + 0
c [unhide-8-8] 1 units, 47 failed, 2453 tauts, 0 hbrs, 7113 literals
c [transred-4] limit 1014715 with penalty 0 = 0 + 0
c [transred-4] removed 516 transitive binary clauses
c [transred-4] found 14 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-4-1] eliminated 1 clauses out of 15 (7%) of length 8
c [cce-4-1] eliminated 4 clauses out of 191 (2%) of length 6
c [cce-4-1] eliminated 19 clauses out of 603 (3%) of length 5
c [cce-4-1] eliminated 87 clauses out of 1509 (6%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 113 large clauses in 5825486 steps
c [cce-4-1] allowing another 2912743 steps for small clauses
c [cce-4-1] scheduling 26909 clauses = 20935 binary + 5974 ternary
c [cce-4-1] tried to eliminate 26909 small clauses 100%
c [cce-4-1] eliminated 4766 binary clauses 23%
c [cce-4-1] eliminated 959 ternary clauses 16%
c [cce-4-1] eliminated 5725 small clauses 21%
c [cce-4-1] eliminated 6204 small clauses in 145671936 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 6317 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2126630 steps for small clauses
c [cce-4-2] scheduling 21184 clauses = 16169 binary + 5015 ternary
c [cce-4-2] tried to eliminate 21184 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 6317 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 5740 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 405886220 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 603 variables 11% in round 1 in 1825364 steps
c [elim-8-1] backward subsumption/strengthening limit 1825300
c [elim-8-1-1] backward checking 2480 touched variables 43%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 4 and strengthened 14 clauses in 271804 steps
c [elim-8-1] rescheduled 70 variables 1% by backward subsumption
c [elim-8-2] eliminated 5 variables 0% in round 2 in 32172 steps
c [elim-8-2] backward subsumption/strengthening limit 32100
c [elim-8-2-1] backward checking 36 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 0 clauses in 15339 steps
c [elim-8-2] rescheduled 7 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 2929 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 608 = 11% variables out of 5740 scheduled
c [bca-4] limit of 10000000 steps and 57480 added (scaled 2)
c [bca-4] 7577 out of 10266 literals actually usable 74%
c [bca-4] added 14 blocked clauses in 19869 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 745 pos 19.4% + 3090 neg 80.6% = 3835 sched 74.7% ret 1297
c [sweep-4-1] 1113394 steps 35 queries 464.77 avg class size
c [sweep-4-1] 700 decisions 33 SAT calls 151.24 avg env size
c [sweep-4-1] 3422 variables remain 67% (1694 retained 33%)
c [decomp-19] removed 17 variables
c [sweep-4-1] removed 17 vars (0 failed, 2 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 17 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-8] sorted 1451 enqueued variables after 11141 conflicts
c [score-dist-8] active 3664 (72%), one 0 (0%), zero 1451 (28%)
c [score-dist-8] max exp 515, different 9 (2%)
c [score-dist-8] median active exp 515, avg 514.8
c [simplification-8] removed 771 variables 13.1% (5115 remain 4%)
c [simplification-8] removed 8262 irredundant clauses 22.6% (28341 remain 5%)
c [simplification-8] maximum reduction of 23% = max (13%, 23%)
c [simplification-8] large reduction 23% >= 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 23141 (soft 13141 + delta 10000)
c [simplification-8] new conflict limit 13141 (hard 23141)
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   15.9    5114    28341     11381    4198    865 16507   38    91   11  42%      6   80   43    6  716%
c i   16.0    5112    28341     11558    4362    866 16509   38    89   11  42%      5   79   34    6  564%
c i   16.1    5111    28341     12122    4901    872 16511   38    90   11  42%      5   79   39    6  618%
c i   16.3    5109    28341     12800    5543    880 16514   38    89   11  42%      5   77   36    7  545%
c i   16.3    5108    28341     13078    5802    884 16514   38    90   11  42%      4   77   42    7  623%
c 
c [simplification-9] limit 13141 conflicts (hard 23141) hit after 13141 conflicts
c [quatres-5] found 1590 quaternary clauses 52% in total
c [quatres-5-2] added 2 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 5107 free variables schedulable
c [ternres-5] 72 ternary resolvents (0 bin, 72 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 11 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 10208 literals 100%
c [treelook-4] scheduling used 141461 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 300335 steps
c [treelook-4] 10187 literals remain 100%
c [treelook-4] 5100 variables remain to probed next time 100%
c [treelook-4] removed 4 variables, found 3128 hbrs
c [unhide-9] limit 226739 with penalty 0 = 0 + 0
c [unhide-9-10] 4 units, 74 failed, 2372 tauts, 0 hbrs, 17799 literals
c [transred-5] limit 1133697 with penalty 0 = 0 + 0
c [transred-5] removed 392 transitive binary clauses
c [transred-5] found 11 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 16
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 13
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 12
c [cce-5-1] eliminated 1 clauses out of 9 (11%) of length 10
c [cce-5-1] eliminated 4 clauses out of 13 (31%) of length 9
c [cce-5-1] eliminated 4 clauses out of 27 (15%) of length 8
c [cce-5-1] eliminated 4 clauses out of 66 (6%) of length 7
c [cce-5-1] eliminated 10 clauses out of 223 (4%) of length 6
c [cce-5-1] eliminated 30 clauses out of 619 (5%) of length 5
c [cce-5-1] eliminated 172 clauses out of 1472 (12%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 236 large clauses in 6539111 steps
c [cce-5-1] allowing another 3269555 steps for small clauses
c [cce-5-1] scheduling 20764 clauses = 15411 binary + 5353 ternary
c [cce-5-1] tried to eliminate 5629 small clauses 27%
c [cce-5-1] eliminated 314 binary clauses 2%
c [cce-5-1] eliminated 290 ternary clauses 5%
c [cce-5-1] eliminated 604 small clauses 3%
c [cce-5-1] eliminated 718 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 954 covered clauses in round 1
c [cce-5] eliminated 954 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 5065 variables 100%
c [elim-9] limit of 22673948 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 144 variables 3% in round 1 in 1645861 steps
c [elim-9-1] backward subsumption/strengthening limit 1645800
c [elim-9-1-1] backward checking 879 touched variables 17%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 3 clauses in 96971 steps
c [elim-9-1] rescheduled 36 variables 1% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 13695 steps
c [elim-9-2] backward subsumption/strengthening limit 13600
c [elim-9-2-1] backward checking 15 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 5164 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 145 = 3% variables out of 5065 scheduled
c [bca-5] limit of 10000000 steps and 54425 added (scaled 2)
c [bca-5] 6965 out of 9842 literals actually usable 71%
c [bca-5] added 14 blocked clauses in 19882 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 675 pos 20.5% + 2621 neg 79.5% = 3296 sched 67.0% ret 1624
c [sweep-5-1] 10020510 steps 619 queries 13.60 avg class size
c [sweep-5-1] 6070 decisions 527 SAT calls 50.02 avg env size
c [sweep-5-1] 53 variables remain 1% (4611 retained 99%)
c [decomp-22] removed 416 variables
c [sweep-5-1] removed 416 vars (1 failed, 135 eqs, 87 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 416 vars in TOTAL (1 rounds, 618 queries)
c [sort-queue-9] sorted 1245 enqueued variables after 13141 conflicts
c [score-dist-9] active 3259 (72%), one 0 (0%), zero 1245 (28%)
c [score-dist-9] max exp 515, different 9 (2%)
c [score-dist-9] median active exp 515, avg 514.8
c [simplification-9] removed 603 variables 11.8% (4504 remain 3%)
c [simplification-9] removed 3672 irredundant clauses 13.0% (24669 remain 4%)
c [simplification-9] maximum reduction of 13% = max (12%, 13%)
c [simplification-9] large reduction 13% >= 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 25141 (soft 15141 + delta 10000)
c [simplification-9] new conflict limit 15141 (hard 25141)
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   17.9    4503    24669     13271    5419    826 20053   38    90   12  42%      3   77   41    7  590%
c i   17.9    4502    24669     13350    5496    826 20053   38    90   12  42%      3   77   40    7  572%
c i   17.9    4501    24669     13491    5624    827 20054   38    90   12  42%      3   77   44    7  625%
c i   18.0    4498    24669     13588    5716    829 20054   38    91   12  42%      3   78   43    7  607%
c i   18.0    4497    24669     13595    5722    829 20054   38    91   12  42%      2   78   44    7  613%
c i   18.0    4496    24669     13659    5781    831 20054   39    91   12  42%      2   78   46    7  637%
c i   18.0    4495    24669     13776    5882    832 20055   39    91   12  43%      2   78   46    7  643%
c i   18.0    4492    24669     13886    5979    835 20055   39    91   12  43%      2   78   46    7  634%
c i   18.0    4491    24669     13891    5983    835 20055   39    91   12  43%      2   78   46    7  628%
c i   18.0    4489    24669     13893    5984    835 20055   39    91   12  43%      2   78   46    7  627%
c i   18.0    4488    24669     13894    5984    835 20055   39    91   12  43%      2   78   45    7  625%
c i   18.1    4486    24669     13921    6008    835 20056   39    91   12  43%      2   77   42    7  583%
c i   18.1    4485    24669     14126    6205    835 20057   39    89   12  43%      2   76   35    7  480%
c i   18.1    4484    24669     14236    6313    835 20057   38    88   12  43%      1   74   30    7  403%
c i   18.1    4483    24669     14342    6414    835 20057   38    87   12  43%      1   74   29    7  392%
c i   18.2    4482    24669     14502    6561    835 20059   38    87   12  43%      1   73   29    7  391%
c i   18.2    4481    24669     14573    6630    835 20059   38    87   12  43%      1   73   32    8  424%
c i   18.2    4477    24669     14699    6745    835 20059   37    87   12  43%      1   73   33    8  432%
c i   18.3    4476    24669     15073    7103    837 20059   38    87   12  43%      1   72   38    8  496%
c 
c [simplification-10] limit 15159 conflicts (hard 25141) hit after 15162 conflicts
c [quatres-6] found 1168 quaternary clauses 52% in total
c [quatres-6-2] added 3 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 4475 free variables schedulable
c [ternres-6] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 786 at-most-one constraints of average size 3.6
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 786 out of 786 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 82 xors of average arity 2.6
c [gauss-3] connected 211 occurrences of 89 variables (average 2.4)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 10 variables
c [basicprobe-4] limit 6271652 penalty 0 = 0 + 0
c [basicprobe-4-0] 112 probes remain 3% after last round
c [basicprobe-4-0] 300 units = 271 failed (90%) + 29 lifted (10%)
c [basicprobe-4-0] removed 446 variables, found 13445 hbrs
c [bate-2] eliminated 53 asymmetric tautologies during probing
c [unhide-10] limit 250866 with penalty 0 = 0 + 0
c [unhide-10-11] 1 units, 121 failed, 2692 tauts, 0 hbrs, 7027 literals
c [transred-6] limit 1254330 with penalty 0 = 0 + 0
c [transred-6] removed 702 transitive binary clauses
c [transred-6] found 14 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 3937 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 155 blocked clauses
c [block-3] 155 < 1/100 * 20883 = 208 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-6-1] eliminated 2 clauses out of 27 (7%) of length 7
c [cce-6-1] eliminated 2 clauses out of 77 (3%) of length 6
c [cce-6-1] eliminated 3 clauses out of 297 (1%) of length 5
c [cce-6-1] eliminated 41 clauses out of 865 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 50 large clauses in 1835403 steps
c [cce-6-1] allowing another 917701 steps for small clauses
c [cce-6-1] scheduling 15460 clauses = 12355 binary + 3105 ternary
c [cce-6-1] tried to eliminate 10580 small clauses 68%
c [cce-6-1] eliminated 819 binary clauses 7%
c [cce-6-1] eliminated 232 ternary clauses 7%
c [cce-6-1] eliminated 1051 small clauses 7%
c [cce-6-1] eliminated 1051 small clauses in 30000005 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1101 covered clauses in round 1
c [cce-6] eliminated 1101 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3930 variables 100%
c [elim-10] limit of 25086609 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 619 variables 16% in round 1 in 1123232 steps
c [elim-10-1] backward subsumption/strengthening limit 1123200
c [elim-10-1-1] backward checking 1762 touched variables 45%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 6 clauses in 172322 steps
c [elim-10-1] rescheduled 38 variables 1% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 19606 steps
c [elim-10-2] backward subsumption/strengthening limit 19600
c [elim-10-2-1] backward checking 8 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 1 and strengthened 1 clauses in 6461 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 1242 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 625 = 16% variables out of 3930 scheduled
c [bca-6] limit of 10000000 steps and 36888 added (scaled 2)
c [bca-6] 4591 out of 6612 literals actually usable 69%
c [bca-6] added 8 blocked clauses in 14139 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 3 pos 12.0% + 22 neg 88.0% = 25 sched 0.8% ret 3280
c [sweep-6-1] 110017 steps 19 queries 5.11 avg class size
c [sweep-6-1] 185 decisions 18 SAT calls 22.39 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-24] removed 8 variables
c [sweep-6-1] removed 8 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6-2] 504 pos 15.3% + 2793 neg 84.7% = 3297 sched 100.0% ret 0
c [sweep-6-2] 999136 steps 44 queries 135.30 avg class size
c [sweep-6-2] 849 decisions 42 SAT calls 91.93 avg env size
c [sweep-6-2] 1870 variables remain 57% (1423 retained 43%)
c [decomp-25] removed 6 variables
c [sweep-6-2] removed 6 vars (0 failed, 2 eqs, 5 impls)
c [sweep-6] removed 14 vars in TOTAL (2 rounds, 61 queries)
c [sort-queue-10] sorted 728 enqueued variables after 15162 conflicts
c [score-dist-10] active 2563 (78%), one 0 (0%), zero 728 (22%)
c [score-dist-10] max exp 515, different 9 (2%)
c [score-dist-10] median active exp 515, avg 514.9
c [simplification-10] removed 1184 variables 26.5% (3291 remain 2%)
c [simplification-10] removed 6547 irredundant clauses 26.5% (18122 remain 3%)
c [simplification-10] maximum reduction of 27% = max (26%, 27%)
c [simplification-10] large reduction 27% >= 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 27162 (soft 17162 + delta 10000)
c [simplification-10] new conflict limit 17162 (hard 27162)
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   19.7    3290    18122     15190    4343    434 13682   38    87   10  44%      1   73   45    8  570%
c i   19.8    3289    18122     15592    4714    439 13685   38    87   11  44%      2   72   39    8  487%
c i   19.9    3288    18122     16217    5312    443 13691   37    85   12  44%      3   69   29    8  358%
c i   20.0    3287    18122     16465    5550    444 13694   37    85   12  43%      2   68   30    8  358%
c 
c [simplification-11] limit 17162 conflicts (hard 27162) hit after 17162 conflicts
c [quatres-7] found 1099 quaternary clauses 53% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 3287 free variables schedulable
c [ternres-7] 50 ternary resolvents (0 bin, 50 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 6 variables
c [simpleprobe-5] all 3285 free variables schedulable
c [simpleprobe-5] limit 5376048 penalty 0 = 0 + 0
c [decomp-27] removed 44 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 44 variables, found 1465 hbrs, 26 units
c [unhide-11] limit 268802 with penalty 0 = 0 + 0
c [unhide-11-13] 1 units, 8 failed, 1587 tauts, 0 hbrs, 10184 literals
c [transred-7] limit 1344012 with penalty 0 = 0 + 0
c [transred-7] removed 822 transitive binary clauses
c [transred-7] found 9 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-7-1] eliminated 3 clauses out of 29 (10%) of length 7
c [cce-7-1] eliminated 4 clauses out of 112 (4%) of length 6
c [cce-7-1] eliminated 15 clauses out of 352 (4%) of length 5
c [cce-7-1] eliminated 71 clauses out of 940 (8%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 96 large clauses in 2539293 steps
c [cce-7-1] allowing another 1269646 steps for small clauses
c [cce-7-1] scheduling 12964 clauses = 10371 binary + 2593 ternary
c [cce-7-1] tried to eliminate 10739 small clauses 83%
c [cce-7-1] eliminated 703 binary clauses 7%
c [cce-7-1] eliminated 224 ternary clauses 9%
c [cce-7-1] eliminated 927 small clauses 7%
c [cce-7-1] eliminated 1034 small clauses in 30000005 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1130 covered clauses in round 1
c [cce-7] eliminated 1130 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 3222 variables 100%
c [elim-11] limit of 26880240 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 194 variables 6% in round 1 in 976521 steps
c [elim-11-1] backward subsumption/strengthening limit 976500
c [elim-11-1-1] backward checking 965 touched variables 30%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 3 and strengthened 5 clauses in 105216 steps
c [elim-11-1] rescheduled 43 variables 1% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 18869 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 194 = 6% variables out of 3222 scheduled
c [bca-7] limit of 10000000 steps and 33046 added (scaled 2)
c [bca-7] 3938 out of 6058 literals actually usable 65%
c [bca-7] added 12 blocked clauses in 14312 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 355 pos 20.5% + 1377 neg 79.5% = 1732 sched 57.2% ret 1296
c [sweep-7-1] 1017912 steps 48 queries 77.38 avg class size
c [sweep-7-1] 1100 decisions 46 SAT calls 81.50 avg env size
c [sweep-7-1] 1089 variables remain 36% (1938 retained 64%)
c [decomp-28] removed 3 variables
c [sweep-7-1] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-7] removed 3 vars in TOTAL (1 rounds, 47 queries)
c [sort-queue-11] sorted 615 enqueued variables after 17162 conflicts
c [score-dist-11] active 2410 (80%), one 0 (0%), zero 615 (20%)
c [score-dist-11] max exp 516, different 10 (2%)
c [score-dist-11] median active exp 516, avg 515.6
c [simplification-11] removed 262 variables 8.0% (3025 remain 2%)
c [simplification-11] removed 1875 irredundant clauses 10.3% (16247 remain 3%)
c [simplification-11] maximum reduction of 10% = max (8%, 10%)
c [simplification-11] large reduction 10% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 29162 (soft 19162 + delta 10000)
c [simplification-11] new conflict limit 19162 (hard 29162)
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   21.3    3024    16247     17729    6255    499 11050   36    83   12  43%      8   65   31    9  356%
c i   21.6    3023    16247     18987    7467    500 11054   35    81   12  43%     10   62   28    9  300%
c i   21.6    3021    16247     18988    7467    500 11054   35    81   12  43%     10   62   28    9  299%
c 
c [simplification-12] limit 19172 conflicts (hard 29162) hit after 19172 conflicts
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 3021 free variables schedulable
c [ternres-8] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 5 variables
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 6040 literals 100%
c [treelook-5] scheduling used 94732 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 303744 steps
c [treelook-5] 5979 literals remain 99%
c [treelook-5] 3012 variables remain to probed next time 100%
c [treelook-5] removed 8 variables, found 2120 hbrs
c [unhide-12] limit 286541 with penalty 0 = 0 + 0
c [unhide-12-15] 1 units, 0 failed, 977 tauts, 0 hbrs, 10032 literals
c [transred-8] limit 1432709 with penalty 0 = 0 + 0
c [transred-8] removed 515 transitive binary clauses
c [transred-8] found 4 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-8-1] eliminated 2 clauses out of 105 (2%) of length 6
c [cce-8-1] eliminated 3 clauses out of 366 (1%) of length 5
c [cce-8-1] eliminated 21 clauses out of 893 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 27 large clauses in 2420511 steps
c [cce-8-1] allowing another 1210255 steps for small clauses
c [cce-8-1] scheduling 12286 clauses = 9349 binary + 2937 ternary
c [cce-8-1] tried to eliminate 12286 small clauses 100%
c [cce-8-1] eliminated 195 binary clauses 2%
c [cce-8-1] eliminated 155 ternary clauses 5%
c [cce-8-1] eliminated 350 small clauses 3%
c [cce-8-1] eliminated 376 small clauses in 31478397 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 403 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1137417 steps for small clauses
c [cce-8-2] scheduling 11936 clauses = 9154 binary + 2782 ternary
c [cce-8-2] tried to eliminate 11936 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 403 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 3007 variables 100%
c [elim-12] limit of 28654196 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 58 variables 2% in round 1 in 923938 steps
c [elim-12-1] backward subsumption/strengthening limit 923900
c [elim-12-1-1] backward checking 388 touched variables 13%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 39681 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 58 = 2% variables out of 3007 scheduled
c [bca-8] limit of 10000000 steps and 31836 added (scaled 2)
c [bca-8] 3733 out of 5900 literals actually usable 63%
c [bca-8] added 6 blocked clauses in 15343 steps
c [sweep-8] limit 1000000 penalty 0 = 0 + 0
c [sweep-8-1] 261 pos 24.2% + 816 neg 75.8% = 1077 sched 36.5% ret 1872
c [sweep-8-1] 1024420 steps 51 queries 51.65 avg class size
c [sweep-8-1] 1335 decisions 50 SAT calls 99.96 avg env size
c [sweep-8-1] 731 variables remain 25% (2216 retained 75%)
c [decomp-31] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 50 queries)
c [sort-queue-12] sorted 579 enqueued variables after 19172 conflicts
c [score-dist-12] active 2368 (80%), one 0 (0%), zero 579 (20%)
c [score-dist-12] max exp 516, different 10 (2%)
c [score-dist-12] median active exp 516, avg 515.7
c [simplification-12] removed 74 variables 2.4% (2947 remain 2%)
c [simplification-12] removed 620 irredundant clauses 3.8% (15627 remain 3%)
c [simplification-12] maximum reduction of 4% = max (2%, 4%)
c [simplification-12] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-12] new conflict interval 4000
c [simplification-12] penalized conflict interval 4000 = 1 * 4000
c [simplification-12] hard conflict limit 33172 (soft 23172 + delta 10000)
c [simplification-12] new conflict limit 23172 (hard 33172)
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   23.7    2946    15627     20787    8677    588 11489   35    79   13  45%     15   59   33   10  333%
c i   23.9    2945    15627     21694    9551    591 11489   36    80   13  45%     10   58   42   10  405%
c i   24.0    2944    15627     21954    9801    592 11490   36    80   13  45%      8   58   38   10  360%
c 
c [simplification-13] limit 23172 conflicts (hard 33172) hit after 23173 conflicts
c [quatres-8] found 1003 quaternary clauses 47% in total
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 2944 free variables schedulable
c [ternres-9] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-32] removed 3 variables
c [basicprobe-5] limit 8113874 penalty 0 = 0 + 0
c [basicprobe-5-0] 387 sched 14%, 89 failed, 6 lifted, 3567 hbrs
c [decomp-33] removed 113 variables
c [basicprobe-5-1] 759 sched 27%, 45 failed, 1 lifted, 5394 hbrs
c [decomp-34] removed 54 variables
c [basicprobe-5-2] 563 probes remain 20% after last round
c [basicprobe-5-2] 148 units = 141 failed (95%) + 7 lifted (5%)
c [basicprobe-5-2] removed 176 variables, found 9346 hbrs
c [bate-3] eliminated 34 asymmetric tautologies during probing
c [unhide-13] limit 324554 with penalty 0 = 0 + 0
c [unhide-13-17] 0 units, 0 failed, 1104 tauts, 0 hbrs, 20673 literals
c [transred-9] limit 1622774 with penalty 0 = 0 + 0
c [transred-9] removed 633 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 9
c [cce-9-1] eliminated 1 clauses out of 14 (7%) of length 8
c [cce-9-1] eliminated 2 clauses out of 26 (8%) of length 7
c [cce-9-1] eliminated 2 clauses out of 83 (2%) of length 6
c [cce-9-1] eliminated 5 clauses out of 307 (2%) of length 5
c [cce-9-1] eliminated 15 clauses out of 824 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 26 large clauses in 1892258 steps
c [cce-9-1] allowing another 946129 steps for small clauses
c [cce-9-1] scheduling 11192 clauses = 8862 binary + 2330 ternary
c [cce-9-1] tried to eliminate 11192 small clauses 100%
c [cce-9-1] eliminated 436 binary clauses 5%
c [cce-9-1] eliminated 140 ternary clauses 6%
c [cce-9-1] eliminated 576 small clauses 5%
c [cce-9-1] eliminated 576 small clauses in 24413221 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 602 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 81 (1%) of length 6
c [cce-9-2] eliminated 3 clauses out of 302 (1%) of length 5
c [cce-9-2] eliminated 1 clauses out of 809 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 5 large clauses in 1745227 steps
c [cce-9-2] allowing another 872613 steps for small clauses
c [cce-9-2] scheduling 10616 clauses = 8426 binary + 2190 ternary
c [cce-9-2] tried to eliminate 2320 small clauses 22%
c [cce-9-2] eliminated 3 binary clauses 0%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 5 small clauses 0%
c [cce-9-2] eliminated 5 small clauses in 5586790 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 10 covered clauses in round 2
c [cce-9] eliminated 612 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 2768 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 184 variables 7% in round 1 in 806371 steps
c [elim-13-1] backward subsumption/strengthening limit 806300
c [elim-13-1-1] backward checking 866 touched variables 31%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 15 clauses in 88386 steps
c [elim-13-1] rescheduled 37 variables 1% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 22437 steps
c [elim-13-2] backward subsumption/strengthening limit 22400
c [elim-13-2-1] backward checking 13 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 1 clauses in 5586 steps
c [elim-13-2] rescheduled 9 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 4779 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 186 = 7% variables out of 2768 scheduled
c [bca-9] limit of 10000000 steps and 27589 added (scaled 2)
c [bca-9] 3073 out of 5166 literals actually usable 59%
c [bca-9] added 19 blocked clauses in 16217 steps
c [sweep-9] limit 1000000 penalty 0 = 0 + 0
c [sweep-9-1] 164 pos 24.9% + 494 neg 75.1% = 658 sched 25.5% ret 1924
c [sweep-9-1] 1004000 steps 78 queries 25.50 avg class size
c [sweep-9-1] 1304 decisions 75 SAT calls 53.76 avg env size
c [sweep-9-1] 429 variables remain 17% (2152 retained 83%)
c [decomp-35] removed 4 variables
c [sweep-9-1] removed 4 vars (0 failed, 2 eqs, 3 impls)
c [sweep-9] removed 4 vars in TOTAL (1 rounds, 77 queries)
c [sort-queue-13] sorted 398 enqueued variables after 23173 conflicts
c [score-dist-13] active 2180 (85%), one 0 (0%), zero 398 (15%)
c [score-dist-13] max exp 516, different 10 (2%)
c [score-dist-13] median active exp 516, avg 515.8
c [simplification-13] removed 366 variables 12.4% (2578 remain 2%)
c [simplification-13] removed 2115 irredundant clauses 13.5% (13512 remain 2%)
c [simplification-13] maximum reduction of 14% = max (12%, 14%)
c [simplification-13] large reduction 14% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 35173 (soft 25173 + delta 10000)
c [simplification-13] new conflict limit 25173 (hard 35173)
c 
c [simplification-14] limit 25173 conflicts (hard 35173) hit after 25173 conflicts
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] all 2578 free variables schedulable
c [ternres-10] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 11 xors of average arity 3.0
c [gauss-4] connected 33 occurrences of 18 variables (average 1.8)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 2578 free variables schedulable
c [simpleprobe-6] limit 6880032 penalty 0 = 0 + 0
c [decomp-37] removed 3 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 3 variables, found 798 hbrs, 2 units
c [transred-10] limit 1720008 with penalty 0 = 0 + 0
c [transred-10] removed 792 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 2575 variables 100%
c [block-4] limit of 6250000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 11 blocked clauses
c [block-4] 11 < 1/100 * 13472 = 134 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-10-1] eliminated 1 clauses out of 28 (4%) of length 7
c [cce-10-1] eliminated 1 clauses out of 98 (1%) of length 6
c [cce-10-1] eliminated 4 clauses out of 336 (1%) of length 5
c [cce-10-1] eliminated 23 clauses out of 846 (3%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 31 large clauses in 2044947 steps
c [cce-10-1] allowing another 1022473 steps for small clauses
c [cce-10-1] scheduling 9946 clauses = 8126 binary + 1820 ternary
c [cce-10-1] tried to eliminate 9946 small clauses 100%
c [cce-10-1] eliminated 38 binary clauses 0%
c [cce-10-1] eliminated 44 ternary clauses 2%
c [cce-10-1] eliminated 82 small clauses 1%
c [cce-10-1] eliminated 82 small clauses in 21730364 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 113 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 990149 steps for small clauses
c [cce-10-2] scheduling 9864 clauses = 8088 binary + 1776 ternary
c [cce-10-2] tried to eliminate 3502 small clauses 36%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 113 covered clauses in TOTAL during 2 rounds
c [cce-10] 113 < 1/100 * 13461 = 134 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2575 variables 100%
c [elim-14] limit of 34400161 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 25 variables 1% in round 1 in 776343 steps
c [elim-14-1] backward subsumption/strengthening limit 776300
c [elim-14-1-1] backward checking 202 touched variables 8%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 1 clauses in 23676 steps
c [elim-14-1] rescheduled 8 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 2669 steps
c [elim-14-2] backward subsumption/strengthening limit 2600
c [elim-14-2-1] backward checking 8 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 2601 steps
c [elim-14-2] fully rescheduled 2549 variables 99%
c [elim-14-3] no variable eliminated in round 3 in 772285 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 26 = 1% variables out of 2575 scheduled
c [bca-10] limit of 10000000 steps and 27211 added (scaled 2)
c [bca-10] 2962 out of 5100 literals actually usable 58%
c [bca-10] added 4 blocked clauses in 17596 steps
c [sweep-10] limit 1000000 penalty 0 = 0 + 0
c [sweep-10-1] 107 pos 25.2% + 318 neg 74.8% = 425 sched 16.7% ret 2124
c [sweep-10-1] 969846 steps 255 queries 7.03 avg class size
c [sweep-10-1] 1586 decisions 252 SAT calls 23.62 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-38] removed 6 variables
c [sweep-10-1] removed 6 vars (0 failed, 3 eqs, 4 impls)
c [sweep-10-2] 422 pos 16.6% + 2121 neg 83.4% = 2543 sched 100.0% ret 0
c [sweep-10-2] 67176 steps 2 queries 1271.50 avg class size
c [sweep-10-2] 100 decisions 1 SAT calls 195.00 avg env size
c [sweep-10-2] 2543 variables remain 100% (0 retained 0%)
c [sweep-10-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] removed 6 vars in TOTAL (2 rounds, 255 queries)
c [sort-queue-14] sorted 377 enqueued variables after 25173 conflicts
c [score-dist-14] active 2166 (85%), one 0 (0%), zero 377 (15%)
c [score-dist-14] max exp 516, different 10 (2%)
c [score-dist-14] median active exp 516, avg 515.8
c [simplification-14] removed 35 variables 1.4% (2543 remain 2%)
c [simplification-14] removed 196 irredundant clauses 1.5% (13316 remain 2%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-14] new conflict interval 14000
c [simplification-14] penalized conflict interval 14000 = 1 * 14000
c [simplification-14] hard conflict limit 49173 (soft 39173 + delta 10000)
c [simplification-14] new conflict limit 39173 (hard 49173)
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   27.4    2542    13316     25896   11393    449 11519   35    73   15  48%     43   48   37   12  309%
c i   28.7    2541    13316     31758   17019    464 11524   36    72   18  50%     70   43   34   14  245%
c 
c [simplification-15] limit 39173 conflicts (hard 49173) hit after 39173 conflicts
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] all 2541 free variables schedulable
c [ternres-11] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 444 at-most-one constraints of average size 3.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 444 out of 444 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-40] removed 4 variables
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 5078 literals 100%
c [treelook-6] scheduling used 122593 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 311741 steps
c [treelook-6] 4980 literals remain 98%
c [treelook-6] 2528 variables remain to probed next time 100%
c [treelook-6] removed 11 variables, found 452 hbrs
c [unhide-14] limit 251840 with penalty 1 = 1 + 0
c [unhide-14-18] 0 units, 0 failed, 506 tauts, 0 hbrs, 29752 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 358 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 2528 variables 100%
c [elim-15] limit of 50368070 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 11 variables 0% in round 1 in 760100 steps
c [elim-15-1] backward subsumption/strengthening limit 760100
c [elim-15-1-1] backward checking 78 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 9432 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 11 = 0% variables out of 2528 scheduled
c [elim-15] 11 < 1/100 * 2528 = 25 considered unsuccessful
c [bca-11] limit of 10000000 steps and 26833 added (scaled 2)
c [bca-11] 2642 out of 5036 literals actually usable 52%
c [bca-11] added 6 blocked clauses in 29971 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 10000000 penalty 0 = 0 + 0
c [sweep-11-1] 387 pos 15.4% + 2130 neg 84.6% = 2517 sched 100.0% ret 0
c [sweep-11-1] 5557616 steps 342 queries 14.54 avg class size
c [sweep-11-1] 5424 decisions 339 SAT calls 64.75 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-42] removed 5 variables
c [sweep-11-1] removed 5 vars (0 failed, 3 eqs, 4 impls)
c [sweep-11-2] 386 pos 15.4% + 2126 neg 84.6% = 2512 sched 100.0% ret 0
c [sweep-11-2] 4577350 steps 113 queries 52.00 avg class size
c [sweep-11-2] 3527 decisions 111 SAT calls 138.32 avg env size
c [sweep-11-2] 499 variables remain 20% (2010 retained 80%)
c [decomp-43] removed 4 variables
c [sweep-11-2] removed 4 vars (0 failed, 1 eqs, 0 impls)
c [sweep-11] removed 9 vars in TOTAL (2 rounds, 453 queries)
c [sort-queue-15] sorted 317 enqueued variables after 39173 conflicts
c [score-dist-15] active 2191 (87%), one 0 (0%), zero 317 (13%)
c [score-dist-15] max exp 517, different 11 (2%)
c [score-dist-15] median active exp 517, avg 516.7
c [simplification-15] removed 33 variables 1.3% (2508 remain 2%)
c [simplification-15] removed 252 irredundant clauses 1.9% (13064 remain 2%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-15] new conflict interval 20666
c [simplification-15] penalized conflict interval 20666 = 1 * 20666
c [simplification-15] hard conflict limit 70172 (soft 59839 + delta 10333)
c [simplification-15] new conflict limit 59839 (hard 70172)
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   32.8    2507    13064     42089   27496    444 10919   36    67   27  53%    129   33   33   17  193%
c i   37.5    2506    13064     56683   41494    458 10926   40    69   30  59%    177   28   42   22  194%
c 
c [simplification-16] limit 59839 conflicts (hard 70172) hit after 59840 conflicts
c [quatres-9] found 1086 quaternary clauses 33% in total
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-12] limit 4156886 with penalty 0 = 0 + 0
c [ternres-12] all 2506 free variables schedulable
c [ternres-12] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-44] removed 2 variables
c [basicprobe-6] limit 20784432 penalty 0 = 0 + 0
c [basicprobe-6-0] 585 sched 23%, 12 failed, 1 lifted, 1271 hbrs
c [decomp-45] removed 12 variables
c [basicprobe-6-1] 754 sched 30%, 3 failed, 0 lifted, 816 hbrs
c [decomp-46] removed 3 variables
c [basicprobe-6-2] 750 sched 30%, 1 failed, 0 lifted, 55 hbrs
c [decomp-47] removed 1 variables
c [basicprobe-6-3] 752 sched 30%, 0 failed, 0 lifted, 24 hbrs
c [basicprobe-6-4] 740 probes remain 30% after last round
c [basicprobe-6-4] 17 units = 16 failed (94%) + 1 lifted (6%)
c [basicprobe-6-4] removed 16 variables, found 2167 hbrs
c [bate-4] eliminated 13 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 332 transitive binary clauses
c [cce-11] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 14
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-11-1] eliminated 1 clauses out of 324 (0%) of length 5
c [cce-11-1] eliminated 21 clauses out of 809 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 24 large clauses in 1960254 steps
c [cce-11-1] allowing another 980127 steps for small clauses
c [cce-11-1] scheduling 9968 clauses = 7904 binary + 2064 ternary
c [cce-11-1] tried to eliminate 7276 small clauses 73%
c [cce-11-1] eliminated 162 binary clauses 2%
c [cce-11-1] eliminated 35 ternary clauses 2%
c [cce-11-1] eliminated 197 small clauses 2%
c [cce-11-1] eliminated 197 small clauses in 15000000 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 221 covered clauses in round 1
c [cce-11] eliminated 221 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 25898 added (scaled 2)
c [bca-12] 2399 out of 4982 literals actually usable 48%
c [bca-12] added 10 blocked clauses in 49988 steps
c [sweep-12] limit 1247065 penalty 0 = 0 + 0
c [sweep-12-1] 115 pos 23.0% + 384 neg 77.0% = 499 sched 20.0% ret 1991
c [sweep-12-1] 1538316 steps 40 queries 25.27 avg class size
c [sweep-12-1] 936 decisions 39 SAT calls 113.54 avg env size
c [sweep-12-1] 382 variables remain 15% (2108 retained 85%)
c [sweep-12-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 0 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-16] sorted 286 enqueued variables after 59840 conflicts
c [score-dist-16] active 2204 (89%), one 0 (0%), zero 286 (11%)
c [score-dist-16] max exp 517, different 11 (2%)
c [score-dist-16] median active exp 517, avg 516.8
c [simplification-16] removed 16 variables 0.6% (2490 remain 2%)
c [simplification-16] removed 396 irredundant clauses 3.0% (12668 remain 2%)
c [simplification-16] maximum reduction of 3% = max (1%, 3%)
c [simplification-16] geometric conflict interval increment 5166 = 20666 / 4
c [simplification-16] new conflict interval 25832
c [simplification-16] penalized conflict interval 25832 = 1 * 25832
c [simplification-16] hard conflict limit 98588 (soft 85672 + delta 12916)
c [simplification-16] new conflict limit 85672 (hard 98588)
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 -   43.4    2490    12668     67817   17265    488 12434   33    55   22  60%    114    9   37   24  157%
c 
c [simplification-17] limit 85672 conflicts (hard 98588) hit after 85675 conflicts
c [ternres-13] limit 6023085 with penalty 0 = 0 + 0
c [ternres-13] all 2490 free variables schedulable
c [ternres-13] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] all 2490 free variables schedulable
c [simpleprobe-7] limit 24092342 penalty 0 = 0 + 0
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 0 variables, found 545 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 497 transitive binary clauses
c [cce-12] limit of 30115428 steps penalty 0 = 0 + 0
c [cce-12-1] completed large round (ATE)
c [cce-12-1] allowing another 890037 steps for small clauses
c [cce-12-1] scheduling 9369 clauses = 7740 binary + 1629 ternary
c [cce-12-1] tried to eliminate 9369 small clauses 100%
c [cce-12-1] eliminated 46 binary clauses 1%
c [cce-12-1] eliminated 7 ternary clauses 0%
c [cce-12-1] eliminated 53 small clauses 1%
c [cce-12-1] eliminated 53 small clauses in 18829078 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 53 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 889022 steps for small clauses
c [cce-12-2] scheduling 9316 clauses = 7694 binary + 1622 ternary
c [cce-12-2] tried to eliminate 5425 small clauses 58%
c [cce-12-2] incomplete small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 53 covered clauses in TOTAL during 2 rounds
c [cce-12] 53 < 1/100 * 12666 = 126 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2490 variables 100%
c [elim-16] limit of 60230857 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 44 variables 2% in round 1 in 728633 steps
c [elim-16-1] backward subsumption/strengthening limit 728600
c [elim-16-1-1] backward checking 297 touched variables 12%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 1 clauses in 30172 steps
c [elim-16-1] rescheduled 6 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 8479 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 44 = 2% variables out of 2490 scheduled
c [bca-13] limit of 10000000 steps and 25711 added (scaled 2)
c [bca-13] 2521 out of 4894 literals actually usable 52%
c [bca-13] added 8 blocked clauses in 36965 steps
c [sort-queue-17] sorted 257 enqueued variables after 85675 conflicts
c [score-dist-17] active 2189 (89%), one 0 (0%), zero 257 (11%)
c [score-dist-17] max exp 518, different 11 (2%)
c [score-dist-17] median active exp 518, avg 517.7
c [simplification-17] removed 44 variables 1.8% (2446 remain 2%)
c [simplification-17] removed 96 irredundant clauses 0.8% (12572 remain 2%)
c [simplification-17] maximum reduction of 2% = max (2%, 1%)
c [simplification-17] geometric conflict interval increment 8610 = 25832 / 3
c [simplification-17] new conflict interval 34442
c [simplification-17] penalized conflict interval 34442 = 1 * 34442
c [simplification-17] hard conflict limit 137338 (soft 120117 + delta 17221)
c [simplification-17] new conflict limit 120117 (hard 137338)
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 -   55.2    2446    12572    111111   24748    497 12093   15    19   20  79%    554  -24   12   24   51%
c 
c [simplification-18] limit 120117 conflicts (hard 137338) hit after 128003 conflicts
c [quatres-10] found 1183 quaternary clauses 26% in total
c [quatres-10-2] added 6 quaternary resolvents
c [ternres-14] limit 9215558 with penalty 0 = 0 + 0
c [ternres-14] all 2446 free variables schedulable
c [ternres-14] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-14] fully completed ternary resolution
c [treelook-7] limit 921555 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 4892 literals 100%
c [treelook-7] scheduling used 156885 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 921555 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 926122 steps
c [treelook-7] 4703 literals remain 96%
c [treelook-7] 2446 variables remain to probed next time 100%
c [treelook-7] removed 0 variables, found 4959 hbrs
c [unhide-15] limit 460777 with penalty 2 = 2 + 0
c [unhide-15-19] 0 units, 0 failed, 41 tauts, 0 hbrs, 29065 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 644 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2446 variables 100%
c [elim-17] limit of 184311169 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 4 variables 0% in round 1 in 724767 steps
c [elim-17-1] backward subsumption/strengthening limit 724700
c [elim-17-1-1] backward checking 41 touched variables 2%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 6003 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 4 = 0% variables out of 2446 scheduled
c [elim-17] 4 < 1/100 * 2446 = 24 considered unsuccessful
c [bca-14] limit of 10000000 steps and 25695 added (scaled 2)
c [bca-14] 2549 out of 4886 literals actually usable 52%
c [bca-14] added 8 blocked clauses in 45979 steps
c [sweep-13] limit 1382333 penalty 1 = 1 + 0
c [sweep-13-1] 88 pos 23.8% + 281 neg 76.2% = 369 sched 15.1% ret 2073
c [sweep-13-1] 1449854 steps 75 queries 10.64 avg class size
c [sweep-13-1] 1077 decisions 73 SAT calls 45.56 avg env size
c [sweep-13-1] 195 variables remain 8% (2247 retained 92%)
c [decomp-54] removed 1 variables
c [sweep-13-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-13] 1 < 1/1000 * 2442 = 2 considered unsuccessful
c [sweep-13] removed 1 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-18] sorted 251 enqueued variables after 128003 conflicts
c [score-dist-18] active 2190 (90%), one 0 (0%), zero 251 (10%)
c [score-dist-18] max exp 518, different 10 (2%)
c [score-dist-18] median active exp 518, avg 517.8
c [simplification-18] removed 5 variables 0.2% (2441 remain 2%)
c [simplification-18] removed 12 irredundant clauses 0.1% (12560 remain 2%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 34442
c [simplification-18] new conflict interval 68884
c [simplification-18] penalized conflict interval 68884 = 1 * 68884
c [simplification-18] hard conflict limit 231329 (soft 196887 + delta 34442)
c [simplification-18] new conflict limit 196887 (hard 231329)
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 -   64.2    2441    12560    145118   27379    525 16349   17    25   22  69%    744  -12   37   22  167%
c i   64.2    2440    12560    145274   27527    526 16349   18    26   26  68%    745  -11   34   22  154%
c i   65.5    2420    12560    151153   32945    538 16350   26    42   26  63%   -512    5   33   23  146%
c -   72.1    2420    12560    177783   27083    565 16358   17    22   22  75%    -64  -15   15   23   63%
c i   75.2    2419    12560    191930   40069    584 16366   26    42   28  62%    147    6   35   23  152%
c -   79.8    2419    12560    212326   28089    598 16370   21    32   32  68%    -93   -4   13   23   58%
c 
c [simplification-19] limit 196887 conflicts (hard 231329) hit after 218005 conflicts
c [quatres-11] found 1261 quaternary clauses 23% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1 quaternary resolvents
c [ternres-15] limit 16235518 with penalty 0 = 0 + 0
c [ternres-15] all 2419 free variables schedulable
c [ternres-15] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 202943 penalty 4 = 4 + 0
c [gauss-5] extracted 16 xors of average arity 2.9
c [gauss-5] connected 47 occurrences of 23 variables (average 2.0)
c [gauss-5] limit 202943 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-55] removed 2 variables
c [basicprobe-7] limit 81177594 penalty 0 = 0 + 0
c [basicprobe-7-0] 720 sched 31%, 69 failed, 3 lifted, 2583 hbrs
c [decomp-56] removed 90 variables
c [basicprobe-7-1] 671 sched 29%, 15 failed, 1 lifted, 2383 hbrs
c [decomp-57] removed 18 variables
c [basicprobe-7-2] 661 sched 29%, 3 failed, 0 lifted, 659 hbrs
c [decomp-58] removed 3 variables
c [basicprobe-7-3] 649 sched 28%, 3 failed, 0 lifted, 51 hbrs
c [decomp-59] removed 4 variables
c [basicprobe-7-4] 644 sched 28%, 1 failed, 0 lifted, 20 hbrs
c [decomp-60] removed 1 variables
c [basicprobe-7-5] 645 sched 28%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-7-6] 645 sched 28%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-7-7] 645 sched 28%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-8] 645 sched 28%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 95 units = 91 failed (96%) + 4 lifted (4%)
c [basicprobe-7-8] removed 116 variables, found 5716 hbrs
c [bate-5] eliminated 36 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 893 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2301 variables 100%
c [block-5] limit of 10147199 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 11 blocked clauses
c [block-5] 11 < 1/100 * 11420 = 114 considered unsuccessful
c [cce-13] boosting limit by 10
c [cce-13] limit of 405887970 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-13-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-13-1] eliminated 2 clauses out of 59 (3%) of length 6
c [cce-13-1] eliminated 8 clauses out of 236 (3%) of length 5
c [cce-13-1] eliminated 19 clauses out of 611 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 31 large clauses in 1192278 steps
c [cce-13-1] allowing another 596139 steps for small clauses
c [cce-13-1] scheduling 8513 clauses = 7006 binary + 1507 ternary
c [cce-13-1] tried to eliminate 8513 small clauses 100%
c [cce-13-1] eliminated 276 binary clauses 4%
c [cce-13-1] eliminated 69 ternary clauses 5%
c [cce-13-1] eliminated 345 small clauses 4%
c [cce-13-1] eliminated 345 small clauses in 14794493 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 376 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 57 (2%) of length 6
c [cce-13-2] eliminated 3 clauses out of 228 (1%) of length 5
c [cce-13-2] eliminated 3 clauses out of 592 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 7 large clauses in 1114537 steps
c [cce-13-2] allowing another 557268 steps for small clauses
c [cce-13-2] scheduling 8168 clauses = 6730 binary + 1438 ternary
c [cce-13-2] tried to eliminate 8168 small clauses 100%
c [cce-13-2] eliminated 20 binary clauses 0%
c [cce-13-2] eliminated 15 ternary clauses 1%
c [cce-13-2] eliminated 35 small clauses 0%
c [cce-13-2] eliminated 35 small clauses in 13965042 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 42 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 56 (2%) of length 6
c [cce-13-3] eliminated 4 clauses out of 225 (2%) of length 5
c [cce-13-3] eliminated 5 clauses out of 589 (1%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 10 large clauses in 1090320 steps
c [cce-13-3] allowing another 545160 steps for small clauses
c [cce-13-3] scheduling 8133 clauses = 6710 binary + 1423 ternary
c [cce-13-3] tried to eliminate 8133 small clauses 100%
c [cce-13-3] eliminated 8 binary clauses 0%
c [cce-13-3] eliminated 4 ternary clauses 0%
c [cce-13-3] eliminated 12 small clauses 0%
c [cce-13-3] eliminated 12 small clauses in 13760153 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 22 covered clauses in round 3
c [cce-13] eliminated 440 covered clauses in TOTAL during 3 rounds
c [bca-15] limit of 10000000 steps and 22513 added (scaled 2)
c [bca-15] 2575 out of 4604 literals actually usable 56%
c [bca-15] added 8 blocked clauses in 37598 steps
c [sort-queue-19] sorted 217 enqueued variables after 218005 conflicts
c [score-dist-19] active 2084 (91%), one 0 (0%), zero 217 (9%)
c [score-dist-19] max exp 519, different 11 (2%)
c [score-dist-19] median active exp 519, avg 518.7
c [simplification-19] removed 118 variables 4.9% (2301 remain 2%)
c [simplification-19] removed 1591 irredundant clauses 12.7% (10969 remain 2%)
c [simplification-19] maximum reduction of 13% = max (5%, 13%)
c [simplification-19] large reduction 13% >= 5% limit
c [simplification-19] next conflict interval 2180 = min (218005/100, 68884)
c [simplification-19] penalized conflict interval 2180 = 1 * 2180
c [simplification-19] hard conflict limit 230185 (soft 220185 + delta 10000)
c [simplification-19] new conflict limit 220185 (hard 230185)
c 
c [simplification-20] limit 220185 conflicts (hard 230185) hit after 220186 conflicts
c [quatres-12] found 1108 quaternary clauses 21% in total
c [quatres-12-1] removed 6 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 1 quaternary resolvents
c [ternres-16] limit 16359136 with penalty 0 = 0 + 0
c [ternres-16] all 2301 free variables schedulable
c [ternres-16] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-16] fully completed ternary resolution
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 524 transitive binary clauses
c [cce-14] limit of 81795682 steps penalty 0 = 0 + 0
c [cce-14-1] completed large round (ATE)
c [cce-14-1] allowing another 501792 steps for small clauses
c [cce-14-1] scheduling 8632 clauses = 6702 binary + 1930 ternary
c [cce-14-1] tried to eliminate 8632 small clauses 100%
c [cce-14-1] eliminated 42 ternary clauses 2%
c [cce-14-1] eliminated 42 small clauses 0%
c [cce-14-1] eliminated 42 small clauses in 13620253 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 42 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 500557 steps for small clauses
c [cce-14-2] scheduling 8590 clauses = 6702 binary + 1888 ternary
c [cce-14-2] tried to eliminate 8590 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 42 covered clauses in TOTAL during 2 rounds
c [cce-14] 42 < 1/100 * 10969 = 109 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2301 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 3271827300 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 215 variables 9% in round 1 in 640991 steps
c [elim-18-1] backward subsumption/strengthening limit 640900
c [elim-18-1-1] backward checking 785 touched variables 34%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 5 clauses in 74989 steps
c [elim-18-1] rescheduled 39 variables 2% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 16835 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 215 = 9% variables out of 2301 scheduled
c [bca-16] limit of 10000000 steps and 22003 added (scaled 2)
c [bca-16] 2343 out of 4174 literals actually usable 56%
c [bca-16] added 13 blocked clauses in 33594 steps
c [sort-queue-20] sorted 196 enqueued variables after 220186 conflicts
c [score-dist-20] active 1890 (91%), one 0 (0%), zero 196 (9%)
c [score-dist-20] max exp 519, different 10 (2%)
c [score-dist-20] median active exp 519, avg 518.7
c [simplification-20] removed 215 variables 9.3% (2086 remain 2%)
c [simplification-20] removed 257 irredundant clauses 2.3% (10712 remain 2%)
c [simplification-20] maximum reduction of 9% = max (9%, 2%)
c [simplification-20] large reduction 9% >= 5% limit
c [simplification-20] next conflict interval 2201 = min (220186/100, 68884)
c [simplification-20] penalized conflict interval 2201 = 1 * 2201
c [simplification-20] hard conflict limit 232387 (soft 222387 + delta 10000)
c [simplification-20] new conflict limit 222387 (hard 232387)
c 
c [simplification-21] limit 222387 conflicts (hard 232387) hit after 222388 conflicts
c [quatres-13] found 1070 quaternary clauses 21% in total
c [ternres-17] limit 16480094 with penalty 0 = 0 + 0
c [ternres-17] all 2086 free variables schedulable
c [ternres-17] 115 ternary resolvents (0 bin, 115 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 515002 penalty 4 = 4 + 0
c [card-6] found 808 at-most-one constraints of average size 3.7
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 515002 for elimination
c [card-6] 808 out of 808 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 135 at-most-one constraints, 133 used 99%
c [card-6] exported 2178 binary clauses, 16.4 per/constraint
c [simpleprobe-8] all 2086 free variables schedulable
c [simpleprobe-8] limit 32960189 penalty 1 = 1 + 0
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 0 variables, found 856 hbrs, 0 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 895 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2086 variables 100%
c [elim-19] limit of 329601896 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 8 variables 0% in round 1 in 620977 steps
c [elim-19-1] backward subsumption/strengthening limit 620900
c [elim-19-1-1] backward checking 80 touched variables 4%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 1 clauses in 9493 steps
c [elim-19-1] rescheduled 11 variables 1% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 5636 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 8 = 0% variables out of 2086 scheduled
c [elim-19] 8 < 1/100 * 2086 = 20 considered unsuccessful
c [bca-17] limit of 10000000 steps and 21957 added (scaled 2)
c [bca-17] 2320 out of 4158 literals actually usable 56%
c [bca-17] added 9 blocked clauses in 35529 steps
c [sweep-14] limit 1236007 penalty 2 = 2 + 0
c [sweep-14-1] 31 pos 16.8% + 153 neg 83.2% = 184 sched 8.9% ret 1894
c [sweep-14-1] 600082 steps 129 queries 6.85 avg class size
c [sweep-14-1] 777 decisions 128 SAT calls 25.84 avg env size
c [sweep-14-1] fully completed sweeping round
c [sweep-14-1] removed 0 vars (0 failed, 0 eqs, 4 impls)
c [sweep-14-2] 333 pos 16.0% + 1745 neg 84.0% = 2078 sched 100.0% ret 0
c [sweep-14-2] 766523 steps 8 queries 380.62 avg class size
c [sweep-14-2] 443 decisions 7 SAT calls 152.43 avg env size
c [sweep-14-2] 2040 variables remain 98% (38 retained 2%)
c [sweep-14-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 0 vars in TOTAL (2 rounds, 135 queries)
c [sort-queue-21] sorted 193 enqueued variables after 222388 conflicts
c [score-dist-21] active 1885 (91%), one 0 (0%), zero 193 (9%)
c [score-dist-21] max exp 519, different 10 (2%)
c [score-dist-21] median active exp 519, avg 518.7
c [simplification-21] removed 8 variables 0.4% (2078 remain 2%)
c [simplification-21] removed 26 irredundant clauses 0.2% (10686 remain 2%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 68884
c [simplification-21] new conflict interval 137768
c [simplification-21] penalized conflict interval 137768 = 1 * 137768
c [simplification-21] hard conflict limit 429040 (soft 360156 + delta 68884)
c [simplification-21] new conflict limit 360156 (hard 429040)
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 -   92.9    2078    10686    255536   28480    692 16136   23    34   19  68%    446   -1   16   23   70%
c i   97.7    2077    10686    279790   49037    707 16148   13    17   26  80%    625  -15    8   21   37%
c -  100.9    2060    10686    293486   30061    728 16152   24    35   20  69%   -431    2   13   22   58%
c -  108.8    2060    10686    330349   30016    761 16163   26    38   28  70%    195    2   18   24   74%
c i  114.3    2059    10686    357650   55017    780 16165   25    35   36  72%    477   -2    9   25   34%
c i  114.4    2047    10686    358499   55727    782 16167   22    31   36  72%   -196   -6    7   25   29%
c i  114.4    2046    10686    358503   55730    782 16167   22    31   36  72%   -198   -6    7   25   29%
c i  114.5    2045    10686    358507   55727    782 16170   22    31   36  72%   -201   -6    7   25   28%
c -  116.7    1990    10686    368051   30947    797 16173   22    31   28  72%   -509   -6   15   25   58%
c 
c [simplification-22] limit 360160 conflicts (hard 429040) hit after 395574 conflicts
c [ternres-18] limit 28922776 with penalty 0 = 0 + 0
c [ternres-18] all 1990 free variables schedulable
c [ternres-18] 21 ternary resolvents (0 bin, 21 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-69] removed 100 variables
c [unhide-16] limit 723069 with penalty 3 = 3 + 0
c [unhide-16-20] 0 units, 1 failed, 3645 tauts, 0 hbrs, 36888 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 639 transitive binary clauses
c [transred-18] found 2 units
c [cce-15] limit of 72306941 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-15-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-15-1] eliminated 1 clauses out of 4 (25%) of length 15
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-15-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-15-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-15-1] eliminated 1 clauses out of 9 (11%) of length 8
c [cce-15-1] eliminated 3 clauses out of 26 (12%) of length 7
c [cce-15-1] eliminated 4 clauses out of 58 (7%) of length 6
c [cce-15-1] eliminated 14 clauses out of 200 (7%) of length 5
c [cce-15-1] eliminated 40 clauses out of 538 (7%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 74 large clauses in 1133733 steps
c [cce-15-1] allowing another 566866 steps for small clauses
c [cce-15-1] scheduling 7423 clauses = 6140 binary + 1283 ternary
c [cce-15-1] tried to eliminate 7423 small clauses 100%
c [cce-15-1] eliminated 269 binary clauses 4%
c [cce-15-1] eliminated 76 ternary clauses 6%
c [cce-15-1] eliminated 345 small clauses 5%
c [cce-15-1] eliminated 363 small clauses in 13087011 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 437 covered clauses in round 1
c [cce-15-2] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-15-2] eliminated 1 clauses out of 8 (12%) of length 8
c [cce-15-2] eliminated 3 clauses out of 54 (6%) of length 6
c [cce-15-2] eliminated 3 clauses out of 186 (2%) of length 5
c [cce-15-2] eliminated 5 clauses out of 498 (1%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 13 large clauses in 1022549 steps
c [cce-15-2] allowing another 511274 steps for small clauses
c [cce-15-2] scheduling 7078 clauses = 5871 binary + 1207 ternary
c [cce-15-2] tried to eliminate 7078 small clauses 100%
c [cce-15-2] eliminated 13 binary clauses 0%
c [cce-15-2] eliminated 8 ternary clauses 1%
c [cce-15-2] eliminated 21 small clauses 0%
c [cce-15-2] eliminated 21 small clauses in 12090518 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 34 covered clauses in round 2
c [cce-15-3] eliminated 1 clauses out of 51 (2%) of length 6
c [cce-15-3] eliminated 4 clauses out of 493 (1%) of length 4
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 5 large clauses in 1012758 steps
c [cce-15-3] allowing another 506379 steps for small clauses
c [cce-15-3] scheduling 7057 clauses = 5858 binary + 1199 ternary
c [cce-15-3] tried to eliminate 7057 small clauses 100%
c [cce-15-3] eliminated 4 binary clauses 0%
c [cce-15-3] eliminated 4 ternary clauses 0%
c [cce-15-3] eliminated 8 small clauses 0%
c [cce-15-3] eliminated 8 small clauses in 11971711 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 13 covered clauses in round 3
c [cce-15] eliminated 484 covered clauses in TOTAL during 3 rounds
c [bca-18] limit of 10000000 steps and 19652 added (scaled 2)
c [bca-18] 2256 out of 3952 literals actually usable 57%
c [bca-18] added 4 blocked clauses in 51731 steps
c [sort-queue-22] sorted 173 enqueued variables after 395574 conflicts
c [score-dist-22] active 1802 (91%), one 0 (0%), zero 173 (9%)
c [score-dist-22] max exp 520, different 10 (2%)
c [score-dist-22] median active exp 520, avg 519.6
c [simplification-22] removed 15 variables 0.8% (1975 remain 1%)
c [simplification-22] removed 1155 irredundant clauses 10.8% (9531 remain 2%)
c [simplification-22] maximum reduction of 11% = max (1%, 11%)
c [simplification-22] large reduction 11% >= 5% limit
c [simplification-22] next conflict interval 3955 = min (395574/100, 137768)
c [simplification-22] penalized conflict interval 3955 = 1 * 3955
c [simplification-22] hard conflict limit 409529 (soft 399529 + delta 10000)
c [simplification-22] new conflict limit 399529 (hard 409529)
c 
c [simplification-23] limit 399529 conflicts (hard 409529) hit after 399529 conflicts
c [quatres-14] found 1424 quaternary clauses 25% in total
c [quatres-14-1] removed 9 duplicate quaternary clauses
c [quatres-14-2] added 9 single-self-subsuming ternary resolvents
c [quatres-14-2] added 2 quaternary resolvents
c [ternres-19] limit 29255810 with penalty 0 = 0 + 0
c [ternres-19] all 1975 free variables schedulable
c [ternres-19] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-70] removed 2 variables
c [treelook-8] limit 1462790 penalty 1 = 1 + 0 boost 1
c [treelook-8] scheduled 3946 literals 100%
c [treelook-8] scheduling used 176554 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 1462790 penalty 1 = 1 + 0 boost 1
c [treelook-8] used 1465955 steps
c [treelook-8] 3615 literals remain 93%
c [treelook-8] 1947 variables remain to probed next time 100%
c [treelook-8] removed 26 variables, found 5909 hbrs
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 812 transitive binary clauses
c [transred-19] found 1 units
c [cce-16] limit of 146279052 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 183 (1%) of length 5
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 1 large clauses in 899786 steps
c [cce-16-1] allowing another 449893 steps for small clauses
c [cce-16-1] scheduling 6985 clauses = 5877 binary + 1108 ternary
c [cce-16-1] tried to eliminate 6985 small clauses 100%
c [cce-16-1] eliminated 50 binary clauses 1%
c [cce-16-1] eliminated 1 ternary clauses 0%
c [cce-16-1] eliminated 51 small clauses 1%
c [cce-16-1] eliminated 52 small clauses in 11053859 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 53 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 449636 steps for small clauses
c [cce-16-2] scheduling 6934 clauses = 5827 binary + 1107 ternary
c [cce-16-2] tried to eliminate 6934 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 53 covered clauses in TOTAL during 2 rounds
c [cce-16] 53 < 1/100 * 9345 = 93 considered unsuccessful
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 1946 variables 100%
c [elim-20] limit of 292558105 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 118 variables 6% in round 1 in 520346 steps
c [elim-20-1] backward subsumption/strengthening limit 520300
c [elim-20-1-1] backward checking 517 touched variables 27%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 1 and strengthened 0 clauses in 46507 steps
c [elim-20-1] rescheduled 2 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 630 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 118 = 6% variables out of 1946 scheduled
c [bca-19] limit of 10000000 steps and 18916 added (scaled 2)
c [bca-19] 2060 out of 3658 literals actually usable 56%
c [bca-19] added 5 blocked clauses in 46892 steps
c [sort-queue-23] sorted 134 enqueued variables after 399529 conflicts
c [score-dist-23] active 1694 (93%), one 0 (0%), zero 134 (7%)
c [score-dist-23] max exp 520, different 10 (2%)
c [score-dist-23] median active exp 520, avg 519.6
c [simplification-23] removed 147 variables 7.4% (1828 remain 1%)
c [simplification-23] removed 369 irredundant clauses 3.9% (9162 remain 1%)
c [simplification-23] maximum reduction of 7% = max (7%, 4%)
c [simplification-23] large reduction 7% >= 5% limit
c [simplification-23] next conflict interval 3995 = min (399529/100, 137768)
c [simplification-23] penalized conflict interval 3995 = 1 * 3995
c [simplification-23] hard conflict limit 413524 (soft 403524 + delta 10000)
c [simplification-23] new conflict limit 403524 (hard 413524)
c 
c [simplification-24] limit 403524 conflicts (hard 413524) hit after 403526 conflicts
c [quatres-15] found 1412 quaternary clauses 26% in total
c [quatres-15-2] added 2 quaternary resolvents
c [ternres-20] limit 29555153 with penalty 0 = 0 + 0
c [ternres-20] all 1828 free variables schedulable
c [ternres-20] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-20] fully completed ternary resolution
c [basicprobe-8] limit 147775769 penalty 0 = 0 + 0
c [basicprobe-8-0] 579 sched 32%, 12 failed, 1 lifted, 1371 hbrs
c [decomp-73] removed 16 variables
c [basicprobe-8-1] 566 sched 31%, 3 failed, 0 lifted, 69 hbrs
c [decomp-74] removed 3 variables
c [basicprobe-8-2] 563 sched 31%, 0 failed, 0 lifted, 36 hbrs
c [basicprobe-8-3] 563 sched 31%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-3] fully completed probing
c [basicprobe-8-3] 16 units = 15 failed (94%) + 1 lifted (6%)
c [basicprobe-8-3] removed 19 variables, found 1476 hbrs
c [bate-6] eliminated 23 asymmetric tautologies during probing
c [unhide-17] limit 1477757 with penalty 2 = 2 + 0
c [unhide-17-23] 0 units, 0 failed, 1616 tauts, 0 hbrs, 31422 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 493 transitive binary clauses
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 1809 variables 100%
c [elim-21] limit of 591103077 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 24 variables 1% in round 1 in 501808 steps
c [elim-21-1] backward subsumption/strengthening limit 501800
c [elim-21-1-1] backward checking 167 touched variables 9%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 13992 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 24 = 1% variables out of 1809 scheduled
c [bca-20] limit of 10000000 steps and 18478 added (scaled 2)
c [bca-20] 1974 out of 3572 literals actually usable 55%
c [bca-20] added 11 blocked clauses in 50014 steps
c [sort-queue-24] sorted 116 enqueued variables after 403526 conflicts
c [score-dist-24] active 1669 (94%), one 0 (0%), zero 116 (6%)
c [score-dist-24] max exp 520, different 10 (2%)
c [score-dist-24] median active exp 520, avg 519.6
c [simplification-24] removed 43 variables 2.4% (1785 remain 1%)
c [simplification-24] removed 220 irredundant clauses 2.4% (8942 remain 1%)
c [simplification-24] maximum reduction of 2% = max (2%, 2%)
c [simplification-24] geometric conflict interval increment 45922 = 137768 / 3
c [simplification-24] new conflict interval 183690
c [simplification-24] penalized conflict interval 183690 = 1 * 183690
c [simplification-24] hard conflict limit 679061 (soft 587216 + delta 91845)
c [simplification-24] new conflict limit 587216 (hard 679061)
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 -  133.1    1785     8942    424815   30654    789 12771   24    33   22  73%    379   -2   12   25   49%
c i  133.4    1784     8942    426438   31925    805 12777   19    25   25  75%    395   -9    7   24   29%
c i  133.8    1783     8942    429137   34282    807 12778   17    23   25  74%   -537  -12   11   24   45%
c -  141.9    1783     8942    464155   31452    837 12785   31    43   22  73%     39    9   34   25  136%
c -  150.4    1783     8942    504042   32774    859 12787   20    25   22  81%    488   -9   14   25   55%
c -  159.3    1783     8942    545091   33413    877 12788   29    40   32  73%    737    8   31   25  126%
c i  161.1    1782     8942    554973   42204    884 12788   29    40   37  73%    778    6   18   25   73%
c -  167.9    1782     8942    585735   34098    911 12791   26    33   33  78%   -379   -0   21   25   81%
c 
c [simplification-25] limit 587216 conflicts (hard 679061) hit after 610246 conflicts
c [quatres-16] found 1597 quaternary clauses 25% in total
c [quatres-16-1] removed 9 duplicate quaternary clauses
c [quatres-16-2] added 5 single-self-subsuming ternary resolvents
c [quatres-16-2] added 8 quaternary resolvents
c [ternres-21] limit 45090707 with penalty 0 = 0 + 0
c [ternres-21] all 1782 free variables schedulable
c [ternres-21] 37 ternary resolvents (0 bin, 37 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 563633 penalty 4 = 4 + 0
c [gauss-6] extracted 9 xors of average arity 3.0
c [gauss-6] connected 27 occurrences of 9 variables (average 3.0)
c [gauss-6] limit 563633 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 351 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 1782 variables 100%
c [block-6] limit of 28181692 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [cce-17] limit of 112726769 steps penalty 1 = 1 + 0
c [cce-17-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-17-1] eliminated 1 clauses out of 30 (3%) of length 7
c [cce-17-1] eliminated 3 clauses out of 66 (5%) of length 6
c [cce-17-1] eliminated 16 clauses out of 540 (3%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 21 large clauses in 1207881 steps
c [cce-17-1] allowing another 603940 steps for small clauses
c [cce-17-1] scheduling 7029 clauses = 5578 binary + 1451 ternary
c [cce-17-1] tried to eliminate 7029 small clauses 100%
c [cce-17-1] eliminated 117 binary clauses 2%
c [cce-17-1] eliminated 81 ternary clauses 6%
c [cce-17-1] eliminated 198 small clauses 3%
c [cce-17-1] eliminated 198 small clauses in 11169669 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 219 covered clauses in round 1
c [cce-17-2] eliminated 2 clauses out of 524 (0%) of length 4
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] eliminated 2 large clauses in 1167820 steps
c [cce-17-2] allowing another 583910 steps for small clauses
c [cce-17-2] scheduling 6831 clauses = 5461 binary + 1370 ternary
c [cce-17-2] tried to eliminate 6831 small clauses 100%
c [cce-17-2] eliminated 14 binary clauses 0%
c [cce-17-2] eliminated 9 ternary clauses 1%
c [cce-17-2] eliminated 23 small clauses 0%
c [cce-17-2] eliminated 23 small clauses in 10715621 steps
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 25 covered clauses in round 2
c [cce-17-3] completed large round (ACCE)
c [cce-17-3] allowing another 578512 steps for small clauses
c [cce-17-3] scheduling 6808 clauses = 5447 binary + 1361 ternary
c [cce-17-3] tried to eliminate 6808 small clauses 100%
c [cce-17-3] eliminated 1 ternary clauses 0%
c [cce-17-3] eliminated 1 small clauses 0%
c [cce-17-3] eliminated 1 small clauses in 10673502 steps
c [cce-17-3] completed small round (ACCE)
c [cce-17-3] eliminated 1 covered clauses in round 3
c [cce-17] eliminated 245 covered clauses in TOTAL during 3 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 1782 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 37 variables 2% in round 1 in 487305 steps
c [elim-22-1] backward subsumption/strengthening limit 487300
c [elim-22-1-1] backward checking 260 touched variables 15%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 25132 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 37 = 2% variables out of 1782 scheduled
c [bca-21] limit of 10000000 steps and 17846 added (scaled 2)
c [bca-21] 1935 out of 3492 literals actually usable 55%
c [bca-21] added 6 blocked clauses in 57286 steps
c [sweep-15] limit 1690901 penalty 3 = 3 + 0
c [sweep-15-1] 253 pos 14.7% + 1464 neg 85.3% = 1717 sched 98.4% ret 28
c [sweep-15-1] 1936629 steps 17 queries 178.18 avg class size
c [sweep-15-1] 692 decisions 16 SAT calls 130.69 avg env size
c [sweep-15-1] 1417 variables remain 81% (328 retained 19%)
c [sweep-15-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] removed 0 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-25] sorted 100 enqueued variables after 610246 conflicts
c [score-dist-25] active 1645 (94%), one 0 (0%), zero 100 (6%)
c [score-dist-25] max exp 521, different 11 (2%)
c [score-dist-25] median active exp 521, avg 520.5
c [simplification-25] removed 37 variables 2.1% (1745 remain 1%)
c [simplification-25] removed 319 irredundant clauses 3.6% (8623 remain 1%)
c [simplification-25] maximum reduction of 4% = max (2%, 4%)
c [simplification-25] geometric conflict interval increment 36738 = 183690 / 5
c [simplification-25] new conflict interval 220428
c [simplification-25] penalized conflict interval 220428 = 1 * 220428
c [simplification-25] hard conflict limit 940888 (soft 830674 + delta 110214)
c [simplification-25] new conflict limit 830674 (hard 940888)
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  177.6    1744     8623    625999   66016    956 12017   18    22   28  83%    265  -10   10   25   41%
c -  178.7    1735     8623    630731   34868    959 12019   22    29   23  76%   -720   -3   26   24  105%
c -  188.2    1735     8623    674418   35916   1001 12036   24    29   23  82%    123   -2   20   24   84%
c i  190.7    1734     8623    688296   47586   1018 12046   34    42   29  82%    295   10   16   25   63%
c i  192.0    1678     8623    694935   53004   1050 12057   29    34   31  84%   -527    2   14   26   53%
c i  192.0    1193     8623    694936   53004   1050 12057   29    34   31  84%   -527    2   14   26   53%
c 0  192.0    1042     8623    694936   53004   1050 12057   29    34   31  84%   -527    2   14   26   53%
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: 207 basic ate = 183 trn 88% + 24 lrg 12% in 6 updates
c bcas: 21 count, 206 added (209 skipped), 674127 steps
c bkwd: tried 179734 clauses, 359062 lits, 2.00 lits/clause
c bkwd: checked 3877422 occs, 21.57 occs/clause, 10.80 occs/lit
c bkwd: subsumed 78 binary, 137 ternary, 107 large
c bkwd: strengthened 18 binary, 2 ternary (100% self), 402 large (0% self)
c blkd: 6 bces, 767 removed, 476766 resolutions, 1296901 steps
c blkd: 1966 blocking literals 1%, 11 pure
c bump: 696212 bumped seen, 77457988 lits 111.3 on average
c card: 6 count, 0 units, 5372 am1, 11209169 steps
c card: 21 rescheduled, 180 eliminated, 448 resolved, 69282 subsumed
c card: 19971 at-most-one constraints found, average size 4.39
c card: 19971 at-most-one constraints used 100%, average size 4.39
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 17 cces, 16522 eliminated, 15266 ate 92%, 1256 abce 8%
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: 2059333 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 190 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 77 decompositions, 41671 equivalent 29%
c deco: 1019 decision-only clauses 0%, 46% reduction
c decs: 2057216 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 22 elims, 13895 eliminated 10%, 67 pure 0%
c elms: 60 rounds, 2.7 rounds/bve
c elms: 13166 small 95%, 651 large 5%
c elms: 47604 tried small, 13168 succeeded 28%, 34436 failed 72%
c elms: 3846 subsumed, 5727 strengthened, 493 blocked
c elms: 2749965 copies, 2497025 resolutions, 1472480 ipos
c elms: 468549 subchks, 340164 strchks
c gaus: 6 extractions, 358 extracted, 2.9 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7612668 steps, 3806334 extr 50%, 6832 elim 0%
c glue: 25.7 orig avg, 25.7 real avg, 4.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 118989 = 17644 simple 15% + 89561 trn 75% + 11784 lrg 10%, 1114 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 696212 clauses, 52.5 length
c lrnd: 36555115 lits = 53402186 orig - 16847071 removed 32%
c lrnd: 236526 uips 34%, 419898 flips 60%
c mins: 691130 mins 99%, 262 bin 0%, 3746 size 1%
c mins: 68301165 poisoned searches, 11844167 hits, 17% hit rate
c mins: 108794426 used twice searches, 13513496 hits, 12% hit rate
c move: moved 14605, 11212 bin 77%, 3393 trn 23%
c otfs: 1387 driving 27%, 3681 restarting 73%
c otfs: str 5068, 5040 red 99%, 28 irr 1%
c otfs: str 5068, 0 bin 0%, 33 trn 1%, 5035 lrg 99%
c otfs: sub 18, 18 red 100%, 0 irr 0%
c otfs: sub 18, 0 bin 0%, 0 trn 0%, 18 lrg 100%
c phas: 3 computed, 14223 set, 0 pos (0%), 14223 neg (100%)
c prbs: 8 basic, 26401 probed, 708 failed, 53 lifted
c prbs: 8 simple, 193815 probed, 1270 failed, 18391 eqs
c prbs: 8 treelook, 678 probed, 43 failed, 0 lifted
c prom: 128137 locked 9% out of 1483456 tried
c prps: 188671648 props, 87 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 16 count, 53 quat, 17 self1, 0 self2, 34 dup
c queu: 25 sorted, 2057216 next (46 steps 0.00)
c queu: 77644924 enq (326533228 steps 4.21), 77457988 deq 100%
c redc: 5062 clauses 19%, 26188 tried 4%, 2 sat 0%
c redc: 15186 lits 5%, 328973 tried 1%, 2 sat 0%
c redc: 748 times jump level reduced, 5.6 levels on average
c reds: 16 count, 43433.5 conflicts per reduce
c reds: 0 memlim 0%, 16 arith 100%
c reds: 460055 collected 88%, 62676 retired 12%
c rmbd: 3864 removed, 1043 red 27%
c rsts: 15709 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: 25 count, 24 confs 96%, 0 vars 0%
c simp: 1 its 4%, 0 bin 0%, 0 trns 0%
c subl: 696212 count (584681 tried 0.8), 74465 sub out of 694597 (10.7%)
c swps: 15 count, 19 rounds, 1946 queries (102.4/round)
c swps: 1832 sat calls, 71 unsat (1.5% success rate)
c swps: 27294 decisions 14.9, 2663 conflicts 1.5
c swps; 58.8 avg class size, 61.1 avg environment size
c swps: 1 failed, 136 impls, 169 equivs
c swp0: 641 type 0 queries, 310 unsat (48.4%), 592 sat (92.4%)
c swp1: 1305 type 1 queries, 699 unsat (53.6%), 1185 sat (90.8%)
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: 5507464 calls to obtain time
c tops: 85252 fixed 60%, 115 its, 6042.92 confs/it
c trds: 21 transitive reductions, 11684 removed, 81 failed
c trds: 72837 nodes, 199056 edges, 32578167 steps
c trim: 699948 words, 2.7 MB
c trnr: 21 count, 2 bin, 893 trn, 15892231 steps
c unhd: 17 count, 23 rounds, 9080538 steps
c unhd: 346 non-trivial sccs of average size 2.4
c unhd: 21 units, 21 bin, 0 trn, 0 lrg
c unhd: 1858 failed, 1853 stamp, 0 lits, 4 bin, 1 trn, 0 lrg
c unhd: 37193 tauts, 2193 bin 6%, 697 trn 2%, 2407 lrg 6%
c unhd: 37193 tauts, 31896 stamp 86%, 26294 red 71%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 236200 str, 21 bin 0%, 545 trn 0%, 235634 lrg 100%, 233689 red 99%
c vars: 1042 remaining 1% and 140818 removed 99% out of 141860
c vars: 85252 fixed 60%, 13895 eliminated 10%, 41671 equivalent 29%
c vsts: 5294793225 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 29.0 search visits per propagation, 7461.3 per conflict
c wchs: 2490314989 pushed, 7974563 enlarged, 295 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         694650        460055         62676      18102149       5181346        331613
c 
c  0 0         14358   2      2718   1         0   0   5203405  29    976461  19     25017   8     0.3
c  1 5         10110   1      4900   1      1186   2   1604039   9    399970   8     14630   4     0.2
c  2 6         43228   6     26262   6      3868   6   2761864  15<   763609  15     38266  12     1.1
c  3 9        102702  15     68433  15      7321  12   3238907  18   1026524  20<    66794  20     2.2
c  4 14       156125  22    111611  24     10189  16   2672278  15    918257  18     71523  22<    2.6
c  5 21       153378  22<   109486  24<    11172  18<  1379547   8    573898  11     56141  17     3.0
c  6 30       103856  15     70504  15     10659  17    654199   4    291696   6     31865  10     2.3
c  7 41        59963   9     37643   8      8583  14    391215   2    147225   3     17090   5     2.4
c  8 54        31808   5     19008   4      5641   9    133875   1     57211   1      7056   2     2.1
c  9 69        12744   2      7062   2      2692   4     40742   0     18044   0      2097   1     1.5
c 10 86         5234   1      2253   0      1219   2     18660   0      7119   0       957   0     1.0
c 11 126        1126   0       175   0       146   0      3390   0      1318   0       171   0     0.2
c 12 230          18   0         0   0         0   0        28   0        14   0         6   0     0.0
c 
c avg                  4.7           4.7           5.3           2.4           2.9           3.8
c std                  1.9           1.7           2.0           2.0           2.1           2.0
c 
c   16.718   9% cce
c    8.436   4% bump
c    5.757   3% probe
c    3.077   2% unhide
c    2.652   1% elim
c    2.154   1% sweep
c    1.917   1% transred
c 
c    2.580 < 1% rest (below)
c 
c    1.158   1% decide
c    0.494   0% bca
c    0.291   0% gauss
c    0.264   0% card
c    0.200   0% block
c    0.098   0% ternres
c    0.075   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.268   1% preprocessing     4%
c   34.121  18% inprocessing     96%
c ==================================
c   35.389  18% simplifying
c  156.637  82% search
c ==================================
c  192.029 100% all
c 
c        694936 conflicts,        3618.9 confs/sec
c           854 ternaries,         813.7 confs/ternary
c           349 binaries,         1991.2 confs/binary
c           115 iterations,       6042.9 confs/iteration
c 
c            16 reductions,          0.1 redus/sec,  43433.5 confs/reduction
c         15709 restarts,           81.8 rests/sec,     44.2 confs/restart
c       2057216 decisions,       10713.1 decis/sec,      3.0 decis/conflict
c     188671648 propagations,   982517.1 props/sec,     91.7 props/decision
c 
c 192.0 seconds, 52.0 MB
c launch: done
