c launch: /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version ayv 86bf266b9332599f1b876e28a02fe8427aeaa2db
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat Oct 11 12:11:52 CEST 2014
c compiled Sat Oct 11 12:11:52 CEST 2014
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNDBLSCR  -I../yalsat -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT
c -DNLGLDRUPLIG
c Linux cluster2 3.13.0-36-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 260342 1391257' header
c read 260342 variables, 1391257 clauses, 3358569 literals in 0.00 seconds
c
c --abstime=0
c --actavgmax=112
c --actdblarithlim=3
c --actgeomlim=2
c --actgsdul=7
c --acts=2
c --actstdmax=112
c --actstdmin=10
c --actvlim=200000
c --agile=1
c --agilelim=30
c --agilesinint=100000
c --bate=1
c --batewait=2
c --bca=1
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bva=0
c --bias=2
c --binlocsdel=10
c --binsimpdel=2
c --bkwdscale=2
c --blkboost=10
c --blkboostvlim=1000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim=1000000
c --blkocclim1=100000
c --blkocclim2=10000
c --blkreleff=100
c --blkrtc=0
c --blksched2b2=0
c --blkschedmin=0
c --blkschedprod=0
c --blkschedpure=1
c --blkschedsum=1
c --blksmall=1
c --blksuccesslim=10000
c --blksuccessrat=1000
c --block=1
c --blockwait=1
c --boost=1
c --bumpbcplits=0
c --bumpclslits=0
c --bumpseenaftermin=0
c --bumpseenbeforemin=1
c --bumpseenlits=1
c --bumpseenminsize=3
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 --cce=3
c --cceboost=10
c --cceboostvlim=1000000
c --cce2wait=1
c --cce3wait=2
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --cceonlyifstuck=0
c --ccereleff=20
c --ccertc=0
c --ccesuccesslim=10000
c --ccesuccessrat=1000
c --ccewait=2
c --cgrclsr=1
c --cgrclsrwait=2
c --cgreleff=1
c --cgrextand=1
c --cgrexteq=1
c --cgrextite=1
c --cgrextunits=1
c --cgrextxor=1
c --cgrmaxeff=8000000
c --cgrmaxority=20
c --cgrmineff=200000
c --cintinc=20000
c --cintincdiv=1
c --cintmaxhard=10000000
c --cintmaxsoft=1000000
c --cliff=1
c --cliffmaxeff=100000000
c --cliffmineff=10000000
c --cliffreleff=8
c --cliffwait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=30
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --drup=0
c --druplig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=40
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim=1000000
c --elmocclim1=1000
c --elmocclim2=100
c --elmreleff=200
c --elmroundlim=3
c --elmrtc=0
c --elmsched2b2=0
c --elmschediff=0
c --elmschedmin=0
c --elmschedprod=0
c --elmschedpure=1
c --elmschedsum=1
c --elmsuccesslim=1000
c --elmsuccessrat=1000
c --exitonabort=0
c --factmax=100000
c --factor=3
c --flipdur=10
c --flipint=10
c --flipldmod=4
c --fliplevels=6
c --flipping=1
c --fliptop=1
c --flipvlim=100000
c --force=0
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=3
c --gluescale=4
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --itlocsdel=100
c --itsimpdel=20
c --jwhred=1
c --keepmaxglue=1
c --lftmaxeff=20000000
c --lftmineff=500000
c --lftreleff=6
c --lftroundlim=5
c --lhbr=1
c --lift=1
c --liftlrg=3
c --liftwait=2
c --lkhd=2
c --lkhdmisifelmrtc=0
c --locs=0
c --locsboost=2
c --locscint=10000
c --locsdec=2
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsclim=1000000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxglue=2147483647
c --maxscorexp=500
c --mega=0
c --megaint=4
c --megawait=2
c --memlim=-1
c --minimize=2
c --minlocalgluelim=30
c --minrecgluelim=20
c --mocint=1000
c --move=2
c --otfs=1
c --otfsbump=0
c --otfsconf=0
c --penmax=4
c --phase=0
c --phaseflip=0
c --phasegluebit=0
c --phaseneginit=0
c --plain=0
c --plim=-1
c --prbasic=1
c --prbasicmaxeff=100000000
c --prbasicmineff=1000000
c --prbasicreleff=10
c --prbasicroundlim=9
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 --psm=3
c --pure=1
c --randec=0
c --randecflipint=0
c --randecint=1000
c --rdp=0
c --rdpclslim=3
c --rdplim=100
c --rdpmaxeff=10000000
c --rdpmineff=10000
c --rdpmodelm=0
c --rdpreleff=2
c --rdpwait=2
c --redfixed=0
c --redinoutinc=100
c --redlbound=0
c --redlexpfac=10
c --redlinc=1000
c --redlinit=4000
c --redlmaxabs=1000000
c --redlmaxinc=200
c --redlmaxrel=300
c --redlminabs=500
c --redlmininc=10
c --redlminrel=10
c --redloutinc=10000
c --redoutclim=5000
c --redoutvlim=1000
c --reduce=2
c --rephase=1
c --rephaseinc=10000
c --restart=2
c --restartinit=0
c --restartint=5
c --restartintscale=0
c --reusetrail=1
c --rmincpen=4
c --rstinoutinc=110
c --saturating=70
c --scincinc=200
c --score=5
c --seed=0
c --simpdelay=0
c --simpen=0
c --simpidiv=3
c --simpinterdelay=2000
c --simpiscale=100
c --simplify=2
c --simprtc=5
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 --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --tabr=3
c --tabrcfactor=2
c --tabrkeep=3
c --tabrvfactor=4
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=20
c --treelookfull=0
c --treelooklrg=1
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=1
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 --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --verbose=1
c [freezer] frozen 0 variables out of 247193 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 [init-scores] score increment factor 1.200000d+00 (--scincinc=200)
c [init-scores] maxium score limit 1.000000d+500 (--maxscorexp=500)
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c *    0.0  247193  1377238         0       0      0     0  12  0.0   0.0   57
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 22110 at-most-one constraints of average size 5.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 22110 out of 22110 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62800 variables
c [simpleprobe-1] all 197542 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 1589 variables
c [simpleprobe-1] 17818 variables remain 9% (178135 retained)
c [simpleprobe-1] removed 1589 variables, found 23045 hbrs, 362 units
c [unhide-1] limit 524244 based on 1048489 irredundant clauses
c [unhide-1-1] 0 units, 5256 failed, 11191 tauts, 0 hbrs, 10941 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194150 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] eliminated 75217 variables 39% in round 1 in 106761426 steps
c [elim-1-1] backward subsumption/strengthening limit 213522852
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 31345273 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 75217 = 39% variables out of 194150
c [phase-1] phase bias: 27093 positive 23%, 91840 negative 77%
c [simplification-1] removed 84831 variables 41.6% (118933 remain 48%)
c [simplification-1] removed 519427 irredundant clauses 37.7% (857811 remain 62%)
c [simplification-1] maximum reduction of 42% = max (42%, 38%)
c [simplification-1] large reduction 42% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] new conflict limit 1000
c [cut-width] 191163, max 399242, min4 70310 at 75%, min10 28538 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    7.6  118932   857811         3       0      1 15447  48  1.0   5.5   54
c i    7.6  118921   857811        12       2      2 15449  47  1.7   4.1   54
c i    7.6  118915   857811        13       2      2 15449  49  1.5   3.7   54
c i    7.6  118825   857811        22       9      3 15449  45  2.0   5.7   54
c i    7.6  118728   857811        41      17      5 15457  33  2.1  13.4   54
c i    7.7  118692   857811        51      22      7 15459  20  2.1  22.8   54
c i    7.7  118685   857811        57      25      7 15461  17  2.1  28.0   54
c R    7.7  118389   857811        62      27      7 15464  13  2.1  29.8   54
c i    7.7  118388   857811        96      39     12 15480   5  2.3  71.6   54
c i    7.8  118336   857811       114      47     13 15488   4  2.4  70.0   54
c R    7.8  118222   857811       162      73     14 15509   3  2.6  90.1   54
c i    7.9  118221   857811       191      88     19 15517   2  2.8  98.0   54
c i    7.9  118127   857811       198      88     20 15520   3  2.7  96.9   54
c i    8.0  117699   857811       245     113     24 15537   2  2.8 113.8   54
c i    8.0  117607   857811       258     122     25 15539   2  2.9 112.3   54
c i    8.1  117250   857811       288     130     30 15555   6  2.8 134.8   54
c i    8.3  117236   857811       366     170     40 15582   1  2.8 138.3   54
c i    8.3  117235   857811       372     170     41 15586   1  2.8 137.9   54
c R    8.3  117227   857811       407     189     45 15598   2  2.8 137.8   54
c i    8.4  117226   857811       414     193     45 15599   5  2.9 137.1   54
c i    8.4  116758   857811       436     205     46 15607   4  2.9 141.4   55
c i    8.5  116234   857811       439     206     46 15608   3  2.9 140.7   55
c i    8.5  116221   857811       472     225     52 15615   1  2.9 138.7   55
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    8.6  115929   857811       499     244     54 15619   1  3.0 135.9   55
c i    8.6  115322   857811       531     268     56 15624   1  3.2 141.0   55
c i    8.7  114818   857811       566     286     61 15634   1  3.3 139.7   55
c i    8.7  114771   857811       581     296     63 15635   2  3.3 140.2   55
c i    8.8  114236   857811       594     304     64 15638   2  3.3 141.4   55
c i    8.8  114166   857811       596     304     65 15638   1  3.3 141.5   55
c i    8.8  114161   857811       603     307     66 15640   2  3.3 141.8   55
c i    8.8  114067   857811       607     309     66 15641   2  3.3 141.6   55
c i    8.9  114057   857811       689     345     72 15678   1  3.5 139.3   55
c i    8.9  113856   857811       733     377     76 15684   1  3.6 138.7   55
c i    9.2  113576   857811       923     488     89 15745   2  3.8 150.6   55
c R    9.3  112775   857811       973     521     93 15756   2  3.8 150.4   55
c i    9.3  112774   857811       975     521     94 15756   2  3.8 150.1   55
c i    9.3  112766   857811       976     521     94 15756   2  3.8 149.9   55
c i    9.3  112754   857811       982     523     95 15758   2  3.8 149.9   55
c i    9.3  112404   857811       987     526     96 15758   2  3.8 149.5   55
c i    9.4  112399   857811      1012     541     98 15765   1  3.8 148.8   55
c i    9.4  112051   857811      1014     542     98 15765   1  3.8 148.7   55
c i    9.5  111504   857811      1096     588    110 15786   2  3.8 147.8   55
c i    9.5  111494   857811      1151     628    117 15791   1  3.9 146.9   55
c i    9.5  111434   857811      1157     632    117 15792   1  3.9 146.8   55
c i    9.5  111212   857811      1158     632    117 15792   1  3.9 146.6   55
c i    9.7  111207   857811      1257     699    125 15813   2  4.4 146.2   55
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    9.7  111175   857811      1272     711    126 15814   2  4.5 146.5   55
c i    9.7  111061   857811      1283     715    128 15818   2  4.4 146.6   55
c i    9.9  111045   857811      1448     804    144 15865   2  4.5 153.7   55
c i   10.0  111029   857811      1527     858    151 15879   2  4.6 154.8   55
c i   10.0  110935   857811      1536     864    152 15880   2  4.6 154.6   55
c i   10.0  110897   857811      1537     864    152 15880   2  4.6 154.5   55
c i   10.0  110750   857811      1565     885    154 15882   2  5.2 154.2   55
c i   10.2  110544   857811      1694     969    163 15914   2  5.1 154.6   55
c i   10.3  110531   857811      1867    1102    178 15929   3  5.3 154.3   55
c R   10.6  110531   857811      2288    1425    209 15984   3  5.9 172.0   56
c i   10.6  110530   857811      2292    1426    210 15985   3  5.9 171.8   56
c i   10.6  110519   857811      2304    1433    212 15987   2  5.9 171.5   56
c i   10.8  110431   857811      2434    1508    224 16019   2  6.0 171.2   56
c i   10.8  110271   857811      2436    1507    225 16019   2  6.0 171.2   56
c i   10.9  109588   857811      2491    1545    234 16026   1  6.0 169.9   56
c i   11.0  109576   857811      2579    1599    244 16047   3  5.9 169.2   56
c i   11.0  108899   857811      2581    1600    244 16047   2  5.9 169.0   56
c i   11.1  108887   857811      2706    1700    247 16059   1  6.1 170.8   56
c i   11.1  108886   857811      2714    1704    250 16059   1  6.1 170.5   56
c i   11.3  108834   857811      2784    1751    259 16071   1  6.1 169.8   56
c i   11.6  108746   857811      2944    1860    283 16094   1  6.0 170.7   56
c i   11.7  108642   857811      3023    1903    293 16115   2  6.0 169.9   56
c i   11.7  108121   857811      3035    1910    295 16117   2  6.0 170.5   56
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   11.8  108112   857811      3122    1968    303 16136   2  5.9 170.0   56
c i   11.9  108102   857811      3186    2011    306 16153   9  5.9 174.5   56
c 
c [simplification-2] limit of 3269 conflicts hit after 3269 conflicts
c [decomp-3] removed 11987 variables
c [simpleprobe-2] 16054 schedulable variables 15%
c [simpleprobe-2] limit 4993848 penalty 0 = 0 + 0
c [decomp-4] removed 372 variables
c [simpleprobe-2] 23654 variables remain 22% (82920 retained)
c [simpleprobe-2] removed 372 variables, found 10803 hbrs, 85 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 42135 literals 20%
c [treelook-1] scheduling used 360959 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 340434 steps
c [treelook-1] 42131 literals remain 20%
c [treelook-1] 42059 variables remain to probed next time 39%
c [treelook-1] removed 0 variables, found 2638 hbrs
c [basicprobe-1] limit 1571664 based on 785832 irredundant clauses
c [basicprobe-1-0] 38135 probes remain 36% after last round
c [basicprobe-1-0] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 790 variables, found 10888 hbrs
c [unhide-2] limit 392916 based on 785832 irredundant clauses
c [unhide-2-2] 4 units, 4339 failed, 5430 tauts, 0 hbrs, 3671 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 103921 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 12868 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 23 clauses out of 474 (5%) of length 10
c [cce-1-1] eliminated 295 clauses out of 2920 (10%) of length 9
c [cce-1-1] eliminated 24 clauses out of 340 (7%) of length 8
c [cce-1-1] eliminated 55 clauses out of 575 (10%) of length 7
c [cce-1-1] eliminated 4505 clauses out of 6703 (67%) of length 6
c [cce-1-1] eliminated 15628 clauses out of 59861 (26%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 20530 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 385103 clauses = 361032 binary + 24071 ternary
c [cce-1] tried to eliminate 4528 small clauses 1%
c [cce-1] eliminated 1818 small clauses 0%
c [cce-1] eliminated 1674 binary clauses 0%
c [cce-1] eliminated 144 ternary clauses 1%
c [cce-1-1] eliminated 1818 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 22348 covered clauses in round 1
c [cce-1] eliminated 22348 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 103921 variables 100%
c [elim-2] limit of 24969242 steps penalty 0 = 0 + 0
c [elim-2] incomplete 25152 not tried 24% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 13121 = 13% variables out of 103921
c [bca-1] limit of 10000000 steps
c [bca-1] 175361 out of 181602 literals actually usable 97%
c [bca-1] added 2136 blocked clauses in 527309 steps
c [phase-2] phase bias: 28 positive 2%, 1329 negative 98%
c [simplification-2] removed 17289 variables 16.0% (90800 remain 37%)
c [simplification-2] removed 167835 irredundant clauses 19.6% (689976 remain 50%)
c [simplification-2] maximum reduction of 20% = max (16%, 20%)
c [simplification-2] large reduction 20% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 5269
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   29.0   90799   689976      3304     958    347 40431   3  5.9 177.3   48
c i   29.2   90432   689976      3427    1040    359 40455   1  6.0 175.6   48
c i   29.5   90426   689976      3529    1081    372 40501   0  5.9 174.5   48
c i   29.5   90425   689976      3530    1081    372 40501   0  5.9 174.5   48
c i   29.5   90424   689976      3641    1152    387 40522   3  5.8 174.4   48
c i   29.7   90414   689976      3715    1197    397 40539   1  5.8 175.8   48
c i   29.7   90165   689976      3736    1209    403 40541   1  5.8 175.8   48
c i   29.8   89925   689976      3737    1209    403 40541   1  5.8 175.7   48
c i   30.1   89916   689976      3925    1321    423 40591   2  5.8 174.8   49
c i   30.2   89780   689976      3983    1356    430 40602   0  5.8 174.2   49
c i   30.3   89643   689976      4324    1617    458 40639   4  5.8 173.9   49
c i   30.4   89585   689976      4389    1648    468 40659   3  5.7 173.5   49
c i   30.4   89584   689976      4406    1658    469 40664   3  5.7 173.4   49
c i   30.5   89536   689976      4576    1788    482 40684   3  5.7 173.6   49
c i   30.5   89255   689976      4580    1791    482 40684   3  5.7 173.5   49
c i   30.5   89077   689976      4585    1794    482 40685   3  5.7 173.7   49
c i   30.5   89068   689976      4611    1809    487 40689   2  5.7 177.1   49
c i   30.6   89000   689976      4765    1906    503 40728   2  5.9 179.5   49
c i   30.7   88961   689976      4870    1978    516 40740   2  5.9 186.5   49
c i   30.8   88414   689976      5093    2162    530 40748   4  7.0 193.5   49
c i   30.8   88214   689976      5122    2180    536 40752   4  6.9 193.2   49
c R   30.8   88120   689976      5193    2230    546 40763   3  6.9 193.1   49
c i   30.9   88119   689976      5212    2236    546 40774   1  6.9 192.4   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   30.9   88085   689976      5243    2256    547 40783   1  6.9 191.4   49
c i   30.9   88080   689976      5248    2258    548 40783   1  6.9 191.4   49
c i   30.9   88073   689976      5249    2258    548 40783   1  6.9 191.3   49
c i   30.9   88066   689976      5278    2279    551 40786   1  6.8 190.9   49
c i   31.0   88056   689976      5331    2320    553 40794   2  6.8 190.3   49
c i   31.0   88008   689976      5371    2348    560 40798   3  6.8 190.0   49
c i   31.0   88002   689976      5373    2349    560 40798   3  6.8 190.0   49
c i   31.0   88001   689976      5407    2380    560 40799   2  6.8 189.6   49
c i   31.1   87993   689976      5537    2464    573 40827   3  6.8 188.4   49
c i   31.3   87960   689976      5672    2564    587 40846   1  6.7 188.6   49
c i   31.3   87905   689976      5701    2581    589 40855   1  6.7 188.1   49
c i   31.3   87852   689976      5746    2611    591 40867   2  6.7 187.6   49
c i   31.4   87818   689976      5801    2648    599 40872   2  6.7 186.8   49
c i   31.4   87772   689976      5844    2678    606 40877   2  6.7 186.2   49
c i   31.5   87765   689976      5991    2789    615 40897   3  6.8 185.9   49
c i   31.6   87755   689976      6008    2792    615 40910   0  6.8 186.6   49
c i   31.7   87751   689976      6009    2792    615 40910   0  6.8 186.6   49
c i   31.7   87742   689976      6017    2799    615 40910   0  6.8 186.6   49
c i   31.7   87734   689976      6018    2799    615 40910   0  6.8 186.7   49
c i   31.7   87696   689976      6019    2799    615 40910   0  6.8 186.8   49
c i   31.8   87688   689976      6177    2933    624 40922   3  6.9 189.5   49
c i   32.1   87684   689976      6432    3124    640 40964   1  7.0 191.4   49
c i   32.4   87679   689976      6686    3324    659 40993   2  7.0 191.2   50
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   32.6   87672   689976      6890    3465    680 41031   1  7.1 189.0   50
c i   32.6   87662   689976      6939    3509    680 41034   2  7.1 189.1   50
c i   32.7   87634   689976      6978    3533    686 41040   2  7.1 190.4   50
c i   32.8   87626   689976      7195    3709    701 41048   3  7.6 192.0   50
c 
c [simplification-3] limit of 7537 conflicts hit after 7537 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 87497 free variables schedulable
c [ternres-1] 82 ternary resolvents (0 bin, 82 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 18194 at-most-one constraints of average size 4.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 18194 out of 18194 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 486 xors of average arity 2.1
c [gauss-1] connected 1020 occurrences of 500 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-6] removed 323 variables
c [cgrclsr-1] limit 334269 based on 668539 irredundant clauses
c [cgrclsr-1] all 87174 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 5 variables
c [lift-1] limit 1472238 with penalty 0 = 0 + 0
c [lift-1] using 70223 probes 81%
c [lift-1] 2 units, 1 impls, 0 eqs in 1 rounds
c [lift-1] 87164 variables remain 100% (3 retained)
c [lift-1] removed 2 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 60, lifted 102
c [unhide-3] limit 490746 with penalty 0 = 0 + 0
c [unhide-3-3] 3 units, 1495 failed, 19786 tauts, 0 hbrs, 7299 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 231 transitive binary clauses
c [transred-1] found 2 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 85619 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 223 blocked clauses
c [block-2] 223 < 1/1000 * 645534 = 645 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 448 (0%) of length 7
c [cce-2-1] eliminated 1 clauses out of 3378 (0%) of length 6
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 3 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 534247 clauses = 296680 binary + 237567 ternary
c [cce-2] tried to eliminate 249 small clauses 0%
c [cce-2] eliminated 76 small clauses 0%
c [cce-2] eliminated 53 binary clauses 0%
c [cce-2] eliminated 23 ternary clauses 0%
c [cce-2-1] eliminated 76 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 79 covered clauses in round 1
c [cce-2] eliminated 79 covered clauses in TOTAL during 1 rounds
c [cce-2] 79 < 1/1000 * 634830 = 634 considered unsuccessful
c [elim-3] 24293 variables 28% will be scheduled this time
c [elim-3] scheduled 24293 variables 28%
c [elim-3] limit of 49074633 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 857 variables 1% in round 1 in 47052095 steps
c [elim-3-1] backward subsumption/strengthening limit 2022538
c [elim-3-1] subsumed 1 and strengthened 0 clauses in 2022543 steps
c [elim-3] incomplete 3 not tried 0% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 857 = 1% variables out of 85610
c [bca-2] limit of 10000000 steps
c [bca-2] 155165 out of 169508 literals actually usable 92%
c [bca-2] added 100 blocked clauses in 441560 steps
c [phase-3] phase bias: 153 positive 63%, 89 negative 37%
c [simplification-3] removed 2744 variables 3.1% (84753 remain 34%)
c [simplification-3] removed 60434 irredundant clauses 8.8% (629542 remain 46%)
c [simplification-3] maximum reduction of 9% = max (3%, 9%)
c [simplification-3] large reduction 9% >= 5% limit
c [simplification-3] new conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] new conflict limit 9537
c [tabula-rasa-1] number clauses 629542 drops below limit 688619
c [flush-cache] 0 binary, 0 ternary, 3472 large
c [flushphases] 84753 phases reset fully
c [phase-4] phase bias: 3466 positive 31%, 7591 negative 69%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] conflict limit 20000 does not change
c [tabula-rasa-1] new variable limit 21188 and clause limit 314771
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   39.1   84752   629542      7563      22    805 135983  17  7.6 191.9   47
c i   39.2   84749   629542      7632      73    815 135990   9  7.6 191.3   47
c i   39.2   84748   629542      7651      89    817 135990   6  7.6 191.1   47
c i   39.3   84741   629542      7744     160    825 136001   3  7.6 190.5   48
c i   39.3   84714   629542      7747     160    825 136003   3  7.6 190.5   48
c i   39.3   84686   629542      7753     163    826 136004   3  7.6 190.4   48
c i   39.3   84658   629542      7837     224    835 136017   5  7.5 190.0   48
c i   39.5   84623   629542      8062     401    856 136038   3  7.5 190.7   48
c i   39.5   84463   629542      8063     401    856 136038   2  7.5 190.7   48
c i   39.6   84449   629542      8177     493    864 136049   2  7.5 190.3   48
c i   39.6   84443   629542      8178     493    864 136049   1  7.5 190.3   48
c i   39.7   84435   629542      8312     590    880 136066   3  7.5 190.8   48
c i   39.8   84434   629542      8518     740    896 136101   2  7.5 189.9   48
c i   39.8   84429   629542      8534     751    899 136101   2  7.5 189.7   48
c i   39.9   84276   629542      8600     796    907 136112   2  7.5 189.1   48
c i   39.9   84273   629542      8606     801    907 136112   2  7.5 189.1   48
c i   39.9   84272   629542      8619     812    907 136113   3  7.5 189.0   48
c i   40.1   84266   629542      8945    1057    936 136160   2  7.5 187.5   48
c i   40.3   84216   629542      9082    1161    942 136184   2  7.6 186.7   48
c i   40.3   84214   629542      9108    1175    944 136192   2  7.6 186.6   48
c i   40.5   84204   629542      9404    1380    967 136244   2  7.6 186.0   48
c i   40.5   84199   629542      9413    1388    967 136244   2  7.6 185.9   48
c i   40.6   84194   629542      9606    1520    988 136282   5  7.5 188.3   48
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   40.7   84065   629542      9819    1701   1003 136297   4  7.5 193.6   49
c i   40.8   84031   629542      9898    1752   1008 136317   2  7.5 195.3   49
c i   40.8   84022   629542      9899    1752   1008 136317   2  7.5 195.2   49
c i   40.8   84014   629542      9900    1752   1008 136317   2  7.5 195.2   49
c i   40.9   84005   629542      9964    1794   1015 136331   2  7.5 196.9   49
c i   40.9   83976   629542      9966    1794   1015 136332   2  7.5 196.9   49
c i   41.0   83968   629542     10056    1854   1024 136348   2  7.6 196.9   49
c i   41.2   83965   629542     10422    2137   1055 136389   3  7.7 198.9   49
c i   41.2   83964   629542     10435    2146   1055 136392   2  7.7 199.0   49
c i   41.2   83962   629542     10445    2150   1057 136395   1  7.7 199.2   49
c i   41.2   83955   629542     10448    2151   1057 136396   2  7.7 199.1   49
c i   41.3   83951   629542     10647    2294   1065 136435   3  7.7 199.3   49
c i   41.3   83947   629542     10667    2299   1065 136449   2  7.7 198.6   49
c i   41.3   83944   629542     10668    2299   1065 136449   2  7.7 198.6   49
c i   41.3   83941   629542     10677    2305   1066 136450   2  7.7 198.5   49
c i   41.3   83716   629542     10709    2327   1070 136452   2  7.7 198.4   49
c i   41.3   83708   629542     10715    2330   1070 136454   2  7.7 198.3   49
c i   41.3   83706   629542     10718    2331   1071 136454   2  7.7 198.2   49
c i   41.4   83585   629542     10731    2341   1072 136455   2  7.7 198.2   49
c i   41.4   83581   629542     10733    2342   1072 136455   2  7.7 198.1   49
c i   41.5   83573   629542     10952    2500   1082 136505   4  7.7 204.6   49
c i   41.6   83566   629542     10966    2509   1086 136505   4  7.7 204.5   49
c i   41.6   83369   629542     10968    2510   1086 136505   4  7.7 204.4   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   41.6   83201   629542     11005    2531   1092 136508   3  7.7 204.4   49
c i   41.6   83194   629542     11165    2645   1098 136541   2  7.9 204.1   49
c i   41.6   83049   629542     11177    2655   1099 136541   3  7.9 204.0   49
c i   41.9   82935   629542     11649    2981   1125 136608   2  8.3 204.8   49
c R   41.9   82585   629542     11694    3014   1126 136616   2  8.3 204.5   49
c i   42.0   82584   629542     11747    3049   1129 136630   3  8.3 204.1   49
c i   42.0   82580   629542     11796    3092   1133 136631   3  8.4 203.7   49
c i   42.0   82570   629542     11811    3099   1135 136635   3  8.3 203.7   49
c i   42.1   82566   629542     11878    3157   1140 136637   2  8.3 203.1   49
c 
c [simplification-4] limit of 11923 conflicts hit after 11923 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 82563 free variables schedulable
c [ternres-2] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-2] 62160 variables remain 75% (20403 retained)
c [decomp-7] removed 2299 variables
c [treelook-2] limit 153405 based on 613622 irredundant clauses
c [treelook-2] scheduled 32276 literals 20%
c [treelook-2] scheduling used 166096 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 153405 based on 613622 irredundant clauses
c [treelook-2] used 505621 steps
c [treelook-2] 32273 literals remain 20%
c [treelook-2] 17169 variables remain to probed next time 21%
c [treelook-2] removed 1 variables, found 4160 hbrs
c [cgrclsr-2] limit 339454 penalty 0 = 0 + 0
c [cgrclsr-2] all 82453 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 7 variables
c [lift-2] limit 2036728 with penalty 0 = 0 + 0
c [lift-2] using 67537 probes 82%
c [lift-2] 15 units, 4 impls, 1 eqs in 1 rounds
c [lift-2] 82413 variables remain 100% (16 retained)
c [lift-2] removed 17 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 6, lifted 19
c [unhide-4] limit 678909 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 786 failed, 29075 tauts, 0 hbrs, 5809 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 210 transitive binary clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 81523 variables 100%
c [elim-4] limit of 67890946 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 2382 variables 3% in round 1 in 65623690 steps
c [elim-4-1] backward subsumption/strengthening limit 2267256
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 2267286 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2382 = 3% variables out of 81523
c [bca-3] limit of 10000000 steps
c [bca-3] 139864 out of 158284 literals actually usable 88%
c [bca-3] added 135 blocked clauses in 369175 steps
c [rephase-1] after 11923 conflicts (new increment 20000, next 31923)
c [flushphases] 40 phases reset
c [phase-5] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-4] removed 3422 variables 4.1% (79141 remain 32%)
c [simplification-4] removed 33131 irredundant clauses 5.3% (596411 remain 43%)
c [simplification-4] maximum reduction of 5% = max (4%, 5%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] new conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] new conflict limit 13923
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   47.0   79140   596411     12012    3019    972 162233   2  8.4 205.0   48
c i   47.0   78527   596411     12016    3020    973 162234   3  8.4 204.9   48
c i   47.1   78241   596411     12169    3143    982 162250   3  8.4 204.2   48
c i   47.1   78234   596411     12179    3147    983 162252   3  8.4 204.1   48
c i   47.1   78230   596411     12253    3214    987 162254   2  8.4 203.9   48
c i   47.1   78225   596411     12254    3214    987 162254   2  8.4 203.9   48
c i   47.1   78224   596411     12255    3214    987 162254   2  8.4 203.9   48
c i   47.1   78220   596411     12256    3214    987 162254   2  8.4 203.9   48
c i   47.1   78215   596411     12257    3214    987 162254   2  8.4 203.9   48
c i   47.1   78210   596411     12258    3214    987 162254   2  8.4 203.9   48
c i   47.1   78205   596411     12259    3214    987 162254   2  8.4 203.9   48
c i   47.1   78201   596411     12260    3214    987 162254   2  8.4 203.9   48
c i   47.1   78196   596411     12261    3214    987 162254   2  8.4 203.9   48
c i   47.1   78191   596411     12262    3214    987 162254   2  8.4 203.9   48
c i   47.1   78186   596411     12263    3214    987 162254   2  8.4 203.9   48
c i   47.1   78182   596411     12264    3214    987 162254   1  8.4 203.9   48
c i   47.1   78176   596411     12265    3214    987 162254   1  8.4 203.9   48
c i   47.2   78173   596411     12330    3254    992 162271   2  8.4 203.9   48
c i   47.2   78166   596411     12331    3254    992 162271   2  8.4 203.9   48
c i   47.2   78162   596411     12357    3274    994 162274   3  8.4 203.8   48
c i   47.2   78090   596411     12392    3299    999 162277   2  8.4 203.5   48
c i   47.3   77848   596411     12430    3325   1001 162284   2  8.4 203.5   48
c i   47.3   77845   596411     12480    3365   1002 162288   1  8.5 203.3   48
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   47.5   77842   596411     12711    3534   1006 162303   2  8.6 203.0   48
c i   47.6   77834   596411     12816    3611   1012 162320   3  8.6 202.7   48
c i   47.7   77827   596411     12880    3666   1017 162323   3  8.6 202.6   48
c i   47.7   77692   596411     12881    3666   1017 162323   2  8.6 202.6   48
c i   47.7   77688   596411     12898    3680   1017 162325   2  8.6 202.5   48
c i   47.7   77679   596411     12932    3698   1021 162335   2  8.6 202.3   48
c i   47.7   77669   596411     12933    3698   1021 162335   2  8.6 202.3   48
c i   47.8   77666   596411     13023    3769   1027 162342   4  8.7 201.9   48
c i   47.9   77656   596411     13118    3838   1037 162354   4  8.7 201.5   48
c i   47.9   77652   596411     13122    3841   1037 162354   3  8.7 201.5   48
c i   48.0   77648   596411     13391    4022   1071 162399   3  8.6 199.8   48
c i   48.2   77643   596411     14133    4571   1106 162445   3  9.2 198.0   48
c i   48.3   77637   596411     14143    4579   1106 162446   3  9.2 197.9   48
c i   48.4   77636   596411     14243    4659   1111 162460   2  9.2 197.5   48
c i   48.4   77630   596411     14248    4661   1112 162460   2  9.2 197.5   48
c i   48.4   77629   596411     14342    4728   1119 162473   3  9.2 197.1   48
c i   48.4   77625   596411     14343    4728   1119 162473   3  9.2 197.1   48
c i   48.4   77622   596411     14373    4752   1123 162474   3  9.2 197.0   48
c i   48.5   77600   596411     14465    4825   1135 162480   3  9.1 196.9   48
c i   48.6   77595   596411     14490    4842   1137 162484   3  9.1 197.0   49
c i   48.6   77590   596411     14492    4843   1137 162484   3  9.1 196.9   49
c i   48.6   77587   596411     14504    4854   1137 162484   2  9.1 196.9   49
c i   48.6   77582   596411     14609    4954   1138 162484   3  9.2 196.5   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   48.8   77548   596411     14927    5229   1153 162497   4  9.3 195.9   49
c i   48.8   77547   596411     14936    5235   1154 162498   3  9.3 195.8   49
c i   48.8   77540   596411     14937    5235   1154 162498   3  9.3 195.8   49
c i   48.9   77536   596411     15042    5316   1166 162505   3  9.3 195.6   49
c i   48.9   77533   596411     15054    5323   1167 162508   2  9.3 195.4   49
c -   49.0   77533   596411     15151    3396   1174 162513   2  9.3 195.2   47
c i   49.0   77532   596411     15181    3421   1175 162516   2  9.3 195.0   47
c i   49.1   77523   596411     15182    3421   1175 162516   2  9.3 195.0   47
c i   49.1   77513   596411     15183    3421   1175 162516   1  9.3 194.9   47
c i   49.1   77507   596411     15184    3421   1175 162516   1  9.3 194.9   47
c i   49.1   77501   596411     15185    3421   1175 162516   1  9.3 194.8   47
c i   49.1   77494   596411     15186    3421   1175 162516   1  9.3 194.8   47
c i   49.1   77463   596411     15193    3421   1175 162522   1  9.3 194.8   47
c i   49.1   77459   596411     15194    3421   1175 162522   1  9.3 194.7   47
c i   49.1   77452   596411     15196    3422   1175 162522   1  9.3 194.7   47
c i   49.1   77444   596411     15286    3485   1182 162538   2  9.3 194.7   47
c i   49.1   77439   596411     15290    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77429   596411     15291    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77428   596411     15292    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77427   596411     15293    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77425   596411     15294    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77423   596411     15295    3487   1182 162539   2  9.3 194.7   47
c i   49.1   77422   596411     15296    3487   1182 162539   2  9.3 194.7   47
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   49.1   77420   596411     15299    3489   1182 162539   2  9.3 194.7   47
c i   49.2   77419   596411     15329    3509   1186 162542   2  9.3 194.5   47
c i   49.2   77418   596411     15332    3511   1186 162542   2  9.3 194.5   47
c i   49.2   77405   596411     15425    3587   1193 162551   2  9.3 194.2   47
c i   49.2   77400   596411     15455    3611   1194 162554   2  9.3 194.1   47
c i   49.2   77393   596411     15463    3615   1194 162557   2  9.3 194.0   47
c i   49.3   77388   596411     15485    3627   1195 162564   2  9.3 193.9   47
c i   49.3   77384   596411     15573    3688   1201 162582   2  9.3 193.5   48
c i   49.3   77382   596411     15580    3692   1201 162584   2  9.3 193.4   48
c i   49.4   77335   596411     15596    3702   1204 162586   2  9.3 193.3   48
c i   49.6   77284   596411     15892    3919   1230 162620   3  9.3 194.4   48
c i   49.6   77283   596411     15914    3936   1234 162620   4  9.3 194.4   48
c i   49.6   77282   596411     15915    3936   1234 162620   3  9.3 194.4   48
c i   49.7   77281   596411     15928    3938   1238 162626   2  9.3 194.4   48
c i   49.7   77246   596411     15996    3994   1244 162627   3  9.3 194.9   48
c i   49.7   77169   596411     16022    4007   1248 162629   3  9.3 194.9   48
c i   49.7   77168   596411     16024    4008   1248 162629   3  9.3 194.9   48
c i   49.8   77164   596411     16266    4187   1262 162643   3  9.6 194.7   48
c i   49.8   77162   596411     16285    4201   1265 162644   3  9.6 194.6   48
c i   49.8   77160   596411     16338    4238   1268 162655   5  9.6 194.6   48
c i   49.9   77157   596411     16380    4268   1269 162659   4  9.6 194.6   48
c i   49.9   77149   596411     16388    4271   1269 162663   2  9.6 194.6   48
c i   49.9   77123   596411     16390    4272   1269 162663   1  9.6 194.6   48
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   49.9   77122   596411     16394    4272   1269 162666   1  9.6 194.6   48
c 
c [simplification-5] limit of 16637 conflicts hit after 16637 conflicts
c [ternres-3] limit 4341413 with penalty 0 = 0 + 0
c [ternres-3] 58064 schedulable variables 73%
c [ternres-3] 25 ternary resolvents (0 bin, 25 trn)
c [ternres-3] 36964 variables remain 48% (40115 retained)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 46 xors of average arity 2.3
c [gauss-2] connected 104 occurrences of 92 variables (average 1.1)
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-9] removed 134 variables
c [basicprobe-2] limit 4341413 penalty 0 = 0 + 0
c [basicprobe-2-0] 22066 probes remain 29% after last round
c [basicprobe-2-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 101 variables, found 43479 hbrs
c [bate-1] eliminated 22 asymmetric tautologies during probing
c [cgrclsr-3] limit 434141 penalty 0 = 0 + 0
c [cgrclsr-3] all 76844 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 8 variables
c [lift-3] limit 2604847 with penalty 0 = 0 + 0
c [lift-3] using 63757 probes 83%
c [lift-3] 382 units, 7 impls, 0 eqs in 1 rounds
c [lift-3] 76249 variables remain 100% (26 retained)
c [lift-3] removed 561 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 1, lifted 43
c [unhide-5] limit 868282 with penalty 0 = 0 + 0
c [unhide-5-5] 68 units, 832 failed, 14612 tauts, 0 hbrs, 3790 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 219 transitive binary clauses
c [transred-3] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 75174 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 203 blocked clauses
c [block-3] 203 < 1/1000 * 559275 = 559 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 100
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 96
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 94
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 92
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 90
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 87
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 86
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 85
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 84
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 83
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 82
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 81
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 80
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 79
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 78
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 77
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 76
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 75
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 74
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 73
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 72
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 71
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 70
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 69
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 68
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 67
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 66
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 65
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 64
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 63
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 62
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 61
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 60
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 59
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 58
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 57
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 56
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 55
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 54
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 53
c [cce-3-1] eliminated 7 clauses out of 9 (78%) of length 52
c [cce-3-1] eliminated 7 clauses out of 10 (70%) of length 51
c [cce-3-1] eliminated 8 clauses out of 11 (73%) of length 50
c [cce-3-1] eliminated 9 clauses out of 12 (75%) of length 49
c [cce-3-1] eliminated 9 clauses out of 12 (75%) of length 48
c [cce-3-1] eliminated 9 clauses out of 12 (75%) of length 47
c [cce-3-1] eliminated 9 clauses out of 12 (75%) of length 46
c [cce-3-1] eliminated 8 clauses out of 11 (73%) of length 45
c [cce-3-1] eliminated 11 clauses out of 13 (85%) of length 44
c [cce-3-1] eliminated 8 clauses out of 12 (67%) of length 43
c [cce-3-1] eliminated 10 clauses out of 12 (83%) of length 42
c [cce-3-1] eliminated 8 clauses out of 12 (67%) of length 41
c [cce-3-1] eliminated 10 clauses out of 12 (83%) of length 40
c [cce-3-1] eliminated 8 clauses out of 12 (67%) of length 39
c [cce-3-1] eliminated 10 clauses out of 13 (77%) of length 38
c [cce-3-1] eliminated 10 clauses out of 14 (71%) of length 37
c [cce-3-1] eliminated 11 clauses out of 15 (73%) of length 36
c [cce-3-1] eliminated 12 clauses out of 16 (75%) of length 35
c [cce-3-1] eliminated 12 clauses out of 16 (75%) of length 34
c [cce-3-1] eliminated 11 clauses out of 16 (69%) of length 33
c [cce-3-1] eliminated 13 clauses out of 16 (81%) of length 32
c [cce-3-1] eliminated 11 clauses out of 16 (69%) of length 31
c [cce-3-1] eliminated 13 clauses out of 17 (76%) of length 30
c [cce-3-1] eliminated 12 clauses out of 17 (71%) of length 29
c [cce-3-1] eliminated 15 clauses out of 18 (83%) of length 28
c [cce-3-1] eliminated 12 clauses out of 18 (67%) of length 27
c [cce-3-1] eliminated 14 clauses out of 18 (78%) of length 26
c [cce-3-1] eliminated 13 clauses out of 18 (72%) of length 25
c [cce-3-1] eliminated 13 clauses out of 18 (72%) of length 24
c [cce-3-1] eliminated 14 clauses out of 17 (82%) of length 23
c [cce-3-1] eliminated 13 clauses out of 17 (76%) of length 22
c [cce-3-1] eliminated 13 clauses out of 18 (72%) of length 21
c [cce-3-1] eliminated 14 clauses out of 18 (78%) of length 20
c [cce-3-1] eliminated 13 clauses out of 18 (72%) of length 19
c [cce-3-1] eliminated 14 clauses out of 20 (70%) of length 18
c [cce-3-1] eliminated 15 clauses out of 20 (75%) of length 17
c [cce-3-1] eliminated 15 clauses out of 20 (75%) of length 16
c [cce-3-1] eliminated 14 clauses out of 20 (70%) of length 15
c [cce-3-1] eliminated 16 clauses out of 20 (80%) of length 14
c [cce-3-1] eliminated 14 clauses out of 20 (70%) of length 13
c [cce-3-1] eliminated 16 clauses out of 20 (80%) of length 12
c [cce-3-1] eliminated 13 clauses out of 19 (68%) of length 11
c [cce-3-1] eliminated 16 clauses out of 142 (11%) of length 10
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 626 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 280768 clauses = 259235 binary + 21533 ternary
c [cce-3] tried to eliminate 324 small clauses 0%
c [cce-3] eliminated 120 small clauses 0%
c [cce-3] eliminated 112 binary clauses 0%
c [cce-3] eliminated 8 ternary clauses 0%
c [cce-3-1] eliminated 120 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 746 covered clauses in round 1
c [cce-3] eliminated 746 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 75140 variables 100%
c [elim-5] limit of 86828264 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 1505 variables 2% in round 1 in 53279616 steps
c [elim-5-1] backward subsumption/strengthening limit 33548648
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 18786537 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1528 = 2% variables out of 75140
c [bca-4] limit of 10000000 steps
c [bca-4] 127137 out of 147226 literals actually usable 86%
c [bca-4] added 49 blocked clauses in 325377 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 3467 variables 4.5% (73612 remain 30%)
c [simplification-5] removed 52973 irredundant clauses 8.9% (543438 remain 39%)
c [simplification-5] maximum reduction of 9% = max (4%, 9%)
c [simplification-5] large reduction 9% >= 5% limit
c [simplification-5] new conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] new conflict limit 18637
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   56.4   73611   543438     16773    4177   1219 216850   4  9.6 197.1   46
c i   56.5   73547   543438     17016    4377   1239 216865   2  9.6 197.4   46
c i   56.6   73546   543438     17027    4385   1241 216865   2  9.6 197.4   46
c i   56.6   73545   543438     17061    4403   1241 216880   1  9.6 197.1   46
c i   56.6   73528   543438     17101    4434   1244 216882   3  9.5 197.0   46
c i   56.8   73526   543438     17237    4541   1254 216897   2  9.6 197.7   47
c i   57.0   73519   543438     17729    4974   1280 216919   3  9.6 196.8   47
c i   57.3   73347   543438     18112    5292   1302 216947   3  9.6 197.5   47
c i   57.3   73344   543438     18113    5292   1302 216947   3  9.6 197.5   47
c i   57.3   73341   543438     18114    5292   1302 216947   3  9.6 197.5   47
c i   57.3   73338   543438     18115    5292   1302 216947   3  9.6 197.5   47
c i   57.3   73335   543438     18116    5292   1302 216947   3  9.6 197.5   47
c i   57.7   73334   543438     18509    5620   1317 216988   3  9.7 198.8   47
c i   57.7   73333   543438     18553    5651   1320 216997   3  9.6 198.7   47
c i   57.7   73332   543438     18563    5660   1320 216997   3  9.6 198.7   47
c i   57.8   73331   543438     18641    5723   1323 217006   3  9.6 198.4   47
c i   57.8   73329   543438     18662    5740   1326 217006   3  9.6 198.4   47
c i   57.9   73321   543438     18676    5743   1327 217015   1  9.6 199.4   47
c i   58.1   73316   543438     19228    6250   1339 217019   4 10.5 202.0   47
c i   58.1   73314   543438     19250    6271   1339 217019   4 10.5 202.0   47
c i   58.2   73309   543438     19396    6377   1356 217038   2 10.5 201.5   47
c 
c [simplification-6] limit of 19431 conflicts hit after 19431 conflicts
c [ternres-4] limit 4916366 with penalty 0 = 0 + 0
c [ternres-4] 35137 schedulable variables 48%
c [ternres-4] 47 ternary resolvents (0 bin, 47 trn)
c [ternres-4] 10958 variables remain 15% (62324 retained)
c [card-3] limit 614545 penalty 2 = 2 + 0
c [card-3] found 12165 at-most-one constraints of average size 3.9
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 614545 for elimination
c [card-3] 12165 out of 12165 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 355 variables
c [simpleprobe-3] 19307 schedulable variables 26%
c [simpleprobe-3] limit 19665466 penalty 0 = 0 + 0
c [decomp-11] removed 791 variables
c [simpleprobe-3] 24499 variables remain 34% (47967 retained)
c [simpleprobe-3] removed 791 variables, found 65545 hbrs, 323 units
c [cgrclsr-4] limit 491636 penalty 0 = 0 + 0
c [cgrclsr-4] all 72466 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-4] limit 2949819 with penalty 0 = 0 + 0
c [lift-4] using 60920 probes 84%
c [lift-4] 27 units, 8 impls, 0 eqs in 1 rounds
c [lift-4] 72379 variables remain 100% (55 retained)
c [lift-4] removed 32 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 2, lifted 17
c [unhide-6] limit 983273 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 1241 failed, 36943 tauts, 0 hbrs, 13341 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 230 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 60
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 59
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 53
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 35
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 34
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 33
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 32
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 31
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 30
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 29
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 28
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 27
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 26
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 25
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 21
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 20
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 19
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 18
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 17
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 16
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 15
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 14
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 13
c [cce-4-1] eliminated 2 clauses out of 7 (29%) of length 12
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 11
c [cce-4-1] eliminated 6 clauses out of 125 (5%) of length 10
c [cce-4-1] eliminated 13 clauses out of 555 (2%) of length 9
c [cce-4-1] eliminated 19 clauses out of 388 (5%) of length 8
c [cce-4-1] eliminated 17 clauses out of 541 (3%) of length 7
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 104 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 273090 clauses = 252130 binary + 20960 ternary
c [cce-4] tried to eliminate 671 small clauses 0%
c [cce-4] eliminated 258 small clauses 0%
c [cce-4] eliminated 231 binary clauses 0%
c [cce-4] eliminated 27 ternary clauses 0%
c [cce-4-1] eliminated 7699 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 7803 covered clauses in round 1
c [cce-4] eliminated 7803 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 71669 variables 100%
c [elim-6] limit of 98327332 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 1231 variables 2% in round 1 in 50717578 steps
c [elim-6-1] backward subsumption/strengthening limit 47609754
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 17886458 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 1283 = 2% variables out of 71669
c [bca-5] limit of 10000000 steps
c [bca-5] 118562 out of 140774 literals actually usable 84%
c [bca-5] added 88 blocked clauses in 300424 steps
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 2896 variables 4.0% (70386 remain 28%)
c [simplification-6] removed 22798 irredundant clauses 4.2% (520640 remain 38%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 24000
c [simplification-6] penalized conflict interval 24000 = 1 * 24000
c [simplification-6] new conflict limit 43431
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   64.7   70385   520640     19451    5769   1341 250294   3 10.5 201.9   46
c i   64.8   70381   520640     19594    5865   1357 250321   3 10.5 201.7   46
c i   65.5   70293   520640     20099    6267   1386 250378   3 10.5 206.6   47
c i   65.7   70266   520640     20397    6484   1412 250430   2 10.5 206.7   47
c i   65.9   70157   520640     20618    6641   1428 250470   3 10.5 207.4   47
c i   66.1   70156   520640     20736    6691   1440 250523   0 10.5 206.6   47
c i   66.1   70152   520640     20737    6691   1440 250523   0 10.5 206.6   47
c i   66.1   70148   520640     20799    6728   1460 250527   3 10.5 206.3   47
c -   66.6   70146   520640     21461    4826   1495 250575   5 10.6 208.9   46
c i   66.6   70145   520640     21486    4849   1496 250575   3 10.6 209.6   46
c i   66.7   70142   520640     21624    4961   1505 250582   5 10.7 209.6   46
c i   66.7   70141   520640     21708    5029   1511 250589   4 10.7 210.1   46
c i   66.7   70026   520640     21791    5097   1515 250596   4 10.7 210.6   46
c i   66.8   70022   520640     21830    5131   1517 250598   3 10.7 211.0   46
c i   66.8   70021   520640     21860    5155   1521 250599   2 10.7 210.9   46
c i   66.8   70016   520640     21861    5155   1521 250599   2 10.7 210.9   46
c i   66.8   70010   520640     21862    5155   1521 250599   2 10.7 210.8   46
c i   66.8   70005   520640     21874    5161   1523 250601   3 10.7 210.8   46
c i   66.9   69988   520640     22073    5308   1541 250623   1 10.7 210.6   46
c i   67.0   69987   520640     22405    5569   1543 250628   3 11.5 211.3   46
c i   67.0   69986   520640     22605    5742   1550 250633   5 11.6 211.3   46
c i   67.0   69942   520640     22616    5749   1553 250633   5 11.6 211.2   46
c R   67.7   69940   520640     26010    8515   1604 250678   4 17.9 214.3   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   67.7   69939   520640     26018    8522   1604 250678   3 17.9 214.2   49
c i   67.7   69938   520640     26043    8544   1604 250678   2 17.9 214.3   49
c i   67.7   69926   520640     26047    8547   1604 250678   3 17.9 214.3   49
c i   67.8   69922   520640     26117    8598   1610 250689   3 17.9 214.1   49
c i   67.8   69912   520640     26118    8598   1610 250689   2 17.9 214.0   49
c i   67.9   69906   520640     26188    8659   1612 250692   3 17.9 214.6   49
c -   67.9   69787   520640     26208    5675   1613 250694   3 17.9 214.4   45
c i   68.0   69786   520640     26283    5742   1614 250698   3 17.9 214.5   46
c i   68.2   69591   520640     26489    5915   1623 250711   3 17.9 214.5   46
c i   68.7   69589   520640     27216    6530   1658 250764   3 17.8 216.4   46
c i   69.1   69271   520640     27660    6881   1703 250795   3 17.7 216.2   46
c i   69.3   69230   520640     27966    7126   1718 250809   4 17.8 215.8   46
c i   69.4   69229   520640     28219    7339   1738 250816   4 17.9 217.5   46
c i   69.5   69228   520640     28364    7445   1748 250829   2 17.9 217.2   46
c i   69.6   69217   520640     28429    7493   1755 250838   2 17.9 217.2   46
c i   69.7   69216   520640     28531    7569   1764 250846   3 18.0 217.3   47
c i   69.9   69206   520640     28796    7754   1774 250861   3 18.1 216.7   47
c i   70.0   69079   520640     28845    7793   1779 250865   2 18.1 216.6   47
c i   70.1   69070   520640     28939    7876   1780 250872   3 18.0 216.8   47
c i   70.1   69062   520640     28943    7878   1781 250872   2 18.0 216.8   47
c i   70.1   68767   520640     28965    7897   1781 250873   3 18.0 216.7   47
c i   70.2   68765   520640     29104    8010   1793 250876   3 18.1 216.8   47
c i   70.5   68764   520640     29477    8282   1830 250921   3 18.0 216.9   47
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   70.5   68759   520640     29497    8299   1829 250923   3 18.0 217.0   47
c i   70.5   68755   520640     29498    8299   1829 250923   2 18.0 217.0   47
c i   70.5   68749   520640     29499    8299   1829 250923   2 18.0 216.9   47
c i   70.5   68742   520640     29516    8315   1829 250923   2 18.0 216.8   47
c i   70.5   68738   520640     29517    8315   1829 250923   2 18.0 216.8   47
c i   70.6   68732   520640     29522    8319   1829 250923   2 18.0 216.7   47
c i   70.6   68730   520640     29539    8331   1830 250926   2 18.0 216.7   47
c i   71.0   68729   520640     30088    8770   1864 250974   3 18.0 215.6   47
c i   71.0   68726   520640     30093    8774   1864 250974   3 18.0 215.5   47
c i   71.0   68723   520640     30188    8840   1874 250979   3 18.0 215.4   47
c i   71.4   68719   520640     31367    9850   1908 251016   2 18.5 217.5   48
c i   71.6   68718   520640     31528    9984   1914 251029   3 18.6 217.7   48
c i   71.6   68717   520640     31529    9984   1914 251029   3 18.6 217.7   48
c i   71.6   68714   520640     31530    9984   1914 251029   2 18.6 217.7   48
c i   71.6   68710   520640     31531    9984   1914 251029   2 18.6 217.7   48
c i   71.6   68705   520640     31553    9999   1917 251031   3 18.6 217.6   48
c i   71.7   68704   520640     31609   10040   1920 251041   2 18.6 217.5   48
c i   72.0   68650   520640     31964   10335   1938 251064   2 18.7 216.9   48
c i   72.3   68649   520640     32319   10636   1947 251079   2 18.9 217.2   49
c -   72.3   68637   520640     32338    7149   1947 251082   3 18.9 217.2   46
c i   72.9   68636   520640     32881    7611   1977 251107   3 18.9 216.8   46
c i   72.9   68632   520640     32887    7613   1977 251110   3 18.9 216.8   46
c i   72.9   68627   520640     32897    7622   1977 251110   3 18.9 216.8   47
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   72.9   68623   520640     32980    7694   1979 251117   3 18.9 216.5   47
c i   72.9   68604   520640     32981    7694   1979 251117   3 18.9 216.5   47
c i   73.0   68598   520640     33096    7787   1981 251117   3 18.9 216.6   47
c i   73.8   68337   520640     34365    8826   2046 251215   2 19.2 216.4   47
c i   74.2   68330   520640     34995    9350   2085 251250   3 19.2 217.0   47
c i   74.5   68329   520640     35213    9527   2099 251268   2 19.1 216.8   47
c i   74.7   68203   520640     35353    9658   2102 251272   3 19.1 217.1   48
c i   74.7   68199   520640     35672    9913   2108 251297   4 19.1 216.9   48
c i   74.9   68029   520640     36316   10461   2127 251316   5 19.8 217.8   48
c i   74.9   68028   520640     36452   10575   2130 251318   4 19.9 217.9   48
c i   75.0   68027   520640     36645   10748   2133 251322   5 20.1 218.1   48
c i   75.1   68026   520640     36974   11053   2134 251329   6 21.4 220.0   49
c i   75.1   68025   520640     36991   11068   2135 251329   6 21.5 220.2   49
c i   75.1   67976   520640     36992   11068   2135 251329   6 21.5 220.2   49
c i   75.8   67949   520640     38321   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67946   520640     38322   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67942   520640     38323   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67939   520640     38324   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67936   520640     38325   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67933   520640     38326   12172   2178 251389   2 21.9 220.5   50
c i   75.8   67930   520640     38327   12172   2178 251389   2 21.9 220.5   50
c i   75.9   67927   520640     38445   12279   2182 251393   2 21.9 220.3   50
c i   75.9   67925   520640     38463   12292   2184 251394   2 21.9 220.3   50
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   75.9   67922   520640     38475   12303   2183 251395   2 21.9 220.3   50
c -   76.1   67922   520640     38600    8415   2190 251400   4 21.9 220.4   46
c i   76.2   67921   520640     38860    8640   2196 251413   3 21.9 220.3   46
c i   77.0   67920   520640     40132    9698   2255 251486   4 21.8 220.3   47
c i   77.0   67917   520640     40196    9758   2255 251488   4 21.7 220.2   47
c i   77.1   67914   520640     40224    9785   2255 251488   4 21.7 220.1   47
c i   77.1   67911   520640     40331    9883   2258 251489   3 21.7 220.0   47
c i   77.6   67907   520640     41009   10470   2296 251509   4 21.6 220.0   47
c i   77.8   67903   520640     41312   10722   2310 251533   3 21.6 220.7   47
c i   77.8   67901   520640     41329   10738   2310 251533   3 21.6 220.7   47
c i   77.9   67894   520640     41339   10744   2312 251534   3 21.6 220.7   47
c i   77.9   67893   520640     41380   10779   2315 251536   3 21.6 220.5   47
c i   77.9   67812   520640     41397   10792   2316 251538   3 21.6 220.4   47
c i   77.9   67808   520640     41402   10794   2317 251539   3 21.6 220.4   47
c i   78.2   67806   520640     41600   10962   2327 251552   2 21.6 221.4   47
c i   78.3   67801   520640     41751   11087   2336 251560   2 21.6 221.1   47
c i   78.6   67791   520640     42103   11392   2356 251572   4 21.6 221.1   48
c i   78.6   67790   520640     42261   11521   2365 251579   5 21.6 220.8   48
c i   78.7   67789   520640     42413   11661   2371 251581   5 21.6 220.7   48
c i   78.8   67784   520640     42717   11930   2382 251588   4 21.6 220.7   48
c i   78.8   67783   520640     42718   11930   2382 251588   4 21.6 220.7   48
c i   78.9   67781   520640     43093   12238   2387 251605   4 21.6 220.8   48
c i   78.9   67778   520640     43094   12238   2387 251605   4 21.6 220.8   48
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   79.0   67777   520640     43330   12444   2392 251614   4 21.5 220.3   48
c i   79.9   67776   520640     44591   13517   2445 251668   3 21.6 219.4   49
c i   79.9   67773   520640     44611   13534   2445 251668   2 21.6 219.4   49
c i   80.0   67218   520640     44774   13662   2454 251683   3 21.6 219.0   49
c -   80.7   66919   520640     45815   10020   2486 251729   4 21.9 218.6   46
c i   80.9   66918   520640     46092   10256   2497 251747   3 21.9 217.9   47
c i   81.7   66847   520640     47108   11087   2543 251805   3 22.5 217.1   47
c i   81.8   66846   520640     47232   11195   2546 251806   3 22.6 217.1   47
c i   81.8   66845   520640     47259   11216   2546 251806   3 22.6 217.1   47
c i   81.9   66814   520640     47619   11462   2557 251810   4 22.6 216.9   48
c i   81.9   66801   520640     47971   11745   2569 251821   5 22.5 216.7   48
c i   82.0   66799   520640     48140   11884   2569 251822   4 22.5 216.6   48
c i   82.0   66798   520640     48177   11908   2569 251823   3 22.5 216.6   48
c i   82.0   66795   520640     48217   11939   2569 251823   4 22.5 216.5   48
c 
c [simplification-7] limit of 48927 conflicts hit after 48930 conflicts
c [ternres-5] limit 10193540 with penalty 0 = 0 + 0
c [ternres-5] 10014 schedulable variables 14%
c [ternres-5] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-12] removed 3664 variables
c [treelook-3] limit 509677 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 63583 literals 48%
c [treelook-3] scheduling used 510195 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 509677 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 542129 steps
c [treelook-3] 63563 literals remain 48%
c [treelook-3] 10660 variables remain to probed next time 16%
c [treelook-3] removed 11 variables, found 2471 hbrs
c [lift-5] limit 6116124 with penalty 0 = 0 + 0
c [lift-5] using 56096 probes 84%
c [lift-5] 79 units, 21 impls, 2 eqs in 1 rounds
c [lift-5] 66180 variables remain 100% (135 retained)
c [lift-5] removed 396 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 29, lifted 74
c [unhide-7] limit 2038708 with penalty 0 = 0 + 0
c [unhide-7-7] 23 units, 209 failed, 22935 tauts, 0 hbrs, 18197 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 277 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 8 (25%) of length 27
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-5-1] eliminated 2 clauses out of 9 (22%) of length 25
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-5-1] eliminated 2 clauses out of 8 (25%) of length 23
c [cce-5-1] eliminated 3 clauses out of 8 (38%) of length 22
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 21
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-5-1] eliminated 3 clauses out of 12 (25%) of length 19
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 18
c [cce-5-1] eliminated 3 clauses out of 12 (25%) of length 17
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 16
c [cce-5-1] eliminated 3 clauses out of 11 (27%) of length 15
c [cce-5-1] eliminated 3 clauses out of 8 (38%) of length 14
c [cce-5-1] eliminated 3 clauses out of 10 (30%) of length 13
c [cce-5-1] eliminated 3 clauses out of 8 (38%) of length 12
c [cce-5-1] eliminated 3 clauses out of 10 (30%) of length 11
c [cce-5-1] eliminated 3 clauses out of 103 (3%) of length 10
c [cce-5-1] eliminated 3 clauses out of 495 (1%) of length 9
c [cce-5-1] eliminated 3 clauses out of 349 (1%) of length 8
c [cce-5-1] eliminated 7 clauses out of 531 (1%) of length 7
c [cce-5-1] eliminated 2 clauses out of 2638 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 62 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 359804 clauses = 228799 binary + 131005 ternary
c [cce-5] tried to eliminate 563 small clauses 0%
c [cce-5] eliminated 138 small clauses 0%
c [cce-5] eliminated 104 binary clauses 0%
c [cce-5] eliminated 34 ternary clauses 0%
c [cce-5-1] eliminated 1869 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1931 covered clauses in round 1
c [cce-5] eliminated 1931 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 65983 variables 100%
c [elim-7] limit of 203870803 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 1439 variables 2% in round 1 in 42287703 steps
c [elim-7-1] backward subsumption/strengthening limit 84575406
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 13835323 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1443 = 2% variables out of 65983
c [bca-6] limit of 10000000 steps
c [bca-6] 99319 out of 129082 literals actually usable 77%
c [bca-6] added 59 blocked clauses in 250418 steps
c [rephase-2] after 48930 conflicts (new increment 40000, next 88930)
c [flushphases] 0 phases reset
c [simplification-7] removed 2255 variables 3.4% (64540 remain 26%)
c [simplification-7] removed 87823 irredundant clauses 16.9% (432817 remain 31%)
c [simplification-7] maximum reduction of 17% = max (3%, 17%)
c [simplification-7] large reduction 17% >= 5% limit
c [simplification-7] new conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] new conflict limit 50930
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   87.9   64539   432817     48931   10845   2385 273392   8 22.8 217.3   40
c i   88.0   64538   432817     49150   11037   2390 273399   5 22.7 217.1   42
c i   88.1   64525   432817     49466   11266   2403 273418   4 23.0 217.0   42
c 
c [simplification-8] limit of 51108 conflicts hit after 51109 conflicts
c [ternres-6] limit 10374554 with penalty 0 = 0 + 0
c [ternres-6] all 64525 free variables schedulable
c [ternres-6] 279 ternary resolvents (0 bin, 279 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 518727 penalty 2 = 2 + 0
c [gauss-3] extracted 8 xors of average arity 3.0
c [gauss-3] connected 24 occurrences of 21 variables (average 1.1)
c [gauss-3] limit 518727 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 41 variables
c [basicprobe-3] limit 10374554 penalty 0 = 0 + 0
c [basicprobe-3-0] 19591 probes remain 31% after last round
c [basicprobe-3-0] 124 units = 124 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 387 variables, found 96340 hbrs
c [bate-2] eliminated 62 asymmetric tautologies during probing
c [cgrclsr-5] limit 518727 penalty 1 = 1 + 0
c [cgrclsr-5] all 64097 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [cgrclsr-5] removed 1 variables
c [lift-6] limit 6224732 with penalty 0 = 0 + 0
c [lift-6] using 53884 probes 84%
c [lift-6] 159 units, 25 impls, 0 eqs in 1 rounds
c [lift-6] 63470 variables remain 100% (214 retained)
c [lift-6] removed 412 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 32, lifted 4
c [unhide-8] limit 2074910 with penalty 0 = 0 + 0
c [unhide-8-8] 3 units, 235 failed, 29151 tauts, 0 hbrs, 18150 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 198 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 63499 variables 100%
c [block-4] limit of 25936387 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 25 blocked clauses
c [block-4] 25 < 1/1000 * 425966 = 425 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 127
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 125
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 123
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 121
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 119
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 117
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 115
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 114
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 113
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 112
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 111
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 109
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 107
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 105
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 104
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 103
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 102
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 101
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 100
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 99
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 98
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 97
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 96
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 95
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 94
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 93
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 92
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 91
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 90
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 89
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 88
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 87
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 86
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 85
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 84
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 83
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 82
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 81
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 80
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 79
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 78
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 77
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 76
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 75
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 74
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 73
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 72
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 71
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 70
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 69
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 68
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 67
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 66
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 65
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 64
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 63
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 62
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 61
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 60
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 59
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 58
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 57
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 56
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 55
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 54
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 53
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 52
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 51
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 50
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 49
c [cce-6-1] eliminated 4 clauses out of 8 (50%) of length 48
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 47
c [cce-6-1] eliminated 4 clauses out of 9 (44%) of length 46
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 45
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 44
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 43
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 42
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 41
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 40
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 39
c [cce-6-1] eliminated 6 clauses out of 11 (55%) of length 38
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 37
c [cce-6-1] eliminated 6 clauses out of 13 (46%) of length 36
c [cce-6-1] eliminated 6 clauses out of 11 (55%) of length 35
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 34
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 33
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 32
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 31
c [cce-6-1] eliminated 6 clauses out of 14 (43%) of length 30
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 29
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 28
c [cce-6-1] eliminated 5 clauses out of 11 (45%) of length 27
c [cce-6-1] eliminated 4 clauses out of 10 (40%) of length 26
c [cce-6-1] eliminated 5 clauses out of 12 (42%) of length 25
c [cce-6-1] eliminated 4 clauses out of 12 (33%) of length 24
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 23
c [cce-6-1] eliminated 3 clauses out of 12 (25%) of length 22
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 21
c [cce-6-1] eliminated 3 clauses out of 12 (25%) of length 20
c [cce-6-1] eliminated 6 clauses out of 13 (46%) of length 19
c [cce-6-1] eliminated 3 clauses out of 12 (25%) of length 18
c [cce-6-1] eliminated 6 clauses out of 13 (46%) of length 17
c [cce-6-1] eliminated 3 clauses out of 12 (25%) of length 16
c [cce-6-1] eliminated 6 clauses out of 13 (46%) of length 15
c [cce-6-1] eliminated 4 clauses out of 14 (29%) of length 14
c [cce-6-1] eliminated 8 clauses out of 13 (62%) of length 13
c [cce-6-1] eliminated 4 clauses out of 15 (27%) of length 12
c [cce-6-1] eliminated 8 clauses out of 14 (57%) of length 11
c [cce-6-1] eliminated 9 clauses out of 106 (8%) of length 10
c [cce-6-1] eliminated 14 clauses out of 462 (3%) of length 9
c [cce-6-1] eliminated 9 clauses out of 365 (2%) of length 8
c [cce-6-1] eliminated 16 clauses out of 509 (3%) of length 7
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 516 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 242872 clauses = 222942 binary + 19930 ternary
c [cce-6] tried to eliminate 611 small clauses 0%
c [cce-6] eliminated 179 small clauses 0%
c [cce-6] eliminated 155 binary clauses 0%
c [cce-6] eliminated 24 ternary clauses 0%
c [cce-6-1] eliminated 179 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 695 covered clauses in round 1
c [cce-6] eliminated 695 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 63498 variables 100%
c [elim-8] limit of 207491098 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 766 variables 1% in round 1 in 38796315 steps
c [elim-8-1] backward subsumption/strengthening limit 77592630
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 13221344 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 766 = 1% variables out of 63498
c [bca-7] limit of 10000000 steps
c [bca-7] 95472 out of 125466 literals actually usable 76%
c [bca-7] added 112 blocked clauses in 239550 steps
c [simplification-8] removed 1793 variables 2.8% (62732 remain 25%)
c [simplification-8] removed 10877 irredundant clauses 2.5% (421940 remain 31%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 6000 = 24000 / 4
c [simplification-8] new conflict interval 30000
c [simplification-8] penalized conflict interval 30000 = 1 * 30000
c [simplification-8] new conflict limit 81109
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   96.1   62731   421940     51276   11637   2650 357643   7 23.5 217.2   44
c i   96.3   62730   421940     51836   12134   2668 357650   3 23.7 217.2   44
c i   96.5   62729   421940     52392   12592   2677 357657   3 23.9 217.4   45
c i   96.5   62727   421940     52499   12676   2692 357660   3 24.0 217.3   45
c i   96.7   62726   421940     53802   13766   2715 357669   6 25.8 218.1   46
c i   96.7   62685   421940     53803   13766   2715 357669   6 25.8 218.1   46
c i   96.8   62643   421940     54054   13980   2716 357669   6 25.8 218.0   47
c i   96.9   62642   421940     54514   14302   2722 357677   3 26.7 218.1   47
c i   97.1   62641   421940     55672   15039   2733 357694   5 28.4 218.1   48
c i   97.2   62640   421940     56172   15458   2745 357713   4 28.5 218.1   48
c -   97.3   62640   421940     56411   10677   2752 357719   4 28.6 218.0   43
c R   97.4   62640   421940     57315   11232   2756 357729   4 28.9 217.7   43
c i   97.4   62639   421940     57316   11232   2756 357729   4 28.9 217.7   43
c i   97.7   62638   421940     57584   11466   2771 357731   3 28.8 217.7   44
c i   98.7   62637   421940     58910   12609   2818 357791   3 28.5 216.6   44
c i   98.7   62636   421940     59007   12697   2822 357792   4 28.5 216.5   44
c i   98.9   62635   421940     59734   13264   2848 357799   4 28.4 215.9   44
c i   99.1   62631   421940     59948   13452   2857 357803   4 28.3 215.7   44
c i   99.5   62630   421940     60625   13968   2883 357824   6 28.5 215.4   45
c i   99.5   62629   421940     60655   13995   2885 357824   5 28.5 215.3   45
c i   99.8   62626   421940     61173   14431   2907 357846   3 28.5 214.6   45
c i  100.0   62623   421940     61461   14689   2919 357856   6 28.4 214.6   45
c i  100.0   62621   421940     61463   14689   2919 357857   6 28.4 214.6   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  100.0   62617   421940     61464   14689   2919 357857   6 28.4 214.6   45
c i  100.0   62614   421940     61465   14689   2919 357857   6 28.4 214.6   45
c i  100.2   62611   421940     61818   14975   2924 357867   3 28.4 214.3   45
c i  100.4   62610   421940     62666   15713   2943 357878   4 28.7 214.6   45
c i  100.6   62607   421940     63184   16155   2962 357888   4 28.6 214.2   45
c i  100.8   62604   421940     63767   16586   2976 357897   4 28.7 213.6   46
c i  100.9   62601   421940     64158   16893   2987 357908   2 28.6 213.2   46
c i  101.0   62600   421940     64258   16973   2993 357910   4 28.6 213.1   46
c i  101.1   62598   421940     64477   17168   2997 357913   4 28.6 213.0   46
c -  101.2   62596   421940     64798   11934   3007 357926   7 28.6 212.9   43
c i  101.4   62595   421940     65240   12328   3019 357934   3 28.5 213.0   43
c i  101.4   62591   421940     65248   12330   3019 357935   3 28.5 213.0   43
c i  101.6   62590   421940     65550   12588   3030 357945   3 28.6 212.8   43
c i  101.6   62589   421940     65552   12589   3030 357945   3 28.6 212.8   43
c i  101.7   62588   421940     65780   12787   3036 357956   5 28.6 212.5   43
c i  101.7   62585   421940     65886   12874   3038 357958   3 28.6 212.6   43
c i  101.9   62584   421940     66063   13033   3047 357964   4 28.6 212.4   43
c i  102.1   62581   421940     66281   13218   3055 357977   3 28.5 212.3   44
c i  102.3   62580   421940     66507   13413   3066 357986   5 28.5 212.3   44
c i  102.3   62577   421940     66534   13437   3068 357986   4 28.5 212.5   44
c i  102.6   62576   421940     67184   13991   3087 358028   4 28.5 212.4   44
c i  103.2   62518   421940     69209   15528   3140 358076   3 29.4 212.2   45
c i  103.4   62515   421940     69446   15720   3156 358087   3 29.3 212.0   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  103.5   62513   421940     69544   15805   3160 358094   4 29.3 212.0   45
c i  103.6   62511   421940     69694   15927   3162 358113   1 29.3 211.8   45
c i  103.7   62510   421940     69804   16019   3166 358118   4 29.3 211.6   45
c i  103.7   62507   421940     69878   16083   3168 358119   2 29.3 211.5   45
c i  103.7   62503   421940     69879   16083   3168 358119   2 29.3 211.5   45
c i  103.8   62500   421940     69890   16092   3169 358119   3 29.3 211.5   45
c i  104.3   62494   421940     70605   16744   3193 358138   4 29.2 212.3   46
c i  105.3   62493   421940     72446   18339   3241 358187   5 29.5 211.4   46
c i  105.4   62492   421940     72564   18437   3252 358191   3 29.5 211.2   46
c i  105.4   62488   421940     72565   18437   3252 358191   2 29.5 211.2   46
c i  105.5   62486   421940     72584   18448   3255 358195   2 29.5 211.2   46
c i  105.7   62482   421940     72965   18766   3267 358204   3 29.6 210.8   47
c i  105.7   62468   421940     73039   18817   3269 358205   4 29.6 210.7   47
c -  106.0   62468   421940     73806   13414   3293 358221   5 29.7 210.5   43
c i  106.4   62467   421940     74571   13961   3307 358234   2 30.0 210.2   44
c i  106.5   62425   421940     74806   14162   3321 358248   6 30.0 210.0   44
c i  106.8   62421   421940     75133   14450   3329 358263   4 29.9 209.8   44
c i  106.9   62420   421940     75523   14797   3344 358266   5 29.9 210.1   44
c i  106.9   62417   421940     75524   14797   3344 358266   5 29.9 210.1   44
c i  107.5   62413   421940     76061   15245   3371 358307   4 29.8 209.7   44
c i  107.5   62410   421940     76062   15245   3371 358307   4 29.8 209.7   44
c i  107.7   62409   421940     76300   15456   3379 358320   4 29.7 209.6   44
c i  107.8   62406   421940     76542   15654   3384 358322   4 29.9 209.7   44
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  107.8   62404   421940     76666   15743   3384 358324   3 30.0 209.6   44
c i  107.8   62403   421940     76677   15749   3384 358325   3 30.0 209.6   45
c i  107.8   62402   421940     76708   15779   3384 358325   3 30.0 209.6   45
c i  107.8   62401   421940     76735   15800   3388 358325   4 30.0 209.6   45
c i  107.8   62400   421940     76750   15814   3388 358325   4 30.0 209.6   45
c i  107.9   62396   421940     76835   15892   3393 358326   3 29.9 209.6   45
c i  108.0   62395   421940     77018   16064   3397 358327   5 29.9 209.6   45
c i  108.0   62393   421940     77037   16081   3397 358327   5 29.9 209.6   45
c i  108.3   62391   421940     77404   16395   3402 358330   3 30.0 209.4   45
c i  108.3   62390   421940     77405   16395   3402 358330   3 30.0 209.4   45
c i  108.3   62389   421940     77406   16395   3402 358330   3 30.0 209.4   45
c i  108.3   62388   421940     77407   16395   3402 358330   3 30.0 209.4   45
c i  108.3   62372   421940     77408   16395   3402 358330   3 30.0 209.4   45
c i  108.9   62371   421940     78332   17195   3424 358360   4 29.9 209.0   45
c i  109.1   62367   421940     78493   17336   3431 358366   2 29.9 209.1   45
c i  109.3   62366   421940     78917   17686   3448 358379   5 30.1 209.5   46
c i  109.6   62364   421940     80054   18697   3468 358398   4 30.4 210.4   46
c i  109.7   62363   421940     80212   18840   3472 358402   5 30.5 210.4   46
c i  109.7   62362   421940     80341   18958   3476 358406   4 30.5 210.5   46
c i  110.3   62361   421940     82140   20360   3506 358431   5 31.3 210.9   49
c i  110.4   62360   421940     82519   20644   3515 358435   5 31.5 210.9   49
c i  110.4   62357   421940     82525   20649   3515 358435   5 31.6 210.9   49
c i  110.4   62354   421940     82543   20664   3516 358436   5 31.5 210.9   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  110.5   62353   421940     82674   20765   3519 358445   4 31.6 210.8   50
c -  110.7   62353   421940     83371   14803   3530 358461   6 31.5 210.6   43
c i  110.7   62352   421940     83511   14928   3533 358466   7 31.5 210.6   44
c 
c [simplification-9] limit of 84573 conflicts hit after 84574 conflicts
c [ternres-7] limit 14635373 with penalty 0 = 0 + 0
c [ternres-7] all 62352 free variables schedulable
c [ternres-7] 204 ternary resolvents (0 bin, 204 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-15] removed 593 variables
c [simpleprobe-4] 21550 schedulable variables 35%
c [simpleprobe-4] limit 58541494 penalty 0 = 0 + 0
c [decomp-16] removed 2054 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2054 variables, found 102900 hbrs, 1253 units
c [cgrclsr-6] limit 1463537 penalty 0 = 0 + 0
c [cgrclsr-6] all 60085 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 1 variables
c [lift-7] limit 8781224 with penalty 0 = 0 + 0
c [lift-7] using 50783 probes 85%
c [lift-7] 261 units, 50 impls, 0 eqs in 1 rounds
c [lift-7] 59343 variables remain 99% (371 retained)
c [lift-7] removed 370 variables
c [cliff-7] limit of 11708298 steps penalty 0 = 0 + 0
c [cliff-7] failed 37, lifted 22
c [unhide-9] limit 2927074 with penalty 0 = 0 + 0
c [unhide-9-10] 1 units, 107 failed, 63209 tauts, 0 hbrs, 25147 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 356 transitive binary clauses
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 65
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 64
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 63
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 62
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 61
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 60
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 59
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 58
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 57
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 56
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 55
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 54
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 53
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 52
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 51
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 50
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 49
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 48
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 47
c [cce-7-1] eliminated 1 clauses out of 8 (12%) of length 46
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 45
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 44
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 43
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 42
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 41
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 40
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 39
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 38
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 37
c [cce-7-1] eliminated 1 clauses out of 8 (12%) of length 36
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 35
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 34
c [cce-7-1] eliminated 2 clauses out of 8 (25%) of length 33
c [cce-7-1] eliminated 1 clauses out of 9 (11%) of length 32
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 31
c [cce-7-1] eliminated 1 clauses out of 11 (9%) of length 30
c [cce-7-1] eliminated 2 clauses out of 8 (25%) of length 29
c [cce-7-1] eliminated 1 clauses out of 8 (12%) of length 28
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 27
c [cce-7-1] eliminated 1 clauses out of 8 (12%) of length 26
c [cce-7-1] eliminated 2 clauses out of 8 (25%) of length 25
c [cce-7-1] eliminated 1 clauses out of 10 (10%) of length 24
c [cce-7-1] eliminated 2 clauses out of 8 (25%) of length 23
c [cce-7-1] eliminated 1 clauses out of 9 (11%) of length 22
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-7-1] eliminated 1 clauses out of 10 (10%) of length 20
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 19
c [cce-7-1] eliminated 2 clauses out of 12 (17%) of length 18
c [cce-7-1] eliminated 4 clauses out of 10 (40%) of length 17
c [cce-7-1] eliminated 2 clauses out of 12 (17%) of length 16
c [cce-7-1] eliminated 4 clauses out of 12 (33%) of length 15
c [cce-7-1] eliminated 1 clauses out of 11 (9%) of length 14
c [cce-7-1] eliminated 2 clauses out of 9 (22%) of length 13
c [cce-7-1] eliminated 1 clauses out of 10 (10%) of length 12
c [cce-7-1] eliminated 2 clauses out of 10 (20%) of length 11
c [cce-7-1] eliminated 2 clauses out of 90 (2%) of length 10
c [cce-7-1] eliminated 1 clauses out of 418 (0%) of length 9
c [cce-7-1] eliminated 2 clauses out of 335 (1%) of length 8
c [cce-7-1] eliminated 4 clauses out of 465 (1%) of length 7
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 101 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 225989 clauses = 207524 binary + 18465 ternary
c [cce-7] tried to eliminate 919 small clauses 0%
c [cce-7] eliminated 249 small clauses 0%
c [cce-7] eliminated 223 binary clauses 0%
c [cce-7] eliminated 26 ternary clauses 0%
c [cce-7-1] eliminated 632 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 733 covered clauses in round 1
c [cce-7] eliminated 733 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 59578 variables 100%
c [elim-9] limit of 292707473 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 1501 variables 3% in round 1 in 39475188 steps
c [elim-9-1] backward subsumption/strengthening limit 78950376
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 11914193 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1501 = 3% variables out of 59578
c [bca-8] limit of 10000000 steps
c [bca-8] 84146 out of 116156 literals actually usable 72%
c [bca-8] added 87 blocked clauses in 212375 steps
c [simplification-9] removed 4275 variables 6.9% (58077 remain 23%)
c [simplification-9] removed 40026 irredundant clauses 9.5% (381914 remain 28%)
c [simplification-9] maximum reduction of 9% = max (7%, 9%)
c [simplification-9] large reduction 9% >= 5% limit
c [simplification-9] new conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] new conflict limit 86574
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  120.2   58076   381914     84652   14182   3378 407156   4 31.5 210.1   43
c i  120.3   58075   381914     84855   14355   3388 407171   4 31.5 210.0   43
c i  120.5   58061   381914     85072   14538   3400 407186   3 31.4 209.9   43
c i  120.5   58058   381914     85079   14542   3401 407187   3 31.4 209.9   43
c i  120.6   58053   381914     85227   14675   3406 407190   4 31.4 209.7   43
c i  121.1   58052   381914     86313   15615   3433 407224   3 31.4 209.3   44
c i  121.4   58051   381914     86803   16058   3445 407230   4 31.5 209.1   44
c 
c [simplification-10] limit of 86864 conflicts hit after 86864 conflicts
c [ternres-8] limit 14994821 with penalty 0 = 0 + 0
c [ternres-8] all 58051 free variables schedulable
c [ternres-8] 204 ternary resolvents (0 bin, 204 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 937176 penalty 3 = 3 + 0
c [card-4] found 15279 at-most-one constraints of average size 3.7
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 937176 for elimination
c [card-4] 15279 out of 15279 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-17] removed 73 variables
c [treelook-4] limit 749741 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 68267 literals 59%
c [treelook-4] scheduling used 749746 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 749741 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 825478 steps
c [treelook-4] 68257 literals remain 59%
c [treelook-4] 8661 variables remain to probed next time 15%
c [treelook-4] removed 0 variables, found 5636 hbrs
c [cgrclsr-7] limit 1499482 penalty 0 = 0 + 0
c [cgrclsr-7] all 58004 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [lift-8] limit 8996893 with penalty 0 = 0 + 0
c [lift-8] using 49170 probes 85%
c [lift-8] 96 units, 48 impls, 1 eqs in 1 rounds
c [lift-8] 57228 variables remain 99% (527 retained)
c [lift-8] removed 249 variables
c [cliff-8] limit of 11995857 steps penalty 0 = 0 + 0
c [cliff-8] failed 16, lifted 8
c [unhide-10] limit 2998964 with penalty 0 = 0 + 0
c [unhide-10-11] 0 units, 42 failed, 22167 tauts, 0 hbrs, 19569 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 289 transitive binary clauses
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 54
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 53
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 52
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 51
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 50
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 49
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 48
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 47
c [cce-8-1] eliminated 2 clauses out of 9 (22%) of length 46
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 45
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 44
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 43
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 42
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 41
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 40
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 39
c [cce-8-1] eliminated 6 clauses out of 13 (46%) of length 38
c [cce-8-1] eliminated 4 clauses out of 9 (44%) of length 37
c [cce-8-1] eliminated 4 clauses out of 13 (31%) of length 36
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 35
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 34
c [cce-8-1] eliminated 5 clauses out of 12 (42%) of length 33
c [cce-8-1] eliminated 4 clauses out of 14 (29%) of length 32
c [cce-8-1] eliminated 4 clauses out of 11 (36%) of length 31
c [cce-8-1] eliminated 5 clauses out of 17 (29%) of length 30
c [cce-8-1] eliminated 6 clauses out of 14 (43%) of length 29
c [cce-8-1] eliminated 6 clauses out of 15 (40%) of length 28
c [cce-8-1] eliminated 6 clauses out of 16 (38%) of length 27
c [cce-8-1] eliminated 8 clauses out of 16 (50%) of length 26
c [cce-8-1] eliminated 9 clauses out of 20 (45%) of length 25
c [cce-8-1] eliminated 9 clauses out of 20 (45%) of length 24
c [cce-8-1] eliminated 11 clauses out of 22 (50%) of length 23
c [cce-8-1] eliminated 10 clauses out of 20 (50%) of length 22
c [cce-8-1] eliminated 11 clauses out of 21 (52%) of length 21
c [cce-8-1] eliminated 10 clauses out of 21 (48%) of length 20
c [cce-8-1] eliminated 10 clauses out of 21 (48%) of length 19
c [cce-8-1] eliminated 11 clauses out of 22 (50%) of length 18
c [cce-8-1] eliminated 10 clauses out of 22 (45%) of length 17
c [cce-8-1] eliminated 11 clauses out of 24 (46%) of length 16
c [cce-8-1] eliminated 14 clauses out of 27 (52%) of length 15
c [cce-8-1] eliminated 14 clauses out of 29 (48%) of length 14
c [cce-8-1] eliminated 13 clauses out of 24 (54%) of length 13
c [cce-8-1] eliminated 14 clauses out of 28 (50%) of length 12
c [cce-8-1] eliminated 13 clauses out of 26 (50%) of length 11
c [cce-8-1] eliminated 14 clauses out of 103 (14%) of length 10
c [cce-8-1] eliminated 12 clauses out of 425 (3%) of length 9
c [cce-8-1] eliminated 14 clauses out of 334 (4%) of length 8
c [cce-8-1] eliminated 15 clauses out of 466 (3%) of length 7
c [cce-8-1] eliminated 5 clauses out of 2566 (0%) of length 6
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 333 large clauses in 30000001 steps
c [cce-8-1] allowing another 15000000 steps for small clauses
c [cce-8] scheduling 221427 clauses = 203261 binary + 18166 ternary
c [cce-8] tried to eliminate 784 small clauses 0%
c [cce-8] eliminated 233 small clauses 0%
c [cce-8] eliminated 217 binary clauses 0%
c [cce-8] eliminated 16 ternary clauses 0%
c [cce-8-1] eliminated 448 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 781 covered clauses in round 1
c [cce-8] eliminated 781 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 57686 variables 100%
c [elim-10] limit of 299896434 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 410 variables 1% in round 1 in 34879291 steps
c [elim-10-1] backward subsumption/strengthening limit 69758582
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 11679951 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 423 = 1% variables out of 57686
c [bca-9] limit of 10000000 steps
c [bca-9] 81644 out of 114528 literals actually usable 71%
c [bca-9] added 62 blocked clauses in 208588 steps
c [simplification-10] removed 788 variables 1.4% (57263 remain 23%)
c [simplification-10] removed 5818 irredundant clauses 1.5% (376096 remain 27%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 10000 = 30000 / 3
c [simplification-10] new conflict interval 40000
c [simplification-10] penalized conflict interval 40000 = 1 * 40000
c [simplification-10] new conflict limit 126864
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  128.1   57262   376096     87544   16201   3581 431610   4 31.4 208.5   44
c i  128.3   57261   376096     88145   16724   3592 431616   4 31.5 208.3   45
c i  129.2   57260   376096     89873   18212   3635 431647   3 31.5 207.8   46
c i  129.5   57254   376096     90339   18627   3653 431655   6 31.5 207.7   47
c i  130.6   57253   376096     92317   20331   3704 431708   3 31.7 207.2   47
c i  130.7   57252   376096     92423   20412   3706 431711   5 31.7 207.1   47
c i  130.7   57251   376096     92424   20412   3706 431711   5 31.7 207.1   47
c i  130.7   57250   376096     92531   20501   3707 431712   6 31.7 207.1   47
c i  130.9   57249   376096     92710   20652   3711 431714   3 31.7 207.0   48
c i  131.0   57248   376096     92859   20776   3717 431729   3 31.7 206.8   48
c i  131.2   57247   376096     93335   21177   3737 431737   4 31.9 207.0   49
c i  131.2   57246   376096     93569   21378   3738 431743   4 32.1 207.5   49
c i  131.3   57244   376096     93570   21378   3738 431743   4 32.1 207.5   49
c i  131.3   57240   376096     93627   21430   3740 431743   4 32.2 207.5   49
c i  131.3   57239   376096     93783   21562   3741 431747   6 32.2 207.5   49
c i  131.4   57238   376096     94126   21848   3758 431750   4 32.5 207.6   49
c i  131.6   57237   376096     94952   22561   3772 431757   7 32.8 208.0   50
c -  131.6   57237   376096     94952   15517   3772 431757   7 32.8 208.0   43
c i  131.8   57236   376096     95473   16007   3779 431758   4 32.8 208.2   44
c i  131.8   57235   376096     95564   16088   3781 431761   5 32.8 208.2   44
c i  132.1   57234   376096     95943   16424   3792 431771   3 32.8 208.0   44
c i  132.4   57232   376096     96628   17045   3812 431781   4 32.7 207.5   45
c i  132.6   57231   376096     97025   17383   3823 431800   4 32.7 207.2   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  133.3   57213   376096     98306   18501   3859 431830   3 32.6 206.7   45
c i  133.5   57122   376096     98771   18909   3871 431839   4 32.6 206.5   46
c i  133.7   57121   376096     98899   19027   3872 431842   2 32.6 206.6   46
c i  133.8   57120   376096     99032   19146   3875 431849   5 32.6 206.5   46
c i  133.8   57119   376096     99033   19146   3875 431849   5 32.6 206.5   46
c i  133.8   57118   376096     99038   19150   3875 431849   5 32.6 206.5   46
c i  133.8   57114   376096     99223   19307   3878 431849   4 32.6 206.5   46
c i  133.8   57113   376096     99224   19307   3878 431849   4 32.6 206.5   46
c i  133.9   57112   376096     99309   19380   3880 431853   4 32.6 206.4   46
c i  133.9   56995   376096     99316   19385   3880 431854   4 32.6 206.4   46
c i  133.9   56968   376096     99342   19395   3881 431857   3 32.6 206.4   46
c i  134.1   56810   376096     99708   19696   3893 431862   4 32.6 206.2   46
c i  134.2   56807   376096     99798   19775   3895 431862   6 32.6 206.1   46
c i  134.2   56804   376096     99848   19814   3895 431862   5 32.6 206.1   46
c i  134.3   56803   376096    100628   20401   3899 431868   6 32.7 206.0   47
c i  135.5   56802   376096    103096   22411   3960 431916   4 33.2 205.3   48
c i  135.7   56800   376096    103336   22630   3968 431919   3 33.2 205.1   48
c i  136.1   56799   376096    103916   23111   3988 431925   5 33.3 204.7   48
c i  136.2   56798   376096    104102   23235   3990 431928   4 33.5 204.7   49
c i  136.2   56797   376096    104103   23235   3990 431928   4 33.5 204.7   49
c i  136.4   56796   376096    104478   23556   4003 431937   5 33.4 204.4   49
c i  136.5   56795   376096    104608   23669   4009 431942   4 33.4 204.3   49
c i  136.7   56792   376096    104904   23930   4015 431949   3 33.4 204.2   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  136.8   56791   376096    105448   24361   4022 431963   4 33.6 204.2   49
c i  136.9   56790   376096    105690   24539   4023 431969   5 33.7 204.2   50
c -  136.9   56790   376096    105746   17108   4023 431969   5 33.7 204.2   43
c i  137.0   56789   376096    105836   17163   4023 431970   6 33.7 204.2   44
c i  137.0   56778   376096    105839   17165   4023 431970   6 33.7 204.2   44
c i  137.5   56754   376096    108047   19070   4054 431987   5 33.7 204.1   46
c i  138.5   56753   376096    112935   22697   4086 432010   4 38.8 205.7   52
c i  138.8   56752   376096    114473   23886   4098 432016   8 39.4 205.8   54
c i  139.0   56751   376096    115118   24386   4107 432016   5 39.6 205.9   54
c i  139.0   56750   376096    115119   24386   4107 432016   5 39.6 205.9   54
c i  139.0   56747   376096    115120   24386   4107 432016   5 39.6 205.9   54
c i  139.0   56746   376096    115121   24386   4107 432016   5 39.6 205.9   54
c i  139.0   56745   376096    115122   24386   4107 432016   5 39.6 205.9   54
c i  139.0   56744   376096    115123   24386   4107 432016   5 39.6 205.9   54
c i  139.2   56743   376096    116242   25264   4113 432024   4 39.7 205.7   54
c i  139.3   56742   376096    116384   25391   4118 432025   4 39.7 205.7   54
c i  139.3   56741   376096    116385   25391   4118 432025   4 39.7 205.7   54
c -  139.5   56741   376096    117360   18142   4127 432038   9 40.2 205.8   43
c i  139.9   56740   376096    119573   20035   4147 432048   6 41.0 206.3   46
c i  139.9   56739   376096    119596   20055   4148 432048   7 41.0 206.3   46
c i  139.9   56738   376096    119628   20073   4148 432048   6 41.0 206.3   46
c i  140.4   56737   376096    122210   22131   4170 432061   5 41.2 206.1   48
c i  140.5   56736   376096    122509   22388   4171 432065   5 41.2 206.0   48
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  140.6   56734   376096    122976   22736   4176 432075   6 41.3 206.0   48
c i  140.7   56715   376096    123459   23104   4181 432090   3 41.5 206.1   49
c i  140.7   56714   376096    123460   23104   4181 432090   2 41.5 206.1   49
c i  140.7   56713   376096    123461   23104   4181 432090   2 41.5 206.1   49
c i  140.7   56710   376096    123565   23201   4184 432090   6 41.5 206.1   49
c i  141.1   56709   376096    124495   23856   4192 432100   4 41.7 206.0   49
c R  141.3   56706   376096    125257   24366   4200 432103   2 42.0 205.9   50
c i  141.6   56705   376096    125749   24807   4206 432113   5 41.9 205.6   51
c i  142.3   56704   376096    126868   25771   4254 432137   4 41.8 205.1   51
c i  142.5   56674   376096    127209   26055   4264 432150   3 41.7 205.0   51
c i  142.5   56673   376096    127231   26068   4266 432151   3 41.7 205.0   51
c i  142.5   56669   376096    127353   26144   4270 432156   3 41.7 204.9   51
c i  142.9   56668   376096    128065   26779   4283 432173   4 41.7 204.5   51
c i  143.0   56665   376096    128103   26812   4284 432174   4 41.7 204.5   51
c i  143.0   56664   376096    128115   26819   4285 432175   4 41.7 204.5   51
c i  143.3   56663   376096    128614   27243   4292 432182   4 41.7 204.4   52
c -  143.7   56661   376096    129397   19411   4317 432207   5 41.6 204.0   43
c 
c [simplification-11] limit of 129712 conflicts hit after 129712 conflicts
c [ternres-9] limit 19436344 with penalty 0 = 0 + 0
c [ternres-9] all 56661 free variables schedulable
c [ternres-9] 75 ternary resolvents (0 bin, 75 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-19] removed 648 variables
c [basicprobe-4] limit 19436344 penalty 0 = 0 + 0
c [basicprobe-4-0] 17455 probes remain 31% after last round
c [basicprobe-4-0] 245 units = 245 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 361 variables, found 172324 hbrs
c [bate-3] eliminated 108 asymmetric tautologies during probing
c [lift-9] limit 11661806 with penalty 0 = 0 + 0
c [lift-9] using 47886 probes 85%
c [lift-9] 120 units, 58 impls, 3 eqs in 1 rounds
c [lift-9] 55054 variables remain 99% (780 retained)
c [lift-9] removed 420 variables
c [cliff-9] limit of 15549075 steps penalty 0 = 0 + 0
c [cliff-9] failed 20, lifted 24
c [unhide-11] limit 3887268 with penalty 0 = 0 + 0
c [unhide-11-13] 5 units, 104 failed, 34020 tauts, 0 hbrs, 29883 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 223 transitive binary clauses
c [cce-9] limit of 38872688 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 41
c [cce-9-1] eliminated 1 clauses out of 10 (10%) of length 40
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 39
c [cce-9-1] eliminated 1 clauses out of 10 (10%) of length 38
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 37
c [cce-9-1] eliminated 1 clauses out of 10 (10%) of length 36
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 35
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 34
c [cce-9-1] eliminated 2 clauses out of 11 (18%) of length 33
c [cce-9-1] eliminated 1 clauses out of 9 (11%) of length 32
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 31
c [cce-9-1] eliminated 1 clauses out of 14 (7%) of length 30
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 29
c [cce-9-1] eliminated 1 clauses out of 11 (9%) of length 28
c [cce-9-1] eliminated 2 clauses out of 12 (17%) of length 27
c [cce-9-1] eliminated 1 clauses out of 10 (10%) of length 26
c [cce-9-1] eliminated 2 clauses out of 11 (18%) of length 25
c [cce-9-1] eliminated 1 clauses out of 11 (9%) of length 24
c [cce-9-1] eliminated 2 clauses out of 14 (14%) of length 23
c [cce-9-1] eliminated 1 clauses out of 13 (8%) of length 22
c [cce-9-1] eliminated 2 clauses out of 12 (17%) of length 21
c [cce-9-1] eliminated 1 clauses out of 9 (11%) of length 20
c [cce-9-1] eliminated 2 clauses out of 16 (12%) of length 19
c [cce-9-1] eliminated 1 clauses out of 12 (8%) of length 18
c [cce-9-1] eliminated 2 clauses out of 14 (14%) of length 17
c [cce-9-1] eliminated 1 clauses out of 14 (7%) of length 16
c [cce-9-1] eliminated 2 clauses out of 14 (14%) of length 15
c [cce-9-1] eliminated 1 clauses out of 17 (6%) of length 14
c [cce-9-1] eliminated 2 clauses out of 14 (14%) of length 13
c [cce-9-1] eliminated 1 clauses out of 15 (7%) of length 12
c [cce-9-1] eliminated 2 clauses out of 13 (15%) of length 11
c [cce-9-1] eliminated 1 clauses out of 77 (1%) of length 10
c [cce-9-1] eliminated 20 clauses out of 340 (6%) of length 9
c [cce-9-1] eliminated 7 clauses out of 326 (2%) of length 8
c [cce-9-1] eliminated 30 clauses out of 435 (7%) of length 7
c [cce-9-1] eliminated 5 clauses out of 2580 (0%) of length 6
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 110 large clauses in 38872689 steps
c [cce-9-1] allowing another 19436344 steps for small clauses
c [cce-9] scheduling 213027 clauses = 194839 binary + 18188 ternary
c [cce-9] tried to eliminate 1212 small clauses 1%
c [cce-9] eliminated 347 small clauses 0%
c [cce-9] eliminated 301 binary clauses 0%
c [cce-9] eliminated 46 ternary clauses 0%
c [cce-9-1] eliminated 668 small clauses in 38872689 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 778 covered clauses in round 1
c [cce-9] eliminated 778 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 55720 variables 100%
c [elim-11] limit of 388726881 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 724 variables 1% in round 1 in 34995331 steps
c [elim-11-1] backward subsumption/strengthening limit 69990662
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 10762791 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 726 = 1% variables out of 55720
c [bca-10] limit of 10000000 steps
c [bca-10] 76776 out of 109990 literals actually usable 70%
c [bca-10] added 323 blocked clauses in 197950 steps
c [rephase-3] after 129712 conflicts (new increment 80000, next 209712)
c [flushphases] 0 phases reset
c [simplification-11] removed 1667 variables 2.9% (54994 remain 22%)
c [simplification-11] removed 24156 irredundant clauses 6.4% (351940 remain 26%)
c [simplification-11] maximum reduction of 6% = max (3%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] new conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] new conflict limit 131712
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  153.0   54993   351940    130485   18095   4297 603798  10 41.5 204.2   48
c 
c [simplification-12] limit of 131782 conflicts hit after 131782 conflicts
c [ternres-10] limit 19654017 with penalty 0 = 0 + 0
c [ternres-10] all 54993 free variables schedulable
c [ternres-10] 198 ternary resolvents (1 bin, 197 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 491350 penalty 3 = 3 + 0
c [gauss-4] extracted 8 xors of average arity 3.0
c [gauss-4] connected 24 occurrences of 24 variables (average 1.0)
c [gauss-4] limit 491350 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 2 variables
c [simpleprobe-5] all 54991 free variables schedulable
c [simpleprobe-5] limit 78616070 penalty 0 = 0 + 0
c [decomp-21] removed 251 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 251 variables, found 67728 hbrs, 193 units
c [cgrclsr-8] limit 982700 penalty 1 = 1 + 0
c [cgrclsr-8] all 54740 free variables schedulable
c [cgrclsr-8] fully completed congruence closure
c [lift-10] limit 11792410 with penalty 0 = 0 + 0
c [lift-10] using 46417 probes 85%
c [lift-10] 110 units, 62 impls, 8 eqs in 1 rounds
c [lift-10] 53422 variables remain 98% (1049 retained)
c [lift-10] removed 269 variables
c [cliff-10] limit of 15723214 steps penalty 0 = 0 + 0
c [cliff-10] failed 15, lifted 2
c [unhide-12] limit 3930803 with penalty 0 = 0 + 0
c [unhide-12-14] 0 units, 129 failed, 42313 tauts, 0 hbrs, 15597 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 167 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 54417 variables 100%
c [block-5] limit of 24567521 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 4 blocked clauses
c [block-5] 4 < 1/1000 * 347516 = 347 considered unsuccessful
c [cce-10] limit of 39308035 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 122
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 121
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 120
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 119
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 118
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 78
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 77
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 76
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 75
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 74
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 73
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 72
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 71
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 70
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 68
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 67
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 66
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 65
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 64
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 63
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 62
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 61
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 60
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 59
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 58
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 57
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 56
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 55
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 43
c [cce-10-1] eliminated 1 clauses out of 11 (9%) of length 42
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 41
c [cce-10-1] eliminated 1 clauses out of 11 (9%) of length 40
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 39
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 38
c [cce-10-1] eliminated 2 clauses out of 10 (20%) of length 37
c [cce-10-1] eliminated 3 clauses out of 11 (27%) of length 36
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 35
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 34
c [cce-10-1] eliminated 3 clauses out of 13 (23%) of length 33
c [cce-10-1] eliminated 3 clauses out of 11 (27%) of length 32
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 31
c [cce-10-1] eliminated 3 clauses out of 15 (20%) of length 30
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 29
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 28
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 27
c [cce-10-1] eliminated 3 clauses out of 13 (23%) of length 26
c [cce-10-1] eliminated 3 clauses out of 13 (23%) of length 25
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 24
c [cce-10-1] eliminated 3 clauses out of 17 (18%) of length 23
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 22
c [cce-10-1] eliminated 3 clauses out of 16 (19%) of length 21
c [cce-10-1] eliminated 3 clauses out of 11 (27%) of length 20
c [cce-10-1] eliminated 3 clauses out of 19 (16%) of length 19
c [cce-10-1] eliminated 3 clauses out of 14 (21%) of length 18
c [cce-10-1] eliminated 3 clauses out of 17 (18%) of length 17
c [cce-10-1] eliminated 3 clauses out of 16 (19%) of length 16
c [cce-10-1] eliminated 3 clauses out of 17 (18%) of length 15
c [cce-10-1] eliminated 3 clauses out of 18 (17%) of length 14
c [cce-10-1] eliminated 3 clauses out of 18 (17%) of length 13
c [cce-10-1] eliminated 3 clauses out of 16 (19%) of length 12
c [cce-10-1] eliminated 3 clauses out of 18 (17%) of length 11
c [cce-10-1] eliminated 5 clauses out of 84 (6%) of length 10
c [cce-10-1] eliminated 8 clauses out of 317 (3%) of length 9
c [cce-10-1] eliminated 7 clauses out of 312 (2%) of length 8
c [cce-10-1] eliminated 9 clauses out of 416 (2%) of length 7
c [cce-10-1] eliminated 3 clauses out of 2557 (0%) of length 6
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 165 large clauses in 39308036 steps
c [cce-10-1] allowing another 19654018 steps for small clauses
c [cce-10] scheduling 209057 clauses = 191906 binary + 17151 ternary
c [cce-10] tried to eliminate 1218 small clauses 1%
c [cce-10] eliminated 345 small clauses 0%
c [cce-10] eliminated 316 binary clauses 0%
c [cce-10] eliminated 29 ternary clauses 0%
c [cce-10-1] eliminated 345 small clauses in 39308036 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 510 covered clauses in round 1
c [cce-10] eliminated 510 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 54417 variables 100%
c [elim-12] limit of 393080350 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 302 variables 1% in round 1 in 34285239 steps
c [elim-12-1] backward subsumption/strengthening limit 68570478
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 10630780 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 302 = 1% variables out of 54417
c [bca-11] limit of 10000000 steps
c [bca-11] 74597 out of 108232 literals actually usable 69%
c [bca-11] added 50 blocked clauses in 192936 steps
c [simplification-12] removed 878 variables 1.6% (54115 remain 22%)
c [simplification-12] removed 5746 irredundant clauses 1.6% (346194 remain 25%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 13333 = 40000 / 3
c [simplification-12] new conflict interval 53333
c [simplification-12] penalized conflict interval 53333 = 1 * 53333
c [simplification-12] new conflict limit 185115
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  163.8   54114   346194    134271   20601   4450 637065   4 41.2 202.4   49
c i  163.8   54113   346194    134272   20601   4450 637065   4 41.2 202.3   49
c i  163.9   54109   346194    134513   20815   4460 637070   6 41.2 202.2   49
c i  164.2   54092   346194    135557   21705   4471 637073   8 41.4 202.3   50
c i  164.2   54091   346194    135743   21845   4471 637074   6 41.4 202.3   51
c i  164.9   54090   346194    137602   23471   4499 637106   5 41.6 202.6   52
c i  165.4   54087   346194    138548   24321   4518 637122   3 41.5 202.2   52
c i  167.0   54086   346194    142142   27380   4573 637176   7 41.7 201.1   53
c i  167.1   54085   346194    142450   27664   4576 637179   3 41.7 201.2   54
c i  167.7   54083   346194    143454   28511   4591 637193   5 41.7 200.9   56
c -  167.9   54082   346194    143733   19735   4600 637201   4 41.7 200.7   47
c i  168.0   54081   346194    143965   19953   4605 637203   4 41.7 200.6   48
c i  168.1   54074   346194    144064   20040   4612 637206   4 41.6 200.5   48
c i  168.3   54073   346194    144518   20438   4623 637217   5 41.6 200.6   48
c i  169.1   54071   346194    145971   21733   4645 637240   4 41.5 200.2   49
c i  169.1   54067   346194    145973   21734   4645 637240   4 41.5 200.2   49
c i  169.3   54064   346194    146190   21916   4654 637241   3 41.5 200.1   49
c i  169.3   54063   346194    146355   22063   4656 637242   5 41.5 200.0   49
c i  169.3   54062   346194    146356   22063   4656 637242   5 41.5 200.0   49
c i  169.3   54061   346194    146357   22063   4656 637242   5 41.5 200.0   49
c i  169.6   54060   346194    147070   22632   4670 637243   6 41.5 199.9   50
c i  170.5   54059   346194    151552   26108   4721 637270   4 42.1 200.0   53
c i  171.1   53982   346194    152739   27126   4748 637295   4 42.1 199.6   53
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  171.6   53981   346194    153848   28070   4765 637310   6 42.0 199.2   54
c i  172.0   53980   346194    154348   28523   4776 637321   3 42.0 198.9   55
c i  172.2   53979   346194    154688   28823   4781 637325   4 42.1 198.8   55
c i  172.2   53978   346194    154689   28823   4781 637325   4 42.1 198.8   55
c i  172.5   53977   346194    155257   29322   4795 637338   3 42.0 198.7   55
c i  172.7   53976   346194    155470   29517   4800 637341   4 42.0 198.6   55
c i  172.7   53972   346194    155558   29589   4805 637347   3 42.0 198.5   55
c i  172.9   53971   346194    156197   30082   4819 637369   4 42.0 198.5   55
c i  172.9   53970   346194    156198   30082   4819 637369   3 42.0 198.5   55
c i  172.9   53969   346194    156199   30082   4819 637369   2 42.0 198.5   55
c i  172.9   53968   346194    156200   30082   4819 637369   2 42.0 198.5   55
c i  172.9   53965   346194    156211   30091   4819 637369   2 42.0 198.4   55
c -  173.3   53963   346194    156997   21257   4832 637375   5 42.0 198.3   47
c i  173.7   53962   346194    157775   21923   4849 637397   5 41.9 198.1   49
c i  174.7   53961   346194    159596   23547   4882 637419   3 41.9 197.6   50
c i  175.2   53960   346194    160342   24176   4892 637439   4 41.9 197.3   50
c i  175.5   53959   346194    160926   24671   4900 637450   5 41.9 197.3   50
c i  175.6   53958   346194    161003   24731   4901 637451   5 41.9 197.3   50
c i  175.6   53957   346194    161004   24731   4901 637451   5 41.9 197.3   50
c i  175.9   53956   346194    162243   25843   4911 637472   5 42.0 197.5   52
c i  176.1   53951   346194    163096   26594   4920 637490   4 42.2 197.9   53
c i  176.1   53950   346194    163166   26638   4921 637490   4 42.2 197.8   53
c i  176.1   53949   346194    163174   26644   4921 637490   4 42.2 197.8   53
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  176.2   53948   346194    163412   26808   4922 637492   4 42.2 197.8   53
c i  176.8   53947   346194    164417   27703   4935 637523   3 42.2 197.6   53
c i  176.9   53946   346194    164505   27784   4936 637524   4 42.2 197.6   53
c i  177.5   53945   346194    165781   28929   4954 637541   5 42.1 197.3   54
c i  178.4   53944   346194    167249   30212   4978 637552   3 42.1 196.7   55
c i  178.9   53943   346194    168441   31254   4996 637559   4 42.0 196.6   56
c i  179.4   53942   346194    169219   31880   5019 637586   4 42.0 196.4   56
c i  179.6   53918   346194    169458   32100   5025 637587   4 42.0 196.3   56
c i  179.6   53916   346194    169581   32197   5026 637590   5 42.0 196.2   56
c i  179.7   53677   346194    169761   32366   5027 637591   3 42.0 196.1   56
c -  180.1   53630   346194    170277   22807   5033 637599   5 41.9 196.0   48
c i  180.3   53629   346194    170637   23132   5034 637600   4 42.0 195.9   49
c i  180.4   53628   346194    171010   23460   5036 637600   5 41.9 196.0   49
c i  180.5   53627   346194    171128   23554   5044 637610   3 41.9 195.9   49
c i  180.5   53477   346194    171136   23560   5045 637610   3 41.9 195.9   49
c i  181.8   53306   346194    174217   26042   5092 637656   6 42.5 195.7   51
c i  181.9   53305   346194    174231   26051   5092 637656   5 42.5 195.7   51
c i  182.1   53304   346194    175573   26924   5101 637658   7 42.8 195.6   52
c i  182.2   53303   346194    175911   27149   5103 637660   3 42.9 195.6   53
c i  182.9   53302   346194    178390   29097   5136 637672   5 43.5 195.9   55
c i  183.0   53301   346194    178812   29378   5137 637672   4 43.7 195.9   55
c i  183.0   53300   346194    178916   29431   5138 637672   5 43.7 195.9   55
c i  183.1   53299   346194    179211   29640   5141 637675   7 43.8 195.9   56
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  184.0   53298   346194    182981   32645   5185 637702   5 44.3 196.3   58
c i  184.0   53297   346194    182987   32650   5185 637702   5 44.3 196.3   58
c i  184.4   53294   346194    183486   33076   5197 637706   4 44.3 196.1   58
c i  184.6   53293   346194    183803   33365   5199 637707   5 44.3 196.0   58
c i  184.9   53292   346194    184195   33709   5207 637712   4 44.3 195.9   58
c i  184.9   53291   346194    184196   33709   5207 637712   4 44.3 195.9   58
c i  184.9   53290   346194    184197   33709   5207 637712   4 44.3 195.9   58
c i  184.9   53289   346194    184198   33709   5207 637712   4 44.3 195.9   58
c i  184.9   53288   346194    184199   33709   5207 637712   4 44.3 195.9   58
c i  184.9   53287   346194    184244   33748   5207 637712   5 44.3 195.8   58
c i  185.4   53284   346194    185314   34699   5219 637719   4 44.2 195.9   60
c -  185.5   53284   346194    185378   24251   5223 637725   3 44.2 195.8   48
c i  186.6   53283   346194    187242   25886   5265 637752   5 44.2 195.4   49
c i  186.6   53281   346194    187447   26061   5266 637756   5 44.2 195.4   50
c 
c [simplification-13] limit of 188135 conflicts hit after 188135 conflicts
c [ternres-11] limit 26036009 with penalty 0 = 0 + 0
c [ternres-11] all 53281 free variables schedulable
c [ternres-11] 117 ternary resolvents (0 bin, 117 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-22] removed 865 variables
c [lift-11] limit 15621605 with penalty 0 = 0 + 0
c [lift-11] using 44864 probes 84%
c [lift-11] 240 units, 86 impls, 16 eqs in 1 rounds
c [lift-11] 51486 variables remain 97% (1374 retained)
c [lift-11] removed 390 variables
c [cliff-11] limit of 20828807 steps penalty 0 = 0 + 0
c [cliff-11] failed 25, lifted 3
c [unhide-13] limit 5207201 with penalty 0 = 0 + 0
c [unhide-13-16] 1 units, 25 failed, 27030 tauts, 0 hbrs, 66096 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 237 transitive binary clauses
c [cce-11] limit of 52072019 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 85
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 84
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 83
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 82
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 81
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 80
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 79
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 78
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 77
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 76
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 75
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 74
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 73
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 72
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 71
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 70
c [cce-11-1] eliminated 2 clauses out of 4 (50%) of length 69
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 68
c [cce-11-1] eliminated 2 clauses out of 6 (33%) of length 67
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 66
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 65
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 64
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 63
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 62
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 61
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 60
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 59
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 58
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 57
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 56
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 55
c [cce-11-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 53
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 52
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 51
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 50
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 49
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 48
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 47
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 46
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 45
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 44
c [cce-11-1] eliminated 1 clauses out of 8 (12%) of length 43
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 42
c [cce-11-1] eliminated 1 clauses out of 10 (10%) of length 41
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 40
c [cce-11-1] eliminated 1 clauses out of 10 (10%) of length 39
c [cce-11-1] eliminated 2 clauses out of 10 (20%) of length 38
c [cce-11-1] eliminated 1 clauses out of 9 (11%) of length 37
c [cce-11-1] eliminated 2 clauses out of 12 (17%) of length 36
c [cce-11-1] eliminated 1 clauses out of 11 (9%) of length 35
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 34
c [cce-11-1] eliminated 1 clauses out of 10 (10%) of length 33
c [cce-11-1] eliminated 2 clauses out of 10 (20%) of length 32
c [cce-11-1] eliminated 1 clauses out of 13 (8%) of length 31
c [cce-11-1] eliminated 2 clauses out of 13 (15%) of length 30
c [cce-11-1] eliminated 1 clauses out of 13 (8%) of length 29
c [cce-11-1] eliminated 2 clauses out of 14 (14%) of length 28
c [cce-11-1] eliminated 1 clauses out of 12 (8%) of length 27
c [cce-11-1] eliminated 2 clauses out of 16 (12%) of length 26
c [cce-11-1] eliminated 1 clauses out of 9 (11%) of length 25
c [cce-11-1] eliminated 2 clauses out of 17 (12%) of length 24
c [cce-11-1] eliminated 1 clauses out of 12 (8%) of length 23
c [cce-11-1] eliminated 2 clauses out of 16 (12%) of length 22
c [cce-11-1] eliminated 1 clauses out of 11 (9%) of length 21
c [cce-11-1] eliminated 4 clauses out of 17 (24%) of length 20
c [cce-11-1] eliminated 2 clauses out of 17 (12%) of length 19
c [cce-11-1] eliminated 3 clauses out of 16 (19%) of length 18
c [cce-11-1] eliminated 3 clauses out of 19 (16%) of length 17
c [cce-11-1] eliminated 3 clauses out of 18 (17%) of length 16
c [cce-11-1] eliminated 5 clauses out of 19 (26%) of length 15
c [cce-11-1] eliminated 5 clauses out of 22 (23%) of length 14
c [cce-11-1] eliminated 4 clauses out of 24 (17%) of length 13
c [cce-11-1] eliminated 9 clauses out of 23 (39%) of length 12
c [cce-11-1] eliminated 9 clauses out of 28 (32%) of length 11
c [cce-11-1] eliminated 10 clauses out of 84 (12%) of length 10
c [cce-11-1] eliminated 8 clauses out of 309 (3%) of length 9
c [cce-11-1] eliminated 10 clauses out of 305 (3%) of length 8
c [cce-11-1] eliminated 11 clauses out of 407 (3%) of length 7
c [cce-11-1] eliminated 53 clauses out of 2557 (2%) of length 6
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 236 large clauses in 52072020 steps
c [cce-11-1] allowing another 26036010 steps for small clauses
c [cce-11] scheduling 201769 clauses = 184809 binary + 16960 ternary
c [cce-11] tried to eliminate 1513 small clauses 1%
c [cce-11] eliminated 349 small clauses 0%
c [cce-11] eliminated 293 binary clauses 0%
c [cce-11] eliminated 56 ternary clauses 0%
c [cce-11-1] eliminated 413 small clauses in 52072020 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 649 covered clauses in round 1
c [cce-11] eliminated 649 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 52815 variables 100%
c [elim-13] limit of 520720192 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 506 variables 1% in round 1 in 31631642 steps
c [elim-13-1] backward subsumption/strengthening limit 63263284
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 9813246 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 506 = 1% variables out of 52815
c [bca-12] limit of 10000000 steps
c [bca-12] 67839 out of 104620 literals actually usable 65%
c [bca-12] added 56 blocked clauses in 178972 steps
c [simplification-13] removed 972 variables 1.8% (52309 remain 21%)
c [simplification-13] removed 21150 irredundant clauses 6.1% (325044 remain 24%)
c [simplification-13] maximum reduction of 6% = max (2%, 6%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] new conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] new conflict limit 190135
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  195.1   52308   325044    188742   24079   5211 681957   5 44.1 195.1   50
c i  195.5   52305   325044    189638   24870   5224 681982   4 44.1 194.8   50
c i  195.8   52304   325044    190183   25375   5233 681988   6 44.0 194.6   51
c 
c [simplification-14] limit of 190259 conflicts hit after 190259 conflicts
c [ternres-12] limit 26292142 with penalty 0 = 0 + 0
c [ternres-12] all 52304 free variables schedulable
c [ternres-12] 98 ternary resolvents (0 bin, 98 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-23] removed 5 variables
c [treelook-5] limit 657303 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 57866 literals 55%
c [treelook-5] scheduling used 657311 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 657303 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 657730 steps
c [treelook-5] 57843 literals remain 55%
c [treelook-5] 7797 variables remain to probed next time 15%
c [treelook-5] removed 6 variables, found 3096 hbrs
c [lift-12] limit 15775285 with penalty 0 = 0 + 0
c [lift-12] using 43866 probes 84%
c [lift-12] 135 units, 117 impls, 2 eqs in 1 rounds
c [lift-12] 50267 variables remain 97% (1740 retained)
c [lift-12] removed 291 variables
c [cliff-12] limit of 21033714 steps penalty 0 = 0 + 0
c [cliff-12] failed 20, lifted 4
c [unhide-14] limit 5258428 with penalty 0 = 0 + 0
c [unhide-14-18] 1 units, 33 failed, 18584 tauts, 0 hbrs, 36520 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 114 transitive binary clauses
c [cce-12] limit of 52584285 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 113
c [cce-12-1] eliminated 1 clauses out of 4 (25%) of length 112
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 111
c [cce-12-1] eliminated 1 clauses out of 5 (20%) of length 110
c [cce-12-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-12-1] eliminated 1 clauses out of 4 (25%) of length 108
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 107
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 106
c [cce-12-1] eliminated 2 clauses out of 4 (50%) of length 105
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 104
c [cce-12-1] eliminated 2 clauses out of 4 (50%) of length 103
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 102
c [cce-12-1] eliminated 2 clauses out of 5 (40%) of length 101
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 100
c [cce-12-1] eliminated 2 clauses out of 4 (50%) of length 99
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 98
c [cce-12-1] eliminated 2 clauses out of 4 (50%) of length 97
c [cce-12-1] eliminated 1 clauses out of 5 (20%) of length 96
c [cce-12-1] eliminated 2 clauses out of 2 (100%) of length 95
c [cce-12-1] eliminated 1 clauses out of 5 (20%) of length 94
c [cce-12-1] eliminated 2 clauses out of 2 (100%) of length 93
c [cce-12-1] eliminated 1 clauses out of 6 (17%) of length 92
c [cce-12-1] eliminated 2 clauses out of 2 (100%) of length 91
c [cce-12-1] eliminated 1 clauses out of 6 (17%) of length 90
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 89
c [cce-12-1] eliminated 1 clauses out of 6 (17%) of length 88
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 87
c [cce-12-1] eliminated 1 clauses out of 5 (20%) of length 86
c [cce-12-1] eliminated 1 clauses out of 21 (5%) of length 13
c [cce-12-1] eliminated 3 clauses out of 71 (4%) of length 10
c [cce-12-1] eliminated 1 clauses out of 290 (0%) of length 9
c [cce-12-1] eliminated 3 clauses out of 291 (1%) of length 8
c [cce-12-1] eliminated 2 clauses out of 380 (1%) of length 7
c [cce-12-1] eliminated 17 clauses out of 2497 (1%) of length 6
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 69 large clauses in 52584286 steps
c [cce-12-1] allowing another 26292143 steps for small clauses
c [cce-12] scheduling 254682 clauses = 180858 binary + 73824 ternary
c [cce-12] tried to eliminate 1681 small clauses 1%
c [cce-12] eliminated 399 small clauses 0%
c [cce-12] eliminated 276 binary clauses 0%
c [cce-12] eliminated 123 ternary clauses 0%
c [cce-12-1] eliminated 447 small clauses in 52584286 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 516 covered clauses in round 1
c [cce-12] eliminated 516 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 51958 variables 100%
c [elim-14] limit of 525842852 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 181 variables 0% in round 1 in 29299920 steps
c [elim-14-1] backward subsumption/strengthening limit 58599840
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 9568188 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 181 = 0% variables out of 51958
c [bca-13] limit of 10000000 steps
c [bca-13] 66394 out of 103556 literals actually usable 64%
c [bca-13] added 52 blocked clauses in 177124 steps
c [simplification-14] removed 527 variables 1.0% (51777 remain 21%)
c [simplification-14] removed 5846 irredundant clauses 1.8% (319198 remain 23%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 17777 = 53333 / 3
c [simplification-14] new conflict interval 71110
c [simplification-14] penalized conflict interval 71110 = 1 * 71110
c [simplification-14] new conflict limit 261369
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  205.2   51776   319198    194474   28399   5422 704458   4 44.1 193.9   54
c i  205.4   51775   319198    195017   28868   5428 704465   4 44.1 193.8   54
c i  205.5   51774   319198    195088   28930   5429 704465   4 44.1 193.9   54
c i  206.6   51771   319198    197210   30750   5451 704498   4 44.1 193.4   54
c i  206.7   51770   319198    197296   30820   5452 704506   4 44.1 193.4   54
c i  207.3   51769   319198    198425   31797   5466 704514   4 44.1 193.2   55
c i  207.5   51768   319198    198798   32114   5470 704524   3 44.1 193.0   56
c i  208.1   51767   319198    200486   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51766   319198    200487   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51765   319198    200488   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51764   319198    200489   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51763   319198    200490   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51762   319198    200491   33407   5502 704552   4 44.3 193.0   57
c i  208.1   51761   319198    200492   33407   5502 704552   4 44.3 193.0   57
c i  208.2   51760   319198    200589   33490   5502 704554   6 44.3 192.9   57
c i  209.0   51739   319198    202243   34930   5537 704575   5 44.3 192.7   59
c i  209.0   51738   319198    202245   34931   5537 704575   5 44.3 192.7   59
c i  209.0   51737   319198    202246   34931   5537 704575   5 44.3 192.7   59
c i  209.0   51736   319198    202247   34931   5537 704575   5 44.3 192.7   59
c i  209.0   51735   319198    202248   34931   5537 704575   5 44.3 192.7   59
c i  209.2   51734   319198    202656   35289   5551 704579   5 44.3 192.7   59
c -  209.4   51734   319198    202927   24533   5559 704584   4 44.2 192.6   49
c i  209.5   51733   319198    203107   24699   5561 704586   5 44.2 192.6   50
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  209.9   51732   319198    203911   25424   5576 704597   4 44.1 192.3   50
c i  210.7   51731   319198    206377   27307   5600 704616   4 44.5 192.1   52
c i  210.9   51730   319198    207271   27882   5611 704622   7 44.6 192.1   53
c i  211.0   51729   319198    207593   28144   5615 704622   8 44.7 192.1   53
c i  211.1   51728   319198    208263   28644   5622 704622   6 44.8 192.1   53
c i  211.2   51726   319198    208709   29004   5625 704624   6 44.8 192.1   53
c i  212.6   51725   319198    211505   31372   5670 704652   4 44.8 191.5   55
c i  212.6   51724   319198    211621   31459   5671 704654   3 44.8 191.5   55
c i  212.7   51723   319198    211830   31651   5673 704658   4 44.8 191.4   55
c i  213.8   51722   319198    213724   33249   5696 704673   4 44.8 191.0   56
c -  216.5   51722   319198    219175   26261   5785 704741   4 44.9 190.0   49
c i  216.6   51721   319198    219824   26778   5789 704744   8 45.1 190.1   50
c i  217.1   51720   319198    221238   27960   5798 704758   4 45.5 190.7   52
c i  217.1   51717   319198    221377   28089   5803 704761   5 45.5 190.6   52
c i  217.3   51716   319198    221652   28338   5809 704765   6 45.5 190.5   52
c i  218.1   51714   319198    222859   29332   5833 704795   3 45.4 190.1   53
c i  219.8   51713   319198    226611   32489   5884 704847   4 45.4 189.5   54
c i  221.9   51712   319198    230379   35718   5941 704909   4 45.4 188.7   57
c i  222.4   51711   319198    231380   36498   5952 704915   4 45.6 188.6   58
c i  222.5   51710   319198    231584   36631   5954 704919   3 45.6 188.6   59
c i  222.9   51709   319198    232906   37560   5964 704929   2 45.8 188.6   59
c i  222.9   51708   319198    232997   37648   5964 704929   4 45.8 188.6   59
c i  223.1   51707   319198    233910   38373   5968 704943   7 45.9 188.7   61
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  223.3   51706   319198    234254   38637   5971 704946   5 46.0 188.7   61
c -  223.7   51706   319198    235800   27862   5977 704953   3 46.6 189.0   49
c i  225.0   51705   319198    242105   32560   6019 704980   4 48.2 189.6   56
c i  225.9   51704   319198    245939   35331   6041 705000   8 48.7 189.7   59
c i  226.4   51703   319198    247479   36357   6062 705002   4 49.1 189.8   61
c i  226.5   51702   319198    247550   36420   6062 705003   4 49.1 189.8   61
c i  227.1   51701   319198    250241   38590   6082 705037   7 49.7 190.3   64
c -  228.0   51701   319198    254285   29055   6104 705050   9 50.6 190.6   49
c i  228.3   51700   319198    255620   30206   6109 705060   5 50.7 190.8   51
c i  228.3   51699   319198    255927   30377   6109 705060   4 50.8 190.8   51
c i  228.4   51698   319198    256101   30504   6112 705061   4 50.8 190.8   51
c i  228.4   51697   319198    256369   30718   6114 705061   6 50.8 190.8   52
c i  228.5   51696   319198    256751   30969   6116 705062   5 50.9 190.8   52
c i  228.7   51695   319198    257172   31261   6118 705064   5 50.9 190.7   52
c i  228.9   51694   319198    258087   31970   6125 705078   4 51.0 190.8   53
c i  228.9   51693   319198    258088   31970   6125 705078   2 51.0 190.8   53
c i  228.9   51692   319198    258178   32028   6126 705078   3 51.1 190.8   53
c i  229.1   51691   319198    258798   32548   6129 705086   9 51.2 190.9   53
c i  229.2   51690   319198    258924   32626   6134 705089   6 51.2 190.9   53
c i  229.8   51689   319198    261467   34554   6140 705101   5 52.4 191.6   58
c i  229.8   51688   319198    261604   34679   6140 705103   4 52.4 191.6   58
c 
c [simplification-15] limit of 264009 conflicts hit after 264009 conflicts
c [ternres-13] limit 33223841 with penalty 0 = 0 + 0
c [ternres-13] all 51688 free variables schedulable
c [ternres-13] 152 ternary resolvents (0 bin, 152 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1038245 penalty 4 = 4 + 0
c [card-5] found 13406 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1038245 for elimination
c [card-5] 13406 out of 13406 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-25] removed 93 variables
c [basicprobe-5] limit 33223841 penalty 0 = 0 + 0
c [basicprobe-5-0] 14456 probes remain 28% after last round
c [basicprobe-5-0] 333 units = 333 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 412 variables, found 213700 hbrs
c [bate-4] eliminated 165 asymmetric tautologies during probing
c [cgrclsr-9] limit 830596 penalty 2 = 2 + 0
c [cgrclsr-9] all 51272 free variables schedulable
c [cgrclsr-9] fully completed congruence closure
c [lift-13] limit 19934304 with penalty 0 = 0 + 0
c [lift-13] using 42883 probes 84%
c [lift-13] 83 units, 152 impls, 7 eqs in 1 rounds
c [lift-13] 48848 variables remain 96% (2267 retained)
c [lift-13] removed 157 variables
c [cliff-13] limit of 26579073 steps penalty 0 = 0 + 0
c [cliff-13] failed 38, lifted 10
c [unhide-15] limit 6644768 with penalty 0 = 0 + 0
c [unhide-15-20] 1 units, 62 failed, 30678 tauts, 0 hbrs, 307484 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 108 transitive binary clauses
c [cce-13] limit of 66447682 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2 clauses out of 15 (13%) of length 20
c [cce-13-1] eliminated 1 clauses out of 12 (8%) of length 19
c [cce-13-1] eliminated 2 clauses out of 19 (11%) of length 18
c [cce-13-1] eliminated 1 clauses out of 16 (6%) of length 17
c [cce-13-1] eliminated 4 clauses out of 22 (18%) of length 16
c [cce-13-1] eliminated 1 clauses out of 13 (8%) of length 15
c [cce-13-1] eliminated 3 clauses out of 21 (14%) of length 14
c [cce-13-1] eliminated 1 clauses out of 21 (5%) of length 13
c [cce-13-1] eliminated 2 clauses out of 18 (11%) of length 12
c [cce-13-1] eliminated 1 clauses out of 22 (5%) of length 11
c [cce-13-1] eliminated 3 clauses out of 62 (5%) of length 10
c [cce-13-1] eliminated 1 clauses out of 233 (0%) of length 9
c [cce-13-1] eliminated 5 clauses out of 280 (2%) of length 8
c [cce-13-1] eliminated 2 clauses out of 378 (1%) of length 7
c [cce-13-1] eliminated 8 clauses out of 2510 (0%) of length 6
c [cce-13-1] eliminated 1693 clauses out of 17502 (10%) of length 5
c [cce-13-1] incomplete large round (ACCE)
c [cce-13-1] eliminated 1730 large clauses in 66447683 steps
c [cce-13-1] allowing another 33223841 steps for small clauses
c [cce-13] scheduling 193724 clauses = 176956 binary + 16768 ternary
c [cce-13] tried to eliminate 2115 small clauses 1%
c [cce-13] eliminated 494 small clauses 0%
c [cce-13] eliminated 419 binary clauses 0%
c [cce-13] eliminated 75 ternary clauses 0%
c [cce-13-1] eliminated 654 small clauses in 66447683 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 2384 covered clauses in round 1
c [cce-13] eliminated 2384 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 51015 variables 100%
c [elim-15] limit of 664476825 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 1707 variables 3% in round 1 in 30823740 steps
c [elim-15-1] backward subsumption/strengthening limit 61647480
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 9227339 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 1707 = 3% variables out of 51015
c [bca-14] limit of 10000000 steps
c [bca-14] 62317 out of 98618 literals actually usable 63%
c [bca-14] added 88 blocked clauses in 171891 steps
c [rephase-4] after 264009 conflicts (new increment 160000, next 424009)
c [flushphases] 0 phases reset
c [simplification-15] removed 2380 variables 4.6% (49308 remain 20%)
c [simplification-15] removed 13011 irredundant clauses 4.1% (306187 remain 22%)
c [simplification-15] maximum reduction of 5% = max (5%, 4%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] new conflict interval 2640 = min (264009/100, 71110)
c [simplification-15] penalized conflict interval 2640 = 1 * 2640
c [simplification-15] new conflict limit 266649
c [tabula-rasa-2] number clauses 306187 drops below limit 314771
c [flush-cache] 0 binary, 0 ternary, 26915 large
c [flushphases] 49308 phases reset fully
c [phase-8] phase bias: 2714 positive 26%, 7650 negative 74%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] conflict limit 20000 does not change
c [tabula-rasa-2] new variable limit 12327 and clause limit 153093
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  244.0   49307   306187    264536     485   6124 899579   5 52.3 192.1   48
c i  244.2   49306   306187    264983     899   6137 899584   4 52.3 192.3   49
c i  244.3   49305   306187    265778    1604   6157 899592   8 52.2 192.3   49
c i  244.4   49304   306187    266222    2001   6169 899599   5 52.1 192.3   49
c i  244.4   49303   306187    266367    2127   6174 899601   5 52.1 192.3   49
c i  244.4   49302   306187    266371    2130   6174 899601   5 52.1 192.3   49
c 
c [simplification-16] limit of 266841 conflicts hit after 266842 conflicts
c [ternres-14] limit 33409206 with penalty 0 = 0 + 0
c [ternres-14] all 49302 free variables schedulable
c [ternres-14] 211 ternary resolvents (0 bin, 211 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-26] removed 7 variables
c [simpleprobe-6] all 49301 free variables schedulable
c [simpleprobe-6] limit 133636824 penalty 0 = 0 + 0
c [decomp-27] removed 87 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 87 variables, found 78873 hbrs, 74 units
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 41640 probes 85%
c [lift-14] 92 units, 110 impls, 0 eqs in 1 rounds
c [lift-14] 46295 variables remain 94% (2796 retained)
c [lift-14] removed 123 variables
c [cliff-14] limit of 26727364 steps penalty 0 = 0 + 0
c [cliff-14] failed 28, lifted 5
c [unhide-16] limit 6681841 with penalty 0 = 0 + 0
c [unhide-16-23] 1 units, 37 failed, 69270 tauts, 0 hbrs, 16493 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 83 transitive binary clauses
c [cce-14] limit of 66818412 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 3 (33%) of length 104
c [cce-14-1] eliminated 2 clauses out of 4 (50%) of length 103
c [cce-14-1] eliminated 1 clauses out of 4 (25%) of length 102
c [cce-14-1] eliminated 2 clauses out of 5 (40%) of length 101
c [cce-14-1] eliminated 1 clauses out of 15 (7%) of length 19
c [cce-14-1] eliminated 2 clauses out of 16 (12%) of length 18
c [cce-14-1] eliminated 4 clauses out of 25 (16%) of length 17
c [cce-14-1] eliminated 2 clauses out of 14 (14%) of length 16
c [cce-14-1] eliminated 2 clauses out of 21 (10%) of length 15
c [cce-14-1] eliminated 1 clauses out of 8 (12%) of length 14
c [cce-14-1] eliminated 3 clauses out of 27 (11%) of length 13
c [cce-14-1] eliminated 3 clauses out of 20 (15%) of length 12
c [cce-14-1] eliminated 3 clauses out of 23 (13%) of length 11
c [cce-14-1] eliminated 3 clauses out of 55 (5%) of length 10
c [cce-14-1] eliminated 4 clauses out of 172 (2%) of length 9
c [cce-14-1] eliminated 2 clauses out of 201 (1%) of length 8
c [cce-14-1] eliminated 6 clauses out of 289 (2%) of length 7
c [cce-14-1] eliminated 16 clauses out of 2615 (1%) of length 6
c [cce-14-1] eliminated 2049 clauses out of 15712 (13%) of length 5
c [cce-14-1] incomplete large round (ACCE)
c [cce-14-1] eliminated 2107 large clauses in 66818413 steps
c [cce-14-1] allowing another 33409206 steps for small clauses
c [cce-14] scheduling 240394 clauses = 170514 binary + 69880 ternary
c [cce-14] tried to eliminate 2103 small clauses 1%
c [cce-14] eliminated 421 small clauses 0%
c [cce-14] eliminated 298 binary clauses 0%
c [cce-14] eliminated 123 ternary clauses 0%
c [cce-14-1] eliminated 459 small clauses in 66818413 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 2566 covered clauses in round 1
c [cce-14] eliminated 2566 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 49041 variables 100%
c [elim-16] limit of 668184120 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 1648 variables 3% in round 1 in 28693915 steps
c [elim-16-1] backward subsumption/strengthening limit 57387830
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 8958516 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 1648 = 3% variables out of 49041
c [bca-15] limit of 10000000 steps
c [bca-15] 86930 out of 94788 literals actually usable 92%
c [bca-15] added 191 blocked clauses in 209870 steps
c [rephase-5] after 266842 conflicts (new increment 20000, next 286842)
c [flushphases] 1293 phases reset
c [phase-9] phase bias: 17 positive 68%, 8 negative 32%
c [simplification-16] removed 1909 variables 3.9% (47393 remain 19%)
c [simplification-16] removed 9292 irredundant clauses 3.0% (296895 remain 22%)
c [simplification-16] maximum reduction of 4% = max (4%, 3%)
c [simplification-16] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-16] new conflict interval 24000
c [simplification-16] penalized conflict interval 24000 = 1 * 24000
c [simplification-16] new conflict limit 290842
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  256.2   47392   296895    269688    3953   6036 963715   7 52.3 192.5   51
c -  256.3   47392   296895    270492    2657   6051 963717   7 52.4 192.5   49
c R  256.4   47392   296895    271566    3642   6060 963724   6 52.4 192.6   50
c i  256.5   47391   296895    271769    3830   6068 963728   4 52.3 192.5   50
c i  256.7   47390   296895    272236    4243   6085 963737   5 52.3 192.3   50
c i  257.0   47389   296895    273060    5006   6111 963745   5 52.2 192.2   50
c i  257.0   47388   296895    273061    5006   6111 963745   5 52.2 192.2   50
c -  257.5   47388   296895    274461    3746   6151 963768   5 52.0 191.9   49
c i  257.8   47387   296895    275165    4379   6171 963791   4 51.9 191.7   49
c i  258.8   47386   296895    278010    6899   6242 963843   5 51.7 191.2   51
c -  259.1   47386   296895    279143    4875   6267 963854   9 51.6 191.1   49
c i  259.2   47385   296895    279218    4947   6267 963854   7 51.6 191.0   49
c i  259.2   47384   296895    279219    4947   6267 963854   7 51.6 191.0   49
c i  259.2   47383   296895    279391    5102   6270 963857   6 51.6 191.0   49
c i  259.6   47382   296895    280381    5976   6288 963867   4 51.5 190.7   50
c i  260.2   47381   296895    282289    7508   6321 963877   5 51.6 190.8   51
c i  260.5   47380   296895    283660    8695   6339 963883   4 51.7 190.9   52
c i  260.8   47379   296895    284085    9080   6346 963885   5 51.7 190.7   52
c -  260.9   47379   296895    284421    5835   6353 963888   7 51.7 190.7   49
c i  261.4   47378   296895    285843    7114   6392 963904   5 51.5 190.5   50
c i  261.5   47374   296895    286334    7515   6406 963909   5 51.5 190.4   50
c i  261.5   47361   296895    286362    7532   6406 963909   5 51.5 190.4   51
c i  261.5   47360   296895    286363    7532   6406 963909   5 51.5 190.4   51
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  261.5   47359   296895    286364    7532   6406 963909   5 51.5 190.4   51
c i  261.5   47358   296895    286488    7615   6409 963910   5 51.5 190.3   51
c i  261.5   47357   296895    286550    7635   6412 963914   5 51.5 190.3   51
c i  261.5   47126   296895    286632    7701   6416 963915   5 51.5 190.3   51
c i  262.5   47125   296895    289111    9837   6451 963949   5 51.3 189.9   52
c i  262.5   47124   296895    289112    9837   6451 963949   5 51.3 189.9   52
c -  263.0   47124   296895    290323    6904   6490 963974   5 51.2 189.6   49
c i  263.3   47123   296895    291331    7734   6526 963991   5 51.1 189.4   50
c 
c [simplification-17] limit of 291958 conflicts hit after 291958 conflicts
c [ternres-15] limit 35623781 with penalty 0 = 0 + 0
c [ternres-15] all 47123 free variables schedulable
c [ternres-15] 107 ternary resolvents (0 bin, 107 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 445297 penalty 4 = 4 + 0
c [gauss-5] extracted 8 xors of average arity 2.9
c [gauss-5] connected 23 occurrences of 23 variables (average 1.0)
c [gauss-5] limit 445297 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 17 variables
c [treelook-6] limit 1781189 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 60958 literals 65%
c [treelook-6] scheduling used 1464397 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1781189 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1848339 steps
c [treelook-6] 60914 literals remain 65%
c [treelook-6] 6356 variables remain to probed next time 13%
c [treelook-6] removed 0 variables, found 11264 hbrs
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 40455 probes 86%
c [lift-15] 61 units, 114 impls, 2 eqs in 1 rounds
c [lift-15] 43685 variables remain 93% (3314 retained)
c [lift-15] removed 107 variables
c [cliff-15] limit of 28499024 steps penalty 0 = 0 + 0
c [cliff-15] failed 28, lifted 16
c [unhide-17] limit 7124756 with penalty 0 = 0 + 0
c [unhide-17-26] 10 units, 33 failed, 23608 tauts, 0 hbrs, 26778 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 78 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 46918 variables 100%
c [block-6] limit of 22264863 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 6 blocked clauses
c [block-6] 6 < 1/1000 * 291265 = 291 considered unsuccessful
c [cce-15] limit of 71247562 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 1 clauses out of 4 (25%) of length 91
c [cce-15-1] eliminated 2 clauses out of 4 (50%) of length 90
c [cce-15-1] eliminated 2 clauses out of 7 (29%) of length 89
c [cce-15-1] eliminated 1 clauses out of 3 (33%) of length 88
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 45
c [cce-15-1] eliminated 1 clauses out of 11 (9%) of length 44
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 43
c [cce-15-1] eliminated 1 clauses out of 10 (10%) of length 42
c [cce-15-1] eliminated 2 clauses out of 7 (29%) of length 41
c [cce-15-1] eliminated 1 clauses out of 9 (11%) of length 40
c [cce-15-1] eliminated 2 clauses out of 10 (20%) of length 39
c [cce-15-1] eliminated 1 clauses out of 12 (8%) of length 38
c [cce-15-1] eliminated 2 clauses out of 10 (20%) of length 37
c [cce-15-1] eliminated 1 clauses out of 13 (8%) of length 36
c [cce-15-1] eliminated 2 clauses out of 9 (22%) of length 35
c [cce-15-1] eliminated 1 clauses out of 13 (8%) of length 34
c [cce-15-1] eliminated 2 clauses out of 10 (20%) of length 33
c [cce-15-1] eliminated 3 clauses out of 13 (23%) of length 32
c [cce-15-1] eliminated 5 clauses out of 13 (38%) of length 31
c [cce-15-1] eliminated 4 clauses out of 16 (25%) of length 30
c [cce-15-1] eliminated 4 clauses out of 14 (29%) of length 29
c [cce-15-1] eliminated 3 clauses out of 12 (25%) of length 28
c [cce-15-1] eliminated 3 clauses out of 17 (18%) of length 27
c [cce-15-1] eliminated 5 clauses out of 18 (28%) of length 26
c [cce-15-1] eliminated 4 clauses out of 19 (21%) of length 25
c [cce-15-1] eliminated 5 clauses out of 16 (31%) of length 24
c [cce-15-1] eliminated 3 clauses out of 14 (21%) of length 23
c [cce-15-1] eliminated 2 clauses out of 19 (11%) of length 22
c [cce-15-1] eliminated 4 clauses out of 15 (27%) of length 21
c [cce-15-1] eliminated 1 clauses out of 16 (6%) of length 20
c [cce-15-1] eliminated 2 clauses out of 15 (13%) of length 19
c [cce-15-1] eliminated 1 clauses out of 14 (7%) of length 18
c [cce-15-1] eliminated 2 clauses out of 22 (9%) of length 17
c [cce-15-1] eliminated 1 clauses out of 15 (7%) of length 16
c [cce-15-1] eliminated 2 clauses out of 21 (10%) of length 15
c [cce-15-1] eliminated 3 clauses out of 15 (20%) of length 14
c [cce-15-1] eliminated 5 clauses out of 27 (19%) of length 13
c [cce-15-1] eliminated 4 clauses out of 20 (20%) of length 12
c [cce-15-1] eliminated 3 clauses out of 26 (12%) of length 11
c [cce-15-1] eliminated 6 clauses out of 48 (12%) of length 10
c [cce-15-1] eliminated 3 clauses out of 116 (3%) of length 9
c [cce-15-1] eliminated 3 clauses out of 124 (2%) of length 8
c [cce-15-1] eliminated 4 clauses out of 172 (2%) of length 7
c [cce-15-1] eliminated 5 clauses out of 2610 (0%) of length 6
c [cce-15-1] eliminated 2865 clauses out of 13301 (22%) of length 5
c [cce-15-1] incomplete large round (ACCE)
c [cce-15-1] eliminated 2981 large clauses in 71247563 steps
c [cce-15-1] allowing another 35623781 steps for small clauses
c [cce-15] scheduling 179554 clauses = 162796 binary + 16758 ternary
c [cce-15] tried to eliminate 2327 small clauses 1%
c [cce-15] eliminated 521 small clauses 0%
c [cce-15] eliminated 415 binary clauses 0%
c [cce-15] eliminated 106 ternary clauses 1%
c [cce-15-1] eliminated 521 small clauses in 71247563 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 3502 covered clauses in round 1
c [cce-15] eliminated 3502 covered clauses in TOTAL during 1 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 46917 variables 100%
c [elim-17] limit of 712475622 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 2399 variables 5% in round 1 in 27552779 steps
c [elim-17-1] backward subsumption/strengthening limit 55105558
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 8450003 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 2399 = 5% variables out of 46917
c [bca-16] limit of 10000000 steps
c [bca-16] 74993 out of 89038 literals actually usable 84%
c [bca-16] added 41 blocked clauses in 175573 steps
c [rephase-6] after 291958 conflicts (new increment 40000, next 331958)
c [flushphases] 627 phases reset
c [phase-10] phase bias: 0 positive 0%, 6 negative 100%
c [simplification-17] removed 2605 variables 5.5% (44518 remain 18%)
c [simplification-17] removed 14847 irredundant clauses 5.0% (282048 remain 20%)
c [simplification-17] maximum reduction of 6% = max (6%, 5%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] new conflict interval 2919 = min (291958/100, 24000)
c [simplification-17] penalized conflict interval 2919 = 1 * 2919
c [simplification-17] new conflict limit 294877
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  274.3   44517   282048    294040    7185   6196 953639   3 50.9 189.1   49
c i  274.3   44438   282048    294071    7212   6197 953639   4 50.9 189.1   49
c 
c [simplification-18] limit of 295001 conflicts hit after 295003 conflicts
c [ternres-16] limit 35866586 with penalty 0 = 0 + 0
c [ternres-16] all 44434 free variables schedulable
c [ternres-16] 181 ternary resolvents (0 bin, 181 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-30] removed 91 variables
c [basicprobe-6] limit 35866586 penalty 0 = 0 + 0
c [basicprobe-6-0] 9845 probes remain 22% after last round
c [basicprobe-6-0] 186 units = 185 failed (99%) + 1 lifted (1%)
c [basicprobe-6-0] removed 443 variables, found 204823 hbrs
c [bate-5] eliminated 194 asymmetric tautologies during probing
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 38662 probes 88%
c [lift-16] 67 units, 101 impls, 2 eqs in 1 rounds
c [lift-16] 39999 variables remain 91% (3824 retained)
c [lift-16] removed 161 variables
c [cliff-16] limit of 28693269 steps penalty 0 = 0 + 0
c [cliff-16] failed 7, lifted 5
c [unhide-18] limit 7173317 with penalty 0 = 0 + 0
c [unhide-18-29] 2 units, 19 failed, 43284 tauts, 0 hbrs, 37425 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 14 transitive binary clauses
c [cce-16] limit of 71733173 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 2 clauses out of 5 (40%) of length 85
c [cce-16-1] eliminated 1 clauses out of 4 (25%) of length 84
c [cce-16-1] eliminated 2 clauses out of 5 (40%) of length 83
c [cce-16-1] eliminated 1 clauses out of 4 (25%) of length 82
c [cce-16-1] eliminated 2 clauses out of 5 (40%) of length 81
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 80
c [cce-16-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-16-1] eliminated 2 clauses out of 18 (11%) of length 20
c [cce-16-1] eliminated 1 clauses out of 14 (7%) of length 19
c [cce-16-1] eliminated 3 clauses out of 19 (16%) of length 18
c [cce-16-1] eliminated 1 clauses out of 18 (6%) of length 17
c [cce-16-1] eliminated 2 clauses out of 18 (11%) of length 16
c [cce-16-1] eliminated 1 clauses out of 19 (5%) of length 15
c [cce-16-1] eliminated 2 clauses out of 23 (9%) of length 10
c [cce-16-1] eliminated 5 clauses out of 70 (7%) of length 7
c [cce-16-1] eliminated 9 clauses out of 2751 (0%) of length 6
c [cce-16-1] eliminated 1284 clauses out of 10197 (13%) of length 5
c [cce-16-1] incomplete large round (ACCE)
c [cce-16-1] eliminated 1321 large clauses in 71733174 steps
c [cce-16-1] allowing another 35866587 steps for small clauses
c [cce-16] scheduling 170907 clauses = 154380 binary + 16527 ternary
c [cce-16] tried to eliminate 2406 small clauses 1%
c [cce-16] eliminated 566 small clauses 0%
c [cce-16] eliminated 484 binary clauses 0%
c [cce-16] eliminated 82 ternary clauses 0%
c [cce-16-1] eliminated 590 small clauses in 71733174 steps
c [cce-16-1] incomplete small round (ACCE)
c [cce-16-1] eliminated 1911 covered clauses in round 1
c [cce-16] eliminated 1911 covered clauses in TOTAL during 1 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 43785 variables 100%
c [elim-18] limit of 717331738 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 482 variables 1% in round 1 in 26204645 steps
c [elim-18-1] backward subsumption/strengthening limit 52409290
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 7960762 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 482 = 1% variables out of 43785
c [bca-17] limit of 10000000 steps
c [bca-17] 68614 out of 86608 literals actually usable 79%
c [bca-17] added 55 blocked clauses in 159493 steps
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-18] removed 1131 variables 2.5% (43303 remain 18%)
c [simplification-18] removed 11087 irredundant clauses 3.9% (270961 remain 20%)
c [simplification-18] maximum reduction of 4% = max (3%, 4%)
c [simplification-18] geometric conflict interval increment 4800 = 24000 / 5
c [simplification-18] new conflict interval 28800
c [simplification-18] penalized conflict interval 28800 = 1 * 28800
c [simplification-18] new conflict limit 323803
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  287.9   43302   270961    299787   11205   6326 1098815   4 50.7 189.4   55
c i  288.2   43301   270961    300501   11844   6347 1098833   5 50.7 189.3   56
c -  288.4   43294   270961    300818    7626   6352 1098844   4 50.7 189.2   51
c -  290.9   43294   270961    307928    9010   6493 1098951   7 50.1 188.2   51
c i  293.3   43293   270961    315642   15603   6634 1099017   7 49.6 187.0   56
c -  293.3   43293   270961    315854   10316   6635 1099017   5 49.6 187.0   52
c i  293.9   43292   270961    317309   11663   6656 1099028   5 49.5 186.9   53
c -  295.7   43263   270961    323961   11542   6717 1099071   6 50.3 189.2   52
c 
c [simplification-19] limit of 324495 conflicts hit after 324495 conflicts
c [ternres-17] limit 38551488 with penalty 0 = 0 + 0
c [ternres-17] all 43263 free variables schedulable
c [ternres-17] 228 ternary resolvents (0 bin, 228 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-31] removed 71 variables
c [simpleprobe-7] all 43232 free variables schedulable
c [simpleprobe-7] limit 154205954 penalty 0 = 0 + 0
c [decomp-32] removed 54 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 54 variables, found 88573 hbrs, 36 units
c [cgrclsr-10] limit 481893 penalty 3 = 3 + 0
c [cgrclsr-10] all 43178 free variables schedulable
c [cgrclsr-10] fully completed congruence closure
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 37474 probes 87%
c [lift-17] 35 units, 95 impls, 2 eqs in 1 rounds
c [lift-17] 38753 variables remain 90% (4359 retained)
c [lift-17] removed 66 variables
c [cliff-17] limit of 30841190 steps penalty 0 = 0 + 0
c [cliff-17] failed 0, lifted 3
c [unhide-19] limit 7710297 with penalty 0 = 0 + 0
c [unhide-19-32] 0 units, 5 failed, 56000 tauts, 0 hbrs, 18524 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 68 transitive binary clauses
c [cce-17] limit of 77102977 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 1 clauses out of 4 (25%) of length 86
c [cce-17-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-17-1] eliminated 1 clauses out of 7 (14%) of length 34
c [cce-17-1] eliminated 1 clauses out of 12 (8%) of length 29
c [cce-17-1] eliminated 3 clauses out of 12 (25%) of length 28
c [cce-17-1] eliminated 3 clauses out of 19 (16%) of length 27
c [cce-17-1] eliminated 3 clauses out of 12 (25%) of length 26
c [cce-17-1] eliminated 2 clauses out of 19 (11%) of length 25
c [cce-17-1] eliminated 2 clauses out of 15 (13%) of length 24
c [cce-17-1] eliminated 1 clauses out of 13 (8%) of length 23
c [cce-17-1] eliminated 3 clauses out of 17 (18%) of length 22
c [cce-17-1] eliminated 1 clauses out of 21 (5%) of length 21
c [cce-17-1] eliminated 1 clauses out of 15 (7%) of length 20
c [cce-17-1] eliminated 2 clauses out of 16 (12%) of length 19
c [cce-17-1] eliminated 1 clauses out of 18 (6%) of length 18
c [cce-17-1] eliminated 2 clauses out of 15 (13%) of length 17
c [cce-17-1] eliminated 1 clauses out of 22 (5%) of length 16
c [cce-17-1] eliminated 2 clauses out of 15 (13%) of length 15
c [cce-17-1] eliminated 1 clauses out of 21 (5%) of length 14
c [cce-17-1] eliminated 2 clauses out of 19 (11%) of length 13
c [cce-17-1] eliminated 1 clauses out of 18 (6%) of length 12
c [cce-17-1] eliminated 2 clauses out of 25 (8%) of length 11
c [cce-17-1] eliminated 4 clauses out of 26 (15%) of length 10
c [cce-17-1] eliminated 4 clauses out of 26 (15%) of length 9
c [cce-17-1] eliminated 2 clauses out of 26 (8%) of length 8
c [cce-17-1] eliminated 3 clauses out of 57 (5%) of length 7
c [cce-17-1] eliminated 6 clauses out of 2757 (0%) of length 6
c [cce-17-1] eliminated 424 clauses out of 8922 (5%) of length 5
c [cce-17-1] incomplete large round (ACCE)
c [cce-17-1] eliminated 480 large clauses in 77102978 steps
c [cce-17-1] allowing another 38551489 steps for small clauses
c [cce-17] scheduling 167714 clauses = 151205 binary + 16509 ternary
c [cce-17] tried to eliminate 2513 small clauses 1%
c [cce-17] eliminated 541 small clauses 0%
c [cce-17] eliminated 428 binary clauses 0%
c [cce-17] eliminated 113 ternary clauses 1%
c [cce-17-1] eliminated 541 small clauses in 77102978 steps
c [cce-17-1] incomplete small round (ACCE)
c [cce-17-1] eliminated 1021 covered clauses in round 1
c [cce-17] eliminated 1021 covered clauses in TOTAL during 1 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 43106 variables 100%
c [elim-19] limit of 771029771 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 258 variables 1% in round 1 in 24552365 steps
c [elim-19-1] backward subsumption/strengthening limit 49104730
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 7792932 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 258 = 1% variables out of 43106
c [bca-18] limit of 10000000 steps
c [bca-18] 61706 out of 85698 literals actually usable 72%
c [bca-18] added 32 blocked clauses in 146741 steps
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-19] removed 415 variables 1.0% (42848 remain 17%)
c [simplification-19] removed 4145 irredundant clauses 1.5% (266816 remain 19%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 9600 = 28800 / 3
c [simplification-19] new conflict interval 38400
c [simplification-19] penalized conflict interval 38400 = 1 * 38400
c [simplification-19] new conflict limit 362895
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  310.2   42848   266816    334081   12735   6982 1152348   8 50.0 188.3   54
c i  311.8   42847   266816    337954   16144   7055 1152422   4 49.8 187.7   57
c i  312.3   42811   266816    339695   17578   7074 1152433   6 49.8 187.5   57
c -  313.7   42811   266816    343583   13769   7137 1152467   3 49.7 187.0   54
c -  317.1   42811   266816    354281   15347   7338 1152560   9 49.8 186.1   54
c i  318.6   42810   266816    358684   19112   7397 1152583   5 50.1 185.9   58
c 
c [simplification-20] limit of 363637 conflicts hit after 363637 conflicts
c [ternres-18] limit 42379361 with penalty 0 = 0 + 0
c [ternres-18] all 42712 free variables schedulable
c [ternres-18] 81 ternary resolvents (0 bin, 81 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-33] removed 139 variables
c [lift-18] limit 20000000 with penalty 0 = 0 + 0
c [lift-18] using 36527 probes 86%
c [lift-18] 26 units, 81 impls, 3 eqs in 1 rounds
c [lift-18] 37688 variables remain 88% (4906 retained)
c [lift-18] removed 115 variables
c [cliff-18] limit of 33903489 steps penalty 0 = 0 + 0
c [cliff-18] failed 0, lifted 2
c [unhide-20] limit 8475872 with penalty 0 = 0 + 0
c [unhide-20-35] 0 units, 0 failed, 34772 tauts, 0 hbrs, 180781 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 138 transitive binary clauses
c [cce-18] limit of 84758722 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 2 clauses out of 5 (40%) of length 54
c [cce-18-1] eliminated 1 clauses out of 9 (11%) of length 53
c [cce-18-1] eliminated 1 clauses out of 5 (20%) of length 52
c [cce-18-1] eliminated 1 clauses out of 5 (20%) of length 44
c [cce-18-1] eliminated 2 clauses out of 14 (14%) of length 43
c [cce-18-1] eliminated 1 clauses out of 5 (20%) of length 42
c [cce-18-1] eliminated 2 clauses out of 11 (18%) of length 41
c [cce-18-1] eliminated 2 clauses out of 10 (20%) of length 40
c [cce-18-1] eliminated 1 clauses out of 10 (10%) of length 39
c [cce-18-1] eliminated 3 clauses out of 10 (30%) of length 38
c [cce-18-1] eliminated 1 clauses out of 13 (8%) of length 37
c [cce-18-1] eliminated 1 clauses out of 9 (11%) of length 36
c [cce-18-1] eliminated 2 clauses out of 18 (11%) of length 24
c [cce-18-1] eliminated 1 clauses out of 15 (7%) of length 23
c [cce-18-1] eliminated 2 clauses out of 17 (12%) of length 22
c [cce-18-1] eliminated 1 clauses out of 17 (6%) of length 21
c [cce-18-1] eliminated 1 clauses out of 18 (6%) of length 14
c [cce-18-1] eliminated 1 clauses out of 18 (6%) of length 11
c [cce-18-1] eliminated 1 clauses out of 21 (5%) of length 10
c [cce-18-1] eliminated 2 clauses out of 55 (4%) of length 7
c [cce-18-1] eliminated 6 clauses out of 2759 (0%) of length 6
c [cce-18-1] eliminated 45 clauses out of 8497 (1%) of length 5
c [cce-18-1] incomplete large round (ACCE)
c [cce-18-1] eliminated 80 large clauses in 84758723 steps
c [cce-18-1] allowing another 42379361 steps for small clauses
c [cce-18] scheduling 165867 clauses = 149442 binary + 16425 ternary
c [cce-18] tried to eliminate 2734 small clauses 2%
c [cce-18] eliminated 574 small clauses 0%
c [cce-18] eliminated 474 binary clauses 0%
c [cce-18] eliminated 100 ternary clauses 1%
c [cce-18-1] eliminated 574 small clauses in 84758723 steps
c [cce-18-1] incomplete small round (ACCE)
c [cce-18-1] eliminated 654 covered clauses in round 1
c [cce-18] eliminated 654 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 42592 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20-1] eliminated 158 variables 0% in round 1 in 24517243 steps
c [elim-20-1] backward subsumption/strengthening limit 49034486
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 7675830 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 158 = 0% variables out of 42592
c [bca-19] limit of 10000000 steps
c [bca-19] 54842 out of 84870 literals actually usable 65%
c [bca-19] added 35 blocked clauses in 142172 steps
c [rephase-7] after 363637 conflicts (new increment 80000, next 443637)
c [flushphases] 10 phases reset
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-20] removed 278 variables 0.7% (42434 remain 17%)
c [simplification-20] removed 3323 irredundant clauses 1.2% (263493 remain 19%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 19200 = 38400 / 2
c [simplification-20] new conflict interval 57600
c [simplification-20] penalized conflict interval 57600 = 1 * 57600
c [simplification-20] new conflict limit 421237
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  331.3   42434   263493    366339   16590   7480 1123045   7 50.1 185.2   54
c -  335.5   42434   263493    377651   17797   7618 1123123   5 50.0 184.1   54
c i  336.6   42433   263493    382170   20948   7634 1123135   5 50.4 184.3   59
c -  338.5   42344   263493    392816   19157   7696 1123162  11 51.7 184.4   55
c -  343.1   42344   263493    406316   20290   7847 1123248   6 52.1 183.3   55
c i  343.1   42343   263493    406335   20304   7848 1123248   6 52.1 183.3   56
c i  343.4   42342   263493    406994   20886   7858 1123251   5 52.1 183.2   56
c -  348.1   42342   263493    419983   21742   8001 1123336   5 51.9 181.8   55
c 
c [simplification-21] limit of 421903 conflicts hit after 421905 conflicts
c [ternres-19] limit 47592297 with penalty 0 = 0 + 0
c [ternres-19] all 42342 free variables schedulable
c [ternres-19] 167 ternary resolvents (0 bin, 167 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 1487259 penalty 4 = 4 + 0
c [card-6] found 12177 at-most-one constraints of average size 3.7
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1487259 for elimination
c [card-6] 12177 out of 12177 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-34] removed 98 variables
c [treelook-7] limit 1189807 penalty 1 = 1 + 0 boost 1
c [treelook-7] scheduled 51088 literals 60%
c [treelook-7] scheduling used 1189941 steps
c [treelook-7] not fully scheduled
c [treelook-7] limit 1189807 penalty 1 = 1 + 0 boost 1
c [treelook-7] used 1267285 steps
c [treelook-7] 51064 literals remain 60%
c [treelook-7] 5256 variables remain to probed next time 12%
c [treelook-7] removed 2 variables, found 3845 hbrs
c [lift-19] limit 20000000 with penalty 0 = 0 + 0
c [lift-19] using 35708 probes 84%
c [lift-19] 25 units, 103 impls, 3 eqs in 1 rounds
c [lift-19] 36798 variables remain 87% (5508 retained)
c [lift-19] removed 28 variables
c [cliff-19] limit of 38073837 steps penalty 0 = 0 + 0
c [cliff-19] failed 0, lifted 1
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 89 transitive binary clauses
c [cce-19] limit of 95184594 steps penalty 0 = 0 + 0
c [cce-19-1] eliminated 1 clauses out of 7 (14%) of length 51
c [cce-19-1] eliminated 1 clauses out of 9 (11%) of length 50
c [cce-19-1] eliminated 1 clauses out of 4 (25%) of length 49
c [cce-19-1] eliminated 1 clauses out of 8 (12%) of length 48
c [cce-19-1] eliminated 2 clauses out of 6 (33%) of length 42
c [cce-19-1] eliminated 1 clauses out of 11 (9%) of length 41
c [cce-19-1] eliminated 2 clauses out of 10 (20%) of length 40
c [cce-19-1] eliminated 1 clauses out of 11 (9%) of length 39
c [cce-19-1] eliminated 2 clauses out of 9 (22%) of length 38
c [cce-19-1] eliminated 1 clauses out of 14 (7%) of length 37
c [cce-19-1] eliminated 2 clauses out of 10 (20%) of length 36
c [cce-19-1] eliminated 1 clauses out of 11 (9%) of length 35
c [cce-19-1] eliminated 2 clauses out of 11 (18%) of length 34
c [cce-19-1] eliminated 1 clauses out of 11 (9%) of length 33
c [cce-19-1] eliminated 2 clauses out of 15 (13%) of length 32
c [cce-19-1] eliminated 1 clauses out of 11 (9%) of length 31
c [cce-19-1] eliminated 2 clauses out of 12 (17%) of length 30
c [cce-19-1] eliminated 1 clauses out of 12 (8%) of length 29
c [cce-19-1] eliminated 2 clauses out of 16 (12%) of length 28
c [cce-19-1] eliminated 1 clauses out of 14 (7%) of length 27
c [cce-19-1] eliminated 2 clauses out of 15 (13%) of length 26
c [cce-19-1] eliminated 1 clauses out of 14 (7%) of length 25
c [cce-19-1] eliminated 2 clauses out of 18 (11%) of length 24
c [cce-19-1] eliminated 1 clauses out of 16 (6%) of length 23
c [cce-19-1] eliminated 2 clauses out of 17 (12%) of length 22
c [cce-19-1] eliminated 1 clauses out of 18 (6%) of length 21
c [cce-19-1] eliminated 2 clauses out of 17 (12%) of length 20
c [cce-19-1] eliminated 1 clauses out of 15 (7%) of length 19
c [cce-19-1] eliminated 2 clauses out of 23 (9%) of length 18
c [cce-19-1] eliminated 1 clauses out of 14 (7%) of length 17
c [cce-19-1] eliminated 2 clauses out of 23 (9%) of length 16
c [cce-19-1] eliminated 1 clauses out of 14 (7%) of length 15
c [cce-19-1] eliminated 3 clauses out of 19 (16%) of length 14
c [cce-19-1] eliminated 1 clauses out of 19 (5%) of length 13
c [cce-19-1] eliminated 2 clauses out of 20 (10%) of length 12
c [cce-19-1] eliminated 1 clauses out of 19 (5%) of length 11
c [cce-19-1] eliminated 2 clauses out of 22 (9%) of length 10
c [cce-19-1] eliminated 3 clauses out of 26 (12%) of length 9
c [cce-19-1] eliminated 3 clauses out of 29 (10%) of length 8
c [cce-19-1] eliminated 5 clauses out of 59 (8%) of length 7
c [cce-19-1] eliminated 6 clauses out of 2767 (0%) of length 6
c [cce-19-1] eliminated 56 clauses out of 8073 (1%) of length 5
c [cce-19-1] incomplete large round (ACCE)
c [cce-19-1] eliminated 128 large clauses in 95184595 steps
c [cce-19-1] allowing another 47592297 steps for small clauses
c [cce-19] scheduling 208387 clauses = 148267 binary + 60120 ternary
c [cce-19] tried to eliminate 3201 small clauses 2%
c [cce-19] eliminated 603 small clauses 0%
c [cce-19] eliminated 441 binary clauses 0%
c [cce-19] eliminated 162 ternary clauses 0%
c [cce-19-1] eliminated 612 small clauses in 95184595 steps
c [cce-19-1] incomplete small round (ACCE)
c [cce-19-1] eliminated 740 covered clauses in round 1
c [cce-19] eliminated 740 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 42305 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21-1] eliminated 77 variables 0% in round 1 in 23613113 steps
c [elim-21-1] backward subsumption/strengthening limit 47226226
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 7605162 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 77 = 0% variables out of 42305
c [bca-20] limit of 10000000 steps
c [bca-20] 53804 out of 84458 literals actually usable 64%
c [bca-20] added 1 blocked clauses in 139429 steps
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-21] removed 114 variables 0.3% (42228 remain 17%)
c [simplification-21] removed 1559 irredundant clauses 0.6% (261934 remain 19%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 28800 = 57600 / 2
c [simplification-21] new conflict interval 86400
c [simplification-21] penalized conflict interval 86400 = 1 * 86400
c [simplification-21] new conflict limit 508305
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  359.7   42227   261934    428116   28079   8361 1156070   4 51.7 181.1   62
c i  359.7   42166   261934    428117   28079   8361 1156070   4 51.7 181.1   62
c -  362.2   42108   261934    434972   23169   8423 1156111   9 51.9 180.9   57
c -  367.1   42108   261934    450081   24520   8569 1156180   5 52.0 179.9   57
c i  369.5   42107   261934    457959   30715   8633 1156233   5 52.7 180.2   65
c i  370.2   42106   261934    459531   32128   8645 1156238   5 52.7 180.0   66
c -  373.0   42085   261934    466437   26161   8721 1156300   4 52.8 179.6   57
c i  377.8   42084   261934    480807   37539   8845 1156349   6 53.4 178.8   69
c -  378.8   42078   261934    483104   27466   8871 1156375   6 53.4 178.7   57
c i  383.2   42077   261934    494531   36723   8966 1156422   4 53.4 177.8   65
c -  385.6   42050   261934    500164   28870   9010 1156446   7 53.3 177.2   57
c 
c [simplification-22] limit of 509367 conflicts hit after 509368 conflicts
c [ternres-20] limit 56257963 with penalty 0 = 0 + 0
c [ternres-20] all 42050 free variables schedulable
c [ternres-20] 322 ternary resolvents (1 bin, 321 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-36] removed 179 variables
c [basicprobe-7] limit 56257963 penalty 0 = 0 + 0
c [basicprobe-7-0] 6000 probes remain 14% after last round
c [basicprobe-7-0] 184 units = 182 failed (99%) + 2 lifted (1%)
c [basicprobe-7-0] removed 386 variables, found 195985 hbrs
c [bate-6] eliminated 214 asymmetric tautologies during probing
c [lift-20] limit 20000000 with penalty 0 = 0 + 0
c [lift-20] using 34525 probes 83%
c [lift-20] 17 units, 94 impls, 2 eqs in 1 rounds
c [lift-20] 35672 variables remain 86% (5970 retained)
c [lift-20] removed 21 variables
c [cliff-20] limit of 45006370 steps penalty 0 = 0 + 0
c [cliff-20] failed 1, lifted 6
c [unhide-21] limit 5625796 with penalty 1 = 1 + 0
c [unhide-21-37] 0 units, 2 failed, 35479 tauts, 0 hbrs, 224178 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 112 transitive binary clauses
c [cce-20] limit of 112515926 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 2 clauses out of 8 (25%) of length 46
c [cce-20-1] eliminated 2 clauses out of 2753 (0%) of length 6
c [cce-20-1] eliminated 27 clauses out of 7915 (0%) of length 5
c [cce-20-1] incomplete large round (ACCE)
c [cce-20-1] eliminated 31 large clauses in 112515927 steps
c [cce-20-1] allowing another 56257963 steps for small clauses
c [cce-20] scheduling 201734 clauses = 146421 binary + 55313 ternary
c [cce-20] tried to eliminate 4004 small clauses 2%
c [cce-20] eliminated 839 small clauses 0%
c [cce-20] eliminated 737 binary clauses 1%
c [cce-20] eliminated 102 ternary clauses 0%
c [cce-20-1] eliminated 847 small clauses in 112515927 steps
c [cce-20-1] incomplete small round (ACCE)
c [cce-20-1] eliminated 878 covered clauses in round 1
c [cce-20] eliminated 878 covered clauses in TOTAL during 1 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 41633 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22-1] eliminated 401 variables 1% in round 1 in 25032609 steps
c [elim-22-1] backward subsumption/strengthening limit 50065218
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 7381140 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 401 = 1% variables out of 41633
c [bca-21] limit of 10000000 steps
c [bca-21] 48763 out of 82466 literals actually usable 59%
c [bca-21] added 14 blocked clauses in 139276 steps
c [rephase-8] after 509368 conflicts (new increment 160000, next 669368)
c [flushphases] 9 phases reset
c [phase-15] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-22] removed 818 variables 1.9% (41232 remain 17%)
c [simplification-22] removed 8565 irredundant clauses 3.3% (253369 remain 18%)
c [simplification-22] maximum reduction of 3% = max (2%, 3%)
c [simplification-22] geometric conflict interval increment 21600 = 86400 / 4
c [simplification-22] new conflict interval 108000
c [simplification-22] penalized conflict interval 108000 = 1 * 108000
c [simplification-22] new conflict limit 617368
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  406.1   41232   253369    522541   29925   9286 1239711  11 54.1 177.4   61
c -  409.6   41232   253369    541420   31178   9360 1239756   6 57.6 180.4   61
c i  410.5   41231   253369    546619   35498   9382 1239772   6 58.0 181.0   68
c -  414.0   41229   253369    561005   31883   9490 1239821   4 59.4 181.7   61
c -  418.9   41229   253369    584145   33305   9600 1239863   8 61.7 182.6   61
c R  419.0   41229   253369    584679   33667   9600 1239863   6 61.7 182.6   62
c -  427.1   41229   253369    603960   34532   9793 1239970   6 61.5 181.1   61
c i  431.0   41228   253369    614941   43098   9872 1240006   4 61.2 180.3   68
c 
c [simplification-23] limit of 618064 conflicts hit after 618064 conflicts
c [ternres-21] limit 64600336 with penalty 0 = 0 + 0
c [ternres-21] all 41210 free variables schedulable
c [ternres-21] 171 ternary resolvents (0 bin, 171 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 807504 penalty 4 = 4 + 0
c [gauss-6] extracted 9 xors of average arity 3.0
c [gauss-6] connected 27 occurrences of 27 variables (average 1.0)
c [gauss-6] limit 807504 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 18 variables
c [simpleprobe-8] all 41192 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 31 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 31 variables, found 94276 hbrs, 12 units
c [lift-21] limit 20000000 with penalty 0 = 0 + 0
c [lift-21] using 33540 probes 81%
c [lift-21] 15 units, 82 impls, 4 eqs in 1 rounds
c [lift-21] 34621 variables remain 84% (6519 retained)
c [lift-21] removed 21 variables
c [cliff-21] limit of 51680269 steps penalty 0 = 0 + 0
c [cliff-21] failed 4, lifted 2
c [unhide-22] limit 12920067 with penalty 0 = 0 + 0
c [unhide-22-41] 0 units, 3 failed, 90853 tauts, 0 hbrs, 335230 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 70 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 41132 variables 100%
c [block-7] limit of 40375210 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2 blocked clauses
c [block-7] 2 < 1/1000 * 252013 = 252 considered unsuccessful
c [cce-21] limit of 129200672 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 87
c [cce-21-1] eliminated 2 clauses out of 4 (50%) of length 86
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 82
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 78
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 74
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 70
c [cce-21-1] eliminated 1 clauses out of 8 (12%) of length 66
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 62
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 58
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-21-1] eliminated 1 clauses out of 7 (14%) of length 50
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 47
c [cce-21-1] eliminated 1 clauses out of 8 (12%) of length 46
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 45
c [cce-21-1] eliminated 2 clauses out of 6 (33%) of length 43
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 42
c [cce-21-1] eliminated 1 clauses out of 13 (8%) of length 20
c [cce-21-1] eliminated 1 clauses out of 23 (4%) of length 18
c [cce-21-1] eliminated 1 clauses out of 16 (6%) of length 17
c [cce-21-1] eliminated 1 clauses out of 17 (6%) of length 16
c [cce-21-1] eliminated 1 clauses out of 17 (6%) of length 15
c [cce-21-1] eliminated 2 clauses out of 17 (12%) of length 14
c [cce-21-1] eliminated 1 clauses out of 18 (6%) of length 11
c [cce-21-1] eliminated 4 clauses out of 25 (16%) of length 10
c [cce-21-1] eliminated 3 clauses out of 29 (10%) of length 9
c [cce-21-1] eliminated 3 clauses out of 31 (10%) of length 8
c [cce-21-1] eliminated 5 clauses out of 60 (8%) of length 7
c [cce-21-1] eliminated 45 clauses out of 2764 (2%) of length 6
c [cce-21-1] eliminated 35 clauses out of 7880 (0%) of length 5
c [cce-21-1] incomplete large round (ACCE)
c [cce-21-1] eliminated 121 large clauses in 129200673 steps
c [cce-21-1] allowing another 64600336 steps for small clauses
c [cce-21] scheduling 159680 clauses = 143631 binary + 16049 ternary
c [cce-21] tried to eliminate 4130 small clauses 3%
c [cce-21] eliminated 714 small clauses 0%
c [cce-21] eliminated 576 binary clauses 0%
c [cce-21] eliminated 138 ternary clauses 1%
c [cce-21-1] eliminated 714 small clauses in 129200673 steps
c [cce-21-1] incomplete small round (ACCE)
c [cce-21-1] eliminated 835 covered clauses in round 1
c [cce-21] eliminated 835 covered clauses in TOTAL during 1 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 41132 variables 100%
c [elim-23] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-23-1] eliminated 158 variables 0% in round 1 in 23052382 steps
c [elim-23-1] backward subsumption/strengthening limit 46104764
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 7282059 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 158 = 0% variables out of 41132
c [bca-22] limit of 10000000 steps
c [bca-22] 45842 out of 81950 literals actually usable 56%
c [bca-22] added 20 blocked clauses in 142694 steps
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-23] removed 236 variables 0.6% (40974 remain 17%)
c [simplification-23] removed 2519 irredundant clauses 1.0% (250850 remain 18%)
c [simplification-23] maximum reduction of 1% = max (1%, 1%)
c [simplification-23] geometric conflict interval increment 54000 = 108000 / 2
c [simplification-23] new conflict interval 162000
c [simplification-23] penalized conflict interval 162000 = 1 * 162000
c [simplification-23] new conflict limit 780064
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  453.0   40974   250850    627735   35603  10209 1259649   5 61.2 179.4   63
c -  460.0   40974   250850    649421   36943  10380 1259732   5 62.2 179.3   63
c -  468.7   40974   250850    671884   38570  10532 1259837   6 62.4 178.5   63
c -  477.8   40974   250850    694936   40385  10684 1259922   5 62.4 177.4   62
c -  485.4   40974   250850    721208   41573  10805 1259981   7 63.0 176.7   62
c i  489.5   40973   250850    731200   49791  10872 1260040   5 63.0 176.2   70
c i  489.6   40972   250850    731548   50084  10875 1260042   6 63.0 176.2   70
c i  489.6   40971   250850    731549   50084  10875 1260042   6 63.0 176.2   70
c -  495.7   40971   250850    746086   43027  10962 1260074   4 63.1 175.5   62
c i  498.0   40970   250850    752095   47822  11009 1260107   5 63.1 175.2   68
c i  502.9   40969   250850    766117   58057  11100 1260134   4 63.3 174.8   78
c i  504.4   40869   250850    770479   60611  11113 1260150   5 63.4 174.7   83
c -  506.0   40769   250850    773750   44817  11145 1260160   7 63.3 174.5   62
c i  506.7   40768   250850    775253   46150  11156 1260160   6 63.2 174.4   65
c i  506.7   40767   250850    775254   46150  11156 1260160   6 63.2 174.4   65
c 
c [simplification-24] limit of 781332 conflicts hit after 781333 conflicts
c [ternres-22] limit 81189013 with penalty 0 = 0 + 0
c [ternres-22] all 40767 free variables schedulable
c [ternres-22] 165 ternary resolvents (0 bin, 165 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-39] removed 216 variables
c [treelook-8] limit 4059450 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 51972 literals 64%
c [treelook-8] scheduling used 1624942 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 4059450 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 4088843 steps
c [treelook-8] 51906 literals remain 64%
c [treelook-8] 5190 variables remain to probed next time 13%
c [decomp-40] removed 3 variables
c [treelook-8] removed 4 variables, found 8364 hbrs
c [cgrclsr-11] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-11] all 40754 free variables schedulable
c [cgrclsr-11] fully completed congruence closure
c [lift-22] limit 20000000 with penalty 0 = 0 + 0
c [lift-22] using 32641 probes 80%
c [lift-22] 88 units, 107 impls, 4 eqs in 1 rounds
c [lift-22] 33647 variables remain 83% (6999 retained)
c [lift-22] removed 108 variables
c [cliff-22] limit of 64951210 steps penalty 0 = 0 + 0
c [cliff-22] failed 6, lifted 0
c [unhide-23] limit 16237802 with penalty 0 = 0 + 0
c [unhide-23-46] 1 units, 11 failed, 31105 tauts, 0 hbrs, 226861 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 63 transitive binary clauses
c [cce-22] limit of 162378026 steps penalty 0 = 0 + 0
c [cce-22-1] eliminated 1 clauses out of 10 (10%) of length 22
c [cce-22-1] eliminated 1 clauses out of 11 (9%) of length 14
c [cce-22-1] eliminated 2 clauses out of 24 (8%) of length 13
c [cce-22-1] eliminated 1 clauses out of 18 (6%) of length 12
c [cce-22-1] eliminated 2 clauses out of 21 (10%) of length 11
c [cce-22-1] eliminated 2 clauses out of 22 (9%) of length 10
c [cce-22-1] eliminated 7 clauses out of 31 (23%) of length 9
c [cce-22-1] eliminated 3 clauses out of 38 (8%) of length 8
c [cce-22-1] eliminated 7 clauses out of 55 (13%) of length 7
c [cce-22-1] eliminated 3 clauses out of 2720 (0%) of length 6
c [cce-22-1] eliminated 236 clauses out of 7804 (3%) of length 5
c [cce-22-1] incomplete large round (ACCE)
c [cce-22-1] eliminated 265 large clauses in 162378027 steps
c [cce-22-1] allowing another 81189013 steps for small clauses
c [cce-22] scheduling 157447 clauses = 141751 binary + 15696 ternary
c [cce-22] tried to eliminate 5397 small clauses 3%
c [cce-22] eliminated 1016 small clauses 1%
c [cce-22] eliminated 812 binary clauses 1%
c [cce-22] eliminated 204 ternary clauses 1%
c [cce-22-1] eliminated 1016 small clauses in 162378027 steps
c [cce-22-1] incomplete small round (ACCE)
c [cce-22-1] eliminated 1281 covered clauses in round 1
c [cce-22] eliminated 1281 covered clauses in TOTAL during 1 rounds
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 40621 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24-1] eliminated 324 variables 1% in round 1 in 23719258 steps
c [elim-24-1] backward subsumption/strengthening limit 47438516
c [elim-24-1] subsumed 0 and strengthened 0 clauses in 7101849 steps
c [elim-24] fully completed in 1 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 324 = 1% variables out of 40621
c [bca-23] limit of 10000000 steps
c [bca-23] 44110 out of 80596 literals actually usable 55%
c [bca-23] added 27 blocked clauses in 141815 steps
c [rephase-9] after 781333 conflicts (new increment 320000, next 1101333)
c [flushphases] 7 phases reset
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-24] removed 470 variables 1.2% (40297 remain 16%)
c [simplification-24] removed 6116 irredundant clauses 2.4% (244734 remain 18%)
c [simplification-24] maximum reduction of 2% = max (1%, 2%)
c [simplification-24] geometric conflict interval increment 54000 = 162000 / 3
c [simplification-24] new conflict interval 216000
c [simplification-24] penalized conflict interval 216000 = 1 * 216000
c [simplification-24] new conflict limit 997333
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  526.6   40296   244734    784973   49140  11287 1206398   4 63.2 173.8   67
c i  528.8   40295   244734    790460   53585  11346 1206432   4 63.1 173.5   71
c i  530.1   40204   244734    795676   57795  11373 1206443   5 63.3 173.8   78
c -  533.1   40179   244734    802255   44173  11425 1206472   6 63.3 173.4   63
c i  534.0   40178   244734    804411   46072  11435 1206479   5 63.2 173.3   64
c i  542.3   40167   244734    829160   64561  11605 1206548   5 63.8 172.8   85
c -  542.7   40167   244734    830813   46231  11612 1206552  11 63.9 172.8   63
c 1  546.3   40167   244734    843933   55591  11640 1206576   8 65.4 174.0   82
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s SATISFIABLE
c
c bate: 765 basic ate = 723 trn 95% + 42 lrg 5% in 6 updates
c bcas: 23 count, 3813 added (327 skipped), 5190712 steps
c bkwd: tried 7737001 clauses, 15474001 lits, 2.00 lits/clause
c bkwd: checked 175956974 occs, 22.74 occs/clause, 11.37 occs/lit
c bkwd: subsumed 0 binary, 1 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 7 bces, 13331 removed, 10590067 resolutions, 37303986 steps
c blkd: 17291 blocking literals 3%, 45 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 0 am1, 14170432 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 116667 subsumed
c card: 93331 at-most-one constraints found, average size 4.28
c card: 93331 at-most-one constraints used 100%, average size 4.28
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: 22 cces, 42899 eliminated, 42390 ate 99%, 509 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 11 count, 7876802 esteps, 517188 csteps
c cgrs: 19 eqs, 3 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 11160 extracted (10567 ands 95%, 584 xors 5%, 9 ites 0%)
c clff: 22 cliffs, 372 lifted, 375 failed
c clff: 34639 decisions, 533054573 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4749826 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 234 gcs, 0 rescored clauses, 439 rescored vars
c dcps: 40 decompositions, 9168 equivalent 4%
c deco: 132280 decision-only clauses 16%, 64% reduction
c decs: 8384520 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 216048 flipped 2.577% (in 1778 phases)
c elms: 24 elims, 107799 eliminated 41%
c elms: 47 rounds, 2.0 rounds/bve
c elms: 85219 small 79%, 22535 large 21%
c elms: 341769 tried small, 85222 succeeded 25%, 256547 failed 75%
c elms: 50084 subsumed, 73144 strengthened, 4636 blocked
c elms: 35978118 copies, 34212917 resolutions, 10774259 ipos
c elms: 11818484 subchks, 12627030 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 6 extractions, 565 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10527258 steps, 5263629 extr 50%, 9405 elim 0%
c glue: 65.4 orig avg, 57.7 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 2820095 = 531743 simple + 2275707 trn 19% + 12645 lrg 81%, 5587 sub 0%
c hght: 174 average, 2.66 height/glue
c ints: 24574 luby (6053904 steps), 0 inout (0 steps)
c lift: 22 phases, 44058 probed (15303 level1 35%, 28755 level2 65%)
c lift: 2135 units, 62 equivalences, 1526 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 836349 clauses, 153.5 length
c lrnd: 403301 uips 48%, 357132 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 128396179 learned lits, 31% minimized
c mins: 675410 mins 81%, 9155 bin 1%, 19504 size 2%, 132280 deco 16%
c move: moved 836349, 21925 bin 3%, 9723 trn 1%, 0 lrg 0%
c otfs: str 33621 dyn (33534 red, 87 irr) 7584 drv 23%, 26037 rst 77%
c otfs: sub 189 dyn (189 red, 0 irr)
c phas: 17 computed, 141986 set, 33472 pos (24%), 108514 neg (76%)
c prbs: 7 basic, 20630 probed, 1117 failed, 3 lifted
c prbs: 8 simple, 1144312 probed, 2338 failed, 668 eqs
c prbs: 8 treelook, 182 probed, 13 failed, 0 lifted
c prps: 1315659976 props, 141 props/dec
c prps: 90% srch, 10% simp, 0% lkhd
c psns: 176173325 searches, 33248830 hits, 19% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 58 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 58 arith 100%, 0 double 0%
c rmbd: 55483 removed, 7167 red 13%
c rphs: 9 recomputed phases
c rsts: 24204 restarts 98%, 370 skipped 2%
c rsts: 0 saturating 0%, 6 agile 2%, 364 reuse 98%
c rsts: 34.7 avg interval, 34.7 scaled, 1.0 factor
c rsts: 5463 kept 22.6% average 24.4%
c simp: 24 count (24 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 836349 count (915744 tried 1.1), 141841 sub out of 813836 (17.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 2 count
c tops: 103208 fixed 40%, 796 its, 1060.22 confs/it
c trvs: 15363199914 traversals, 94% srch, 8% simp, 0% lkhd
c trvs: 12.2 search traversals per propagation, 17027.7 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 22 transitive reductions, 3574 removed, 5 failed
c trds: 17596 nodes, 54823 edges, 44039271 steps
c trim: 8379466 words, 32.0 MB
c trnr: 22 count, 2 bin, 3147 trn, 245833446 steps
c unhd: 23 count, 46 rounds, 155049516 steps
c unhd: 1880 non-trivial sccs of average size 2.2
c unhd: 128 units, 126 bin, 0 trn, 2 lrg
c unhd: 15005 failed, 14863 stamp, 0 lits, 109 bin, 19 trn, 2 lrg
c unhd: 791495 tauts, 13970 bin 2%, 15947 trn 2%, 992 lrg 0%
c unhd: 791495 tauts, 760586 stamp 96%, 700824 red 89%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1647764 str, 126 bin 0%, 3856 trn 0%, 1643782 lrg 100%, 1624932 red 99%
c vars: 40167 remaining 15% and 220175 removed 85% out of 260342
c vars: 103208 fixed 40%, 107799 eliminated 41%, 9168 equivalent 4%
c vsts: 9729360787 visits, 90% srch, 10% simp, 0% lkhd
c vsts: 7.4 search visits per propagation, 10352.0 per conflict
c wchs: 964287263 pushed, 65692366 enlarged, 332 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    813836 100    545720 100  38951960 100   6096586 100    405731 100
c 
c  0      55812   7         0   0  23205476  60   2279093  37    103544  26 
c  1      37794   5       268   0  11060782  28<  1410219  23     76711  19 
c  2      96018  12     83542  15   1647536   4    490820   8<    34686   9 
c  3     107793  13     99727  18    946595   2    406112   7     30720   8<
c  4      99998  12     91124  17    683193   2    350555   6     30109   7 
c  5      87156  11<    79676  15<   466705   1    283330   5     26522   7 
c  6      62994   8     50055   9    267022   1    190622   3     20798   5 
c  7      46065   6     33901   6    170284   0    135599   2     15861   4 
c  8      34158   4     23969   4    110230   0     95542   2     12260   3 
c  9      26101   3     17118   3     76557   0     69863   1      8488   2 
c 10      37575   5     21043   4     88386   0     94877   2     12037   3 
c 11      63533   8     24933   5    119123   0    148960   2     17334   4 
c 12      56209   7     19378   4    105249   0    134484   2     15853   4 
c 13       2630   0       986   0      4822   0      6510   0       808   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             5.4           5.2           0.8           2.3           3.5
c std             3.6           2.8           1.6           3.1           3.7
c 
c   62.530  11% cce
c   42.591   8% analysis
c   39.349   7% elim
c   33.202   6% probe
c   25.923   5% gc
c   24.980   5% unhide
c   23.569   4% lift
c   20.306   4% cliff
c   15.736   3% decide
c   13.014   2% decomp
c    9.421   2% bump
c    8.778   2% defrag
c    8.777   2% mincls
c    7.488   1% restart
c    7.191   1% backward
c    4.447   1% bca
c    3.780   1% cgrclsr
c    3.308   1% block
c    2.991   1% transred
c    1.702   0% gauss
c    1.600   0% phase
c    1.426   0% ternres
c    0.949   0% reduce
c    0.931   0% card
c    0.183   0% tabularasa
c    0.026   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c   14.587   3% probe simple     44%
c   14.547   3% probe basic      44%
c    4.068   1% probe tree-look  12%
c ==================================
c    7.620   1% preprocessing     3%
c  227.545  42% inprocessing     97%
c ==================================
c  235.165  43% simplifying
c  311.152  57% search
c ==================================
c  546.336 100% all
c 
c 8384520 decisions, 15346.8 decisions/sec
c 843933 conflicts, 1544.7 conflicts/sec
c 1315659976 propagations, 2.4 megaprops/sec
c 546.3 seconds, 105.6 MB
c launch: done
