c launch: /data/cnf/sc2014/app/partial-5-17-s.cnf.bz2
c host: atom30
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/partial-5-17-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-5-17-s.cnf.bz2
c no embedded options
c found 'p cnf 252328 1189896' header
c read 252328 variables, 1189896 clauses, 2752826 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 242891 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  242891  1169811         0       0      0     0   9  0.0   0.0   56
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 35004 at-most-one constraints of average size 4.9
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 35004 out of 35004 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 106289 variables
c [simpleprobe-1] all 146039 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 1171 variables
c [simpleprobe-1] 1165 variables remain 1% (143703 retained)
c [simpleprobe-1] removed 1171 variables, found 16430 hbrs, 9 units
c [unhide-1] limit 416334 based on 832668 irredundant clauses
c [unhide-1-1] 1 units, 102 failed, 7557 tauts, 0 hbrs, 8766 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 144695 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 55116 variables 38% in round 1 in 90869103 steps
c [elim-1-1] backward subsumption/strengthening limit 181738206
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 23374307 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 55116 = 38% variables out of 144695
c [phase-1] phase bias: 18773 positive 21%, 70806 negative 79%
c [simplification-1] removed 116658 variables 56.6% (89579 remain 37%)
c [simplification-1] removed 543019 irredundant clauses 46.4% (626792 remain 54%)
c [simplification-1] maximum reduction of 57% = max (57%, 46%)
c [simplification-1] large reduction 57% >= 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] 206505, max 380465, min4 59061 at 74%, min10 59061 at 74%
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 R    6.8   89579   626792        63      53      5  9247  10 17.6 167.4   44
c i    6.9   89578   626792        81      64      6  9252   2 15.1 203.3   44
c i    6.9   89211   626792        87      66      8  9253   3 14.3 197.0   44
c i    6.9   89195   626792        91      68      9  9253   2 13.7 193.8   44
c i    6.9   89158   626792        94      69      9  9254   2 13.3 193.5   44
c i    6.9   89061   626792       139      98     13  9261   2 17.4 173.4   44
c R    7.0   88791   626792       171     119     17  9268   2 16.8 171.2   44
c i    7.0   88790   626792       188     134     18  9268   2 18.3 162.6   44
c i    7.0   88745   626792       217     152     24  9271   2 16.4 157.6   44
c i    7.1   88736   626792       258     180     30  9276   2 15.3 161.9   44
c i    7.1   86731   626792       259     180     30  9276   2 15.2 161.8   44
c i    7.1   86448   626792       262     181     30  9277   2 15.1 160.5   44
c i    7.1   86437   626792       276     188     33  9280   3 14.5 157.1   44
c i    7.1   86248   626792       277     188     33  9280   3 14.4 156.0   44
c i    7.1   86054   626792       280     190     33  9280   3 14.3 153.9   44
c i    7.1   86043   626792       283     192     33  9280   2 14.1 152.5   44
c i    7.1   85996   626792       290     196     34  9281   2 13.8 148.8   44
c i    7.1   85984   626792       291     196     34  9281   1 13.8 147.6   44
c i    7.2   85973   626792       292     196     34  9281   1 13.8 146.4   44
c i    7.2   85964   626792       293     196     34  9281   1 13.7 145.2   44
c i    7.2   85950   626792       294     196     34  9281   1 13.7 144.1   44
c i    7.2   85940   626792       295     196     34  9281   1 13.6 143.0   44
c i    7.2   85927   626792       296     196     34  9281   1 13.6 142.5   44
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    7.2   85914   626792       297     196     34  9281   1 13.5 141.4   44
c i    7.2   85902   626792       299     197     34  9281   0 13.4 139.6   44
c i    7.2   85889   626792       312     205     35  9283   1 13.3 139.7   44
c i    7.2   84486   626792       313     205     35  9283   1 13.2 139.0   44
c i    7.2   84476   626792       314     205     35  9283   1 13.2 138.3   44
c i    7.2   84465   626792       315     205     35  9283   1 13.2 137.6   44
c i    7.2   84454   626792       322     206     35  9288   1 13.1 136.7   44
c i    7.2   84443   626792       323     206     35  9288   1 13.0 136.2   44
c i    7.2   84431   626792       331     210     37  9289   2 13.0 134.9   45
c i    7.2   84420   626792       333     210     38  9289   2 12.9 134.4   45
c i    7.3   84407   626792       387     241     47  9301   2 13.4 134.0   45
c i    7.3   84395   626792       392     244     48  9301   2 13.3 133.7   45
c i    7.3   83968   626792       393     244     48  9301   2 13.3 133.2   45
c i    7.3   83512   626792       396     246     48  9301   2 13.2 132.6   45
c i    7.3   83260   626792       397     246     48  9301   2 13.1 131.9   45
c i    7.3   83256   626792       399     246     48  9302   2 13.1 131.2   45
c i    7.3   83244   626792       401     247     48  9302   2 13.0 130.5   45
c i    7.3   83234   626792       402     247     48  9302   1 13.0 129.9   45
c i    7.3   83224   626792       403     247     48  9302   1 13.0 129.3   45
c i    7.3   83214   626792       404     247     48  9302   1 12.9 128.6   45
c i    7.3   83206   626792       405     247     48  9302   1 12.9 128.0   45
c i    7.3   83195   626792       407     248     48  9302   1 12.8 128.0   45
c R    7.3   82577   626792       418     253     50  9304   1 12.6 127.4   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    7.3   82576   626792       425     257     51  9305   1 12.4 126.3   45
c i    7.3   82566   626792       426     257     51  9305   1 12.4 125.8   45
c i    7.3   82552   626792       427     257     51  9305   1 12.4 125.4   45
c i    7.3   82539   626792       428     257     51  9305   1 12.3 124.9   45
c i    7.3   82528   626792       429     257     51  9305   1 12.3 124.4   45
c i    7.3   82516   626792       430     257     51  9305   1 12.3 123.9   45
c i    7.3   82504   626792       431     257     51  9305   0 12.2 123.5   45
c i    7.3   82493   626792       432     257     51  9305   0 12.2 123.0   45
c i    7.3   82482   626792       433     257     51  9305   0 12.2 122.7   45
c i    7.3   82470   626792       443     263     52  9307   0 12.0 121.8   45
c i    7.4   82461   626792       444     263     52  9307   0 12.0 121.3   45
c i    7.4   82452   626792       445     263     52  9307   0 11.9 120.8   45
c i    7.4   82439   626792       448     265     52  9307   0 11.9 120.4   45
c i    7.4   82275   626792       451     267     52  9307   1 11.8 121.7   45
c i    7.4   82262   626792       452     267     52  9307   1 11.8 122.7   45
c i    7.4   81860   626792       453     267     52  9307   1 11.8 123.5   45
c i    7.4   81850   626792       454     267     52  9307   0 11.8 124.2   45
c i    7.4   81843   626792       455     267     52  9307   0 11.7 125.0   45
c i    7.4   81834   626792       456     267     52  9307   0 11.7 125.7   45
c i    7.5   81825   626792       461     269     53  9308   0 11.6 126.9   45
c i    7.5   81815   626792       482     286     56  9308   1 11.4 128.7   45
c i    7.5   81804   626792       486     288     56  9309   1 11.4 130.4   45
c i    7.6   80339   626792       566     346     65  9315   2 10.8 145.4   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    7.7   80224   626792       608     373     72  9322   2 10.2 145.0   45
c i    7.7   80215   626792       616     374     75  9324   2 10.2 144.2   45
c i    7.7   80204   626792       617     374     75  9324   2 10.2 144.0   45
c i    7.7   80194   626792       618     374     75  9324   2 10.2 143.8   45
c i    7.7   80187   626792       619     374     75  9324   1 10.1 143.5   45
c i    7.7   80179   626792       620     374     75  9324   1 10.1 143.3   45
c i    7.7   80170   626792       678     423     78  9326   2 10.0 141.3   45
c R    7.9   80161   626792      1001     676     98  9359   2 10.1 171.6   45
c i    7.9   80160   626792      1002     676     98  9359   2 10.1 171.7   45
c i    8.0   80150   626792      1021     686    101  9362   1 10.0 171.2   45
c i    8.0   80140   626792      1023     686    101  9363   1 10.0 171.1   45
c i    8.0   79683   626792      1027     688    102  9363   1 10.0 170.3   45
c i    8.3   79598   626792      1226     839    116  9385   1 11.2 168.5   45
c i    8.3   79586   626792      1237     847    116  9387   1 11.1 166.9   45
c i    8.4   78988   626792      1244     852    117  9387   1 11.2 167.1   45
c i    8.5   78913   626792      1275     870    125  9391   2 11.1 166.1   45
c i    8.5   78395   626792      1277     870    126  9391   2 11.1 165.8   45
c i    8.5   78385   626792      1278     870    126  9391   1 11.1 165.5   45
c i    8.5   78376   626792      1279     870    126  9391   1 11.0 165.2   45
c i    8.5   78366   626792      1280     870    126  9391   1 11.0 164.9   45
c i    8.5   78358   626792      1297     884    127  9391   1 11.0 165.0   45
c i    8.5   78345   626792      1298     884    127  9391   1 11.0 165.0   45
c i    8.5   78335   626792      1299     884    127  9391   1 11.0 165.0   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    8.5   78324   626792      1300     884    127  9391   1 11.0 165.0   45
c i    8.6   78311   626792      1473    1009    155  9408   2 11.7 174.9   45
c i    8.7   78276   626792      1510    1032    162  9413   1 11.5 173.7   45
c i    8.8   78173   626792      1599    1099    171  9423   2 11.4 171.8   45
c i    8.9   78162   626792      1684    1154    179  9443   1 11.0 168.0   45
c i    8.9   78152   626792      1704    1166    181  9448   1 11.0 166.9   45
c i    9.0   78115   626792      1749    1199    187  9451   2 11.0 166.4   45
c i    9.1   78103   626792      1986    1348    206  9496   2 11.7 166.1   45
c i    9.1   78091   626792      1995    1354    208  9496   2 11.7 165.7   45
c i    9.2   78084   626792      2011    1364    209  9497   2 12.3 165.6   45
c i    9.2   77605   626792      2100    1444    210  9500   2 14.0 170.5   45
c i    9.3   77597   626792      2126    1467    211  9501   3 13.9 172.0   45
c 
c [simplification-2] limit of 2183 conflicts hit after 2183 conflicts
c [decomp-3] removed 12618 variables
c [simpleprobe-2] 1113 schedulable variables 1%
c [simpleprobe-2] limit 2963887 penalty 0 = 0 + 0
c [simpleprobe-2] 1206 variables remain 2% (75755 retained)
c [simpleprobe-2] removed 0 variables, found 2493 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 45365 literals 29%
c [treelook-1] scheduling used 301439 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 432240 steps
c [treelook-1] 45356 literals remain 29%
c [treelook-1] 44441 variables remain to probed next time 58%
c [treelook-1] removed 3 variables, found 3188 hbrs
c [basicprobe-1] limit 1073708 based on 536854 irredundant clauses
c [basicprobe-1-0] 23738 probes remain 32% after last round
c [basicprobe-1-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3106 variables, found 4468 hbrs
c [unhide-2] limit 268427 based on 536854 irredundant clauses
c [unhide-2-2] 0 units, 182 failed, 4972 tauts, 0 hbrs, 4862 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 73321 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 10126 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 943 clauses out of 1805 (52%) of length 9
c [cce-1-1] eliminated 365 clauses out of 801 (46%) of length 8
c [cce-1-1] eliminated 2717 clauses out of 3454 (79%) of length 7
c [cce-1-1] eliminated 6176 clauses out of 7509 (82%) of length 6
c [cce-1-1] eliminated 21075 clauses out of 37562 (56%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 31276 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 336767 clauses = 242077 binary + 94690 ternary
c [cce-1] tried to eliminate 3658 small clauses 1%
c [cce-1] eliminated 1344 small clauses 0%
c [cce-1] eliminated 1176 binary clauses 0%
c [cce-1] eliminated 168 ternary clauses 0%
c [cce-1-1] eliminated 1344 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 32620 covered clauses in round 1
c [cce-1] eliminated 32620 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 73321 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 13234 not tried 18% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 13194 = 18% variables out of 73321
c [bca-1] limit of 10000000 steps
c [bca-1] 117603 out of 120256 literals actually usable 98%
c [bca-1] added 1475 blocked clauses in 313856 steps
c [phase-2] phase bias: 188 positive 48%, 203 negative 52%
c [simplification-2] removed 17253 variables 22.3% (60127 remain 25%)
c [simplification-2] removed 197403 irredundant clauses 31.5% (429389 remain 37%)
c [simplification-2] maximum reduction of 31% = max (22%, 31%)
c [simplification-2] large reduction 31% >= 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 4183
c [tabula-rasa-1] number variables 60127 drops below limit 60722
c [tabula-rasa-1] number clauses 429389 drops below limit 584905
c [flush-cache] 0 binary, 0 ternary, 422 large
c [flushphases] 60127 phases reset fully
c [phase-3] phase bias: 2338 positive 24%, 7383 negative 76%
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 15031 and clause limit 214694
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   24.7   60126   429389      2188       4    356 16466  17 13.8 174.0   35
c i   24.7   60122   429389      2198      11    358 16466  25 13.8 174.5   35
c i   24.8   59954   429389      2206      17    358 16467  24 13.7 175.2   35
c R   24.8   59946   429389      2304      98    363 16469  16 13.8 175.4   35
c i   24.8   59945   429389      2325     116    363 16470  10 13.7 174.7   35
c i   24.9   59362   429389      2387     167    367 16474   4 13.8 175.9   35
c i   25.0   59242   429389      2516     267    382 16487   2 13.6 175.6   35
c i   25.1   59234   429389      2620     349    396 16493   4 13.7 182.4   35
c i   25.1   59230   429389      2621     349    396 16493   4 13.7 182.4   35
c i   25.1   59226   429389      2625     351    396 16494   4 13.7 182.1   35
c i   25.1   59221   429389      2626     351    396 16494   3 13.7 181.9   35
c i   25.1   59215   429389      2633     354    397 16496   3 13.7 181.7   35
c i   25.1   59210   429389      2634     354    397 16496   2 13.6 181.6   35
c i   25.1   59205   429389      2643     360    397 16498   2 13.6 181.6   35
c i   25.1   59165   429389      2660     371    399 16501   2 13.5 181.3   35
c i   25.1   59154   429389      2665     375    399 16501   2 13.5 181.4   35
c i   25.1   59147   429389      2713     413    399 16501   2 13.5 182.0   35
c i   25.2   59141   429389      2714     413    399 16501   2 13.5 182.0   35
c i   25.2   59135   429389      2719     417    399 16501   2 13.5 181.9   35
c i   25.2   59124   429389      2744     435    400 16505   2 13.5 182.6   35
c i   25.2   59118   429389      2745     435    400 16505   2 13.5 182.4   35
c i   25.2   59112   429389      2756     442    401 16507   2 13.4 182.9   35
c i   25.3   59111   429389      2885     549    410 16518   2 13.2 181.6   35
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   25.3   59103   429389      2911     569    412 16521   2 13.1 182.0   35
c i   25.3   58846   429389      2928     575    415 16527   2 13.1 181.7   35
c i   25.3   58842   429389      2984     617    423 16529   2 13.0 180.3   35
c i   25.4   58833   429389      3082     701    428 16533   2 12.9 180.9   35
c i   25.4   58827   429389      3137     745    430 16537   3 12.8 180.4   35
c i   25.4   58820   429389      3150     751    431 16542   2 12.8 180.1   35
c i   25.5   58811   429389      3170     768    432 16543   2 12.7 179.7   35
c i   25.5   58806   429389      3304     882    437 16551   2 13.7 179.8   35
c i   25.6   58687   429389      3386     954    439 16557   3 13.6 180.3   35
c i   25.7   58684   429389      3553    1082    449 16574   2 13.9 177.7   35
c i   25.7   58675   429389      3579    1100    450 16580   2 13.8 179.2   35
c i   25.7   58671   429389      3596    1109    451 16585   1 13.8 178.9   35
c i   25.7   58662   429389      3617    1126    452 16587   2 13.7 178.8   35
c i   25.8   58655   429389      3643    1148    454 16588   2 13.7 178.4   35
c i   25.8   58650   429389      3725    1217    457 16589   2 13.6 182.1   35
c i   25.9   58639   429389      3785    1263    463 16596   1 13.5 184.3   35
c i   25.9   58631   429389      3795    1268    464 16598   1 13.5 184.6   35
c i   25.9   58625   429389      3799    1271    464 16598   1 13.5 184.8   35
c i   25.9   58617   429389      3812    1278    466 16601   1 13.5 184.6   35
c i   26.0   58612   429389      3828    1291    467 16602   1 13.5 184.3   35
c i   26.0   58607   429389      3923    1363    477 16609   3 13.4 183.3   36
c i   26.0   58515   429389      3944    1377    479 16613   3 13.3 183.2   36
c i   26.0   58508   429389      3945    1377    479 16613   2 13.3 183.1   36
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   26.1   58501   429389      3969    1384    480 16628   2 13.2 183.7   36
c i   26.1   58497   429389      3971    1384    480 16629   1 13.2 183.6   36
c i   26.1   58492   429389      3983    1392    482 16629   1 13.2 183.2   36
c i   26.1   58486   429389      3984    1392    482 16629   1 13.2 183.1   36
c i   26.1   58479   429389      3985    1392    482 16629   1 13.2 183.0   36
c i   26.1   58470   429389      4007    1409    484 16631   1 13.2 183.8   36
c i   26.1   58463   429389      4008    1409    484 16631   1 13.2 183.6   36
c i   26.1   58457   429389      4009    1409    484 16631   1 13.2 183.5   36
c i   26.1   58452   429389      4010    1409    484 16631   1 13.2 183.4   36
c i   26.1   58447   429389      4011    1409    484 16631   1 13.2 183.4   36
c i   26.2   58445   429389      4114    1453    496 16669   2 12.9 182.3   36
c i   26.2   58304   429389      4134    1464    498 16675   2 12.9 182.1   36
c i   26.2   58299   429389      4146    1471    499 16678   2 12.9 182.0   36
c i   26.2   58240   429389      4169    1484    504 16682   3 12.8 181.8   36
c i   26.2   58232   429389      4170    1484    504 16682   3 12.8 181.8   36
c i   26.2   58122   429389      4194    1500    509 16684   2 12.8 181.8   36
c i   26.2   58116   429389      4202    1505    510 16685   2 12.7 181.5   36
c i   26.3   58111   429389      4243    1530    512 16697   2 12.7 181.6   36
c i   26.3   58103   429389      4256    1540    513 16698   1 12.7 181.6   36
c i   26.3   58094   429389      4264    1544    515 16699   1 12.6 181.6   36
c i   26.3   58087   429389      4287    1561    516 16703   2 12.6 181.1   36
c i   26.4   58081   429389      4413    1664    521 16710   3 12.9 183.7   36
c i   26.6   58077   429389      4819    1949    550 16750   2 14.9 188.2   36
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   26.7   58076   429389      4982    2097    552 16750   4 15.0 188.6   36
c i   26.7   58075   429389      4990    2101    555 16750   3 15.0 188.6   36
c i   26.7   58067   429389      4997    2107    555 16750   2 15.0 188.7   36
c R   26.8   58062   429389      5247    2320    572 16760   3 15.1 189.4   36
c i   26.8   58061   429389      5258    2326    572 16764   3 15.1 189.1   36
c i   26.9   58023   429389      5300    2344    580 16778   2 15.0 188.1   36
c i   27.0   58018   429389      5554    2540    596 16798   3 15.0 186.0   36
c i   27.1   58013   429389      5693    2639    608 16819   2 14.8 184.0   36
c i   27.1   58008   429389      5715    2656    611 16820   2 14.8 183.6   36
c 
c [simplification-3] limit of 5830 conflicts hit after 5830 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 58000 free variables schedulable
c [ternres-1] 523 ternary resolvents (2 bin, 521 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 10785 at-most-one constraints of average size 4.4
c [card-2] found 468 at-most-two constraints of average size 4.8
c [card-2] using previous limit 1000000 for elimination
c [card-2] 11228 out of 11253 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 154 xors of average arity 2.3
c [gauss-1] connected 354 occurrences of 243 variables (average 1.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-6] removed 173 variables
c [gauss-1] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 45118 literals 39%
c [treelook-2] scheduling used 370721 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 307880 steps
c [treelook-2] 45107 literals remain 39%
c [treelook-2] 27565 variables remain to probed next time 48%
c [treelook-2] removed 1 variables, found 2760 hbrs
c [cgrclsr-1] limit 205117 based on 410235 irredundant clauses
c [cgrclsr-1] all 57826 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 894721 with penalty 0 = 0 + 0
c [lift-1] using 48583 probes 84%
c [lift-1] 21 units, 1 impls, 0 eqs in 1 rounds
c [lift-1] 57316 variables remain 100% (8 retained)
c [lift-1] removed 502 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 124, lifted 401
c [unhide-3] limit 298240 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 232 failed, 13906 tauts, 0 hbrs, 8836 literals
c [transred-1] limit 1491202 with penalty 0 = 0 + 0
c [transred-1] removed 219 transitive binary clauses
c [transred-1] found 4 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 55971 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 367 blocked clauses
c [block-2] 367 < 1/1000 * 387006 = 387 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 369 (0%) of length 7
c [cce-2-1] eliminated 6 clauses out of 1570 (0%) of length 6
c [cce-2-1] eliminated 1 clauses out of 13839 (0%) of length 5
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 8 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 248596 clauses = 178843 binary + 69753 ternary
c [cce-2] tried to eliminate 637 small clauses 0%
c [cce-2] eliminated 278 small clauses 0%
c [cce-2] eliminated 220 binary clauses 0%
c [cce-2] eliminated 58 ternary clauses 0%
c [cce-2-1] eliminated 278 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 286 covered clauses in round 1
c [cce-2] eliminated 286 covered clauses in TOTAL during 1 rounds
c [cce-2] 286 < 1/1000 * 382193 = 382 considered unsuccessful
c [elim-3] 12880 variables 23% will be scheduled this time
c [elim-3] scheduled 12880 variables 23%
c [elim-3] limit of 29824042 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 995 variables 2% in round 1 in 23116034 steps
c [elim-3-1] backward subsumption/strengthening limit 6708008
c [elim-3-1] subsumed 120 and strengthened 5 clauses in 6708009 steps
c [elim-3] incomplete 240 not tried 0% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 1021 = 2% variables out of 55922
c [bca-2] limit of 10000000 steps
c [bca-2] 100249 out of 109804 literals actually usable 91%
c [bca-2] added 34 blocked clauses in 253142 steps
c [phase-4] phase bias: 39 positive 91%, 4 negative 9%
c [simplification-3] removed 3099 variables 5.3% (54901 remain 23%)
c [simplification-3] removed 50937 irredundant clauses 11.9% (378452 remain 32%)
c [simplification-3] maximum reduction of 12% = max (5%, 12%)
c [simplification-3] large reduction 12% >= 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 7830
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   31.9   54900   378452      6029    2749    960 55476   1 14.8 179.9   34
c i   31.9   54895   378452      6031    2749    960 55477   1 14.8 179.9   34
c i   31.9   54884   378452      6032    2749    960 55477   1 14.8 179.9   34
c i   31.9   54874   378452      6047    2755    965 55480   1 14.8 179.6   34
c i   31.9   54791   378452      6217    2896    968 55488   3 15.0 179.7   34
c i   31.9   54786   378452      6225    2901    970 55488   3 15.0 179.6   34
c i   32.0   54778   378452      6246    2911    974 55494   3 14.9 179.3   34
c i   32.0   54769   378452      6249    2911    974 55496   2 14.9 179.3   34
c i   32.0   54764   378452      6251    2912    974 55496   2 14.9 179.3   34
c i   32.0   54760   378452      6274    2931    974 55499   2 14.9 178.9   34
c i   32.0   54753   378452      6276    2932    974 55499   2 14.9 178.9   34
c i   32.0   54752   378452      6325    2964    977 55511   2 14.8 178.4   34
c i   32.0   54750   378452      6364    2993    977 55517   2 14.9 178.3   34
c i   32.0   54748   378452      6411    3029    983 55521   3 14.8 178.8   34
c i   32.1   54745   378452      6443    3049    987 55528   2 14.7 178.3   34
c i   32.1   54721   378452      6560    3135   1002 55540   2 14.6 177.7   34
c i   32.1   54706   378452      6579    3143   1003 55549   1 14.6 177.3   34
c i   32.2   54512   378452      6659    3197   1015 55561   2 14.5 176.6   34
c i   32.2   54511   378452      6667    3199   1016 55564   2 14.5 176.6   34
c i   32.2   54456   378452      6674    3203   1017 55565   2 14.5 176.5   34
c i   32.2   54452   378452      6686    3209   1020 55567   2 14.4 176.4   34
c i   32.2   54446   378452      6689    3211   1020 55567   2 14.4 176.3   34
c i   32.2   54441   378452      6691    3212   1020 55567   2 14.4 176.3   34
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   32.2   54439   378452      6692    3212   1020 55567   2 14.4 176.3   34
c i   32.2   54431   378452      6693    3212   1020 55567   2 14.4 176.3   34
c i   32.2   54427   378452      6698    3212   1021 55570   2 14.4 176.2   34
c i   32.2   54423   378452      6699    3212   1021 55570   2 14.4 176.2   34
c i   32.2   54420   378452      6704    3213   1023 55571   2 14.4 176.1   34
c i   32.2   54414   378452      6705    3213   1023 55571   1 14.4 176.0   34
c i   32.3   54409   378452      6819    3299   1030 55590   3 14.3 174.7   34
c i   32.4   54352   378452      6838    3315   1030 55591   3 14.3 174.6   34
c i   32.4   54347   378452      6839    3315   1030 55591   3 14.3 174.6   34
c i   32.4   54341   378452      6926    3371   1040 55606   2 14.1 173.8   34
c i   32.5   54332   378452      6984    3412   1048 55614   2 14.1 173.6   34
c i   32.5   54328   378452      6985    3412   1048 55614   2 14.1 173.6   34
c i   32.5   54098   378452      7044    3457   1053 55618   2 14.0 173.4   34
c i   32.6   54094   378452      7488    3754   1086 55699   4 13.9 172.9   34
c i   32.7   54053   378452      7588    3811   1102 55721   2 13.7 172.0   34
c i   32.8   54049   378452      7726    3911   1114 55744   3 13.6 171.9   34
c i   32.9   54042   378452      7828    3984   1121 55762   2 13.5 171.1   34
c i   32.9   53974   378452      7887    4029   1126 55765   2 13.4 171.2   34
c i   33.0   53973   378452      7983    4088   1144 55781   2 13.3 171.7   34
c i   33.0   53922   378452      8022    4113   1148 55788   2 13.3 171.6   34
c i   33.0   53917   378452      8031    4118   1150 55789   2 13.3 171.6   34
c i   33.0   53914   378452      8041    4123   1152 55791   2 13.2 171.5   34
c i   33.0   53847   378452      8042    4123   1152 55791   2 13.2 171.4   34
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   33.0   53842   378452      8050    4127   1153 55793   2 13.2 171.3   34
c i   33.0   53822   378452      8156    4210   1158 55810   2 13.1 170.6   34
c i   33.2   53821   378452      8322    4319   1179 55832   2 13.0 169.4   34
c i   33.3   53816   378452      8629    4539   1218 55863   2 12.8 170.3   34
c i   33.4   53768   378452      8683    4567   1229 55872   2 12.7 170.1   34
c i   33.4   53665   378452      8684    4567   1229 55872   2 12.7 170.1   34
c i   33.4   53656   378452      8685    4567   1229 55872   2 12.7 170.1   34
c i   33.5   53649   378452      8805    4642   1253 55891   2 12.6 169.0   34
c i   33.5   53644   378452      8806    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53638   378452      8807    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53633   378452      8808    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53627   378452      8809    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53620   378452      8810    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53614   378452      8811    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53606   378452      8812    4642   1253 55891   2 12.6 168.9   34
c i   33.5   53601   378452      8835    4657   1259 55892   2 12.6 168.7   34
c i   33.6   53597   378452      9100    4840   1296 55923   2 12.4 168.3   34
c i   33.7   53593   378452      9367    5034   1327 55956   3 12.2 167.7   34
c i   33.7   53562   378452      9369    5035   1327 55956   3 12.2 167.7   34
c i   33.8   53561   378452      9501    5131   1340 55972   3 12.2 167.6   34
c i   33.9   53559   378452      9639    5222   1357 55996   2 12.2 169.4   34
c i   33.9   53472   378452      9655    5231   1358 56000   2 12.2 169.4   34
c i   34.0   53470   378452      9752    5298   1371 56007   2 12.2 171.2   34
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.0   53442   378452      9825    3364   1378 56013   4 12.1 171.1   34
c i   34.0   53441   378452      9864    3389   1386 56017   2 12.1 171.8   34
c i   34.0   53435   378452      9870    3393   1386 56018   2 12.1 171.8   34
c i   34.1   53430   378452      9892    3410   1386 56022   3 12.1 171.7   34
c i   34.1   53424   378452      9970    3461   1395 56038   2 12.1 171.6   34
c i   34.2   53323   378452     10133    3564   1406 56070   2 12.1 170.7   34
c 
c [simplification-4] limit of 10408 conflicts hit after 10409 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 53317 free variables schedulable
c [ternres-2] 110 ternary resolvents (0 bin, 110 trn)
c [ternres-2] 27654 variables remain 52% (25663 retained)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 711 xors of average arity 2.1
c [gauss-2] connected 1488 occurrences of 813 variables (average 1.8)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-9] removed 536 variables
c [gauss-2] exported 0 unary, 17 binary and 0 ternary equations
c [basicprobe-2] limit 2285294 penalty 0 = 0 + 0
c [basicprobe-2-0] 13020 probes remain 25% after last round
c [basicprobe-2-0] 27 units = 27 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 282 variables, found 12691 hbrs
c [bate-1] eliminated 12 asymmetric tautologies during probing
c [lift-2] limit 1371176 with penalty 0 = 0 + 0
c [lift-2] using 45109 probes 86%
c [lift-2] 13 units, 5 impls, 0 eqs in 1 rounds
c [lift-2] 52459 variables remain 100% (21 retained)
c [lift-2] removed 19 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 78, lifted 159
c [unhide-4] limit 457058 with penalty 0 = 0 + 0
c [unhide-4-4] 71 units, 263 failed, 21065 tauts, 0 hbrs, 3082 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 316 transitive binary clauses
c [transred-2] found 7 units
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 51343 variables 100%
c [elim-4] limit of 45705890 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 2392 variables 5% in round 1 in 32797658 steps
c [elim-4-1] backward subsumption/strengthening limit 12908232
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 11286721 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2455 = 5% variables out of 51343
c [bca-3] limit of 10000000 steps
c [bca-3] 87118 out of 97778 literals actually usable 89%
c [bca-3] added 122 blocked clauses in 217767 steps
c [rephase-1] after 10409 conflicts (new increment 20000, next 30409)
c [flushphases] 6 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 4429 variables 8.3% (48888 remain 20%)
c [simplification-4] removed 31748 irredundant clauses 8.4% (346704 remain 30%)
c [simplification-4] maximum reduction of 8% = max (8%, 8%)
c [simplification-4] large reduction 8% >= 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 12409
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   37.5   48887   346704     10512    3068   1181 68074   3 12.8 170.8   32
c i   37.6   48881   346704     10685    3204   1193 68090   6 13.0 171.9   32
c i   37.6   48875   346704     10710    3223   1195 68091   5 13.0 172.1   32
c i   37.6   48869   346704     10716    3226   1197 68091   5 13.0 172.1   32
c i   37.7   48862   346704     11323    3751   1225 68097   3 13.7 172.5   32
c i   37.7   48824   346704     11364    3786   1228 68098   4 13.7 172.4   32
c R   37.8   48823   346704     11757    4120   1232 68103   5 14.2 172.2   33
c i   37.9   48822   346704     11956    4286   1247 68118   3 14.1 171.5   33
c i   38.0   48819   346704     12008    4325   1254 68122   2 14.1 171.1   33
c i   38.0   48817   346704     12033    4344   1256 68125   2 14.1 171.0   33
c i   38.0   48808   346704     12035    4344   1256 68126   2 14.1 171.0   33
c i   38.0   48801   346704     12041    4347   1257 68127   2 14.1 171.0   33
c i   38.0   48796   346704     12054    4353   1258 68131   2 14.1 171.0   33
c i   38.2   48795   346704     12367    4621   1277 68144   3 14.2 170.3   33
c i   38.2   48791   346704     12389    4636   1281 68146   3 14.2 170.2   33
c i   38.2   48786   346704     12398    4641   1282 68147   3 14.2 170.2   33
c i   38.2   48782   346704     12413    4653   1283 68147   3 14.2 170.1   33
c i   38.2   48778   346704     12478    4688   1295 68160   3 14.1 169.9   33
c i   38.3   48638   346704     12497    4701   1295 68163   2 14.2 169.8   33
c i   38.4   48630   346704     12800    4942   1306 68188   5 14.4 169.9   33
c i   38.4   48625   346704     12868    4992   1312 68198   3 14.3 169.5   33
c i   38.5   48621   346704     12946    5062   1314 68201   2 14.5 169.4   33
c i   38.5   48615   346704     12997    5099   1324 68204   2 14.5 169.4   33
c 
c [simplification-5] limit of 13117 conflicts hit after 13117 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 25213 schedulable variables 52%
c [ternres-3] 314 ternary resolvents (0 bin, 314 trn)
c [ternres-3] 1178 variables remain 2% (47432 retained)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 54 xors of average arity 2.6
c [gauss-3] connected 138 occurrences of 98 variables (average 1.4)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-11] removed 56 variables
c [gauss-3] exported 0 unary, 2 binary and 0 ternary equations
c [cgrclsr-2] limit 172296 based on 344592 irredundant clauses
c [cgrclsr-2] all 48554 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 1581247 with penalty 0 = 0 + 0
c [lift-3] using 42226 probes 87%
c [lift-3] 19 units, 13 impls, 0 eqs in 1 rounds
c [lift-3] 48498 variables remain 100% (37 retained)
c [lift-3] removed 19 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 3, lifted 51
c [unhide-5] limit 527082 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 382 failed, 8842 tauts, 0 hbrs, 7457 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 261 transitive binary clauses
c [transred-3] found 8 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 48035 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 29 blocked clauses
c [block-3] 29 < 1/1000 * 335474 = 335 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 75
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 65
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 64
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 63
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 62
c [cce-3-1] eliminated 3 clauses out of 4 (75%) 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 5 (60%) of length 58
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 57
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 56
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 55
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 54
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 53
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 52
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 51
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 50
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 49
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 48
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 47
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 46
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 45
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 44
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 43
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 39
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 37
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 35
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 34
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 33
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 29
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 26
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 25
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 24
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 23
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 21
c [cce-3-1] eliminated 4 clauses out of 7 (57%) of length 20
c [cce-3-1] eliminated 7 clauses out of 8 (88%) of length 19
c [cce-3-1] eliminated 5 clauses out of 8 (62%) of length 18
c [cce-3-1] eliminated 7 clauses out of 8 (88%) of length 17
c [cce-3-1] eliminated 5 clauses out of 8 (62%) of length 16
c [cce-3-1] eliminated 7 clauses out of 8 (88%) of length 15
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 14
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 13
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 12
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 11
c [cce-3-1] eliminated 19 clauses out of 22 (86%) of length 10
c [cce-3-1] eliminated 9 clauses out of 32 (28%) of length 9
c [cce-3-1] eliminated 8 clauses out of 100 (8%) of length 8
c [cce-3-1] eliminated 15 clauses out of 241 (6%) of length 7
c [cce-3-1] eliminated 18 clauses out of 1425 (1%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 334 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 229868 clauses = 154225 binary + 75643 ternary
c [cce-3] tried to eliminate 232 small clauses 0%
c [cce-3] eliminated 70 small clauses 0%
c [cce-3] eliminated 65 binary clauses 0%
c [cce-3] eliminated 5 ternary clauses 0%
c [cce-3-1] eliminated 70 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 404 covered clauses in round 1
c [cce-3] eliminated 404 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 48035 variables 100%
c [elim-5] limit of 52708234 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 850 variables 2% in round 1 in 29972056 steps
c [elim-5-1] backward subsumption/strengthening limit 22736178
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 10542206 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 855 = 2% variables out of 48035
c [bca-4] limit of 10000000 steps
c [bca-4] 81730 out of 94362 literals actually usable 87%
c [bca-4] added 47 blocked clauses in 202127 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 1430 variables 2.9% (47180 remain 19%)
c [simplification-5] removed 16832 irredundant clauses 4.9% (329872 remain 28%)
c [simplification-5] maximum reduction of 5% = max (3%, 5%)
c [simplification-5] large reduction 5% >= 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 15117
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   42.4   47179   329872     13184    4297   1558 77199   3 14.7 168.9   32
c i   42.8   47172   329872     14123    5103   1588 77228   2 17.1 173.1   34
c i   42.8   47169   329872     14126    5104   1588 77229   2 17.1 173.0   34
c i   42.8   47163   329872     14134    5108   1590 77229   2 17.1 173.0   34
c i   42.8   47097   329872     14140    5112   1591 77229   2 17.1 173.0   34
c i   42.9   47072   329872     14250    5193   1605 77235   3 17.2 172.9   34
c i   42.9   47068   329872     14251    5193   1605 77235   3 17.2 172.8   34
c i   42.9   47064   329872     14252    5193   1605 77235   3 17.2 172.8   34
c i   43.0   47059   329872     14426    5336   1613 77250   3 17.2 172.4   34
c i   43.1   47053   329872     14503    5399   1620 77251   3 17.2 172.2   34
c i   43.1   47051   329872     14578    5465   1622 77256   2 17.2 171.8   34
c i   43.1   47047   329872     14579    5465   1622 77256   2 17.2 171.8   34
c i   43.1   47043   329872     14599    5478   1624 77260   3 17.2 171.7   34
c i   43.2   47040   329872     14659    5515   1627 77278   1 17.2 171.3   34
c i   43.3   47037   329872     14663    5517   1628 77278   1 17.2 171.2   34
c i   43.3   47036   329872     14666    5519   1628 77278   1 17.2 171.2   34
c i   43.3   47030   329872     14681    5531   1628 77280   1 17.1 171.2   34
c i   43.3   47023   329872     14682    5531   1628 77280   1 17.1 171.2   34
c i   43.3   47017   329872     14702    5545   1631 77282   2 17.1 171.1   34
c i   43.4   47011   329872     15052    5805   1648 77299   3 17.5 171.2   34
c i   43.4   47010   329872     15053    5805   1648 77299   3 17.5 171.2   34
c i   43.4   47005   329872     15054    5805   1648 77299   3 17.5 171.1   34
c i   43.5   46996   329872     15137    5866   1651 77312   3 17.5 170.7   34
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   43.5   46995   329872     15172    5889   1655 77314   2 17.4 170.6   34
c i   43.6   46919   329872     15399    6075   1669 77330   4 17.5 170.3   34
c i   43.7   46917   329872     15577    6222   1671 77337   3 17.8 170.5   34
c 
c [simplification-6] limit of 15957 conflicts hit after 15960 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 1142 schedulable variables 2%
c [ternres-4] 45 ternary resolvents (0 bin, 45 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 8193 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 8193 out of 8193 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 57 xors of average arity 2.6
c [gauss-4] connected 148 occurrences of 118 variables (average 1.3)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 34 variables
c [simpleprobe-3] 801 schedulable variables 2%
c [simpleprobe-3] limit 6208134 penalty 1 = 1 + 0
c [decomp-14] removed 56 variables
c [simpleprobe-3] 1836 variables remain 4% (44986 retained)
c [simpleprobe-3] removed 56 variables, found 8476 hbrs, 23 units
c [lift-4] limit 1862440 with penalty 0 = 0 + 0
c [lift-4] using 41004 probes 88%
c [lift-4] 47 units, 10 impls, 101 eqs in 1 rounds
c [lift-4] 46612 variables remain 100% (57 retained)
c [lift-4] removed 153 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 10, lifted 24
c [unhide-6] limit 620813 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 109 failed, 8474 tauts, 0 hbrs, 21764 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 324 transitive binary clauses
c [transred-4] found 5 units
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 74
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 18
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 16
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 14
c [cce-4-1] eliminated 1 clauses out of 225 (0%) of length 7
c [cce-4-1] eliminated 12 clauses out of 1336 (1%) of length 6
c [cce-4-1] eliminated 19 clauses out of 11355 (0%) of length 5
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 40 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 211174 clauses = 150313 binary + 60861 ternary
c [cce-4] tried to eliminate 870 small clauses 0%
c [cce-4] eliminated 346 small clauses 0%
c [cce-4] eliminated 290 binary clauses 0%
c [cce-4] eliminated 56 ternary clauses 0%
c [cce-4-1] eliminated 3231 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 3271 covered clauses in round 1
c [cce-4] eliminated 3271 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 46320 variables 100%
c [elim-6] limit of 62081343 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 958 variables 2% in round 1 in 34143132 steps
c [elim-6-1] backward subsumption/strengthening limit 27938211
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 10351518 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 969 = 2% variables out of 46320
c [bca-5] limit of 10000000 steps
c [bca-5] 76483 out of 90704 literals actually usable 84%
c [bca-5] added 76 blocked clauses in 189106 steps
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 1561 variables 3.3% (45351 remain 19%)
c [simplification-6] removed 10082 irredundant clauses 3.1% (319790 remain 27%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 25000
c [simplification-6] penalized conflict interval 25000 = 1 * 25000
c [simplification-6] new conflict limit 40960
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   48.1   45350   319790     16680    6384   1708 77446   5 19.3 170.0   36
c -   48.1   45350   319790     16930    4041   1708 77447   4 20.3 169.9   34
c i   48.2   45349   319790     17032    4126   1708 77449   3 20.4 169.7   35
c i   48.4   45344   319790     17257    4310   1729 77460   2 20.2 169.4   35
c i   48.4   45152   319790     17294    4341   1730 77462   3 20.2 169.3   35
c i   48.4   45148   319790     17334    4379   1730 77463   4 20.2 169.3   35
c i   48.5   45147   319790     17538    4556   1739 77476   4 20.0 168.8   35
c i   48.5   45146   319790     17584    4591   1746 77478   3 20.0 168.7   35
c i   48.6   45142   319790     17833    4809   1757 77487   3 19.9 168.5   35
c i   48.6   45140   319790     17862    4837   1757 77487   3 19.9 168.4   35
c i   48.7   45133   319790     18309    5219   1778 77515   4 19.7 167.4   35
c i   48.7   45127   319790     18400    5295   1783 77516   5 19.7 167.4   35
c i   48.7   45124   319790     18407    5297   1783 77520   4 19.7 167.3   35
c i   48.8   45098   319790     18550    5415   1791 77526   4 19.6 166.8   35
c i   48.8   44996   319790     18641    5494   1793 77527   3 19.6 166.6   35
c i   48.8   44991   319790     18646    5497   1793 77528   3 19.6 166.6   35
c i   48.9   44986   319790     18763    5598   1802 77531   4 19.5 166.4   35
c i   49.0   44971   319790     19439    6100   1824 77536   3 20.5 166.1   35
c i   49.1   44968   319790     19619    6252   1838 77545   4 20.5 166.2   35
c i   49.1   44965   319790     19628    6259   1838 77546   3 20.5 166.2   35
c i   49.2   44964   319790     19890    6490   1844 77558   4 20.6 165.9   36
c i   49.4   44919   319790     20614    7075   1868 77583   3 21.0 164.2   36
c i   49.7   44910   319790     21630    7825   1885 77590   4 22.6 165.4   36
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   49.7   44905   319790     21640    7829   1887 77593   4 22.6 165.3   36
c i   49.7   44900   319790     21752    7912   1897 77603   5 22.6 165.3   36
c i   49.7   44894   319790     21753    7912   1897 77603   4 22.6 165.2   36
c i   49.8   44890   319790     21954    8076   1902 77607   3 22.8 165.0   36
c -   49.8   44803   319790     21954    5066   1902 77607   3 22.8 165.0   35
c i   49.8   44802   319790     22025    5116   1905 77617   3 22.7 164.9   35
c i   49.9   44681   319790     22450    5451   1907 77625   4 23.1 165.2   35
c i   50.0   44679   319790     22976    5900   1913 77638   8 23.6 165.4   35
c i   50.1   44674   319790     23904    6590   1916 77645   5 25.4 165.1   36
c i   50.2   44673   319790     23975    6637   1917 77645   5 25.6 165.1   36
c i   50.2   44672   319790     24335    6938   1929 77652   3 25.9 166.0   36
c R   50.7   44671   319790     26122    8141   1951 77674   3 31.8 167.9   38
c i   50.9   44670   319790     26324    8314   1961 77684   2 31.8 167.7   38
c i   50.9   44668   319790     26328    8317   1961 77684   1 31.8 167.7   38
c i   50.9   44662   319790     26337    8323   1962 77685   1 31.8 167.7   38
c i   50.9   44657   319790     26340    8323   1962 77686   1 31.8 167.6   38
c i   50.9   44652   319790     26341    8323   1962 77686   1 31.8 167.6   38
c i   50.9   44649   319790     26342    8323   1962 77686   1 31.8 167.6   38
c i   50.9   44645   319790     26343    8323   1962 77686   1 31.8 167.6   38
c i   50.9   44640   319790     26348    8323   1961 77690   1 31.8 167.6   38
c i   50.9   44637   319790     26349    8323   1961 77690   1 31.8 167.6   38
c i   51.0   44630   319790     26363    8328   1960 77695   1 31.7 167.4   38
c i   51.0   44629   319790     26396    8358   1960 77696   3 31.7 167.3   38
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   51.0   44624   319790     26406    8367   1960 77696   2 31.7 167.2   38
c i   51.0   44615   319790     26429    8387   1961 77697   3 31.7 167.2   38
c i   51.2   44614   319790     26639    8554   1970 77713   3 31.6 167.1   38
c i   51.2   44613   319790     26723    8626   1974 77715   4 31.6 167.1   38
c i   51.2   44612   319790     26757    8649   1978 77716   3 31.6 167.0   38
c i   51.2   44607   319790     26760    8650   1977 77717   3 31.6 167.0   38
c i   51.4   44601   319790     27434    9187   1997 77731   4 31.6 166.0   38
c -   51.5   44595   319790     27594    5834   2003 77738   3 31.5 165.7   35
c i   51.7   44594   319790     27861    6063   2020 77747   3 31.3 165.1   35
c i   51.8   44485   319790     28047    6220   2028 77750   5 31.2 165.0   35
c i   51.8   44484   319790     28226    6365   2034 77756   4 31.5 167.5   35
c i   52.0   44478   319790     28706    6796   2046 77766   4 31.3 167.4   35
c i   52.0   44477   319790     28747    6835   2046 77767   3 31.2 167.3   35
c i   52.3   44472   319790     29482    7482   2071 77786   5 30.8 166.3   36
c i   52.5   44466   319790     29671    7650   2084 77792   3 30.7 166.2   36
c i   52.5   44460   319790     29683    7658   2085 77794   3 30.6 166.2   36
c i   52.5   44455   319790     29684    7658   2085 77794   3 30.6 166.1   36
c i   52.5   44454   319790     29697    7666   2088 77795   3 30.6 166.1   36
c i   52.8   44448   319790     30191    8093   2105 77807   4 30.6 165.6   36
c i   53.2   44445   319790     31452    9123   2143 77856   3 31.3 170.0   37
c i   53.8   44442   319790     32693   10146   2194 77914   2 30.9 169.6   37
c i   53.9   44430   319790     32749   10194   2196 77918   2 30.9 169.5   37
c i   54.0   44262   319790     32898   10318   2203 77922   4 30.8 169.3   38
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   54.0   44257   319790     32899   10318   2203 77922   4 30.8 169.3   38
c i   54.1   44255   319790     33131   10505   2213 77935   3 30.9 169.0   38
c i   54.1   44247   319790     33217   10574   2219 77939   4 30.8 168.9   38
c i   54.2   44244   319790     33402   10723   2222 77942   3 30.9 168.8   38
c -   54.4   44244   319790     33763    6998   2233 77955   3 31.2 169.2   35
c i   54.5   44243   319790     33913    7128   2240 77961   4 31.1 169.0   35
c i   54.5   44238   319790     34043    7244   2243 77963   4 31.1 168.9   35
c i   54.7   44234   319790     34344    7494   2254 77971   3 31.0 168.5   35
c i   54.9   44229   319790     34950    8012   2271 77989   4 30.9 167.8   36
c i   55.0   44225   319790     35027    8073   2279 77994   3 30.9 167.7   36
c i   55.2   44221   319790     35432    8439   2293 78002   3 30.7 167.5   36
c i   55.3   44219   319790     35726    8688   2311 78010   4 30.9 168.3   36
c i   55.4   44214   319790     35748    8702   2313 78015   4 30.9 168.3   36
c i   55.4   44210   319790     35850    8795   2315 78019   3 30.8 168.8   36
c i   55.5   44209   319790     36079    8980   2315 78021   3 31.1 168.9   36
c i   55.5   44207   319790     36087    8985   2317 78021   3 31.1 168.9   36
c i   55.5   44202   319790     36169    9055   2320 78025   4 31.0 169.0   36
c i   55.8   44199   319790     37348   10128   2345 78039   6 31.6 172.1   37
c i   56.5   44194   319790     38648   11142   2378 78062   2 33.9 172.4   38
c i   56.5   44187   319790     38649   11142   2378 78062   2 33.9 172.4   38
c i   56.5   44179   319790     38650   11142   2378 78062   2 33.9 172.4   38
c -   57.2   44129   319790     40336    7964   2427 78098   5 34.2 172.9   35
c i   57.3   44128   319790     40489    8095   2433 78102   4 34.2 172.6   35
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   57.3   44122   319790     40490    8095   2433 78102   4 34.2 172.6   35
c i   57.3   44117   319790     40491    8095   2433 78102   3 34.2 172.6   35
c i   57.3   44112   319790     40507    8105   2435 78102   3 34.2 172.5   35
c i   57.4   44107   319790     40691    8270   2441 78105   3 34.1 172.3   35
c i   57.5   44104   319790     40818    8378   2448 78112   4 34.1 172.1   35
c i   57.6   44100   319790     41273    8786   2462 78130   3 34.0 172.0   36
c i   57.7   44096   319790     41386    8883   2469 78137   3 33.9 172.1   36
c i   57.9   44090   319790     41884    9301   2481 78143   3 33.9 171.7   36
c i   58.2   44032   319790     42641    9969   2505 78165   5 34.0 173.2   36
c i   58.2   44031   319790     42663    9988   2506 78165   4 34.0 173.3   36
c i   58.6   44027   319790     43710   10831   2525 78180   3 34.2 172.5   37
c i   58.7   44022   319790     43836   10938   2528 78182   4 34.2 172.4   37
c 
c [simplification-7] limit of 44418 conflicts hit after 44418 conflicts
c [ternres-5] limit 6606990 with penalty 0 = 0 + 0
c [ternres-5] all 44016 free variables schedulable
c [ternres-5] 370 ternary resolvents (0 bin, 370 trn)
c [ternres-5] 5657 variables remain 13% (38359 retained)
c [decomp-15] removed 1439 variables
c [treelook-3] limit 330349 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 39098 literals 45%
c [treelook-3] scheduling used 334417 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 330349 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 334266 steps
c [treelook-3] 39090 literals remain 45%
c [treelook-3] 18570 variables remain to probed next time 42%
c [treelook-3] removed 1 variables, found 3206 hbrs
c [lift-5] limit 3964194 with penalty 0 = 0 + 0
c [lift-5] using 38923 probes 89%
c [lift-5] 81 units, 15 impls, 0 eqs in 1 rounds
c [lift-5] 43721 variables remain 100% (102 retained)
c [lift-5] removed 88 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 30, lifted 60
c [unhide-7] limit 1321398 with penalty 0 = 0 + 0
c [unhide-7-7] 1 units, 143 failed, 6663 tauts, 0 hbrs, 25081 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 350 transitive binary clauses
c [transred-5] found 6 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 19 (5%) of length 9
c [cce-5-1] eliminated 4 clauses out of 74 (5%) of length 8
c [cce-5-1] eliminated 23 clauses out of 207 (11%) of length 7
c [cce-5-1] eliminated 30 clauses out of 1142 (3%) of length 6
c [cce-5-1] eliminated 31 clauses out of 10416 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 89 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 207218 clauses = 138423 binary + 68795 ternary
c [cce-5] tried to eliminate 529 small clauses 0%
c [cce-5] eliminated 154 small clauses 0%
c [cce-5] eliminated 138 binary clauses 0%
c [cce-5] eliminated 16 ternary clauses 0%
c [cce-5-1] eliminated 2518 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2607 covered clauses in round 1
c [cce-5] eliminated 2607 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 43381 variables 100%
c [elim-7] limit of 132139809 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 1118 variables 3% in round 1 in 34250789 steps
c [elim-7-1] backward subsumption/strengthening limit 68501578
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 9567193 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1121 = 3% variables out of 43381
c [bca-6] limit of 10000000 steps
c [bca-6] 68625 out of 84522 literals actually usable 81%
c [bca-6] added 182 blocked clauses in 173488 steps
c [rephase-2] after 44418 conflicts (new increment 40000, next 84418)
c [flushphases] 0 phases reset
c [simplification-7] removed 1756 variables 4.0% (42260 remain 17%)
c [simplification-7] removed 24436 irredundant clauses 7.6% (295354 remain 25%)
c [simplification-7] maximum reduction of 8% = max (4%, 8%)
c [simplification-7] large reduction 8% >= 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 46418
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   63.4   42259   295354     44710    9672   2453 88084   3 34.2 172.2   36
c i   63.5   42258   295354     44879    9818   2454 88092   3 34.1 172.0   36
c i   63.5   42253   295354     44892    9826   2454 88093   3 34.1 171.9   36
c i   63.6   42248   295354     45043    9958   2457 88098   3 34.0 171.9   36
c i   63.6   42247   295354     45044    9958   2457 88098   3 34.0 171.9   36
c i   63.6   42244   295354     45045    9958   2457 88098   3 34.0 171.9   36
c i   63.6   42243   295354     45151   10046   2459 88103   5 34.1 171.9   36
c i   63.9   42241   295354     45720   10437   2468 88118   3 34.6 172.3   36
c 
c [simplification-8] limit of 46758 conflicts hit after 46758 conflicts
c [ternres-6] limit 6942481 with penalty 0 = 0 + 0
c [ternres-6] 5448 schedulable variables 13%
c [ternres-6] 271 ternary resolvents (1 bin, 270 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] extracted 20 xors of average arity 2.9
c [gauss-5] connected 58 occurrences of 55 variables (average 1.1)
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 55 variables
c [basicprobe-3] limit 6942481 penalty 0 = 0 + 0
c [basicprobe-3-0] 10060 probes remain 24% after last round
c [basicprobe-3-0] 92 units = 92 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 191 variables, found 36692 hbrs
c [bate-2] eliminated 72 asymmetric tautologies during probing
c [cgrclsr-3] limit 173562 penalty 2 = 2 + 0
c [cgrclsr-3] all 41992 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-6] limit 4165489 with penalty 0 = 0 + 0
c [lift-6] using 37264 probes 89%
c [lift-6] 128 units, 6 impls, 1 eqs in 1 rounds
c [lift-6] 41707 variables remain 100% (146 retained)
c [lift-6] removed 139 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 15, lifted 96
c [unhide-8] limit 1388496 with penalty 0 = 0 + 0
c [unhide-8-8] 5 units, 129 failed, 14348 tauts, 0 hbrs, 9729 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 219 transitive binary clauses
c [transred-6] found 7 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 41478 variables 100%
c [block-4] limit of 17356204 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 36 blocked clauses
c [block-4] 36 < 1/1000 * 290456 = 290 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 74
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 73
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 72
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 71
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 70
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 69
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 68
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 67
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 66
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 65
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 64
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 63
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 62
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 61
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 59
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 58
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 57
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 56
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 55
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 54
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 53
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 52
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 51
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 50
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 49
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 48
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 47
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 46
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 45
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 44
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 43
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 42
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 41
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 40
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 39
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 38
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 37
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 36
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 35
c [cce-6-1] eliminated 4 clauses out of 8 (50%) of length 34
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-6-1] eliminated 4 clauses out of 9 (44%) of length 32
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-6-1] eliminated 4 clauses out of 8 (50%) of length 30
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 29
c [cce-6-1] eliminated 4 clauses out of 9 (44%) of length 28
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 27
c [cce-6-1] eliminated 5 clauses out of 10 (50%) of length 26
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 25
c [cce-6-1] eliminated 5 clauses out of 11 (45%) of length 24
c [cce-6-1] eliminated 9 clauses out of 11 (82%) of length 23
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 22
c [cce-6-1] eliminated 9 clauses out of 11 (82%) of length 21
c [cce-6-1] eliminated 6 clauses out of 13 (46%) of length 20
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 19
c [cce-6-1] eliminated 8 clauses out of 15 (53%) of length 18
c [cce-6-1] eliminated 10 clauses out of 13 (77%) of length 17
c [cce-6-1] eliminated 8 clauses out of 15 (53%) of length 16
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 15
c [cce-6-1] eliminated 8 clauses out of 14 (57%) of length 14
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 13
c [cce-6-1] eliminated 8 clauses out of 15 (53%) of length 12
c [cce-6-1] eliminated 12 clauses out of 16 (75%) of length 11
c [cce-6-1] eliminated 9 clauses out of 15 (60%) of length 10
c [cce-6-1] eliminated 11 clauses out of 30 (37%) of length 9
c [cce-6-1] eliminated 9 clauses out of 82 (11%) of length 8
c [cce-6-1] eliminated 13 clauses out of 189 (7%) of length 7
c [cce-6-1] eliminated 12 clauses out of 1081 (1%) of length 6
c [cce-6-1] eliminated 1 clauses out of 10071 (0%) of length 5
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 377 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 188084 clauses = 134654 binary + 53430 ternary
c [cce-6] tried to eliminate 648 small clauses 0%
c [cce-6] eliminated 182 small clauses 0%
c [cce-6] eliminated 155 binary clauses 0%
c [cce-6] eliminated 27 ternary clauses 0%
c [cce-6-1] eliminated 182 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 559 covered clauses in round 1
c [cce-6] eliminated 559 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 41477 variables 100%
c [elim-8] limit of 138849639 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 463 variables 1% in round 1 in 29089911 steps
c [elim-8-1] backward subsumption/strengthening limit 58179822
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 9169599 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 463 = 1% variables out of 41477
c [bca-7] limit of 10000000 steps
c [bca-7] 65675 out of 82030 literals actually usable 80%
c [bca-7] added 29 blocked clauses in 166586 steps
c [simplification-8] removed 1224 variables 2.9% (41014 remain 17%)
c [simplification-8] removed 9029 irredundant clauses 3.1% (286325 remain 24%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-8] new conflict interval 31250
c [simplification-8] penalized conflict interval 31250 = 1 * 31250
c [simplification-8] new conflict limit 78008
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   69.1   41013   286325     46956   10741   2733 113750   3 34.2 171.0   36
c i   69.1   41012   286325     46962   10744   2735 113750   3 34.2 171.0   36
c i   69.3   41010   286325     47450   11153   2755 113768   4 34.1 170.6   37
c i   69.5   41007   286325     48273   11796   2764 113775   5 35.3 171.1   37
c i   69.7   41006   286325     48864   12148   2768 113779   5 35.9 171.1   37
c -   70.2   40999   286325     50635    8493   2780 113782   5 37.9 173.1   35
c i   70.6   40998   286325     52522   10113   2803 113803   6 39.3 176.2   37
c i   71.4   40993   286325     55727   12644   2820 113814   4 48.0 180.3   43
c i   71.5   40984   286325     56251   13073   2835 113822   5 48.3 180.6   44
c R   71.7   40983   286325     57470   14040   2874 113853   7 47.8 180.2   44
c -   72.1   40983   286325     58310    9237   2887 113882   5 47.4 179.0   35
c i   72.2   40982   286325     58518    9429   2891 113889   3 47.3 179.0   35
c i   72.4   40978   286325     58770    9653   2899 113896   4 47.3 178.7   35
c i   72.4   40975   286325     58906    9779   2901 113898   5 47.2 178.5   35
c i   72.4   40969   286325     58907    9779   2901 113898   5 47.2 178.5   35
c i   73.1   40967   286325     60292   11051   2937 113936   3 46.8 178.3   36
c i   73.7   40966   286325     61451   12017   2979 113997   3 46.3 177.2   37
c i   73.9   40965   286325     62033   12513   2995 114019   6 46.3 177.1   37
c i   74.2   40962   286325     63001   13252   3034 114042   3 46.4 176.7   37
c i   74.7   40952   286325     64201   14248   3073 114071   3 45.9 176.0   37
c i   74.8   40944   286325     64398   14411   3080 114076   3 45.9 175.8   37
c i   74.8   40943   286325     64399   14411   3080 114076   3 45.9 175.8   37
c i   75.2   40942   286325     65399   15129   3106 114107   3 45.7 175.2   38
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   75.6   40941   286325     66326   15895   3137 114132   4 45.6 175.0   38
c i   75.7   40939   286325     66513   16028   3142 114133   5 45.5 174.9   38
c i   75.7   40938   286325     66514   16028   3142 114133   5 45.5 174.9   38
c i   75.7   40937   286325     66529   16035   3146 114136   5 45.5 174.9   38
c i   75.8   40936   286325     66643   16133   3149 114140   4 45.4 174.7   38
c -   76.0   40933   286325     67098   10486   3170 114159   6 45.3 174.6   35
c i   76.3   40932   286325     68592   11777   3184 114173   2 45.6 175.2   36
c i   76.3   40931   286325     68616   11794   3184 114178   2 45.6 175.2   36
c i   76.6   40923   286325     69614   12636   3200 114197   3 45.3 174.7   37
c i   76.6   40920   286325     69615   12636   3200 114197   3 45.3 174.7   37
c i   77.8   40919   286325     72116   14830   3255 114264   3 44.7 173.9   38
c i   77.9   40917   286325     72185   14888   3259 114265   3 44.6 173.8   38
c i   78.3   40912   286325     73198   15721   3295 114297   2 44.4 173.0   38
c i   78.3   40910   286325     73199   15721   3295 114297   2 44.4 173.0   38
c i   78.4   40909   286325     73367   15866   3299 114302   2 44.3 172.8   38
c i   78.9   40906   286325     74787   16897   3311 114315   4 45.4 173.1   40
c i   79.1   40900   286325     75145   17212   3324 114323   3 45.3 173.1   40
c i   79.3   40898   286325     75386   17410   3340 114340   4 45.3 172.9   40
c i   79.3   40889   286325     75389   17411   3341 114340   4 45.3 172.9   40
c i   79.4   40887   286325     75651   17647   3343 114346   3 45.2 173.1   40
c -   79.6   40887   286325     76132   11537   3357 114357   6 45.1 172.6   35
c i   79.8   40886   286325     76679   12017   3366 114366   2 45.1 172.4   35
c i   80.1   40882   286325     77427   12640   3387 114377   3 45.0 172.5   36
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   80.1   40880   286325     77457   12665   3388 114377   4 45.0 172.4   36
c i   80.1   40874   286325     77459   12665   3388 114378   4 45.0 172.4   36
c i   80.1   40869   286325     77460   12665   3388 114378   4 45.0 172.4   36
c i   80.1   40868   286325     77461   12665   3388 114378   4 45.0 172.4   36
c i   80.1   40867   286325     77462   12665   3388 114378   4 45.0 172.4   36
c i   80.1   40865   286325     77518   12697   3402 114382   4 45.0 172.4   36
c i   80.1   40859   286325     77521   12698   3403 114382   4 45.0 172.4   36
c i   80.1   40855   286325     77524   12700   3403 114382   4 45.0 172.4   36
c i   80.4   40851   286325     78306   13380   3419 114398   3 44.8 171.9   36
c i   80.9   40850   286325     79612   14496   3443 114415   4 45.0 171.9   37
c 
c [simplification-9] limit of 80346 conflicts hit after 80346 conflicts
c [ternres-7] limit 10725652 with penalty 0 = 0 + 0
c [ternres-7] all 40850 free variables schedulable
c [ternres-7] 444 ternary resolvents (1 bin, 443 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-18] removed 277 variables
c [simpleprobe-4] 1627 schedulable variables 4%
c [simpleprobe-4] limit 42902608 penalty 0 = 0 + 0
c [decomp-19] removed 910 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 910 variables, found 45000 hbrs, 314 units
c [lift-7] limit 6435391 with penalty 0 = 0 + 0
c [lift-7] using 35406 probes 89%
c [lift-7] 51 units, 20 impls, 0 eqs in 1 rounds
c [lift-7] 39400 variables remain 99% (214 retained)
c [lift-7] removed 213 variables
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 46, lifted 103
c [unhide-9] limit 2145130 with penalty 0 = 0 + 0
c [unhide-9-10] 3 units, 86 failed, 26406 tauts, 0 hbrs, 40409 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 370 transitive binary clauses
c [transred-7] found 3 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 4 clauses out of 903 (0%) of length 6
c [cce-7-1] eliminated 31 clauses out of 9366 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 35 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 185321 clauses = 124316 binary + 61005 ternary
c [cce-7] tried to eliminate 595 small clauses 0%
c [cce-7] eliminated 150 small clauses 0%
c [cce-7] eliminated 122 binary clauses 0%
c [cce-7] eliminated 28 ternary clauses 0%
c [cce-7-1] eliminated 750 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 785 covered clauses in round 1
c [cce-7] eliminated 785 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 39312 variables 100%
c [elim-9] limit of 214513041 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 1162 variables 3% in round 1 in 28874795 steps
c [elim-9-1] backward subsumption/strengthening limit 57749590
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 8386897 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1164 = 3% variables out of 39312
c [bca-8] limit of 10000000 steps
c [bca-8] 59339 out of 76298 literals actually usable 78%
c [bca-8] added 83 blocked clauses in 152597 steps
c [simplification-9] removed 2702 variables 6.6% (38148 remain 16%)
c [simplification-9] removed 23263 irredundant clauses 8.1% (263062 remain 22%)
c [simplification-9] maximum reduction of 8% = max (7%, 8%)
c [simplification-9] large reduction 8% >= 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 82346
c 
c [simplification-10] limit of 82370 conflicts hit after 82370 conflicts
c [ternres-8] limit 10886171 with penalty 0 = 0 + 0
c [ternres-8] all 38148 free variables schedulable
c [ternres-8] 375 ternary resolvents (1 bin, 374 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 680385 penalty 3 = 3 + 0
c [card-4] found 9861 at-most-one constraints of average size 3.7
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 680385 for elimination
c [card-4] 9861 out of 9861 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-4] limit 544308 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 51297 literals 67%
c [treelook-4] scheduling used 544343 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 544308 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 672298 steps
c [treelook-4] 51285 literals remain 67%
c [treelook-4] 15379 variables remain to probed next time 40%
c [treelook-4] removed 2 variables, found 900 hbrs
c [lift-8] limit 6531702 with penalty 0 = 0 + 0
c [lift-8] using 34012 probes 89%
c [lift-8] 105 units, 18 impls, 1 eqs in 1 rounds
c [lift-8] 37616 variables remain 99% (302 retained)
c [lift-8] removed 228 variables
c [cliff-8] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-8] failed 18, lifted 44
c [unhide-10] limit 2177234 with penalty 0 = 0 + 0
c [unhide-10-12] 2 units, 65 failed, 10638 tauts, 0 hbrs, 55168 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 312 transitive binary clauses
c [transred-8] found 1 units
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 31
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 30
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 29
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 28
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 27
c [cce-8-1] eliminated 1 clauses out of 6 (17%) of length 26
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 23
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 22
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 21
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 20
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-8-1] eliminated 1 clauses out of 8 (12%) of length 18
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 17
c [cce-8-1] eliminated 1 clauses out of 8 (12%) of length 16
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 15
c [cce-8-1] eliminated 2 clauses out of 9 (22%) of length 14
c [cce-8-1] eliminated 4 clauses out of 9 (44%) of length 13
c [cce-8-1] eliminated 2 clauses out of 10 (20%) of length 12
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 11
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 10
c [cce-8-1] eliminated 4 clauses out of 22 (18%) of length 9
c [cce-8-1] eliminated 2 clauses out of 75 (3%) of length 8
c [cce-8-1] eliminated 5 clauses out of 163 (3%) of length 7
c [cce-8-1] eliminated 12 clauses out of 906 (1%) of length 6
c [cce-8-1] eliminated 55 clauses out of 9118 (1%) of length 5
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 121 large clauses in 30000001 steps
c [cce-8-1] allowing another 15000000 steps for small clauses
c [cce-8] scheduling 167347 clauses = 118454 binary + 48893 ternary
c [cce-8] tried to eliminate 680 small clauses 0%
c [cce-8] eliminated 192 small clauses 0%
c [cce-8] eliminated 157 binary clauses 0%
c [cce-8] eliminated 35 ternary clauses 0%
c [cce-8-1] eliminated 586 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 707 covered clauses in round 1
c [cce-8] eliminated 707 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 37745 variables 100%
c [elim-10] limit of 217723426 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 503 variables 1% in round 1 in 33689600 steps
c [elim-10-1] backward subsumption/strengthening limit 67379200
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 8206028 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 503 = 1% variables out of 37745
c [bca-9] limit of 10000000 steps
c [bca-9] 57463 out of 74486 literals actually usable 77%
c [bca-9] added 42 blocked clauses in 147141 steps
c [simplification-10] removed 906 variables 2.4% (37242 remain 15%)
c [simplification-10] removed 7791 irredundant clauses 3.0% (255271 remain 22%)
c [simplification-10] maximum reduction of 3% = max (2%, 3%)
c [simplification-10] geometric conflict interval increment 7812 = 31250 / 4
c [simplification-10] new conflict interval 39062
c [simplification-10] penalized conflict interval 39062 = 1 * 39062
c [simplification-10] new conflict limit 121432
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   92.2   37241   255271     85396   15233   3622 143121   3 48.4 174.7   39
c i   92.3   37240   255271     85563   15385   3630 143124   4 48.4 174.6   39
c i   92.5   37223   255271     86135   15897   3645 143127   3 48.2 174.7   39
c i   92.6   37199   255271     86334   16077   3650 143136   3 48.2 174.5   39
c i   92.9   37198   255271     86755   16450   3667 143152   3 48.1 174.2   39
c i   93.8   37194   255271     88733   18212   3713 143188   8 47.7 173.9   40
c i   93.8   37193   255271     88819   18289   3713 143188   8 47.6 173.9   40
c i   93.8   37191   255271     89084   18522   3718 143191   7 47.5 173.8   40
c i   93.8   37188   255271     89156   18581   3721 143193   4 47.5 173.7   40
c i   94.1   37161   255271     89698   19040   3733 143205   3 47.4 173.2   40
c -   94.2   37159   255271     89735   12070   3735 143206   3 47.4 173.2   34
c i   95.7   37158   255271     93793   15565   3811 143262   5 47.0 171.9   36
c i   96.8   37155   255271     96650   17667   3830 143281   2 49.1 172.2   39
c i   97.6   37154   255271     98537   19313   3860 143306   5 48.8 171.4   40
c -   98.4   37153   255271    100276   13258   3884 143325   3 48.6 171.1   34
c i   99.4   37152   255271    103098   15681   3930 143371   6 48.5 170.4   36
c i  100.5   37151   255271    105924   17934   3972 143416   4 48.4 169.7   37
c i  101.9   37150   255271    111308   21532   3992 143426   6 50.9 170.1   42
c -  102.3   37150   255271    112424   14223   3996 143426   4 51.9 170.3   34
c i  102.6   37149   255271    113548   15023   4002 143427   2 52.8 170.6   36
c i  102.7   37148   255271    114079   15426   4006 143427   7 52.9 170.6   36
c i  104.6   37147   255271    120811   19512   4037 143450   4 60.8 173.6   46
c 
c [simplification-11] limit of 122540 conflicts hit after 122540 conflicts
c [ternres-9] limit 15224154 with penalty 0 = 0 + 0
c [ternres-9] all 37147 free variables schedulable
c [ternres-9] 202 ternary resolvents (1 bin, 201 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-6] limit 761207 penalty 2 = 2 + 0
c [gauss-6] extracted 22 xors of average arity 2.9
c [gauss-6] connected 63 occurrences of 54 variables (average 1.2)
c [gauss-6] limit 761207 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 18 variables
c [basicprobe-4] limit 15224154 penalty 0 = 0 + 0
c [basicprobe-4-0] 8166 probes remain 22% after last round
c [basicprobe-4-0] 180 units = 178 failed (99%) + 2 lifted (1%)
c [basicprobe-4-0] removed 271 variables, found 73815 hbrs
c [bate-3] eliminated 185 asymmetric tautologies during probing
c [lift-9] limit 9134492 with penalty 0 = 0 + 0
c [lift-9] using 33021 probes 90%
c [lift-9] 107 units, 32 impls, 32 eqs in 1 rounds
c [lift-9] 36207 variables remain 99% (463 retained)
c [lift-9] removed 188 variables
c [cliff-9] limit of 12179323 steps penalty 0 = 0 + 0
c [cliff-9] failed 0, lifted 50
c [unhide-11] limit 3044830 with penalty 0 = 0 + 0
c [unhide-11-14] 1 units, 59 failed, 14287 tauts, 0 hbrs, 112775 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 235 transitive binary clauses
c [transred-9] found 1 units
c [cce-9] limit of 30448309 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 87
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 77
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-9-1] eliminated 3 clauses out of 143 (2%) of length 7
c [cce-9-1] eliminated 4 clauses out of 886 (0%) of length 6
c [cce-9-1] eliminated 274 clauses out of 8789 (3%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 302 large clauses in 30448310 steps
c [cce-9-1] allowing another 15224155 steps for small clauses
c [cce-9] scheduling 161849 clauses = 114843 binary + 47006 ternary
c [cce-9] tried to eliminate 903 small clauses 1%
c [cce-9] eliminated 275 small clauses 0%
c [cce-9] eliminated 216 binary clauses 0%
c [cce-9] eliminated 59 ternary clauses 0%
c [cce-9-1] eliminated 616 small clauses in 30448310 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 918 covered clauses in round 1
c [cce-9] eliminated 918 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 36545 variables 100%
c [elim-11] limit of 304483093 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 731 variables 2% in round 1 in 24245045 steps
c [elim-11-1] backward subsumption/strengthening limit 48490090
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 7859292 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 731 = 2% variables out of 36545
c [bca-10] limit of 10000000 steps
c [bca-10] 53889 out of 71630 literals actually usable 75%
c [bca-10] added 78 blocked clauses in 140262 steps
c [rephase-3] after 122540 conflicts (new increment 80000, next 202540)
c [flushphases] 0 phases reset
c [simplification-11] removed 1333 variables 3.6% (35814 remain 15%)
c [simplification-11] removed 9971 irredundant clauses 3.9% (245300 remain 21%)
c [simplification-11] maximum reduction of 4% = max (4%, 4%)
c [simplification-11] geometric conflict interval increment 7812 = 39062 / 5
c [simplification-11] new conflict interval 46874
c [simplification-11] penalized conflict interval 46874 = 1 * 46874
c [simplification-11] new conflict limit 169414
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  111.6   35814   245300    125414   16793   4044 208592   4 62.7 173.9   41
c i  112.9   35813   245300    128135   18976   4091 208609   5 62.2 173.0   41
c i  113.5   35812   245300    129282   19964   4124 208620   4 62.1 173.0   42
c i  113.5   35811   245300    129285   19965   4125 208620   4 62.1 173.0   42
c -  115.0   35811   245300    133009   14583   4178 208665   8 62.1 172.8   36
c i  115.5   35810   245300    134079   15548   4199 208686   4 61.8 172.5   36
c i  115.7   35808   245300    134438   15861   4214 208691   6 61.7 172.3   37
c i  116.2   35807   245300    136135   17226   4232 208699   7 61.9 172.2   38
c i  116.5   35806   245300    137245   18161   4234 208699   8 62.4 172.5   39
c i  116.7   35805   245300    137616   18490   4252 208708   5 62.3 172.4   39
c i  118.0   35802   245300    140284   20836   4286 208748   3 61.8 171.9   42
c i  118.9   35799   245300    142328   22579   4347 208768   5 61.6 171.8   43
c -  120.2   35798   245300    144921   15751   4404 208809   4 61.3 171.4   36
c i  121.1   35797   245300    146712   17321   4436 208830   6 60.9 170.7   37
c i  121.7   35796   245300    148612   18813   4442 208833   5 61.3 171.0   39
c i  123.0   35795   245300    152750   22014   4481 208851   7 62.8 172.1   43
c i  124.9   35794   245300    156576   25341   4559 208898   6 62.2 171.3   45
c i  125.0   35793   245300    157059   25770   4563 208903   3 62.1 171.3   46
c i  125.2   35791   245300    157304   25966   4567 208907   4 62.1 171.3   46
c -  125.4   35790   245300    157540   16669   4570 208911   4 62.1 171.3   36
c i  126.8   35789   245300    160501   19212   4635 208942   4 61.8 170.6   38
c i  126.8   35782   245300    160502   19212   4635 208942   4 61.8 170.6   38
c i  126.8   35780   245300    160503   19212   4635 208942   4 61.8 170.6   38
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  126.8   35776   245300    160504   19212   4635 208942   4 61.8 170.6   38
c i  126.8   35775   245300    160505   19212   4635 208942   4 61.8 170.6   38
c i  130.4   35773   245300    168932   26030   4750 209014   4 61.3 169.5   43
c 
c [simplification-12] limit of 170756 conflicts hit after 170756 conflicts
c [ternres-10] limit 21549071 with penalty 0 = 0 + 0
c [ternres-10] all 35773 free variables schedulable
c [ternres-10] 322 ternary resolvents (0 bin, 322 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-23] removed 69 variables
c [simpleprobe-5] all 35745 free variables schedulable
c [simpleprobe-5] limit 86196286 penalty 0 = 0 + 0
c [decomp-24] removed 218 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 218 variables, found 23750 hbrs, 97 units
c [cgrclsr-4] limit 269363 penalty 3 = 3 + 0
c [cgrclsr-4] all 35527 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-10] limit 12929442 with penalty 0 = 0 + 0
c [lift-10] using 31867 probes 90%
c [lift-10] 156 units, 45 impls, 1 eqs in 1 rounds
c [lift-10] 34672 variables remain 98% (661 retained)
c [lift-10] removed 194 variables
c [cliff-10] limit of 17239257 steps penalty 0 = 0 + 0
c [cliff-10] failed 14, lifted 47
c [unhide-12] limit 4309814 with penalty 0 = 0 + 0
c [unhide-12-17] 1 units, 50 failed, 27046 tauts, 0 hbrs, 163440 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 259 transitive binary clauses
c [transred-10] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 35213 variables 100%
c [block-5] limit of 26936339 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 21 blocked clauses
c [block-5] 21 < 1/1000 * 238316 = 238 considered unsuccessful
c [cce-10] limit of 43098143 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 26
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 25
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 24
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 23
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 22
c [cce-10-1] eliminated 2 clauses out of 10 (20%) of length 21
c [cce-10-1] eliminated 4 clauses out of 8 (50%) of length 20
c [cce-10-1] eliminated 4 clauses out of 13 (31%) of length 19
c [cce-10-1] eliminated 5 clauses out of 10 (50%) of length 18
c [cce-10-1] eliminated 4 clauses out of 12 (33%) of length 17
c [cce-10-1] eliminated 5 clauses out of 10 (50%) of length 16
c [cce-10-1] eliminated 4 clauses out of 12 (33%) of length 15
c [cce-10-1] eliminated 6 clauses out of 13 (46%) of length 14
c [cce-10-1] eliminated 4 clauses out of 11 (36%) of length 13
c [cce-10-1] eliminated 5 clauses out of 14 (36%) of length 12
c [cce-10-1] eliminated 4 clauses out of 11 (36%) of length 11
c [cce-10-1] eliminated 5 clauses out of 13 (38%) of length 10
c [cce-10-1] eliminated 4 clauses out of 21 (19%) of length 9
c [cce-10-1] eliminated 5 clauses out of 67 (7%) of length 8
c [cce-10-1] eliminated 4 clauses out of 136 (3%) of length 7
c [cce-10-1] eliminated 11 clauses out of 870 (1%) of length 6
c [cce-10-1] eliminated 1862 clauses out of 8214 (23%) of length 5
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 1946 large clauses in 43098144 steps
c [cce-10-1] allowing another 21549072 steps for small clauses
c [cce-10] scheduling 155711 clauses = 110443 binary + 45268 ternary
c [cce-10] tried to eliminate 1130 small clauses 1%
c [cce-10] eliminated 343 small clauses 0%
c [cce-10] eliminated 258 binary clauses 0%
c [cce-10] eliminated 85 ternary clauses 0%
c [cce-10-1] eliminated 343 small clauses in 43098144 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 2289 covered clauses in round 1
c [cce-10] eliminated 2289 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 35213 variables 100%
c [elim-12] limit of 430981431 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 1604 variables 5% in round 1 in 24192266 steps
c [elim-12-1] backward subsumption/strengthening limit 48384532
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 7423852 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 1604 = 5% variables out of 35213
c [bca-11] limit of 10000000 steps
c [bca-11] 49582 out of 67220 literals actually usable 74%
c [bca-11] added 41 blocked clauses in 126912 steps
c [simplification-12] removed 2164 variables 6.0% (33609 remain 14%)
c [simplification-12] removed 13052 irredundant clauses 5.3% (232248 remain 20%)
c [simplification-12] maximum reduction of 6% = max (6%, 5%)
c [simplification-12] large reduction 6% >= 5% limit
c [simplification-12] new conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] new conflict limit 172756
c 
c [simplification-13] limit of 172802 conflicts hit after 172803 conflicts
c [ternres-11] limit 21866068 with penalty 0 = 0 + 0
c [ternres-11] all 33609 free variables schedulable
c [ternres-11] 284 ternary resolvents (1 bin, 283 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-25] removed 48 variables
c [treelook-5] limit 1093303 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 55679 literals 83%
c [treelook-5] scheduling used 1004651 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1093303 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1140288 steps
c [treelook-5] 55661 literals remain 83%
c [treelook-5] 12639 variables remain to probed next time 38%
c [treelook-5] removed 2 variables, found 5757 hbrs
c [lift-11] limit 13119640 with penalty 0 = 0 + 0
c [lift-11] using 30715 probes 92%
c [lift-11] 54 units, 47 impls, 2 eqs in 1 rounds
c [lift-11] 32586 variables remain 97% (903 retained)
c [lift-11] removed 70 variables
c [cliff-11] limit of 17492854 steps penalty 0 = 0 + 0
c [cliff-11] failed 0, lifted 12
c [unhide-13] limit 4373213 with penalty 0 = 0 + 0
c [unhide-13-20] 2 units, 120 failed, 9297 tauts, 0 hbrs, 27714 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 211 transitive binary clauses
c [transred-11] found 2 units
c [cce-11] limit of 43732136 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 2 clauses out of 43 (5%) of length 7
c [cce-11-1] eliminated 28 clauses out of 874 (3%) of length 6
c [cce-11-1] eliminated 75 clauses out of 6326 (1%) of length 5
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 105 large clauses in 43732137 steps
c [cce-11-1] allowing another 21866068 steps for small clauses
c [cce-11] scheduling 158480 clauses = 104305 binary + 54175 ternary
c [cce-11] tried to eliminate 1194 small clauses 1%
c [cce-11] eliminated 260 small clauses 0%
c [cce-11] eliminated 216 binary clauses 0%
c [cce-11] eliminated 44 ternary clauses 0%
c [cce-11-1] eliminated 412 small clauses in 43732137 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 517 covered clauses in round 1
c [cce-11] eliminated 517 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 33421 variables 100%
c [elim-13] limit of 437321360 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 324 variables 1% in round 1 in 23056816 steps
c [elim-13-1] backward subsumption/strengthening limit 46113632
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 7235973 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 324 = 1% variables out of 33421
c [bca-12] limit of 10000000 steps
c [bca-12] 48049 out of 66196 literals actually usable 73%
c [bca-12] added 38 blocked clauses in 124340 steps
c [simplification-13] removed 512 variables 1.5% (33097 remain 14%)
c [simplification-13] removed 4490 irredundant clauses 1.9% (227758 remain 19%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 15624 = 46874 / 3
c [simplification-13] new conflict interval 62498
c [simplification-13] penalized conflict interval 62498 = 1 * 62498
c [simplification-13] new conflict limit 235301
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  147.2   33096   227758    183324   24999   4996 204534   4 63.6 170.3   48
c i  147.9   33093   227758    184728   26233   5022 204562   4 63.4 169.7   50
c -  148.0   33092   227758    184748   16245   5022 204565   5 63.4 169.7   35
c i  148.3   33091   227758    185700   17032   5030 204573   3 63.3 169.6   36
c i  149.3   33090   227758    188895   19677   5065 204595   4 62.9 169.2   38
c -  153.8   33090   227758    198822   17454   5258 204711   5 62.6 168.0   35
c i  155.5   33089   227758    202692   20620   5307 204732   3 62.6 167.6   38
c i  155.8   33088   227758    203260   21116   5319 204735   3 62.5 167.5   38
c i  156.3   33073   227758    204073   21815   5344 204751   3 62.3 167.3   38
c i  156.3   33034   227758    204078   21818   5344 204751   3 62.3 167.3   38
c i  156.4   33032   227758    204246   21966   5347 204754   4 62.3 167.3   38
c i  159.0   33028   227758    211850   27919   5424 204819   4 63.4 167.7   45
c -  160.1   33028   227758    213870   18615   5467 204844   5 63.2 167.6   35
c i  160.5   33027   227758    214945   19428   5474 204845   4 63.2 167.6   36
c i  161.0   33026   227758    216034   20404   5502 204848   4 63.0 167.4   37
c i  162.4   33025   227758    218784   22808   5574 204881   4 62.6 166.8   38
c i  164.5   33024   227758    224042   26844   5628 204913   3 62.5 166.6   41
c i  164.9   33023   227758    224682   27440   5632 204915   3 62.5 166.4   41
c -  167.2   33023   227758    229126   19613   5690 204953   4 62.2 165.8   35
c 
c [simplification-14] limit of 236555 conflicts hit after 236557 conflicts
c [ternres-12] limit 29880475 with penalty 0 = 0 + 0
c [ternres-12] all 33023 free variables schedulable
c [ternres-12] 165 ternary resolvents (0 bin, 165 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-27] removed 123 variables
c [basicprobe-5] limit 29880475 penalty 0 = 0 + 0
c [basicprobe-5-0] 4769 probes remain 15% after last round
c [basicprobe-5-0] 300 units = 293 failed (98%) + 7 lifted (2%)
c [basicprobe-5-0] removed 448 variables, found 106145 hbrs
c [bate-4] eliminated 460 asymmetric tautologies during probing
c [lift-12] limit 17928285 with penalty 0 = 0 + 0
c [lift-12] using 29617 probes 91%
c [lift-12] 89 units, 50 impls, 8 eqs in 1 rounds
c [lift-12] 31128 variables remain 96% (1254 retained)
c [lift-12] removed 144 variables
c [cliff-12] limit of 23904380 steps penalty 0 = 0 + 0
c [cliff-12] failed 6, lifted 14
c [unhide-14] limit 5976095 with penalty 0 = 0 + 0
c [unhide-14-24] 15 units, 58 failed, 26622 tauts, 0 hbrs, 135946 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 124 transitive binary clauses
c [cce-12] limit of 59760951 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-12-1] eliminated 1 clauses out of 1 (100%) of length 112
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-12-1] eliminated 2 clauses out of 2 (100%) of length 89
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-12-1] eliminated 35 clauses out of 806 (4%) of length 6
c [cce-12-1] eliminated 155 clauses out of 5987 (3%) of length 5
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 200 large clauses in 59760952 steps
c [cce-12-1] allowing another 29880476 steps for small clauses
c [cce-12] scheduling 152008 clauses = 100852 binary + 51156 ternary
c [cce-12] tried to eliminate 1460 small clauses 1%
c [cce-12] eliminated 334 small clauses 0%
c [cce-12] eliminated 280 binary clauses 0%
c [cce-12] eliminated 54 ternary clauses 0%
c [cce-12-1] eliminated 334 small clauses in 59760952 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 534 covered clauses in round 1
c [cce-12] eliminated 534 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 32249 variables 100%
c [elim-14] limit of 597609515 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 622 variables 2% in round 1 in 23210741 steps
c [elim-14-1] backward subsumption/strengthening limit 46421482
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 6828969 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 622 = 2% variables out of 32249
c [bca-13] limit of 10000000 steps
c [bca-13] 43621 out of 63256 literals actually usable 69%
c [bca-13] added 28 blocked clauses in 117666 steps
c [rephase-4] after 236557 conflicts (new increment 160000, next 396557)
c [flushphases] 0 phases reset
c [simplification-14] removed 1396 variables 4.2% (31627 remain 13%)
c [simplification-14] removed 11370 irredundant clauses 5.0% (216388 remain 18%)
c [simplification-14] maximum reduction of 5% = max (4%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] new conflict interval 2365 = min (236557/100, 62498)
c [simplification-14] penalized conflict interval 2365 = 1 * 2365
c [simplification-14] new conflict limit 238922
c 
c [simplification-15] limit of 238938 conflicts hit after 238939 conflicts
c [ternres-13] limit 30057578 with penalty 0 = 0 + 0
c [ternres-13] all 31627 free variables schedulable
c [ternres-13] 315 ternary resolvents (1 bin, 314 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 939299 penalty 4 = 4 + 0
c [card-5] found 9153 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 939299 for elimination
c [card-5] 9153 out of 9153 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 751439 penalty 3 = 3 + 0
c [gauss-7] extracted 9 xors of average arity 3.0
c [gauss-7] connected 27 occurrences of 27 variables (average 1.0)
c [gauss-7] limit 751439 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 35 variables
c [simpleprobe-6] all 31592 free variables schedulable
c [simpleprobe-6] limit 120230312 penalty 0 = 0 + 0
c [decomp-29] removed 108 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 108 variables, found 23143 hbrs, 48 units
c [lift-13] limit 18034546 with penalty 0 = 0 + 0
c [lift-13] using 28290 probes 90%
c [lift-13] 77 units, 55 impls, 0 eqs in 1 rounds
c [lift-13] 29823 variables remain 95% (1573 retained)
c [lift-13] removed 88 variables
c [cliff-13] limit of 24046062 steps penalty 0 = 0 + 0
c [cliff-13] failed 0, lifted 12
c [unhide-15] limit 6011515 with penalty 0 = 0 + 0
c [unhide-15-28] 1 units, 38 failed, 25333 tauts, 0 hbrs, 93129 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 195 transitive binary clauses
c [cce-13] limit of 60115156 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2 clauses out of 8 (25%) of length 24
c [cce-13-1] eliminated 1 clauses out of 4 (25%) of length 23
c [cce-13-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-13-1] eliminated 1 clauses out of 5 (20%) of length 21
c [cce-13-1] eliminated 2 clauses out of 6 (33%) of length 20
c [cce-13-1] eliminated 1 clauses out of 9 (11%) of length 19
c [cce-13-1] eliminated 2 clauses out of 6 (33%) of length 12
c [cce-13-1] eliminated 1 clauses out of 12 (8%) of length 11
c [cce-13-1] eliminated 3 clauses out of 9 (33%) of length 10
c [cce-13-1] eliminated 4 clauses out of 16 (25%) of length 9
c [cce-13-1] eliminated 4 clauses out of 19 (21%) of length 8
c [cce-13-1] eliminated 9 clauses out of 51 (18%) of length 7
c [cce-13-1] eliminated 8 clauses out of 791 (1%) of length 6
c [cce-13-1] eliminated 90 clauses out of 5880 (2%) of length 5
c [cce-13-1] incomplete large round (ACCE)
c [cce-13-1] eliminated 129 large clauses in 60115157 steps
c [cce-13-1] allowing another 30057578 steps for small clauses
c [cce-13] scheduling 139133 clauses = 98288 binary + 40845 ternary
c [cce-13] tried to eliminate 1775 small clauses 1%
c [cce-13] eliminated 378 small clauses 0%
c [cce-13] eliminated 274 binary clauses 0%
c [cce-13] eliminated 104 ternary clauses 0%
c [cce-13-1] eliminated 451 small clauses in 60115157 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 580 covered clauses in round 1
c [cce-13] eliminated 580 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 31347 variables 100%
c [elim-15] limit of 601151562 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 188 variables 1% in round 1 in 20670496 steps
c [elim-15-1] backward subsumption/strengthening limit 41340992
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 6665235 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 188 = 1% variables out of 31347
c [bca-14] limit of 10000000 steps
c [bca-14] 42556 out of 62320 literals actually usable 68%
c [bca-14] added 18 blocked clauses in 116471 steps
c [simplification-15] removed 468 variables 1.5% (31159 remain 13%)
c [simplification-15] removed 4445 irredundant clauses 2.1% (211943 remain 18%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 20832 = 62498 / 3
c [simplification-15] new conflict interval 83330
c [simplification-15] penalized conflict interval 83330 = 1 * 83330
c [simplification-15] new conflict limit 322269
c [tabula-rasa-2] number clauses 211943 drops below limit 214694
c [flush-cache] 0 binary, 0 ternary, 21917 large
c [flushphases] 31159 phases reset fully
c [phase-8] phase bias: 1921 positive 32%, 4138 negative 68%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] new conflict limit 258939
c [tabula-rasa-2] new variable limit 7789 and clause limit 105971
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  187.2   31159   211943    244912    2169   5928 270035   4 67.7 167.8   36
c -  188.2   31159   211943    249251    2683   5935 270036   3 71.4 168.7   37
c -  189.3   31159   211943    253541    3264   5951 270045   6 73.1 170.0   37
c 
c [simplification-16] limit of 258991 conflicts hit after 258991 conflicts
c [ternres-14] limit 31664477 with penalty 0 = 0 + 0
c [ternres-14] all 31159 free variables schedulable
c [ternres-14] 118 ternary resolvents (1 bin, 117 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-30] removed 4 variables
c [treelook-6] limit 1583223 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 51179 literals 82%
c [treelook-6] scheduling used 1002170 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1583223 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1585874 steps
c [treelook-6] 51076 literals remain 82%
c [treelook-6] 11481 variables remain to probed next time 37%
c [treelook-6] removed 4 variables, found 6277 hbrs
c [lift-14] limit 18998686 with penalty 0 = 0 + 0
c [lift-14] using 27660 probes 89%
c [lift-14] 66 units, 61 impls, 2 eqs in 1 rounds
c [lift-14] 29039 variables remain 94% (1997 retained)
c [lift-14] removed 115 variables
c [cliff-14] limit of 25331581 steps penalty 0 = 0 + 0
c [cliff-14] failed 3, lifted 4
c [unhide-16] limit 6332895 with penalty 0 = 0 + 0
c [unhide-16-33] 0 units, 36 failed, 15403 tauts, 0 hbrs, 259898 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 134 transitive binary clauses
c [cce-14] limit of 63328954 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-14-1] eliminated 2 clauses out of 6 (33%) of length 38
c [cce-14-1] eliminated 1 clauses out of 787 (0%) of length 6
c [cce-14-1] eliminated 132 clauses out of 5776 (2%) of length 5
c [cce-14-1] incomplete large round (ACCE)
c [cce-14-1] eliminated 136 large clauses in 63328955 steps
c [cce-14-1] allowing another 31664477 steps for small clauses
c [cce-14] scheduling 146093 clauses = 97165 binary + 48928 ternary
c [cce-14] tried to eliminate 1606 small clauses 1%
c [cce-14] eliminated 356 small clauses 0%
c [cce-14] eliminated 275 binary clauses 0%
c [cce-14] eliminated 81 ternary clauses 0%
c [cce-14-1] eliminated 367 small clauses in 63328955 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 503 covered clauses in round 1
c [cce-14] eliminated 503 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 31001 variables 100%
c [elim-16] limit of 633289548 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 185 variables 1% in round 1 in 21267127 steps
c [elim-16-1] backward subsumption/strengthening limit 42534254
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 6561680 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 185 = 1% variables out of 31001
c [bca-15] limit of 10000000 steps
c [bca-15] 54776 out of 61634 literals actually usable 89%
c [bca-15] added 29 blocked clauses in 129038 steps
c [rephase-5] after 258991 conflicts (new increment 20000, next 278991)
c [flushphases] 176 phases reset
c [phase-9] phase bias: 1 positive 33%, 2 negative 67%
c [simplification-16] removed 343 variables 1.1% (30816 remain 13%)
c [simplification-16] removed 2745 irredundant clauses 1.3% (209198 remain 18%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-16] new conflict interval 30000
c [simplification-16] penalized conflict interval 30000 = 1 * 30000
c [simplification-16] new conflict limit 288991
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  199.0   30816   209198    261149    3799   5886 272293   5 78.5 172.3   36
c -  200.8   30816   209198    269525    4307   5902 272310   4 82.8 173.4   36
c R  201.2   30816   209198    271600    5393   5904 272311   8 83.5 173.6   38
c -  203.1   30816   209198    276693    5369   6040 272366   3 83.1 174.0   36
c -  205.8   30816   209198    284034    6318   6173 272428   4 82.7 174.1   36
c 
c [simplification-17] limit of 289405 conflicts hit after 289405 conflicts
c [ternres-15] limit 34714276 with penalty 0 = 0 + 0
c [ternres-15] all 30816 free variables schedulable
c [ternres-15] 133 ternary resolvents (1 bin, 132 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-32] removed 1 variables
c [basicprobe-6] limit 34714276 penalty 0 = 0 + 0
c [basicprobe-6-0] 1466 probes remain 5% after last round
c [basicprobe-6-0] 281 units = 272 failed (97%) + 9 lifted (3%)
c [basicprobe-6-0] removed 395 variables, found 93303 hbrs
c [bate-5] eliminated 426 asymmetric tautologies during probing
c [cgrclsr-5] limit 216964 penalty 4 = 4 + 0
c [cgrclsr-5] all 30420 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 26569 probes 87%
c [lift-15] 64 units, 58 impls, 5 eqs in 1 rounds
c [lift-15] 27917 variables remain 92% (2427 retained)
c [lift-15] removed 76 variables
c [cliff-15] limit of 27771420 steps penalty 0 = 0 + 0
c [cliff-15] failed 0, lifted 0
c [unhide-17] limit 6942855 with penalty 0 = 0 + 0
c [unhide-17-38] 0 units, 11 failed, 20066 tauts, 0 hbrs, 89837 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 131 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 30336 variables 100%
c [block-6] limit of 21696422 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 31 blocked clauses
c [block-6] 31 < 1/1000 * 202782 = 202 considered unsuccessful
c [cce-15] limit of 69428552 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 117
c [cce-15-1] eliminated 2 clauses out of 2 (100%) of length 116
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-15-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-15-1] eliminated 1 clauses out of 12 (8%) of length 10
c [cce-15-1] eliminated 2 clauses out of 9 (22%) of length 9
c [cce-15-1] eliminated 1 clauses out of 21 (5%) of length 8
c [cce-15-1] eliminated 2 clauses out of 40 (5%) of length 7
c [cce-15-1] eliminated 6 clauses out of 790 (1%) of length 6
c [cce-15-1] eliminated 123 clauses out of 5603 (2%) of length 5
c [cce-15-1] eliminated 242 clauses out of 16382 (1%) of length 4
c [cce-15-1] incomplete large round (ACCE)
c [cce-15-1] eliminated 383 large clauses in 69428553 steps
c [cce-15-1] allowing another 34714276 steps for small clauses
c [cce-15] scheduling 133408 clauses = 95351 binary + 38057 ternary
c [cce-15] tried to eliminate 2799 small clauses 2%
c [cce-15] eliminated 642 small clauses 0%
c [cce-15] eliminated 513 binary clauses 1%
c [cce-15] eliminated 129 ternary clauses 0%
c [cce-15-1] eliminated 642 small clauses in 69428553 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 1025 covered clauses in round 1
c [cce-15] eliminated 1025 covered clauses in TOTAL during 1 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 30335 variables 100%
c [elim-17] limit of 694285521 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 394 variables 1% in round 1 in 19500729 steps
c [elim-17-1] backward subsumption/strengthening limit 39001458
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 6246613 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 394 = 1% variables out of 30335
c [bca-16] limit of 10000000 steps
c [bca-16] 46365 out of 59884 literals actually usable 77%
c [bca-16] added 8 blocked clauses in 112999 steps
c [rephase-6] after 289405 conflicts (new increment 40000, next 329405)
c [flushphases] 18 phases reset
c [phase-10] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-17] removed 875 variables 2.8% (29941 remain 12%)
c [simplification-17] removed 8199 irredundant clauses 3.9% (200999 remain 17%)
c [simplification-17] maximum reduction of 4% = max (3%, 4%)
c [simplification-17] geometric conflict interval increment 6000 = 30000 / 5
c [simplification-17] new conflict interval 36000
c [simplification-17] penalized conflict interval 36000 = 1 * 36000
c [simplification-17] new conflict limit 325405
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  216.8   29940   200999    290031   10632   6388 327276   4 82.0 173.8   40
c -  217.9   29934   200999    292731    7437   6433 327303   4 81.6 173.6   37
c i  219.4   29933   200999    298541   11785   6475 327323   4 82.4 174.0   43
c -  220.6   29887   200999    301589    8296   6538 327354   5 82.0 173.7   37
c -  223.9   29887   200999    310200    9184   6647 327395   6 82.0 174.3   37
c i  224.4   29886   200999    311330   10163   6674 327416   4 81.9 174.2   38
c i  225.7   29885   200999    314739   13007   6724 327428   6 81.8 174.3   40
c -  228.0   29883   200999    319849   10299   6828 327466   6 81.4 173.9   37
c 
c [simplification-18] limit of 325881 conflicts hit after 325886 conflicts
c [ternres-16] limit 38867752 with penalty 0 = 0 + 0
c [ternres-16] all 29883 free variables schedulable
c [ternres-16] 180 ternary resolvents (0 bin, 180 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-33] removed 67 variables
c [simpleprobe-7] all 29874 free variables schedulable
c [simpleprobe-7] limit 155471011 penalty 0 = 0 + 0
c [decomp-34] removed 39 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 39 variables, found 20746 hbrs, 19 units
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 25602 probes 86%
c [lift-16] 32 units, 53 impls, 3 eqs in 1 rounds
c [lift-16] 26943 variables remain 90% (2851 retained)
c [lift-16] removed 41 variables
c [unhide-18] limit 7773550 with penalty 0 = 0 + 0
c [unhide-18-43] 0 units, 4 failed, 26507 tauts, 0 hbrs, 114449 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 154 transitive binary clauses
c [cce-16] limit of 77735505 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 2 clauses out of 6 (33%) of length 26
c [cce-16-1] eliminated 3 clauses out of 7 (43%) of length 25
c [cce-16-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-16-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-16-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-16-1] eliminated 1 clauses out of 4 (25%) of length 20
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 19
c [cce-16-1] eliminated 2 clauses out of 8 (25%) of length 18
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 17
c [cce-16-1] eliminated 2 clauses out of 11 (18%) of length 16
c [cce-16-1] eliminated 1 clauses out of 11 (9%) of length 15
c [cce-16-1] eliminated 4 clauses out of 9 (44%) of length 14
c [cce-16-1] eliminated 1 clauses out of 10 (10%) of length 13
c [cce-16-1] eliminated 3 clauses out of 10 (30%) of length 12
c [cce-16-1] eliminated 3 clauses out of 8 (38%) of length 11
c [cce-16-1] eliminated 3 clauses out of 13 (23%) of length 10
c [cce-16-1] eliminated 4 clauses out of 14 (29%) of length 9
c [cce-16-1] eliminated 2 clauses out of 18 (11%) of length 8
c [cce-16-1] eliminated 4 clauses out of 44 (9%) of length 7
c [cce-16-1] eliminated 4 clauses out of 802 (0%) of length 6
c [cce-16-1] eliminated 18 clauses out of 5525 (0%) of length 5
c [cce-16-1] eliminated 984 clauses out of 16162 (6%) of length 4
c [cce-16-1] incomplete large round (ACCE)
c [cce-16-1] eliminated 1049 large clauses in 77735506 steps
c [cce-16-1] allowing another 38867753 steps for small clauses
c [cce-16] scheduling 138965 clauses = 93743 binary + 45222 ternary
c [cce-16] tried to eliminate 2697 small clauses 2%
c [cce-16] eliminated 543 small clauses 0%
c [cce-16] eliminated 467 binary clauses 0%
c [cce-16] eliminated 76 ternary clauses 0%
c [cce-16-1] eliminated 543 small clauses in 77735506 steps
c [cce-16-1] incomplete small round (ACCE)
c [cce-16-1] eliminated 1592 covered clauses in round 1
c [cce-16] eliminated 1592 covered clauses in TOTAL during 1 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 29792 variables 100%
c [elim-18] limit of 777355055 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 501 variables 2% in round 1 in 19032597 steps
c [elim-18-1] backward subsumption/strengthening limit 38065194
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 6127530 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 501 = 2% variables out of 29792
c [bca-17] limit of 10000000 steps
c [bca-17] 43187 out of 58584 literals actually usable 74%
c [bca-17] added 74 blocked clauses in 107632 steps
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-18] removed 592 variables 2.0% (29291 remain 12%)
c [simplification-18] removed 3781 irredundant clauses 1.9% (197218 remain 17%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 12000 = 36000 / 3
c [simplification-18] new conflict interval 48000
c [simplification-18] penalized conflict interval 48000 = 1 * 48000
c [simplification-18] new conflict limit 373886
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  239.5   29291   197218    333888   10892   6954 316661   5 83.3 174.3   37
c -  243.9   29291   197218    345065   11841   7127 316750   5 82.9 173.7   37
c -  248.2   29291   197218    356815   12863   7255 316818   4 82.5 174.0   37
c -  253.4   29291   197218    369233   13951   7423 316872   6 81.6 173.4   37
c 
c [simplification-19] limit of 374460 conflicts hit after 374460 conflicts
c [ternres-17] limit 44949814 with penalty 0 = 0 + 0
c [ternres-17] all 29291 free variables schedulable
c [ternres-17] 112 ternary resolvents (0 bin, 112 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-35] removed 5 variables
c [treelook-7] limit 2247490 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 47477 literals 81%
c [treelook-7] scheduling used 1015077 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 2247490 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 2277483 steps
c [treelook-7] 47409 literals remain 81%
c [treelook-7] 10562 variables remain to probed next time 36%
c [treelook-7] removed 8 variables, found 5134 hbrs
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 24918 probes 85%
c [lift-17] 22 units, 53 impls, 12 eqs in 1 rounds
c [lift-17] 25942 variables remain 89% (3302 retained)
c [lift-17] removed 34 variables
c [cliff-16] limit of 17979925 steps penalty 1 = 1 + 0
c [cliff-16] failed 0, lifted 0
c [unhide-19] limit 8989962 with penalty 0 = 0 + 0
c [unhide-19-49] 1 units, 1 failed, 11211 tauts, 0 hbrs, 87482 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 155 transitive binary clauses
c [cce-17] limit of 89899628 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 1 clauses out of 808 (0%) of length 6
c [cce-17-1] eliminated 268 clauses out of 5773 (5%) of length 5
c [cce-17-1] eliminated 1998 clauses out of 15442 (13%) of length 4
c [cce-17-1] incomplete large round (ACCE)
c [cce-17-1] eliminated 2267 large clauses in 89899629 steps
c [cce-17-1] allowing another 44949814 steps for small clauses
c [cce-17] scheduling 129215 clauses = 92075 binary + 37140 ternary
c [cce-17] tried to eliminate 3365 small clauses 3%
c [cce-17] eliminated 732 small clauses 1%
c [cce-17] eliminated 570 binary clauses 1%
c [cce-17] eliminated 162 ternary clauses 0%
c [cce-17-1] eliminated 732 small clauses in 89899629 steps
c [cce-17-1] incomplete small round (ACCE)
c [cce-17-1] eliminated 2999 covered clauses in round 1
c [cce-17] eliminated 2999 covered clauses in TOTAL during 1 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 29239 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 566 variables 2% in round 1 in 18828430 steps
c [elim-19-1] backward subsumption/strengthening limit 37656860
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 5960870 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 566 = 2% variables out of 29239
c [bca-18] limit of 10000000 steps
c [bca-18] 39696 out of 57348 literals actually usable 69%
c [bca-18] added 258 blocked clauses in 102460 steps
c [rephase-7] after 374460 conflicts (new increment 80000, next 454460)
c [flushphases] 0 phases reset
c [simplification-19] removed 618 variables 2.1% (28673 remain 12%)
c [simplification-19] removed 4703 irredundant clauses 2.4% (192515 remain 16%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 16000 = 48000 / 3
c [simplification-19] new conflict interval 64000
c [simplification-19] penalized conflict interval 64000 = 1 * 64000
c [simplification-19] new conflict limit 438460
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  267.5   28673   192515    389290   14354   7593 306129   7 83.6 173.4   37
c -  273.3   28673   192515    404213   15131   7706 306191   5 87.7 174.6   37
c i  275.4   28672   192515    409702   19869   7760 306219   4 87.7 174.6   43
c -  279.1   28672   192515    417697   16176   7872 306289   5 87.1 174.1   37
c -  284.6   28672   192515    431975   17211   8001 306347   6 86.6 173.7   37
c 
c [simplification-20] limit of 439050 conflicts hit after 439050 conflicts
c [ternres-18] limit 52764570 with penalty 0 = 0 + 0
c [ternres-18] all 28672 free variables schedulable
c [ternres-18] 188 ternary resolvents (0 bin, 188 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-8] limit 659557 penalty 4 = 4 + 0
c [gauss-8] extracted 4 xors of average arity 3.0
c [gauss-8] connected 12 occurrences of 12 variables (average 1.0)
c [gauss-8] limit 659557 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 26 variables
c [basicprobe-7] limit 52764570 penalty 0 = 0 + 0
c [basicprobe-7-0] 3153 sched 11%, 153 failed, 5 lifted, 51975 hbrs
c [decomp-38] removed 204 variables
c [basicprobe-7-1] 6530 probes remain 23% after last round
c [basicprobe-7-1] 193 units = 188 failed (97%) + 5 lifted (3%)
c [basicprobe-7-1] removed 253 variables, found 65017 hbrs
c [bate-6] eliminated 363 asymmetric tautologies during probing
c [lift-18] limit 20000000 with penalty 0 = 0 + 0
c [lift-18] using 23849 probes 84%
c [lift-18] 22 units, 54 impls, 3 eqs in 1 rounds
c [lift-18] 24608 variables remain 87% (3760 retained)
c [lift-18] removed 25 variables
c [unhide-20] limit 10552914 with penalty 0 = 0 + 0
c [unhide-20-56] 0 units, 9 failed, 19084 tauts, 0 hbrs, 131318 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 128 transitive binary clauses
c [transred-18] found 1 units
c [cce-18] limit of 105529141 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 2 clauses out of 6 (33%) of length 28
c [cce-18-1] eliminated 1 clauses out of 8 (12%) of length 27
c [cce-18-1] eliminated 1 clauses out of 7 (14%) of length 20
c [cce-18-1] eliminated 2 clauses out of 5 (40%) of length 19
c [cce-18-1] eliminated 1 clauses out of 6 (17%) of length 18
c [cce-18-1] eliminated 1 clauses out of 14 (7%) of length 8
c [cce-18-1] eliminated 3 clauses out of 45 (7%) of length 7
c [cce-18-1] eliminated 10 clauses out of 815 (1%) of length 6
c [cce-18-1] eliminated 149 clauses out of 5574 (3%) of length 5
c [cce-18-1] eliminated 889 clauses out of 13152 (7%) of length 4
c [cce-18-1] incomplete large round (ACCE)
c [cce-18-1] eliminated 1059 large clauses in 105529142 steps
c [cce-18-1] allowing another 52764571 steps for small clauses
c [cce-18] scheduling 132592 clauses = 89545 binary + 43047 ternary
c [cce-18] tried to eliminate 3539 small clauses 3%
c [cce-18] eliminated 573 small clauses 0%
c [cce-18] eliminated 504 binary clauses 1%
c [cce-18] eliminated 69 ternary clauses 0%
c [cce-18-1] eliminated 591 small clauses in 105529142 steps
c [cce-18-1] incomplete small round (ACCE)
c [cce-18-1] eliminated 1650 covered clauses in round 1
c [cce-18] eliminated 1650 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 28362 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20-1] eliminated 243 variables 1% in round 1 in 17965407 steps
c [elim-20-1] backward subsumption/strengthening limit 35930814
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 5662249 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 243 = 1% variables out of 28362
c [bca-19] limit of 10000000 steps
c [bca-19] 36291 out of 56240 literals actually usable 65%
c [bca-19] added 153 blocked clauses in 101259 steps
c [simplification-20] removed 553 variables 1.9% (28119 remain 12%)
c [simplification-20] removed 6175 irredundant clauses 3.2% (186340 remain 16%)
c [simplification-20] maximum reduction of 3% = max (2%, 3%)
c [simplification-20] geometric conflict interval increment 16000 = 64000 / 4
c [simplification-20] new conflict interval 80000
c [simplification-20] penalized conflict interval 80000 = 1 * 80000
c [simplification-20] new conflict limit 519050
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  301.6   28119   186340    449203   17891   8206 334790   6 86.8 173.7   38
c i  305.6   28118   186340    460619   27487   8288 334825   5 87.4 174.4   51
c -  307.5   28118   186340    464219   18552   8326 334842   5 87.2 174.1   38
c -  314.3   28118   186340    481636   19468   8460 334903   4 87.5 174.0   38
c -  321.9   28118   186340    498705   20435   8607 334978   5 86.8 173.1   38
c i  322.2   28117   186340    499536   21208   8612 334983   5 86.7 173.0   39
c 
c [simplification-21] limit of 519570 conflicts hit after 519570 conflicts
c [ternres-19] limit 62538637 with penalty 0 = 0 + 0
c [ternres-19] all 28117 free variables schedulable
c [ternres-19] 218 ternary resolvents (3 bin, 215 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 1954332 penalty 4 = 4 + 0
c [card-6] found 9594 at-most-one constraints of average size 3.6
c [card-6] found 1349 at-most-two constraints of average size 4.4
c [card-6] using previous limit 1954332 for elimination
c [card-6] 10906 out of 10943 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-39] removed 11 variables
c [simpleprobe-8] all 28108 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 13 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 13 variables, found 23402 hbrs, 6 units
c [lift-19] limit 20000000 with penalty 0 = 0 + 0
c [lift-19] using 23127 probes 82%
c [lift-19] 13 units, 52 impls, 10 eqs in 1 rounds
c [lift-19] 23837 variables remain 85% (4233 retained)
c [lift-19] removed 25 variables
c [unhide-21] limit 12507727 with penalty 0 = 0 + 0
c [unhide-21-64] 0 units, 0 failed, 24116 tauts, 0 hbrs, 290248 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 170 transitive binary clauses
c [cce-19] limit of 125077275 steps penalty 0 = 0 + 0
c [cce-19-1] eliminated 1 clauses out of 10 (10%) of length 10
c [cce-19-1] eliminated 1 clauses out of 805 (0%) of length 6
c [cce-19-1] eliminated 31 clauses out of 5437 (1%) of length 5
c [cce-19-1] eliminated 1189 clauses out of 12289 (10%) of length 4
c [cce-19-1] incomplete large round (ACCE)
c [cce-19-1] eliminated 1222 large clauses in 125077276 steps
c [cce-19-1] allowing another 62538638 steps for small clauses
c [cce-19] scheduling 123899 clauses = 88197 binary + 35702 ternary
c [cce-19] tried to eliminate 5016 small clauses 4%
c [cce-19] eliminated 1016 small clauses 1%
c [cce-19] eliminated 830 binary clauses 1%
c [cce-19] eliminated 186 ternary clauses 1%
c [cce-19-1] eliminated 1016 small clauses in 125077276 steps
c [cce-19-1] incomplete small round (ACCE)
c [cce-19-1] eliminated 2238 covered clauses in round 1
c [cce-19] eliminated 2238 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 28070 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21-1] eliminated 232 variables 1% in round 1 in 16799422 steps
c [elim-21-1] backward subsumption/strengthening limit 33598844
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 5480665 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 232 = 1% variables out of 28070
c [bca-20] limit of 10000000 steps
c [bca-20] 34071 out of 55678 literals actually usable 61%
c [bca-20] added 102 blocked clauses in 105454 steps
c [rephase-8] after 519570 conflicts (new increment 160000, next 679570)
c [flushphases] 0 phases reset
c [simplification-21] removed 279 variables 1.0% (27838 remain 11%)
c [simplification-21] removed 3386 irredundant clauses 1.8% (182954 remain 16%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 26666 = 80000 / 3
c [simplification-21] new conflict interval 106666
c [simplification-21] penalized conflict interval 106666 = 1 * 106666
c [simplification-21] new conflict limit 626236
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  340.6   27838   182954    524833   21037   8822 334032   3 88.7 173.5   39
c -  346.4   27838   182954    548955   21652   8848 334037   5 91.9 174.4   39
c -  352.7   27838   182954    575599   22179   8864 334040   7 94.9 175.2   39
c R  354.3   27838   182954    584212   26190   8864 334040   8 95.8 175.3   47
c -  360.8   27838   182954    598419   22801   9006 334093   6 95.2 174.5   39
c i  362.1   27837   182954    601572   25635   9035 334124   5 94.9 174.3   41
c -  369.5   27837   182954    618632   23840   9168 334173   4 94.4 173.5   38
c 
c [simplification-22] limit of 626566 conflicts hit after 626566 conflicts
c [ternres-20] limit 74474810 with penalty 0 = 0 + 0
c [ternres-20] all 27837 free variables schedulable
c [ternres-20] 193 ternary resolvents (2 bin, 191 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-41] removed 2 variables
c [treelook-8] limit 3723740 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 44803 literals 80%
c [treelook-8] scheduling used 1000204 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 3723740 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 3735703 steps
c [treelook-8] 44537 literals remain 80%
c [treelook-8] 9965 variables remain to probed next time 36%
c [treelook-8] removed 7 variables, found 11180 hbrs
c [lift-20] limit 20000000 with penalty 0 = 0 + 0
c [lift-20] using 22396 probes 80%
c [lift-20] 12 units, 61 impls, 7 eqs in 1 rounds
c [lift-20] 23083 variables remain 83% (4715 retained)
c [lift-20] removed 31 variables
c [cliff-17] limit of 14894962 steps penalty 2 = 2 + 0
c [cliff-17] failed 0, lifted 0
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 219 transitive binary clauses
c [cce-20] limit of 148949621 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 118
c [cce-20-1] eliminated 2 clauses out of 8 (25%) of length 12
c [cce-20-1] eliminated 2 clauses out of 8 (25%) of length 11
c [cce-20-1] eliminated 2 clauses out of 11 (18%) of length 10
c [cce-20-1] eliminated 1 clauses out of 9 (11%) of length 9
c [cce-20-1] eliminated 2 clauses out of 15 (13%) of length 8
c [cce-20-1] eliminated 1 clauses out of 49 (2%) of length 7
c [cce-20-1] eliminated 4 clauses out of 830 (0%) of length 6
c [cce-20-1] eliminated 16 clauses out of 5412 (0%) of length 5
c [cce-20-1] eliminated 994 clauses out of 11161 (9%) of length 4
c [cce-20-1] incomplete large round (ACCE)
c [cce-20-1] eliminated 1027 large clauses in 148949622 steps
c [cce-20-1] allowing another 74474811 steps for small clauses
c [cce-20] scheduling 129691 clauses = 87074 binary + 42617 ternary
c [cce-20] tried to eliminate 4634 small clauses 4%
c [cce-20] eliminated 741 small clauses 1%
c [cce-20] eliminated 624 binary clauses 1%
c [cce-20] eliminated 117 ternary clauses 0%
c [cce-20-1] eliminated 741 small clauses in 148949622 steps
c [cce-20-1] incomplete small round (ACCE)
c [cce-20-1] eliminated 1768 covered clauses in round 1
c [cce-20] eliminated 1768 covered clauses in TOTAL during 1 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 27798 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22-1] eliminated 161 variables 1% in round 1 in 16294010 steps
c [elim-22-1] backward subsumption/strengthening limit 32588020
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 5364984 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 161 = 1% variables out of 27798
c [bca-21] limit of 10000000 steps
c [bca-21] 32894 out of 55276 literals actually usable 60%
c [bca-21] added 84 blocked clauses in 100696 steps
c [simplification-22] removed 200 variables 0.7% (27637 remain 11%)
c [simplification-22] removed 2340 irredundant clauses 1.3% (180614 remain 15%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 53333 = 106666 / 2
c [simplification-22] new conflict interval 159999
c [simplification-22] penalized conflict interval 159999 = 1 * 159999
c [simplification-22] new conflict limit 786565
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  386.8   27637   180614    644189   24516   9349 346207   8 93.9 172.6   39
c i  395.9   27636   180614    663754   40404   9497 346267   7 93.0 171.5   53
c -  396.6   27636   180614    666238   25761   9505 346269   4 93.0 171.6   39
c i  399.9   27635   180614    674094   32400   9557 346307   4 92.8 171.4   46
c -  406.6   27635   180614    687702   26472   9664 346339   6 92.5 170.9   39
c -  413.2   27635   180614    712167   27232   9727 346355   8 93.6 171.1   39
c i  420.2   27634   180614    727346   39438   9832 346402   5 93.0 170.4   50
c -  424.4   27634   180614    737160   28259   9892 346422   5 93.1 170.3   40
c -  435.4   27634   180614    761518   29562  10016 346456   7 92.3 169.4   40
c -  446.6   27634   180614    786361   30026  10145 346515   4 91.9 168.8   40
c 
c [simplification-23] limit of 787247 conflicts hit after 787247 conflicts
c [ternres-21] limit 96068097 with penalty 0 = 0 + 0
c [ternres-21] all 27634 free variables schedulable
c [ternres-21] 119 ternary resolvents (0 bin, 119 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-43] removed 57 variables
c [basicprobe-8] limit 96068097 penalty 0 = 0 + 0
c [basicprobe-8-0] 6499 sched 24%, 112 failed, 0 lifted, 50673 hbrs
c [decomp-44] removed 135 variables
c [basicprobe-8-1] 5367 probes remain 20% after last round
c [basicprobe-8-1] 144 units = 144 failed (100%) + 0 lifted (0%)
c [basicprobe-8-1] removed 175 variables, found 60229 hbrs
c [bate-7] eliminated 132 asymmetric tautologies during probing
c [cgrclsr-6] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-6] all 27405 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [lift-21] limit 20000000 with penalty 0 = 0 + 0
c [lift-21] using 21512 probes 78%
c [lift-21] 10 units, 57 impls, 0 eqs in 1 rounds
c [lift-21] 22259 variables remain 81% (5136 retained)
c [lift-21] removed 10 variables
c [unhide-22] limit 9606809 with penalty 1 = 1 + 0
c [unhide-22-70] 0 units, 1 failed, 24350 tauts, 0 hbrs, 46035 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 194 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 27393 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 5 blocked clauses
c [block-7] 5 < 1/1000 * 177596 = 177 considered unsuccessful
c [cce-21] limit of 192136195 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-21-1] eliminated 2 clauses out of 8 (25%) of length 21
c [cce-21-1] eliminated 1 clauses out of 8 (12%) of length 19
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 16
c [cce-21-1] eliminated 1 clauses out of 11 (9%) of length 14
c [cce-21-1] eliminated 1 clauses out of 9 (11%) of length 13
c [cce-21-1] eliminated 3 clauses out of 9 (33%) of length 12
c [cce-21-1] eliminated 1 clauses out of 8 (12%) of length 11
c [cce-21-1] eliminated 3 clauses out of 13 (23%) of length 10
c [cce-21-1] eliminated 1 clauses out of 13 (8%) of length 9
c [cce-21-1] eliminated 2 clauses out of 12 (17%) of length 8
c [cce-21-1] eliminated 2 clauses out of 55 (4%) of length 7
c [cce-21-1] eliminated 5 clauses out of 794 (1%) of length 6
c [cce-21-1] eliminated 12 clauses out of 5343 (0%) of length 5
c [cce-21-1] eliminated 155 clauses out of 10091 (2%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 191 large clauses in 143877191 steps
c [cce-21-1] allowing another 71938595 steps for small clauses
c [cce-21] scheduling 126768 clauses = 85533 binary + 41235 ternary
c [cce-21] tried to eliminate 8645 small clauses 7%
c [cce-21] eliminated 1429 small clauses 1%
c [cce-21] eliminated 1195 binary clauses 1%
c [cce-21] eliminated 234 ternary clauses 1%
c [cce-21-1] eliminated 1429 small clauses in 192136196 steps
c [cce-21-1] incomplete small round (ACCE)
c [cce-21-1] eliminated 1620 covered clauses in round 1
c [cce-21] eliminated 1620 covered clauses in TOTAL during 1 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 27393 variables 100%
c [elim-23] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-23-1] eliminated 248 variables 1% in round 1 in 16853446 steps
c [elim-23-1] backward subsumption/strengthening limit 33706892
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 5245153 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 248 = 1% variables out of 27393
c [bca-22] limit of 10000000 steps
c [bca-22] 32127 out of 54292 literals actually usable 59%
c [bca-22] added 89 blocked clauses in 99414 steps
c [rephase-9] after 787247 conflicts (new increment 320000, next 1107247)
c [flushphases] 0 phases reset
c [simplification-23] removed 489 variables 1.8% (27145 remain 11%)
c [simplification-23] removed 4994 irredundant clauses 2.8% (175620 remain 15%)
c [simplification-23] maximum reduction of 3% = max (2%, 3%)
c [simplification-23] geometric conflict interval increment 39999 = 159999 / 4
c [simplification-23] new conflict interval 199998
c [simplification-23] penalized conflict interval 199998 = 1 * 199998
c [simplification-23] new conflict limit 987245
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  468.0   27144   175620    805986   43384  10032 355402   4 91.5 168.2   55
c -  472.3   27144   175620    813906   30345  10071 355423   6 91.3 167.9   39
c -  481.9   27144   175620    847616   31101  10106 355436   6 94.9 169.1   41
c i  490.0   27143   175620    868030   45610  10183 355454   5 95.9 169.2   59
c -  494.8   27143   175620    876377   31796  10225 355473   4 95.7 168.9   39
c -  508.4   27143   175620    905440   32850  10342 355510   7 95.4 168.2   40
c i  512.9   27142   175620    919231   41870  10367 355517   4 95.1 167.8   51
c -  521.4   27141   175620    935686   33726  10452 355553   6 94.6 167.3   40
c i  530.8   27140   175620    956135   50271  10543 355594   4 94.4 167.0   58
c -  534.6   27140   175620    964472   34663  10579 355604   4 94.5 166.9   40
c 
c [simplification-24] limit of 987809 conflicts hit after 987809 conflicts
c [ternres-22] limit 123325552 with penalty 0 = 0 + 0
c [ternres-22] all 27140 free variables schedulable
c [ternres-22] 259 ternary resolvents (3 bin, 256 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-45] removed 6 variables
c [simpleprobe-9] all 27139 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 8 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 8 variables, found 24252 hbrs, 2 units
c [lift-22] limit 20000000 with penalty 0 = 0 + 0
c [lift-22] using 20830 probes 77%
c [lift-22] 10 units, 51 impls, 1 eqs in 1 rounds
c [lift-22] 21548 variables remain 79% (5572 retained)
c [lift-22] removed 11 variables
c [unhide-23] limit 20000000 with penalty 0 = 0 + 0
c [unhide-23-81] 0 units, 0 failed, 29287 tauts, 0 hbrs, 907143 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 158 transitive binary clauses
c [cce-22] limit of 246651104 steps penalty 0 = 0 + 0
c [cce-22-1] eliminated 1 clauses out of 3 (33%) of length 41
c [cce-22-1] eliminated 2 clauses out of 5 (40%) of length 40
c [cce-22-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-22-1] eliminated 2 clauses out of 48 (4%) of length 7
c [cce-22-1] eliminated 2 clauses out of 800 (0%) of length 6
c [cce-22-1] eliminated 14 clauses out of 5320 (0%) of length 5
c [cce-22-1] eliminated 55 clauses out of 10022 (1%) of length 4
c [cce-22-1] completed large round (ACCE)
c [cce-22-1] eliminated 77 large clauses in 142547444 steps
c [cce-22-1] allowing another 71273722 steps for small clauses
c [cce-22] scheduling 117823 clauses = 83814 binary + 34009 ternary
c [cce-22] tried to eliminate 14937 small clauses 13%
c [cce-22] eliminated 2386 small clauses 2%
c [cce-22] eliminated 1955 binary clauses 2%
c [cce-22] eliminated 431 ternary clauses 1%
c [cce-22-1] eliminated 2386 small clauses in 246651105 steps
c [cce-22-1] incomplete small round (ACCE)
c [cce-22-1] eliminated 2463 covered clauses in round 1
c [cce-22] eliminated 2463 covered clauses in TOTAL during 1 rounds
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 27120 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24-1] eliminated 199 variables 1% in round 1 in 15642429 steps
c [elim-24-1] backward subsumption/strengthening limit 31284858
c [elim-24-1] subsumed 0 and strengthened 0 clauses in 5110095 steps
c [elim-24] fully completed in 1 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 199 = 1% variables out of 27120
c [bca-23] limit of 10000000 steps
c [bca-23] 29499 out of 53844 literals actually usable 55%
c [bca-23] added 79 blocked clauses in 110955 steps
c [simplification-24] removed 219 variables 0.8% (26921 remain 11%)
c [simplification-24] removed 3233 irredundant clauses 1.8% (172387 remain 15%)
c [simplification-24] maximum reduction of 2% = max (1%, 2%)
c [simplification-24] geometric conflict interval increment 66666 = 199998 / 3
c [simplification-24] new conflict interval 266664
c [simplification-24] penalized conflict interval 266664 = 1 * 266664
c [simplification-24] new conflict limit 1254473
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  564.0   26920   172387    989579   48231  10991 349028   5 95.9 167.4   61
c -  570.7   26920   172387   1001426   34716  11048 349043   6 95.6 167.0   42
c i  582.3   26919   172387   1025874   54275  11134 349092   5 95.3 166.5   59
c i  582.3   26918   172387   1025875   54275  11134 349092   5 95.3 166.5   59
c -  585.3   26918   172387   1031718   36102  11155 349101   4 95.2 166.3   41
c -  599.2   26918   172387   1062161   36637  11257 349134   4 95.1 165.8   41
c -  613.6   26918   172387   1095083   37627  11391 349177   5 94.9 165.3   41
c -  624.3   26918   172387   1134664   38162  11401 349183   7 100.2 167.0   42
c -  636.5   26918   172387   1174537   38829  11405 349187   4 105.8 168.9   42
c -  650.7   26918   172387   1234708   39497  11416 349192   6 110.6 169.9   43
c 
c [simplification-25] limit of 1254855 conflicts hit after 1254855 conflicts
c [ternres-23] limit 154835685 with penalty 0 = 0 + 0
c [ternres-23] all 26918 free variables schedulable
c [ternres-23] 197 ternary resolvents (3 bin, 194 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-47] removed 4 variables
c [treelook-9] limit 7741784 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 43324 literals 80%
c [treelook-9] scheduling used 1038189 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 7741784 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 7755623 steps
c [treelook-9] 42980 literals remain 80%
c [treelook-9] 9618 variables remain to probed next time 36%
c [treelook-9] removed 2 variables, found 17385 hbrs
c [lift-23] limit 20000000 with penalty 0 = 0 + 0
c [lift-23] using 20168 probes 75%
c [lift-23] 3 units, 47 impls, 1 eqs in 1 rounds
c [lift-23] 20877 variables remain 78% (6034 retained)
c [lift-23] removed 4 variables
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 212 transitive binary clauses
c [cce-23] limit of 309671370 steps penalty 0 = 0 + 0
c [cce-23-1] eliminated 1 clauses out of 5 (20%) of length 23
c [cce-23-1] eliminated 5 clauses out of 812 (1%) of length 6
c [cce-23-1] eliminated 10 clauses out of 5336 (0%) of length 5
c [cce-23-1] eliminated 48 clauses out of 10027 (0%) of length 4
c [cce-23-1] completed large round (ACCE)
c [cce-23-1] eliminated 64 large clauses in 147359184 steps
c [cce-23-1] allowing another 73679592 steps for small clauses
c [cce-23] scheduling 122354 clauses = 81560 binary + 40794 ternary
c [cce-23] tried to eliminate 18521 small clauses 15%
c [cce-23] eliminated 2512 small clauses 2%
c [cce-23] eliminated 2030 binary clauses 2%
c [cce-23] eliminated 482 ternary clauses 1%
c [cce-23-1] eliminated 2512 small clauses in 309671371 steps
c [cce-23-1] incomplete small round (ACCE)
c [cce-23-1] eliminated 2576 covered clauses in round 1
c [cce-23] eliminated 2576 covered clauses in TOTAL during 1 rounds
c [elim-25] scheduling all variables this time
c [elim-25] scheduled 26911 variables 100%
c [elim-25] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-25-1] eliminated 218 variables 1% in round 1 in 15765514 steps
c [elim-25-1] backward subsumption/strengthening limit 31531028
c [elim-25-1] subsumed 0 and strengthened 0 clauses in 5004777 steps
c [elim-25] fully completed in 1 rounds
c [elim-25] transition to [ all 0 rem 0 ] state
c [elim-25] eliminated 218 = 1% variables out of 26911
c [bca-24] limit of 10000000 steps
c [bca-24] 29516 out of 53388 literals actually usable 55%
c [bca-24] added 37 blocked clauses in 108640 steps
c [rephase-10] after 1254855 conflicts (new increment 640000, next 1894855)
c [flushphases] 0 phases reset
c [simplification-25] removed 225 variables 0.8% (26693 remain 11%)
c [simplification-25] removed 2922 irredundant clauses 1.7% (169465 remain 14%)
c [simplification-25] maximum reduction of 2% = max (1%, 2%)
c [simplification-25] geometric conflict interval increment 88888 = 266664 / 3
c [simplification-25] new conflict interval 355552
c [simplification-25] penalized conflict interval 355552 = 1 * 355552
c [simplification-25] new conflict limit 1610407
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  676.1   26693   169465   1302878   39493  11684 364860   5 113.1 170.5   43
c -  689.3   26693   169465   1363527   39924  11685 364860   6 115.0 170.9   43
c -  709.3   26693   169465   1440456   40355  11702 364862   5 117.1 171.2   43
c -  722.5   26693   169465   1493632   40883  11716 364867   8 117.2 171.4   43
c -  735.1   26693   169465   1544038   41453  11723 364868   4 117.8 171.7   43
c 
c [simplification-26] limit of 1610431 conflicts hit after 1610433 conflicts
c [ternres-24] limit 190325072 with penalty 0 = 0 + 0
c [ternres-24] all 26693 free variables schedulable
c [ternres-24] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-24] fully completed ternary resolution
c [gauss-9] limit 2379063 penalty 4 = 4 + 0
c [gauss-9] extracted 8 xors of average arity 3.0
c [gauss-9] connected 24 occurrences of 21 variables (average 1.1)
c [gauss-9] limit 2379063 penalty 4 = 4 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-49] removed 1 variables
c [basicprobe-9] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 5443 sched 20%, 51 failed, 0 lifted, 33679 hbrs
c [decomp-50] removed 56 variables
c [basicprobe-9-1] 4462 probes remain 17% after last round
c [basicprobe-9-1] 65 units = 65 failed (100%) + 0 lifted (0%)
c [basicprobe-9-1] removed 70 variables, found 42668 hbrs
c [bate-8] eliminated 47 asymmetric tautologies during probing
c [lift-24] limit 20000000 with penalty 0 = 0 + 0
c [lift-24] using 19401 probes 73%
c [lift-24] 7 units, 50 impls, 1 eqs in 1 rounds
c [lift-24] 20113 variables remain 76% (6501 retained)
c [lift-24] removed 8 variables
c [cliff-18] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-18] failed 0, lifted 0
c [unhide-24] limit 10000000 with penalty 1 = 1 + 0
c [unhide-24-86] 0 units, 0 failed, 21265 tauts, 0 hbrs, 924703 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 102 transitive binary clauses
c [cce-24] limit of 380650145 steps penalty 0 = 0 + 0
c [cce-24-1] eliminated 1 clauses out of 1 (100%) of length 120
c [cce-24-1] eliminated 1 clauses out of 4 (25%) of length 19
c [cce-24-1] eliminated 2 clauses out of 6 (33%) of length 11
c [cce-24-1] eliminated 3 clauses out of 17 (18%) of length 9
c [cce-24-1] eliminated 1 clauses out of 24 (4%) of length 8
c [cce-24-1] eliminated 4 clauses out of 54 (7%) of length 7
c [cce-24-1] eliminated 15 clauses out of 821 (2%) of length 6
c [cce-24-1] eliminated 18 clauses out of 5320 (0%) of length 5
c [cce-24-1] eliminated 55 clauses out of 9998 (1%) of length 4
c [cce-24-1] completed large round (ACCE)
c [cce-24-1] eliminated 100 large clauses in 139026204 steps
c [cce-24-1] allowing another 69513102 steps for small clauses
c [cce-24] scheduling 112191 clauses = 79234 binary + 32957 ternary
c [cce-24] tried to eliminate 27226 small clauses 24%
c [cce-24] eliminated 3519 small clauses 3%
c [cce-24] eliminated 2685 binary clauses 3%
c [cce-24] eliminated 834 ternary clauses 3%
c [cce-24-1] eliminated 3519 small clauses in 380650146 steps
c [cce-24-1] incomplete small round (ACCE)
c [cce-24-1] eliminated 3619 covered clauses in round 1
c [cce-24] eliminated 3619 covered clauses in TOTAL during 1 rounds
c [elim-26] scheduling all variables this time
c [elim-26] scheduled 26614 variables 100%
c [elim-26] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-26-1] eliminated 322 variables 1% in round 1 in 15579540 steps
c [elim-26-1] backward subsumption/strengthening limit 31159080
c [elim-26-1] subsumed 0 and strengthened 0 clauses in 4832649 steps
c [elim-26] fully completed in 1 rounds
c [elim-26] transition to [ all 0 rem 0 ] state
c [elim-26] eliminated 322 = 1% variables out of 26614
c [bca-25] limit of 10000000 steps
c [bca-25] 28910 out of 52586 literals actually usable 55%
c [bca-25] added 87 blocked clauses in 124997 steps
c [simplification-26] removed 401 variables 1.5% (26292 remain 11%)
c [simplification-26] removed 5052 irredundant clauses 3.0% (164413 remain 14%)
c [simplification-26] maximum reduction of 3% = max (2%, 3%)
c [simplification-26] geometric conflict interval increment 88888 = 355552 / 4
c [simplification-26] new conflict interval 444440
c [simplification-26] penalized conflict interval 444440 = 1 * 444440
c [simplification-26] new conflict limit 2054873
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  777.2   26292   164413   1623695   41201  12017 372675   5 120.4 172.5   44
c -  793.8   26292   164413   1682813   41764  12033 372676   6 125.5 174.2   44
c -  809.4   26292   164413   1740721   42456  12051 372680   5 128.1 175.4   44
c -  820.0   26292   164413   1785319   42925  12059 372681   5 129.7 176.5   44
c -  840.5   26292   164413   1867637   43589  12078 372686   5 131.7 177.2   44
c -  860.0   26292   164413   1952758   44025  12082 372689   4 133.0 177.5   62
c -  872.6   26292   164413   2001866   44683  12107 372699   6 133.6 178.5   62
c 
c [simplification-27] limit of 2054939 conflicts hit after 2054940 conflicts
c [ternres-25] limit 200000000 with penalty 0 = 0 + 0
c [ternres-25] all 26292 free variables schedulable
c [ternres-25] 177 ternary resolvents (6 bin, 171 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-51] removed 4 variables
c [simpleprobe-10] all 26288 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-52] removed 6 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 6 variables, found 19455 hbrs, 1 units
c [lift-25] limit 20000000 with penalty 0 = 0 + 0
c [lift-25] using 18607 probes 71%
c [lift-25] 2 units, 33 impls, 4 eqs in 1 rounds
c [lift-25] 19386 variables remain 74% (6890 retained)
c [lift-25] removed 6 variables
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 289 transitive binary clauses
c [cce-25] limit of 469786028 steps penalty 0 = 0 + 0
c [cce-25-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-25-1] eliminated 3 clauses out of 4 (75%) of length 58
c [cce-25-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-25-1] eliminated 2 clauses out of 13 (15%) of length 14
c [cce-25-1] eliminated 1 clauses out of 8 (12%) of length 13
c [cce-25-1] eliminated 2 clauses out of 10 (20%) of length 12
c [cce-25-1] eliminated 2 clauses out of 19 (11%) of length 9
c [cce-25-1] eliminated 3 clauses out of 58 (5%) of length 7
c [cce-25-1] eliminated 9 clauses out of 833 (1%) of length 6
c [cce-25-1] eliminated 27 clauses out of 5337 (1%) of length 5
c [cce-25-1] eliminated 88 clauses out of 10068 (1%) of length 4
c [cce-25-1] completed large round (ACCE)
c [cce-25-1] eliminated 141 large clauses in 139647449 steps
c [cce-25-1] allowing another 69823724 steps for small clauses
c [cce-25] scheduling 115786 clauses = 76103 binary + 39683 ternary
c [cce-25] tried to eliminate 29044 small clauses 25%
c [cce-25] eliminated 2752 small clauses 2%
c [cce-25] eliminated 2197 binary clauses 3%
c [cce-25] eliminated 555 ternary clauses 1%
c [cce-25-1] eliminated 2752 small clauses in 469786029 steps
c [cce-25-1] incomplete small round (ACCE)
c [cce-25-1] eliminated 2893 covered clauses in round 1
c [cce-25] eliminated 2893 covered clauses in TOTAL during 1 rounds
c [elim-27] scheduling all variables this time
c [elim-27] scheduled 26276 variables 100%
c [elim-27] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-27-1] eliminated 216 variables 1% in round 1 in 14991660 steps
c [elim-27-1] backward subsumption/strengthening limit 29983320
c [elim-27-1] subsumed 0 and strengthened 0 clauses in 4718014 steps
c [elim-27] fully completed in 1 rounds
c [elim-27] transition to [ all 0 rem 0 ] state
c [elim-27] eliminated 216 = 1% variables out of 26276
c [bca-26] limit of 10000000 steps
c [bca-26] 28375 out of 52122 literals actually usable 54%
c [bca-26] added 59 blocked clauses in 126968 steps
c [rephase-11] after 2054940 conflicts (new increment 1280000, next 3334940)
c [flushphases] 0 phases reset
c [simplification-27] removed 232 variables 0.9% (26060 remain 11%)
c [simplification-27] removed 3151 irredundant clauses 1.9% (161262 remain 14%)
c [simplification-27] maximum reduction of 2% = max (1%, 2%)
c [simplification-27] geometric conflict interval increment 148146 = 444440 / 3
c [simplification-27] new conflict interval 592586
c [simplification-27] penalized conflict interval 592586 = 1 * 592586
c [simplification-27] new conflict limit 2647526
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  904.1   26060   161262   2069514   44950  12543 391083   4 134.8 179.8   45
c -  913.8   26060   161262   2109191   45436  12548 391083   4 135.1 180.9   45
c -  922.8   26060   161262   2148190   45951  12548 391083   4 135.1 182.0   45
c -  933.8   26060   161262   2190489   46470  12548 391083   4 135.4 183.1   45
c -  944.0   26060   161262   2233120   46976  12555 391083   4 135.8 184.4   45
c -  955.5   26060   161262   2282196   47334  12561 391089   4 135.7 185.2   45
c -  970.3   26060   161262   2339689   48063  12589 391098   5 136.0 185.8   45
c -  988.4   26060   161262   2411819   48591  12599 391101   4 136.3 186.0   64
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1697 basic ate = 1386 trn 82% + 311 lrg 18% in 8 updates
c bcas: 26 count, 3352 added (902 skipped), 3771973 steps
c bkwd: tried 6259781 clauses, 12519442 lits, 2.00 lits/clause
c bkwd: checked 151993957 occs, 24.28 occs/clause, 12.14 occs/lit
c bkwd: subsumed 0 binary, 110 ternary, 10 large
c bkwd: strengthened 2 binary, 1 ternary (100% self), 2 large (0% self)
c blkd: 7 bces, 10615 removed, 6872562 resolutions, 21782621 steps
c blkd: 19415 blocking literals 4%, 51 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 0 am1, 13442811 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 135658 subsumed
c card: 82590 at-most-one constraints found, average size 4.31
c card: 82590 at-most-one constraints used 100%, average size 4.31
c card: 1817 at-most-two constraints found, average size 4.50
c card: 1755 at-most-two constraints used 97%, average size 4.50
c cces: 25 cces, 64185 eliminated, 61170 ate 95%, 3015 abce 5%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 6 count, 1537333 esteps, 97939 csteps
c cgrs: 0 eqs, 0 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: 2071 extracted (1962 ands 95%, 106 xors 5%, 3 ites 0%)
c clff: 18 cliffs, 1077 lifted, 347 failed
c clff: 31756 decisions, 273916905 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3942722 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 250 gcs, 0 rescored clauses, 1288 rescored vars
c dcps: 52 decompositions, 63573 equivalent 25%
c deco: 860358 decision-only clauses 35%, 58% reduction
c decs: 12672351 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 453079 flipped 3.575% (in 2478 phases)
c elms: 27 elims, 83748 eliminated 33%
c elms: 53 rounds, 2.0 rounds/bve
c elms: 58237 small 70%, 25460 large 30%
c elms: 272187 tried small, 58248 succeeded 21%, 213939 failed 79%
c elms: 41591 subsumed, 126037 strengthened, 4418 blocked
c elms: 27387506 copies, 26080903 resolutions, 7907507 ipos
c elms: 8956510 subchks, 6635598 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 9 extractions, 1039 extracted, 2.2 size, 3 max
c gaus: exported 1 units, 19 binary and 0 ternary equations
c gaus: 0 gc, 27106584 steps, 13553292 extr 50%, 26310 elim 0%
c glue: 136.2 orig avg, 118.6 real avg, 8.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 1095087 = 207147 simple + 863061 trn 19% + 24879 lrg 79%, 4453 sub 2%
c hght: 186 average, 1.37 height/glue
c ints: 65534 luby (18677775 steps), 0 inout (0 steps)
c lift: 25 phases, 44500 probed (15216 level1 34%, 29284 level2 66%)
c lift: 1211 units, 195 equivalences, 947 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2450069 clauses, 211.0 length
c lrnd: 1049008 uips 43%, 1262376 flips 52%
c mega: 0 count, 0 failed, 0 rounds
c mins: 516964358 learned lits, 37% minimized
c mins: 1553860 mins 63%, 5833 bin 0%, 30018 size 1%, 860358 deco 35%
c move: moved 2450069, 27570 bin 1%, 9473 trn 0%, 0 lrg 0%
c otfs: str 60673 dyn (60472 red, 201 irr) 14048 drv 23%, 46625 rst 77%
c otfs: sub 427 dyn (427 red, 0 irr)
c phas: 11 computed, 105797 set, 23260 pos (22%), 82537 neg (78%)
c prbs: 9 basic, 65628 probed, 1269 failed, 23 lifted
c prbs: 10 simple, 835792 probed, 519 failed, 2615 eqs
c prbs: 9 treelook, 811 probed, 23 failed, 0 lifted
c prps: 2814739808 props, 214 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c psns: 117350385 searches, 16767907 hits, 14% 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: 88 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 88 arith 100%, 0 double 0%
c rmbd: 37668 removed, 8302 red 22%
c rphs: 11 recomputed phases
c rsts: 32395 restarts 49%, 33139 skipped 51%
c rsts: 32769 saturating 99%, 6 agile 0%, 364 reuse 1%
c rsts: 75.9 avg interval, 75.9 scaled, 1.0 factor
c rsts: 5969 kept 18.4% average 22.5%
c simp: 27 count (27 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2450069 count (3569350 tried 1.5), 843831 sub out of 2432700 (34.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 2 count
c tops: 78947 fixed 31%, 529 its, 4658.07 confs/it
c trvs: 46302558906 traversals, 98% srch, 3% simp, 0% lkhd
c trvs: 16.7 search traversals per propagation, 18402.0 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 25 transitive reductions, 5441 removed, 46 failed
c trds: 37152 nodes, 113358 edges, 49511288 steps
c trim: 58669154 words, 223.8 MB
c trnr: 25 count, 27 bin, 5685 trn, 170166184 steps
c unhd: 24 count, 86 rounds, 152476050 steps
c unhd: 1748 non-trivial sccs of average size 2.4
c unhd: 109 units, 107 bin, 1 trn, 1 lrg
c unhd: 2080 failed, 1939 stamp, 0 lits, 41 bin, 19 trn, 1 lrg
c unhd: 416745 tauts, 20276 bin 5%, 9891 trn 2%, 1622 lrg 0%
c unhd: 416745 tauts, 384956 stamp 92%, 364072 red 87%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3569271 str, 107 bin 0%, 4794 trn 0%, 3564370 lrg 100%, 3549682 red 99%
c vars: 26060 remaining 10% and 226268 removed 90% out of 252328
c vars: 78947 fixed 31%, 83748 eliminated 33%, 63573 equivalent 25%
c vsts: 28558112944 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 10.2 search visits per propagation, 11200.9 per conflict
c wchs: 2810744026 pushed, 52357468 enlarged, 363 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2432700 100   1410368 100 194257728 100  21160561 100   1056873 100
c 
c  0      31813   1         0   0  69621183  36   2636040  12     79409   8 
c  1      19215   1         0   0  40557323  21   1677128   8     56146   5 
c  2      60625   2     19008   1  58322316  30<  4483560  21    145530  14 
c  3     135105   6    123538   9   6744698   3   1852608   9     93000   9 
c  4     181439   7    172633  12   6034351   3   2169207  10<   113546  11 
c  5     208632   9    195869  14   4249433   2   1808360   9    110096  10<
c  6     202336   8    173449  12   2711420   1   1356164   6     97429   9 
c  7     184738   8    144954  10<  1773640   1   1029583   5     79211   7 
c  8     173829   7<   124192   9   1235227   1    821269   4     63175   6 
c  9     151681   6     98588   7    713009   0    568278   3     45189   4 
c 10     209322   9    117116   8    605098   0    613413   3     45700   4 
c 11     445276  18    125862   9    895934   0   1106548   5     66338   6 
c 12     424360  17    113648   8    785879   0   1027608   5     61256   6 
c 13       4329   0      1511   0      8217   0     10795   0       848   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             8.1           7.1           1.5           4.3           5.3
c std             3.3           2.8           1.9           3.5           3.5
c 
c   97.760  10% analysis
c   91.905   9% cce
c   42.057   4% unhide
c   27.154   3% elim
c   25.894   3% probe
c   23.011   2% bump
c   17.887   2% gc
c   16.359   2% decide
c   15.842   2% lift
c   10.507   1% decomp
c   10.382   1% restart
c    8.763   1% cliff
c    6.199   1% mincls
c    5.553   1% defrag
c    4.532   0% backward
c    3.431   0% transred
c    2.918   0% bca
c    2.093   0% gauss
c    1.902   0% block
c    1.341   0% reduce
c    1.274   0% ternres
c    1.149   0% cgrclsr
c    0.884   0% card
c    0.510   0% phase
c    0.097   0% tabularasa
c    0.020   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    7.521   1% probe simple     29%
c   15.350   2% probe basic      59%
c    3.023   0% probe tree-look  12%
c ==================================
c    6.709   1% preprocessing     3%
c  226.530  23% inprocessing     97%
c ==================================
c  233.240  23% simplifying
c  766.124  77% search
c ==================================
c  999.368 100% all
c 
c 12672351 decisions, 12680.4 decisions/sec
c 2464117 conflicts, 2465.7 conflicts/sec
c 2814739808 propagations, 2.8 megaprops/sec
c 999.4 seconds, 171.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
