c launch: /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c host: atom23
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/ACG-15-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c no embedded options
c found 'p cnf 262253 1131732' header
c read 262253 variables, 1131732 clauses, 2644763 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 252004 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  252004  1120813         0       0      0     0  10  0.0   0.0   61
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 15215 at-most-one constraints of average size 5.5
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 15215 out of 15215 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54025 variables
c [simpleprobe-1] all 208228 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 417 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 417 variables, found 11185 hbrs, 20 units
c [unhide-1] limit 427943 based on 855887 irredundant clauses
c [unhide-1-1] 6 units, 1919 failed, 14586 tauts, 0 hbrs, 5999 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 200713 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 87123 variables 43% in round 1 in 120203710 steps
c [elim-1-1] backward subsumption/strengthening limit 240407420
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 19960456 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 87123 = 43% variables out of 200713
c [phase-1] phase bias: 23761 positive 21%, 89829 negative 79%
c [simplification-1] removed 100519 variables 46.9% (113590 remain 45%)
c [simplification-1] removed 453255 irredundant clauses 40.4% (667558 remain 60%)
c [simplification-1] maximum reduction of 47% = max (47%, 40%)
c [simplification-1] large reduction 47% >= 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] 115917, max 298095, min4 29534 at 74%, min10 15625 at 89%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   11.5  113589   667558        15      14      0  4923  17  2.6  19.9   48
c R   11.5  113466   667558        24      23      0  4923  12 11.5  53.5   48
c R   11.6  113466   667558        64      54      5  4927   3  8.8  69.9   48
c i   11.6  113465   667558       105      77      8  4941   2  6.6 110.8   48
c R   11.6  113462   667558       166     117     15  4954   3  6.1 110.7   48
c i   11.7  113461   667558       240     150     21  4988   1  5.4 132.4   48
c i   11.7  113448   667558       241     150     21  4988   1  5.4 131.5   48
c i   11.8  113436   667558       248     155     21  4989   1  5.3 130.1   48
c R   12.0  113325   667558       413     307     24  4998   1 18.6 157.7   48
c i   12.3  113324   667558       668     502     41  5031   2 20.4 177.9   48
c i   12.4  113192   667558       675     507     42  5031   1 20.4 177.4   48
c i   12.4  112666   667558       685     512     44  5033   1 20.2 175.4   48
c i   12.6  112633   667558       872     656     58  5056   3 20.6 205.8   49
c i   12.6  112233   667558       877     658     58  5058   1 20.5 232.4   49
c R   12.8  112106   667558       992     747     65  5065   1 19.3 268.6   49
c i   12.9  112105   667558      1024     771     69  5068   0 20.0 282.6   49
c i   13.1  111758   667558      1242     943     85  5084   1 19.2 273.4   49
c i   13.2  111684   667558      1311     996     92  5089   1 18.6 268.3   49
c i   13.2  111667   667558      1350    1028     93  5089   2 18.8 267.5   49
c i   13.3  111659   667558      1371    1047     94  5089   1 18.9 275.2   49
c i   13.4  111177   667558      1489    1146    103  5098   2 18.4 272.9   49
c i   13.5  110976   667558      1494    1148    104  5099   2 18.3 272.4   49
c i   13.6  110962   667558      1517    1160    109  5104   1 18.3 268.4   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   13.6  110951   667558      1518    1160    109  5104   1 18.3 268.0   49
c i   13.6  110938   667558      1519    1160    109  5104   1 18.3 267.4   49
c i   13.6  110936   667558      1520    1160    109  5104   0 18.3 266.8   49
c i   13.6  110929   667558      1521    1160    109  5104   0 18.3 266.2   49
c i   13.6  110920   667558      1522    1160    109  5104   0 18.3 265.6   49
c i   13.6  110908   667558      1523    1160    109  5104   0 18.2 265.0   49
c i   13.6  110904   667558      1524    1160    109  5104   0 18.2 264.3   49
c i   13.6  110892   667558      1525    1160    109  5104   0 18.2 263.7   49
c i   13.7  110890   667558      1526    1160    109  5104   0 18.2 263.2   49
c i   13.7  110878   667558      1527    1160    109  5104   0 18.2 262.6   49
c i   13.7  110862   667558      1528    1160    109  5104   0 18.2 262.0   49
c i   13.7  110847   667558      1529    1160    109  5104   0 18.2 261.4   49
c i   13.7  110836   667558      1530    1160    109  5104   0 18.2 260.8   49
c i   13.7  110819   667558      1531    1160    109  5104   0 18.1 260.2   49
c i   13.7  110815   667558      1532    1160    109  5104   0 18.1 259.7   49
c i   13.7  110811   667558      1533    1160    109  5104   0 18.1 259.1   49
c i   13.8  110795   667558      1534    1160    109  5104   0 18.1 258.5   49
c i   13.8  110793   667558      1535    1160    109  5104   0 18.1 258.0   49
c i   13.8  110787   667558      1536    1160    109  5104   0 18.1 257.4   49
c i   13.8  110783   667558      1537    1160    109  5104   0 18.1 256.9   49
c i   13.8  110776   667558      1538    1160    109  5104   0 18.1 256.3   49
c i   13.8  110767   667558      1539    1160    109  5104   0 18.1 255.8   49
c i   13.8  110757   667558      1540    1160    109  5104   0 18.0 255.2   49
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   13.8  110747   667558      1541    1160    109  5104   0 18.0 254.7   49
c i   13.9  110737   667558      1542    1160    109  5104   0 18.0 254.2   49
c i   14.1  110728   667558      1622    1223    117  5109   1 18.4 260.6   49
c i   14.4  109715   667558      1895    1437    129  5123   1 21.5 264.4   49
c i   14.5  109666   667558      2012    1539    130  5129   2 21.5 265.3   50
c i   14.5  109649   667558      2013    1539    130  5129   1 21.4 264.8   50
c i   14.5  109641   667558      2015    1540    130  5129   1 21.4 264.3   50
c R   14.6  109623   667558      2305    1740    135  5157   1 21.7 261.2   50
c i   14.7  109622   667558      2307    1741    135  5157   1 21.8 262.5   50
c i   14.7  108766   667558      2308    1741    135  5157   0 21.8 263.8   50
c i   14.7  108755   667558      2309    1741    135  5157   0 21.7 264.9   50
c i   15.1  108740   667558      2468    1876    143  5169   1 23.3 282.8   50
c 
c [simplification-2] limit of 2504 conflicts hit after 2505 conflicts
c [decomp-3] removed 5281 variables
c [simpleprobe-2] all 108309 free variables schedulable
c [simpleprobe-2] limit 3742988 penalty 0 = 0 + 0
c [decomp-4] removed 1441 variables
c [simpleprobe-2] 54583 variables remain 51% (52285 retained)
c [simpleprobe-2] removed 1441 variables, found 11281 hbrs, 242 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 74737 literals 35%
c [treelook-1] scheduling used 375984 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 464114 steps
c [treelook-1] 74721 literals remain 35%
c [treelook-1] 72871 variables remain to probed next time 68%
c [decomp-5] removed 1 variables
c [treelook-1] removed 14 variables, found 3303 hbrs
c [basicprobe-1] limit 1252298 based on 626149 irredundant clauses
c [basicprobe-1-0] 32606 probes remain 31% after last round
c [basicprobe-1-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1095 variables, found 6732 hbrs
c [unhide-2] limit 313074 based on 626149 irredundant clauses
c [unhide-2-2] 10 units, 1354 failed, 2782 tauts, 0 hbrs, 9260 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 103644 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 11630 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 19 clauses out of 410 (5%) of length 10
c [cce-1-1] eliminated 218 clauses out of 2764 (8%) of length 9
c [cce-1-1] eliminated 35 clauses out of 226 (15%) of length 8
c [cce-1-1] eliminated 83 clauses out of 530 (16%) of length 7
c [cce-1-1] eliminated 4022 clauses out of 5259 (76%) of length 6
c [cce-1-1] eliminated 10948 clauses out of 55241 (20%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 15325 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 383223 clauses = 317147 binary + 66076 ternary
c [cce-1] tried to eliminate 2716 small clauses 1%
c [cce-1] eliminated 901 small clauses 0%
c [cce-1] eliminated 771 binary clauses 0%
c [cce-1] eliminated 130 ternary clauses 0%
c [cce-1-1] eliminated 901 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 16226 covered clauses in round 1
c [cce-1] eliminated 16226 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 103644 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 24669 not tried 24% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 9952 = 10% variables out of 103644
c [bca-1] limit of 10000000 steps
c [bca-1] 178789 out of 187386 literals actually usable 95%
c [bca-1] added 1790 blocked clauses in 510537 steps
c [phase-2] phase bias: 10 positive 5%, 175 negative 95%
c [simplification-2] removed 15034 variables 13.8% (93692 remain 37%)
c [simplification-2] removed 118325 irredundant clauses 17.7% (549233 remain 49%)
c [simplification-2] maximum reduction of 18% = max (14%, 18%)
c [simplification-2] large reduction 18% >= 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 4505
c [tabula-rasa-1] number clauses 549233 drops below limit 560406
c [flush-cache] 0 binary, 0 ternary, 943 large
c [flushphases] 93692 phases reset fully
c [phase-3] phase bias: 2024 positive 22%, 7219 negative 78%
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 23423 and clause limit 274616
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   33.6   93691   549233      2527      19    255 28294  12 23.2 279.8   43
c i   33.6   93690   549233      2564      50    257 28297  23 22.9 278.3   43
c i   33.6   93681   549233      2565      50    257 28297  22 22.9 278.3   43
c i   33.6   93671   549233      2566      50    257 28297  21 22.9 278.2   43
c i   33.6   93662   549233      2569      51    257 28298  20 22.9 278.1   43
c i   33.6   93649   549233      2575      51    259 28301  16 22.8 277.8   43
c i   33.7   93011   549233      2732     164    280 28319   4 21.8 273.6   44
c i   33.8   93004   549233      2772     191    284 28326   2 21.6 273.8   44
c i   33.8   93003   549233      2775     191    286 28326   2 21.5 273.4   44
c i   33.8   92998   549233      2778     191    286 28328   2 21.5 273.2   44
c i   33.8   92990   549233      2789     198    287 28330   2 21.4 273.0   44
c i   33.8   92985   549233      2790     198    287 28330   2 21.4 272.9   44
c i   33.8   92974   549233      2791     198    287 28330   2 21.4 272.8   44
c i   33.8   92969   549233      2792     198    287 28330   1 21.4 272.7   44
c i   33.8   92962   549233      2794     199    287 28330   1 21.4 272.5   44
c i   33.8   92951   549233      2816     214    289 28334   2 21.3 271.8   44
c i   33.9   92941   549233      2879     262    288 28343   2 21.0 270.5   44
c i   33.9   92556   549233      2883     264    288 28344   1 21.0 270.2   44
c i   34.2   92551   549233      2959     303    299 28368   1 20.6 268.4   44
c i   34.7   92518   549233      3126     413    304 28416   2 19.9 258.6   44
c i   34.8   92409   549233      3173     445    313 28421   2 19.7 258.3   44
c i   34.9   92087   549233      3310     560    322 28424   2 19.1 257.1   44
c i   34.9   92083   549233      3311     560    322 28424   2 19.1 257.1   44
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   34.9   92078   549233      3312     560    322 28424   2 19.1 257.0   44
c i   34.9   92073   549233      3313     560    322 28424   1 19.1 256.8   44
c i   34.9   92066   549233      3314     560    322 28424   1 19.1 256.7   44
c i   34.9   92058   549233      3315     560    322 28424   1 19.1 256.5   44
c i   34.9   92051   549233      3316     560    322 28424   1 19.1 256.4   44
c i   35.0   92041   549233      3430     657    329 28430   2 18.7 252.8   44
c i   35.0   91747   549233      3431     657    329 28430   2 18.7 252.8   44
c i   35.2   91723   549233      3577     770    340 28446   2 18.2 249.5   44
c i   35.2   91716   549233      3654     835    341 28453   2 18.2 248.5   44
c i   35.2   91715   549233      3676     854    342 28454   3 18.1 248.3   44
c i   35.2   91704   549233      3704     875    345 28454   3 18.0 248.1   44
c i   35.3   91703   549233      3808     973    345 28458   3 18.3 246.7   44
c i   35.3   91692   549233      3934    1073    355 28464   2 17.9 244.5   44
c i   35.4   91689   549233      4003    1132    358 28470   1 17.9 242.6   44
c i   35.5   91685   549233      4083    1198    363 28477   1 17.9 242.3   44
c i   35.7   91669   549233      4635    1658    377 28498   2 18.5 240.9   44
c i   35.7   91656   549233      4886    1845    384 28520   1 18.3 239.6   45
c R   35.8   91648   549233      5282    2138    416 28546   3 17.6 239.3   45
c i   36.0   91647   549233      5372    2193    427 28568   1 17.4 235.6   45
c i   36.1   91615   549233      5417    2233    430 28569   1 17.3 234.8   45
c i   36.2   91256   549233      5465    2268    434 28573   1 17.2 233.6   45
c i   36.4   90614   549233      5665    2428    447 28584   2 17.8 232.2   45
c i   36.5   90582   549233      5774    2510    458 28597   2 17.6 230.6   45
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   36.7   90580   549233      5841    2552    465 28613   1 17.5 229.2   45
c i   36.9   89862   549233      5947    2644    471 28616   1 17.3 228.0   45
c i   36.9   89861   549233      5972    2667    471 28616   2 17.3 227.5   45
c 
c [simplification-3] limit of 6143 conflicts hit after 6153 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 89720 free variables schedulable
c [ternres-1] 4053 ternary resolvents (8 bin, 4045 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 16294 at-most-one constraints of average size 4.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 16294 out of 16294 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 429 xors of average arity 2.1
c [gauss-1] connected 919 occurrences of 546 variables (average 1.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-6] removed 310 variables
c [gauss-1] exported 0 unary, 22 binary and 0 ternary equations
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 55826 literals 31%
c [treelook-2] scheduling used 302827 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 311399 steps
c [treelook-2] 55820 literals remain 31%
c [treelook-2] 46303 variables remain to probed next time 52%
c [treelook-2] removed 2 variables, found 1568 hbrs
c [cgrclsr-1] limit 262957 based on 525914 irredundant clauses
c [cgrclsr-1] all 89408 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 1 variables
c [lift-1] limit 1094958 with penalty 0 = 0 + 0
c [lift-1] using 73244 probes 82%
c [lift-1] 15 units, 3 impls, 0 eqs in 1 rounds
c [lift-1] 89387 variables remain 100% (5 retained)
c [lift-1] removed 15 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 44, lifted 2350
c [unhide-3] limit 364986 with penalty 0 = 0 + 0
c [unhide-3-3] 5 units, 871 failed, 14168 tauts, 0 hbrs, 6190 literals
c [transred-1] limit 1824930 with penalty 0 = 0 + 0
c [transred-1] removed 100 transitive binary clauses
c [transred-1] found 5 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 84563 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 210 blocked clauses
c [block-2] 210 < 1/1000 * 492598 = 492 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 6 clauses out of 448 (1%) of length 7
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 6 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 347984 clauses = 255411 binary + 92573 ternary
c [cce-2] tried to eliminate 308 small clauses 0%
c [cce-2] eliminated 92 small clauses 0%
c [cce-2] eliminated 65 binary clauses 0%
c [cce-2] eliminated 27 ternary clauses 0%
c [cce-2-1] eliminated 92 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 98 covered clauses in round 1
c [cce-2] eliminated 98 covered clauses in TOTAL during 1 rounds
c [cce-2] 98 < 1/1000 * 479706 = 479 considered unsuccessful
c [elim-3] 22913 variables 27% will be scheduled this time
c [elim-3] scheduled 22913 variables 27%
c [elim-3] limit of 36498602 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 1771 variables 2% in round 1 in 29983438 steps
c [elim-3-1] backward subsumption/strengthening limit 6515164
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 6515206 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 1771 = 2% variables out of 84547
c [bca-2] limit of 10000000 steps
c [bca-2] 151663 out of 165554 literals actually usable 92%
c [bca-2] added 34 blocked clauses in 406989 steps
c [phase-4] phase bias: 71 positive 83%, 15 negative 17%
c [simplification-3] removed 6944 variables 7.7% (82776 remain 33%)
c [simplification-3] removed 76589 irredundant clauses 13.9% (472644 remain 42%)
c [simplification-3] maximum reduction of 14% = max (8%, 14%)
c [simplification-3] large reduction 14% >= 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 8153
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   42.8   82775   472644      6216    2633   3206 42998   3 17.0 226.0   41
c i   43.0   82765   472644      6353    2741   3212 43003   2 17.7 224.4   41
c i   43.0   82750   472644      6365    2750   3213 43004   1 17.7 224.3   41
c i   43.3   82746   472644      6606    2943   3231 43023   2 17.5 221.7   41
c i   43.4   82526   472644      6728    3052   3233 43027   1 17.6 221.6   41
c i   43.4   82525   472644      6729    3052   3233 43027   1 17.6 221.6   41
c i   43.5   82524   472644      6760    3078   3234 43030   1 17.6 222.0   41
c i   43.5   82523   472644      6764    3078   3235 43032   1 17.5 221.9   41
c i   43.7   82471   472644      6906    3197   3247 43038   1 17.5 220.9   41
c i   43.7   82420   472644      6935    3217   3250 43043   1 17.4 220.7   41
c i   43.7   82401   472644      6943    3217   3250 43050   1 17.4 220.6   41
c i   43.7   82386   472644      6944    3217   3250 43050   1 17.4 220.5   41
c i   43.8   82376   472644      6945    3217   3250 43050   1 17.4 220.5   41
c i   43.8   82371   472644      6946    3217   3250 43050   0 17.4 220.4   41
c i   43.8   82365   472644      6947    3217   3250 43050   0 17.4 220.4   41
c i   43.8   82356   472644      6948    3217   3250 43050   0 17.4 220.3   41
c i   44.3   82252   472644      7649    3809   3287 43079   1 17.8 222.6   42
c i   44.3   81966   472644      7673    3832   3287 43079   1 17.8 222.7   42
c i   44.4   81965   472644      7693    3849   3287 43081   2 17.8 223.2   42
c i   44.6   81711   472644      7914    4040   3304 43091   2 17.8 221.5   42
c i   44.7   81703   472644      8117    4173   3310 43095   1 18.2 220.2   42
c i   44.8   81658   472644      8128    4182   3311 43095   2 18.2 220.0   42
c i   44.8   81634   472644      8177    4229   3311 43096   1 18.3 219.7   42
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   45.2   81629   472644      8429    4415   3331 43134   1 18.3 221.6   42
c i   45.2   81626   472644      8431    4415   3331 43135   1 18.3 221.6   42
c 
c [simplification-4] limit of 8941 conflicts hit after 8941 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 81611 free variables schedulable
c [ternres-2] 266 ternary resolvents (0 bin, 266 trn)
c [ternres-2] 27234 variables remain 33% (54377 retained)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 769 xors of average arity 2.1
c [gauss-2] connected 1586 occurrences of 1111 variables (average 1.4)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-9] removed 802 variables
c [gauss-2] exported 0 unary, 33 binary and 0 ternary equations
c [decomp-10] removed 1 variables
c [basicprobe-2] limit 2617264 penalty 0 = 0 + 0
c [basicprobe-2-0] 22109 probes remain 27% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 27 variables, found 10656 hbrs
c [bate-1] eliminated 10 asymmetric tautologies during probing
c [cgrclsr-2] limit 261726 penalty 0 = 0 + 0
c [cgrclsr-2] all 80781 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 1570358 with penalty 0 = 0 + 0
c [lift-2] using 66048 probes 82%
c [lift-2] 21 units, 3 impls, 1 eqs in 1 rounds
c [lift-2] 80597 variables remain 100% (12 retained)
c [lift-2] removed 172 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 18, lifted 40
c [unhide-4] limit 523452 with penalty 0 = 0 + 0
c [unhide-4-4] 8 units, 1177 failed, 7959 tauts, 0 hbrs, 14585 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 147 transitive binary clauses
c [transred-2] found 4 units
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 78548 variables 100%
c [elim-4] limit of 52345294 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 3658 variables 5% in round 1 in 43144845 steps
c [elim-4-1] backward subsumption/strengthening limit 9200449
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 9200457 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3663 = 5% variables out of 78548
c [bca-3] limit of 10000000 steps
c [bca-3] 132909 out of 149772 literals actually usable 89%
c [bca-3] added 69 blocked clauses in 349080 steps
c [phase-5] phase bias: 7 positive 19%, 29 negative 81%
c [simplification-4] removed 6726 variables 8.2% (74885 remain 30%)
c [simplification-4] removed 36861 irredundant clauses 7.8% (435783 remain 39%)
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 10941
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   50.7   74884   435783      8945    3809   2629 50645   1 20.7 220.7   39
c i   51.0   74877   435783      9238    4051   2640 50657   2 20.8 222.9   40
c i   51.0   74871   435783      9242    4052   2641 50657   2 20.8 222.7   40
c i   51.0   74870   435783      9296    4100   2644 50659   2 20.7 222.3   40
c i   51.0   74800   435783      9297    4100   2644 50659   1 20.7 222.2   40
c i   51.0   74796   435783      9298    4100   2644 50659   1 20.7 222.2   40
c i   51.1   74787   435783      9338    4130   2646 50666   1 20.6 223.1   40
c i   51.1   74781   435783      9419    4189   2655 50676   2 20.6 222.7   40
c i   51.1   74752   435783      9420    4189   2655 50676   2 20.6 222.7   40
c i   51.2   74751   435783      9464    4223   2658 50681   3 20.5 222.5   40
c i   51.6   74660   435783     10277    4849   2678 50708   1 31.4 230.8   41
c i   51.6   74659   435783     10287    4853   2678 50708   1 31.6 230.9   42
c -   51.8   74659   435783     10606    3087   2694 50727   1 34.8 234.3   39
c i   51.8   74658   435783     10657    3128   2694 50728   1 35.4 235.3   39
c i   52.2   74657   435783     11305    3707   2705 50740   1 38.1 240.2   40
c 
c [simplification-5] limit of 11427 conflicts hit after 11429 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 24883 schedulable variables 33%
c [ternres-3] 1460 ternary resolvents (6 bin, 1454 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 102 xors of average arity 2.4
c [gauss-3] connected 247 occurrences of 196 variables (average 1.3)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 55 variables
c [simpleprobe-3] 38721 schedulable variables 52%
c [simpleprobe-3] limit 12312827 penalty 0 = 0 + 0
c [decomp-12] removed 1640 variables
c [simpleprobe-3] 14594 variables remain 20% (58366 retained)
c [simpleprobe-3] removed 1640 variables, found 47808 hbrs, 293 units
c [lift-3] limit 1846924 with penalty 0 = 0 + 0
c [lift-3] using 59247 probes 81%
c [lift-3] 144 units, 2 impls, 0 eqs in 1 rounds
c [lift-3] 72796 variables remain 100% (20 retained)
c [lift-3] removed 144 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 9, lifted 5
c [unhide-5] limit 615641 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 222 failed, 8325 tauts, 0 hbrs, 11923 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 144 transitive binary clauses
c [transred-3] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 72383 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 40 blocked clauses
c [block-3] 40 < 1/1000 * 416397 = 416 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 79
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 75
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 74
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 73
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 72
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 71
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 70
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 69
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 68
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 67
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 66
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 65
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 64
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 63
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 62
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 61
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 60
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 59
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 58
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 57
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 56
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 55
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 54
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 53
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 52
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 51
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 50
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 49
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 48
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 47
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 46
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 45
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 44
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 43
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 42
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 41
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 40
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 39
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 38
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 37
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 36
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 35
c [cce-3-1] eliminated 3 clauses out of 7 (43%) of length 34
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 33
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 32
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 31
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 30
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 29
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 28
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 27
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 26
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 25
c [cce-3-1] eliminated 4 clauses out of 9 (44%) of length 24
c [cce-3-1] eliminated 9 clauses out of 9 (100%) of length 23
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 22
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 21
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 20
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 19
c [cce-3-1] eliminated 6 clauses out of 11 (55%) of length 18
c [cce-3-1] eliminated 12 clauses out of 13 (92%) of length 17
c [cce-3-1] eliminated 6 clauses out of 12 (50%) of length 16
c [cce-3-1] eliminated 12 clauses out of 12 (100%) of length 15
c [cce-3-1] eliminated 6 clauses out of 12 (50%) of length 14
c [cce-3-1] eliminated 11 clauses out of 11 (100%) of length 13
c [cce-3-1] eliminated 7 clauses out of 12 (58%) of length 12
c [cce-3-1] eliminated 11 clauses out of 12 (92%) of length 11
c [cce-3-1] eliminated 7 clauses out of 154 (5%) of length 10
c [cce-3-1] eliminated 1 clauses out of 882 (0%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 353 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 269717 clauses = 222517 binary + 47200 ternary
c [cce-3] tried to eliminate 194 small clauses 0%
c [cce-3] eliminated 53 small clauses 0%
c [cce-3] eliminated 42 binary clauses 0%
c [cce-3] eliminated 11 ternary clauses 0%
c [cce-3-1] eliminated 53 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 406 covered clauses in round 1
c [cce-3] eliminated 406 covered clauses in TOTAL during 1 rounds
c [cce-3] 406 < 1/1000 * 413236 = 413 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 72383 variables 100%
c [elim-5] limit of 61564135 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 1794 variables 2% in round 1 in 39104203 steps
c [elim-5-1] backward subsumption/strengthening limit 22459932
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 12083053 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1794 = 2% variables out of 72383
c [bca-4] limit of 10000000 steps
c [bca-4] 124939 out of 141180 literals actually usable 88%
c [bca-4] added 30 blocked clauses in 330009 steps
c [rephase-1] after 11429 conflicts (new increment 20000, next 31429)
c [flushphases] 586 phases reset
c [phase-6] phase bias: 5 positive 4%, 109 negative 96%
c [simplification-5] removed 4066 variables 5.4% (70589 remain 28%)
c [simplification-5] removed 26702 irredundant clauses 6.1% (409081 remain 36%)
c [simplification-5] maximum reduction of 6% = max (5%, 6%)
c [simplification-5] large reduction 6% >= 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 13429
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   58.4   70589   409081     11864    3992   2975 101476   1 39.2 239.6   40
c i   58.4   70588   409081     11867    3993   2975 101477   1 39.2 239.5   40
c i   58.9   70581   409081     12415    4459   3000 101502   2 38.5 235.2   40
c i   59.0   70580   409081     12502    4522   3008 101504   1 38.5 234.6   40
c i   59.0   70579   409081     12503    4522   3008 101504   1 38.5 234.5   40
c i   59.0   70578   409081     12534    4549   3008 101506   1 38.5 234.2   40
c i   59.0   70577   409081     12535    4549   3008 101506   1 38.5 234.1   40
c i   59.0   70576   409081     12536    4549   3008 101506   1 38.5 234.0   40
c i   59.0   70575   409081     12537    4549   3008 101506   1 38.5 234.0   40
c i   59.0   70574   409081     12538    4549   3008 101506   1 38.5 233.9   40
c i   59.0   70573   409081     12543    4551   3008 101508   1 38.5 233.8   40
c i   59.0   70457   409081     12544    4551   3008 101508   1 38.5 233.8   40
c i   59.3   70341   409081     12921    4830   3021 101521   2 39.4 234.0   40
c i   59.3   70335   409081     13000    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70334   409081     13001    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70328   409081     13002    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70323   409081     13003    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70315   409081     13004    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70312   409081     13005    4904   3021 101521   2 39.4 233.3   40
c i   59.3   70308   409081     13006    4904   3021 101521   2 39.4 233.3   40
c i   59.8   70300   409081     13537    5380   3042 101535   1 39.0 230.8   41
c i   59.8   70298   409081     13538    5380   3042 101535   1 39.0 230.8   41
c i   60.1   70292   409081     13942    5721   3052 101549   2 40.9 234.8   42
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   60.2   70282   409081     14043    5789   3058 101573   3 40.6 234.8   42
c 
c [simplification-6] limit of 14089 conflicts hit after 14090 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 70158 free variables schedulable
c [ternres-4] 372 ternary resolvents (0 bin, 372 trn)
c [ternres-4] 20095 variables remain 29% (50063 retained)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 10274 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] 10274 out of 10274 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-13] removed 774 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 53803 literals 39%
c [treelook-3] scheduling used 307970 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 310627 steps
c [treelook-3] 53788 literals remain 39%
c [treelook-3] 31002 variables remain to probed next time 44%
c [treelook-3] removed 0 variables, found 5 hbrs
c [cgrclsr-3] limit 202643 based on 405287 irredundant clauses
c [cgrclsr-3] all 69815 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-4] limit 2208822 with penalty 0 = 0 + 0
c [lift-4] using 56839 probes 81%
c [lift-4] 64 units, 11 impls, 19 eqs in 1 rounds
c [lift-4] 69695 variables remain 100% (36 retained)
c [lift-4] removed 84 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 8, lifted 8
c [unhide-6] limit 736274 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 314 failed, 8630 tauts, 0 hbrs, 19155 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 151 transitive binary clauses
c [transred-4] found 1 units
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 69175 variables 100%
c [elim-6] limit of 73627416 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 872 variables 1% in round 1 in 35935613 steps
c [elim-6-1] backward subsumption/strengthening limit 37691803
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 11964930 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 872 = 1% variables out of 69175
c [bca-5] limit of 10000000 steps
c [bca-5] 116917 out of 136608 literals actually usable 86%
c [bca-5] added 84 blocked clauses in 301320 steps
c [phase-7] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-6] removed 1855 variables 2.6% (68303 remain 27%)
c [simplification-6] removed 11957 irredundant clauses 2.9% (397124 remain 35%)
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 39090
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   65.2   68302   397124     14723    6165   2871 97056   0 40.3 231.0   41
c i   65.3   68297   397124     14846    6266   2876 97063   2 40.2 230.1   41
c i   65.4   68018   397124     14897    6310   2876 97066   1 40.2 229.8   41
c -   65.5   68018   397124     15111    4003   2879 97068   3 40.5 229.3   38
c i   65.5   68017   397124     15218    4078   2881 97069   1 40.6 229.0   39
c i   65.5   68016   397124     15219    4078   2881 97069   1 40.6 229.0   39
c i   65.5   68015   397124     15220    4078   2881 97069   1 40.6 229.0   39
c i   65.5   68014   397124     15221    4078   2881 97069   1 40.6 229.0   39
c i   65.5   68013   397124     15222    4078   2881 97069   1 40.6 229.0   39
c i   65.8   68012   397124     15452    4265   2893 97091   1 40.3 227.5   39
c i   65.8   68011   397124     15454    4265   2894 97091   1 40.3 227.5   39
c i   66.2   68010   397124     15954    4707   2901 97103   2 39.8 226.4   39
c i   66.4   67802   397124     16296    4988   2908 97110   1 39.6 226.4   39
c i   66.5   67801   397124     16689    5306   2914 97113   2 39.9 226.7   40
c i   66.8   67800   397124     17335    5755   2922 97119   2 40.8 225.5   40
c i   67.1   67799   397124     17698    6071   2931 97130   2 40.6 224.4   40
c i   67.2   67727   397124     17728    6098   2932 97131   1 40.6 224.2   40
c i   67.2   67723   397124     17729    6098   2932 97131   1 40.6 224.2   40
c i   67.8   67713   397124     18595    6806   2947 97153   3 41.2 223.1   41
c i   67.9   67710   397124     18677    6876   2949 97157   2 41.2 223.3   41
c -   68.9   67706   397124     19937    4914   2969 97194   2 41.7 221.7   38
c i   69.1   67705   397124     20126    5071   2987 97203   2 41.7 221.0   39
c i   69.5   67436   397124     20749    5586   3001 97206   1 41.4 219.7   39
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   69.5   67435   397124     20753    5589   3001 97206   1 41.4 219.7   39
c i   69.7   67425   397124     20976    5792   3008 97213   2 41.3 219.8   40
c i   70.6   67424   397124     22120    6626   3034 97233   2 41.1 219.6   40
c i   70.6   67423   397124     22121    6626   3034 97233   2 41.1 219.6   40
c i   70.7   67422   397124     22262    6762   3034 97234   0 40.9 219.4   41
c i   70.8   67412   397124     22397    6861   3036 97234   0 41.6 219.6   41
c i   71.1   67411   397124     22806    7198   3040 97235   1 41.4 219.1   42
c i   72.2   67410   397124     24405    8459   3072 97271   2 44.7 223.5   43
c i   72.2   67409   397124     24436    8485   3073 97274   2 44.7 223.4   43
c i   72.2   67406   397124     24468    8507   3075 97274   1 44.6 223.4   43
c i   72.4   67403   397124     25254    9116   3079 97279   3 46.4 223.4   44
c -   72.5   67403   397124     25589    5885   3087 97284   3 47.2 223.4   39
c i   72.6   67402   397124     26107    6279   3093 97293   3 48.4 223.7   40
c R   72.7   67402   397124     26339    6464   3093 97297   1 48.2 223.4   40
c i   72.9   67401   397124     26485    6592   3097 97304   1 48.0 222.9   41
c i   73.0   67400   397124     26593    6688   3101 97305   1 48.0 222.6   41
c i   73.7   67198   397124     27368    7345   3118 97317   2 47.7 222.0   41
c i   73.8   67197   397124     27391    7365   3118 97318   1 47.7 222.1   41
c i   74.6   67196   397124     28191    8038   3135 97338   1 47.6 220.5   42
c i   74.9   67119   397124     28726    8391   3162 97370   1 47.9 220.2   42
c i   75.2   67116   397124     28990    8620   3175 97381   2 47.7 219.2   42
c i   75.4   67054   397124     29166    8766   3185 97387   1 47.6 218.9   42
c i   75.6   67053   397124     29327    8914   3185 97389   1 47.5 218.3   42
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   75.6   67046   397124     29334    8919   3185 97389   1 47.5 218.2   42
c i   75.9   67045   397124     29719    9264   3196 97396   1 47.3 217.7   42
c i   76.1   67041   397124     29864    9395   3196 97397   1 47.3 217.6   42
c i   77.0   67033   397124     30769   10117   3209 97406   3 47.3 216.1   43
c -   77.7   67033   397124     31802    6911   3219 97410   1 47.2 215.1   39
c i   78.1   67032   397124     32126    7186   3232 97412   1 47.1 214.4   40
c i   79.0   67031   397124     33126    8049   3244 97431   2 46.6 212.5   41
c i   79.3   67028   397124     33496    8328   3258 97437   2 46.5 211.7   41
c i   79.3   67009   397124     33497    8328   3258 97437   2 46.5 211.7   41
c i   79.4   66968   397124     33732    8556   3259 97437   1 46.2 211.6   41
c i   80.3   66967   397124     34701    9353   3271 97462   1 46.2 210.6   42
c i   80.7   66966   397124     35077    9659   3279 97463   1 46.7 210.4   42
c i   81.1   66965   397124     35487    9990   3283 97473   1 46.7 210.0   42
c i   81.1   66961   397124     35488    9990   3283 97473   0 46.7 210.0   42
c i   81.2   66955   397124     35489    9990   3283 97473   0 46.7 210.0   42
c i   81.2   66949   397124     35490    9990   3283 97473   0 46.7 210.1   42
c i   83.3   66942   397124     38518   12266   3306 97494   2 46.4 208.0   46
c i   83.3   66939   397124     38527   12272   3306 97496   2 46.4 208.0   46
c i   83.3   66935   397124     38528   12272   3306 97496   2 46.4 208.0   46
c i   83.3   66929   397124     38529   12272   3306 97496   1 46.4 207.9   46
c i   83.4   66917   397124     38530   12272   3306 97496   1 46.4 207.9   46
c i   83.4   66914   397124     38531   12272   3306 97496   1 46.4 207.9   46
c i   83.4   66899   397124     38532   12272   3306 97496   1 46.4 207.9   46
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   83.5   66699   397124     38623    7860   3306 97496   1 46.4 207.9   39
c i   83.6   66698   397124     38737    7953   3309 97506   2 46.3 207.5   40
c i   83.6   66685   397124     38738    7953   3309 97506   2 46.3 207.5   40
c i   84.1   66673   397124     39367    8513   3328 97526   1 45.9 206.5   41
c i   85.0   66672   397124     40032    9090   3333 97528   2 46.0 205.4   42
c i   85.0   66670   397124     40233    9230   3335 97528   2 45.9 205.2   42
c i   85.6   66669   397124     40776    9736   3344 97531   1 45.7 205.0   42
c i   86.1   66668   397124     41206   10116   3360 97543   1 45.5 204.2   42
c 
c [simplification-7] limit of 41596 conflicts hit after 41596 conflicts
c [ternres-5] limit 9874482 with penalty 0 = 0 + 0
c [ternres-5] 19087 schedulable variables 28%
c [ternres-5] 1117 ternary resolvents (1 bin, 1116 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 96 xors of average arity 2.3
c [gauss-4] connected 223 occurrences of 188 variables (average 1.2)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [decomp-15] removed 149 variables
c [gauss-4] exported 0 unary, 6 binary and 0 ternary equations
c [basicprobe-3] limit 9874482 penalty 0 = 0 + 0
c [basicprobe-3-0] 19710 probes remain 30% after last round
c [basicprobe-3-0] 59 units = 59 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 392 variables, found 32213 hbrs
c [bate-2] eliminated 41 asymmetric tautologies during probing
c [lift-5] limit 5924689 with penalty 0 = 0 + 0
c [lift-5] using 54209 probes 82%
c [lift-5] 129 units, 19 impls, 0 eqs in 1 rounds
c [lift-5] 65910 variables remain 100% (77 retained)
c [lift-5] removed 140 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 6, lifted 30
c [unhide-7] limit 1974896 with penalty 0 = 0 + 0
c [unhide-7-7] 4 units, 127 failed, 4558 tauts, 0 hbrs, 24718 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 146 transitive binary clauses
c [transred-5] found 1 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 65776 variables 100%
c [elim-7] limit of 197489650 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 1602 variables 2% in round 1 in 36908679 steps
c [elim-7-1] backward subsumption/strengthening limit 73817358
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 11111371 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1618 = 2% variables out of 65776
c [bca-6] limit of 10000000 steps
c [bca-6] 105473 out of 128318 literals actually usable 82%
c [bca-6] added 33 blocked clauses in 262671 steps
c [rephase-2] after 41596 conflicts (new increment 40000, next 81596)
c [flushphases] 3 phases reset
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 2510 variables 3.8% (64158 remain 25%)
c [simplification-7] removed 25204 irredundant clauses 6.3% (371920 remain 33%)
c [simplification-7] maximum reduction of 6% = max (4%, 6%)
c [simplification-7] large reduction 6% >= 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 43596
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   91.4   64157   371920     41686    9560   3062 129244   1 45.8 204.0   42
c i   92.4   64156   371920     42736   10452   3081 129269   1 45.4 203.2   43
c i   92.8   64155   371920     43162   10764   3082 129270   1 46.3 203.5   44
c i   92.9   64154   371920     43339   10917   3084 129281   2 46.2 203.3   44
c 
c [simplification-8] limit of 43758 conflicts hit after 43759 conflicts
c [ternres-6] limit 10450992 with penalty 0 = 0 + 0
c [ternres-6] all 64154 free variables schedulable
c [ternres-6] 897 ternary resolvents (0 bin, 897 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-5] limit 2090198 penalty 0 = 0 + 0
c [gauss-5] extracted 51 xors of average arity 2.8
c [gauss-5] connected 145 occurrences of 113 variables (average 1.3)
c [gauss-5] limit 2090198 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 7 variables
c [simpleprobe-4] 13004 schedulable variables 20%
c [simpleprobe-4] limit 41803969 penalty 0 = 0 + 0
c [decomp-18] removed 418 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 418 variables, found 23138 hbrs, 100 units
c [lift-6] limit 6270595 with penalty 0 = 0 + 0
c [lift-6] using 52034 probes 82%
c [lift-6] 204 units, 26 impls, 1 eqs in 1 rounds
c [lift-6] 63236 variables remain 100% (119 retained)
c [lift-6] removed 374 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 9, lifted 3
c [unhide-8] limit 2090198 with penalty 0 = 0 + 0
c [unhide-8-8] 1 units, 230 failed, 14793 tauts, 0 hbrs, 21450 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 173 transitive binary clauses
c [transred-6] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 63020 variables 100%
c [block-4] limit of 26127481 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 48 blocked clauses
c [block-4] 48 < 1/1000 * 366337 = 366 considered unsuccessful
c [cce-4] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 117
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 116
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 113
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 112
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 110
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 109
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 108
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 107
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 106
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 105
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 104
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 103
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 102
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 101
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 100
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 99
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 98
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 97
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 96
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 95
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 94
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 93
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 92
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 91
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 90
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 89
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 88
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 87
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 86
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 85
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 84
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 83
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 82
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 81
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 80
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 78
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 77
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 76
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 74
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 72
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 71
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 70
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 68
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 67
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 66
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 65
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 64
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 62
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 61
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 59
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 58
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 54
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 53
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 51
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 50
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 49
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 48
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 47
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 45
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 156 large clauses in 7500001 steps
c [cce-4-1] allowing another 3750000 steps for small clauses
c [cce-4] scheduling 238385 clauses = 196500 binary + 41885 ternary
c [cce-4] tried to eliminate 131 small clauses 0%
c [cce-4] eliminated 29 small clauses 0%
c [cce-4] eliminated 24 binary clauses 0%
c [cce-4] eliminated 5 ternary clauses 0%
c [cce-4-1] eliminated 29 small clauses in 7500001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 185 covered clauses in round 1
c [cce-4] eliminated 185 covered clauses in TOTAL during 1 rounds
c [cce-4] 185 < 1/1000 * 363748 = 363 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 63019 variables 100%
c [elim-8] limit of 209019848 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 1001 variables 2% in round 1 in 33319137 steps
c [elim-8-1] backward subsumption/strengthening limit 66638274
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 10685151 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1001 = 2% variables out of 63019
c [bca-7] limit of 10000000 steps
c [bca-7] 100900 out of 124038 literals actually usable 81%
c [bca-7] added 52 blocked clauses in 251583 steps
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 2136 variables 3.3% (62018 remain 25%)
c [simplification-8] removed 11309 irredundant clauses 3.0% (360611 remain 32%)
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 75009
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   99.4   62017   360611     44246   11132   3109 142528   2 46.0 202.1   44
c i  100.0   62016   360611     44849   11603   3115 142542   2 46.2 201.2   44
c -  102.3   62016   360611     47442    8606   3138 142569   1 46.1 198.0   40
c i  102.4   62015   360611     47527    8666   3142 142578   1 46.0 197.9   41
c i  102.4   62012   360611     47539    8676   3142 142578   1 46.0 197.9   41
c i  102.4   62011   360611     47540    8676   3142 142578   1 46.0 197.9   41
c i  102.5   62010   360611     47599    8726   3142 142578   1 46.1 197.8   41
c i  102.7   62009   360611     47870    8934   3146 142581   1 46.1 197.6   41
c i  103.4   62008   360611     48527    9434   3146 142583   1 45.7 197.2   41
c i  103.6   62007   360611     48969    9779   3154 142594   1 45.7 197.1   41
c i  103.6   62006   360611     48973    9782   3154 142594   1 45.7 197.1   41
c i  104.4   62005   360611     49803   10296   3158 142639   1 46.2 196.9   42
c i  104.6   62004   360611     50076   10446   3158 142639   1 46.5 196.8   42
c i  106.0   62003   360611     52085   11733   3184 142661   2 46.3 195.9   43
c i  107.4   61794   360611     53834   12926   3192 142663   1 47.6 195.9   44
c i  107.7   61793   360611     54205   13234   3193 142664   1 47.5 195.7   45
c i  107.9   61792   360611     54444   13402   3194 142665   2 47.9 195.8   46
c i  108.3   61790   360611     54928   13827   3196 142667   1 47.7 195.7   46
c i  108.6   61789   360611     55204   14001   3199 142669   2 47.8 195.6   46
c -  109.6   61789   360611     56322    9503   3199 142675   1 47.1 195.0   40
c i  109.8   61788   360611     56741    9864   3203 142677   3 46.9 194.8   41
c i  110.3   61787   360611     57488   10539   3206 142679   1 46.5 194.6   42
c R  110.5   61787   360611     57851   10750   3206 142679   1 47.0 194.6   43
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  111.2   61786   360611     58559   11313   3211 142687   3 46.9 193.6   43
c i  111.4   61785   360611     58751   11430   3211 142687   1 46.9 193.4   43
c i  111.8   61784   360611     59109   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61783   360611     59110   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61782   360611     59111   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61781   360611     59112   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61777   360611     59113   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61744   360611     59114   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61743   360611     59115   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61742   360611     59116   11734   3215 142696   1 46.9 193.1   43
c i  111.8   61741   360611     59117   11734   3215 142696   1 46.9 193.1   43
c i  112.6   61740   360611     59823   12269   3217 142708   1 46.8 192.3   44
c i  114.7   61739   360611     61781   13796   3239 142714   1 46.7 190.3   45
c i  115.0   61738   360611     62013   13973   3240 142715   1 46.7 190.0   45
c i  117.1   61737   360611     64496   15965   3269 142751   1 46.5 188.3   46
c i  117.1   61736   360611     64521   15986   3269 142751   2 46.5 188.3   46
c i  117.4   61735   360611     64760   16175   3274 142755   1 46.5 188.0   47
c i  117.4   61734   360611     64768   16182   3274 142755   1 46.5 188.0   47
c i  117.5   61733   360611     64824   16231   3275 142755   1 46.5 187.9   47
c i  117.5   61732   360611     64825   16231   3275 142755   1 46.5 187.9   47
c i  117.7   61731   360611     64951   16344   3275 142755   2 46.4 187.9   47
c -  117.8   61720   360611     65045   10424   3276 142755   1 46.5 187.9   40
c i  120.7   61719   360611     67752   12603   3304 142771   1 46.0 185.7   43
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  120.7   61718   360611     67830   12676   3305 142771   1 45.9 185.7   43
c i  121.0   61717   360611     68041   12841   3305 142772   1 45.9 185.6   43
c i  121.0   61716   360611     68094   12885   3310 142772   1 45.9 185.5   43
c i  121.0   61715   360611     68103   12883   3310 142772   1 45.8 185.5   43
c i  122.2   61714   360611     69602   14160   3325 142778   2 45.2 185.1   44
c i  122.2   61713   360611     69661   14191   3328 142780   3 45.2 185.1   44
c i  122.5   61712   360611     70003   14499   3333 142783   1 45.1 184.8   44
c i  124.1   61711   360611     71344   15597   3344 142801   1 45.0 183.4   45
c i  124.1   61710   360611     71355   15607   3344 142801   1 45.0 183.4   45
c i  124.5   61709   360611     71687   15848   3347 142802   0 44.9 183.1   45
c i  125.7   61693   360611     72754   16798   3351 142808   1 44.6 182.3   46
c i  126.6   61692   360611     73518   17445   3360 142822   1 44.6 181.6   46
c i  126.7   61691   360611     73580   17495   3360 142822   1 44.8 181.7   47
c -  127.3   61691   360611     74024   11361   3363 142826   1 44.7 181.3   40
c i  127.5   61690   360611     74357   11633   3368 142836   2 44.7 181.2   42
c 
c [simplification-9] limit of 76803 conflicts hit after 76804 conflicts
c [ternres-7] limit 19512145 with penalty 0 = 0 + 0
c [ternres-7] all 61690 free variables schedulable
c [ternres-7] 708 ternary resolvents (0 bin, 708 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-19] removed 344 variables
c [cgrclsr-4] limit 487803 penalty 2 = 2 + 0
c [cgrclsr-4] all 61674 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-7] limit 11707287 with penalty 0 = 0 + 0
c [lift-7] using 50335 probes 82%
c [lift-7] 331 units, 56 impls, 2 eqs in 1 rounds
c [lift-7] 60692 variables remain 100% (213 retained)
c [lift-7] removed 769 variables
c [cliff-7] limit of 15609716 steps penalty 0 = 0 + 0
c [cliff-7] failed 4, lifted 140
c [unhide-9] limit 3902429 with penalty 0 = 0 + 0
c [unhide-9-10] 8 units, 255 failed, 12571 tauts, 0 hbrs, 41780 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 188 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 60160 variables 100%
c [elim-9] limit of 390242911 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 1952 variables 3% in round 1 in 36639645 steps
c [elim-9-1] backward subsumption/strengthening limit 73279290
c [elim-9-1] subsumed 1 and strengthened 0 clauses in 10523854 steps
c [elim-9-1] rescheduled 4 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 0 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2096 = 3% variables out of 60160
c [bca-8] limit of 10000000 steps
c [bca-8] 94598 out of 116130 literals actually usable 81%
c [bca-8] added 61 blocked clauses in 242289 steps
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 3626 variables 5.9% (58064 remain 23%)
c [simplification-9] removed 22849 irredundant clauses 6.3% (337762 remain 30%)
c [simplification-9] maximum reduction of 6% = max (6%, 6%)
c [simplification-9] large reduction 6% >= 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 78804
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  135.5   58063   337762     77453   11887   2504 127833   1 45.2 180.1   41
c 
c [simplification-10] limit of 78852 conflicts hit after 78853 conflicts
c [ternres-8] limit 20072571 with penalty 0 = 0 + 0
c [ternres-8] all 58063 free variables schedulable
c [ternres-8] 941 ternary resolvents (2 bin, 939 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1254535 penalty 3 = 3 + 0
c [card-4] found 16658 at-most-one constraints of average size 3.7
c [card-4] found 1684 at-most-two constraints of average size 4.8
c [card-4] using previous limit 1254535 for elimination
c [card-4] 18306 out of 18342 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-6] limit 2007257 penalty 1 = 1 + 0
c [gauss-6] extracted 38 xors of average arity 2.8
c [gauss-6] connected 105 occurrences of 79 variables (average 1.3)
c [gauss-6] limit 2007257 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 17 variables
c [treelook-4] limit 501814 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 70610 literals 61%
c [treelook-4] scheduling used 502376 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 501814 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 525082 steps
c [treelook-4] 70580 literals remain 61%
c [treelook-4] 23156 variables remain to probed next time 40%
c [decomp-21] removed 1 variables
c [treelook-4] removed 9 variables, found 3198 hbrs
c [lift-8] limit 12043542 with penalty 0 = 0 + 0
c [lift-8] using 46882 probes 81%
c [lift-8] 374 units, 44 impls, 1 eqs in 1 rounds
c [lift-8] 57284 variables remain 99% (317 retained)
c [lift-8] removed 436 variables
c [cliff-8] limit of 16058057 steps penalty 0 = 0 + 0
c [cliff-8] failed 2, lifted 64
c [unhide-10] limit 4014514 with penalty 0 = 0 + 0
c [unhide-10-12] 2 units, 108 failed, 8149 tauts, 0 hbrs, 30402 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 116 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 57407 variables 100%
c [elim-10] limit of 401451427 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 669 variables 1% in round 1 in 32345514 steps
c [elim-10-1] backward subsumption/strengthening limit 64691028
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 10267057 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 669 = 1% variables out of 57407
c [bca-9] limit of 10000000 steps
c [bca-9] 91752 out of 113478 literals actually usable 81%
c [bca-9] added 41 blocked clauses in 234307 steps
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 1325 variables 2.3% (56738 remain 23%)
c [simplification-10] removed 8605 irredundant clauses 2.5% (329157 remain 29%)
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 117915
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  142.6   56737   329157     79200   12565   2742 138927   1 44.8 178.6   42
c i  142.6   56736   329157     79201   12565   2742 138927   1 44.8 178.6   42
c i  143.0   56734   329157     79594   12922   2744 138928   1 44.7 178.4   42
c i  143.6   56733   329157     80475   13594   2747 138931   1 44.9 178.4   43
c i  144.5   56732   329157     81840   14660   2764 138964   2 44.6 178.0   44
c i  145.0   56731   329157     82434   15158   2765 138975   1 44.4 177.8   45
c i  145.8   56730   329157     83649   16095   2781 138988   0 44.4 177.5   47
c i  145.8   56729   329157     83650   16095   2781 138988   0 44.4 177.5   47
c i  145.8   56728   329157     83651   16095   2781 138988   0 44.4 177.5   47
c i  148.4   56727   329157     86202   18310   2801 139009   1 44.0 176.1   48
c -  148.7   56727   329157     86560   11553   2802 139012   1 43.9 175.9   39
c i  150.2   56726   329157     87889   12696   2815 139034   1 43.6 174.9   42
c i  150.8   56725   329157     88520   13238   2834 139054   2 43.6 174.6   42
c i  152.8   56724   329157     90750   15252   2839 139058   1 43.0 173.6   44
c i  154.9   56723   329157     92753   16942   2855 139070   1 42.8 172.6   45
c i  158.2   56722   329157     96266   19322   2869 139082   1 42.5 171.5   47
c -  159.0   56722   329157     96963   12398   2872 139088   1 42.4 171.0   39
c i  159.0   56721   329157     96967   12400   2872 139088   1 42.4 171.0   39
c i  159.5   56720   329157     97466   12772   2880 139091   1 42.4 170.7   41
c i  160.8   56719   329157     98819   13855   2891 139095   1 42.3 170.0   42
c i  160.9   56718   329157     98890   13920   2891 139095   1 42.3 170.0   43
c i  162.6   56717   329157    100520   15284   2896 139100   1 42.1 169.2   44
c i  163.7   56716   329157    101663   16164   2899 139101   1 42.7 169.2   44
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  164.1   56715   329157    102043   16505   2900 139101   1 42.6 169.0   44
c i  164.2   56714   329157    102093   16533   2900 139102   2 42.6 168.9   44
c i  166.3   56713   329157    104401   18418   2908 139114   1 42.1 167.9   47
c i  167.0   56712   329157    104977   18878   2909 139116   1 42.0 167.6   47
c -  169.4   56673   329157    107837   13223   2920 139128   1 41.5 166.6   39
c i  170.2   56672   329157    108948   13984   2920 139129   1 41.5 166.4   42
c i  170.7   56671   329157    109589   14530   2921 139130   1 41.4 166.2   43
c i  172.9   56670   329157    112140   16355   2931 139138   1 41.2 165.7   44
c i  173.0   56669   329157    112216   16410   2931 139138   1 41.2 165.7   44
c i  175.8   56667   329157    115389   18679   2942 139147   1 40.7 164.8   45
c i  176.0   56666   329157    115557   18826   2941 139148   1 40.7 164.8   45
c i  176.2   56665   329157    115873   19015   2942 139148   1 40.7 164.7   46
c i  178.2   56664   329157    118511   21009   2951 139166   1 40.3 164.0   46
c 
c [simplification-11] limit of 119057 conflicts hit after 119057 conflicts
c [ternres-9] limit 30515856 with penalty 0 = 0 + 0
c [ternres-9] all 56664 free variables schedulable
c [ternres-9] 472 ternary resolvents (1 bin, 471 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-22] removed 93 variables
c [basicprobe-4] limit 30515856 penalty 0 = 0 + 0
c [basicprobe-4-0] 17470 probes remain 31% after last round
c [basicprobe-4-0] 204 units = 203 failed (100%) + 1 lifted (0%)
c [basicprobe-4-0] removed 527 variables, found 74885 hbrs
c [bate-3] eliminated 144 asymmetric tautologies during probing
c [lift-9] limit 18309513 with penalty 0 = 0 + 0
c [lift-9] using 45182 probes 81%
c [lift-9] 548 units, 115 impls, 29 eqs in 1 rounds
c [lift-9] 54817 variables remain 99% (510 retained)
c [lift-9] removed 791 variables
c [cliff-9] limit of 24412684 steps penalty 0 = 0 + 0
c [cliff-9] failed 5, lifted 208
c [unhide-11] limit 6103171 with penalty 0 = 0 + 0
c [unhide-11-15] 12 units, 149 failed, 13798 tauts, 0 hbrs, 78419 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 110 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 54897 variables 100%
c [elim-11] limit of 610317122 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 1537 variables 3% in round 1 in 37964886 steps
c [elim-11-1] backward subsumption/strengthening limit 75929772
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 9718639 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1537 = 3% variables out of 54897
c [bca-10] limit of 10000000 steps
c [bca-10] 85752 out of 106722 literals actually usable 80%
c [bca-10] added 74 blocked clauses in 227324 steps
c [rephase-3] after 119057 conflicts (new increment 80000, next 199057)
c [flushphases] 3 phases reset
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-11] removed 3304 variables 5.8% (53360 remain 21%)
c [simplification-11] removed 19520 irredundant clauses 5.9% (309637 remain 28%)
c [simplification-11] maximum reduction of 6% = max (6%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] new conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] new conflict limit 121057
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  187.4   53359   309637    120271   18535   2672 218018   1 40.0 163.6   45
c 
c [simplification-12] limit of 121083 conflicts hit after 121084 conflicts
c [ternres-10] limit 30915698 with penalty 0 = 0 + 0
c [ternres-10] all 53358 free variables schedulable
c [ternres-10] 711 ternary resolvents (2 bin, 709 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-23] removed 16 variables
c [simpleprobe-5] all 53344 free variables schedulable
c [simpleprobe-5] limit 123662793 penalty 0 = 0 + 0
c [decomp-24] removed 282 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 282 variables, found 31013 hbrs, 127 units
c [lift-10] limit 18549419 with penalty 0 = 0 + 0
c [lift-10] using 42428 probes 80%
c [lift-10] 460 units, 89 impls, 4 eqs in 1 rounds
c [lift-10] 51688 variables remain 99% (714 retained)
c [lift-10] removed 660 variables
c [cliff-10] limit of 24732558 steps penalty 0 = 0 + 0
c [cliff-10] failed 4, lifted 14
c [unhide-12] limit 6183139 with penalty 0 = 0 + 0
c [unhide-12-18] 1 units, 115 failed, 38051 tauts, 0 hbrs, 33591 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 128 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 52246 variables 100%
c [block-5] limit of 38644622 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 6 blocked clauses
c [block-5] 6 < 1/1000 * 300051 = 300 considered unsuccessful
c [cce-5] limit of 7728924 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 154
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 153
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 151
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 150
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 149
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 148
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 147
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 146
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 145
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 144
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 143
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 142
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 141
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 139
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 137
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 135
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 133
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 132
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 131
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 129
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 127
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 125
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 123
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 121
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 118
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 117
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 115
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 113
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 111
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 110
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 109
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 107
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 105
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 103
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 101
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 99
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 98
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 97
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 96
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 95
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 94
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 93
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 92
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 94 large clauses in 7728925 steps
c [cce-5-1] allowing another 3864462 steps for small clauses
c [cce-5] scheduling 217630 clauses = 169043 binary + 48587 ternary
c [cce-5] tried to eliminate 173 small clauses 0%
c [cce-5] eliminated 31 small clauses 0%
c [cce-5] eliminated 17 binary clauses 0%
c [cce-5] eliminated 14 ternary clauses 0%
c [cce-5-1] eliminated 31 small clauses in 7728925 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 125 covered clauses in round 1
c [cce-5] eliminated 125 covered clauses in TOTAL during 1 rounds
c [cce-5] 125 < 1/1000 * 299868 = 299 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 52246 variables 100%
c [elim-12] limit of 618313967 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 1210 variables 2% in round 1 in 32595626 steps
c [elim-12-1] backward subsumption/strengthening limit 65191252
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 9328729 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 1210 = 2% variables out of 52246
c [bca-11] limit of 10000000 steps
c [bca-11] 81996 out of 102074 literals actually usable 80%
c [bca-11] added 110 blocked clauses in 219280 steps
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-12] removed 2322 variables 4.4% (51036 remain 20%)
c [simplification-12] removed 12200 irredundant clauses 3.9% (297437 remain 27%)
c [simplification-12] maximum reduction of 4% = max (4%, 4%)
c [simplification-12] geometric conflict interval increment 7812 = 39062 / 5
c [simplification-12] new conflict interval 46874
c [simplification-12] penalized conflict interval 46874 = 1 * 46874
c [simplification-12] new conflict limit 167958
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  195.4   51035   297437    121119   16673   2758 204375   1 39.9 163.3   43
c i  195.4   51034   297437    121178   16721   2758 204375   1 39.9 163.3   43
c i  196.6   51033   297437    122741   18188   2761 204375   1 39.6 163.0   44
c R  198.6   51033   297437    125942   20945   2767 204433   1 38.9 162.2   45
c i  199.6   51032   297437    127023   21944   2773 204435   1 38.7 161.8   47
c -  199.6   51032   297437    127023   13444   2773 204435   1 38.7 161.8   39
c i  199.7   51031   297437    127119   13536   2773 204435   1 38.7 161.8   41
c i  202.1   51030   297437    129957   15978   2782 204454   2 38.2 160.7   42
c i  202.1   51029   297437    129971   15987   2783 204457   2 38.2 160.7   42
c i  202.1   50987   297437    129993   16000   2786 204462   2 38.2 160.7   42
c i  202.1   50982   297437    129994   16000   2786 204462   2 38.2 160.7   42
c i  204.9   50975   297437    133674   19063   2807 204480   1 37.8 159.8   43
c i  206.2   50974   297437    135102   20203   2818 204490   1 37.5 159.3   44
c i  206.2   50973   297437    135141   20237   2818 204490   1 37.5 159.3   44
c i  208.8   50972   297437    138502   22911   2849 204536   1 36.9 158.2   45
c -  209.2   50968   297437    138971   14305   2859 204548   1 36.8 158.0   39
c i  209.8   50967   297437    139614   14885   2868 204553   1 36.7 157.7   41
c i  209.8   50966   297437    139617   14885   2868 204554   1 36.7 157.7   41
c i  212.7   50963   297437    143304   17952   2878 204578   1 36.8 156.9   43
c i  213.5   50962   297437    144172   18756   2880 204578   1 36.7 156.6   44
c -  218.6   50962   297437    151174   15099   2891 204586   1 35.7 155.0   40
c i  219.8   50961   297437    152833   16566   2895 204591   2 35.4 154.6   42
c i  220.1   50960   297437    153163   16847   2898 204595   2 35.4 154.4   42
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  220.4   50959   297437    153591   17218   2899 204595   1 35.4 154.3   42
c i  226.0   50958   297437    160373   22914   2916 204608   1 34.5 152.7   44
c i  227.4   50957   297437    162108   24221   2919 204608   1 34.3 152.3   45
c i  227.9   50956   297437    162832   24812   2921 204609   1 34.2 152.2   45
c i  227.9   50955   297437    162833   24812   2921 204609   1 34.2 152.2   45
c -  229.2   50955   297437    164496   15939   2937 204610   1 33.9 152.0   39
c i  230.8   50954   297437    166469   17641   2946 204611   2 33.7 151.5   42
c i  230.8   50953   297437    166488   17655   2946 204611   2 33.7 151.4   42
c 
c [simplification-13] limit of 168980 conflicts hit after 168981 conflicts
c [ternres-11] limit 42124782 with penalty 0 = 0 + 0
c [ternres-11] all 50946 free variables schedulable
c [ternres-11] 517 ternary resolvents (2 bin, 515 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-7] limit 2106239 penalty 2 = 2 + 0
c [gauss-7] extracted 57 xors of average arity 2.8
c [gauss-7] connected 162 occurrences of 132 variables (average 1.2)
c [gauss-7] limit 2106239 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 13 variables
c [treelook-5] limit 2106239 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 85268 literals 84%
c [treelook-5] scheduling used 1154984 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2106239 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2148321 steps
c [treelook-5] 85244 literals remain 84%
c [treelook-5] 19312 variables remain to probed next time 38%
c [treelook-5] removed 0 variables, found 10052 hbrs
c [cgrclsr-5] limit 526559 penalty 3 = 3 + 0
c [cgrclsr-5] all 50933 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 40572 probes 80%
c [lift-11] 658 units, 145 impls, 4 eqs in 1 rounds
c [lift-11] 49032 variables remain 98% (984 retained)
c [lift-11] removed 917 variables
c [cliff-11] limit of 33699826 steps penalty 0 = 0 + 0
c [cliff-11] failed 4, lifted 249
c [unhide-13] limit 8424956 with penalty 0 = 0 + 0
c [unhide-13-22] 4 units, 80 failed, 19716 tauts, 0 hbrs, 56721 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 104 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 49684 variables 100%
c [elim-13] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 977 variables 2% in round 1 in 31568678 steps
c [elim-13-1] backward subsumption/strengthening limit 63137356
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 8928488 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 977 = 2% variables out of 49684
c [bca-12] limit of 10000000 steps
c [bca-12] 76860 out of 97416 literals actually usable 79%
c [bca-12] added 75 blocked clauses in 204986 steps
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-13] removed 2239 variables 4.4% (48707 remain 19%)
c [simplification-13] removed 14363 irredundant clauses 4.8% (283074 remain 25%)
c [simplification-13] maximum reduction of 5% = max (4%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] new conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] new conflict limit 170981
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  240.4   48706   283074    169532   17512   2756 228444   1 33.5 150.5   42
c 
c [simplification-14] limit of 171013 conflicts hit after 171015 conflicts
c [ternres-12] limit 42596798 with penalty 0 = 0 + 0
c [ternres-12] all 48706 free variables schedulable
c [ternres-12] 379 ternary resolvents (3 bin, 376 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-27] removed 12 variables
c [basicprobe-5] limit 42596798 penalty 0 = 0 + 0
c [basicprobe-5-0] 14769 probes remain 31% after last round
c [basicprobe-5-0] 311 units = 311 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 428 variables, found 91048 hbrs
c [bate-4] eliminated 211 asymmetric tautologies during probing
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 37999 probes 79%
c [lift-12] 401 units, 124 impls, 27 eqs in 1 rounds
c [lift-12] 46339 variables remain 97% (1298 retained)
c [lift-12] removed 630 variables
c [cliff-12] limit of 34077438 steps penalty 0 = 0 + 0
c [cliff-12] failed 2, lifted 59
c [unhide-14] limit 8519359 with penalty 0 = 0 + 0
c [unhide-14-26] 7 units, 84 failed, 21182 tauts, 0 hbrs, 28885 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 129 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 47437 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 1216 variables 3% in round 1 in 31057436 steps
c [elim-14-1] backward subsumption/strengthening limit 62114872
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 8586304 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1216 = 3% variables out of 47437
c [bca-13] limit of 10000000 steps
c [bca-13] 72731 out of 92444 literals actually usable 79%
c [bca-13] added 82 blocked clauses in 196453 steps
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-14] removed 2485 variables 5.1% (46221 remain 18%)
c [simplification-14] removed 13633 irredundant clauses 4.8% (269441 remain 24%)
c [simplification-14] maximum reduction of 5% = max (5%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] new conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] new conflict limit 173015
c [tabula-rasa-2] number clauses 269441 drops below limit 274616
c [flush-cache] 0 binary, 0 ternary, 17137 large
c [flushphases] 46221 phases reset fully
c [phase-16] phase bias: 2589 positive 32%, 5502 negative 68%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] conflict limit 20000 does not change
c [tabula-rasa-2] new variable limit 11555 and clause limit 134720
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  249.6   46220   269441    171032      14   2730 310030  15 33.3 150.1   36
c i  249.6   46219   269441    171044      23   2732 310030  10 33.3 150.1   36
c i  249.6   46218   269441    171117      73   2733 310047   8 33.3 150.1   36
c i  249.7   46214   269441    171264     208   2739 310049   3 33.3 150.4   36
c i  249.8   46213   269441    171544     427   2747 310067   2 33.3 150.5   36
c i  249.8   46205   269441    171546     428   2747 310067   2 33.3 150.5   36
c i  250.5   46204   269441    172619    1313   2770 310115   2 33.3 151.3   37
c i  250.6   46203   269441    172889    1530   2774 310116   1 33.4 151.8   38
c i  250.8   46202   269441    173207    1812   2787 310135   1 33.4 152.1   38
c i  250.8   46201   269441    173219    1820   2787 310135   1 33.4 152.1   38
c i  250.9   46200   269441    173310    1903   2787 310139   1 33.4 152.7   38
c i  251.0   46166   269441    173429    2005   2794 310140   1 33.4 152.9   38
c 
c [simplification-15] limit of 173477 conflicts hit after 173477 conflicts
c [ternres-13] limit 43015064 with penalty 0 = 0 + 0
c [ternres-13] all 46165 free variables schedulable
c [ternres-13] 498 ternary resolvents (4 bin, 494 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1344220 penalty 4 = 4 + 0
c [card-5] found 16482 at-most-one constraints of average size 3.7
c [card-5] found 903 at-most-two constraints of average size 4.7
c [card-5] using previous limit 1344220 for elimination
c [card-5] 17376 out of 17385 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-28] removed 60 variables
c [simpleprobe-6] all 46161 free variables schedulable
c [simpleprobe-6] limit 172060259 penalty 0 = 0 + 0
c [decomp-29] removed 171 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 171 variables, found 42525 hbrs, 98 units
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 35736 probes 78%
c [lift-13] 465 units, 133 impls, 11 eqs in 1 rounds
c [lift-13] 43712 variables remain 96% (1683 retained)
c [lift-13] removed 595 variables
c [cliff-13] limit of 34412051 steps penalty 0 = 0 + 0
c [cliff-13] failed 0, lifted 59
c [unhide-15] limit 8603012 with penalty 0 = 0 + 0
c [unhide-15-31] 3 units, 34 failed, 46086 tauts, 0 hbrs, 20158 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 108 transitive binary clauses
c [transred-13] found 1 units
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 45291 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 830 variables 2% in round 1 in 28950520 steps
c [elim-15-1] backward subsumption/strengthening limit 57901040
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 8295268 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 830 = 2% variables out of 45291
c [bca-14] limit of 10000000 steps
c [bca-14] 78828 out of 88924 literals actually usable 89%
c [bca-14] added 513 blocked clauses in 215132 steps
c [rephase-4] after 173477 conflicts (new increment 20000, next 193477)
c [flushphases] 472 phases reset
c [phase-17] phase bias: 2 positive 67%, 1 negative 33%
c [simplification-15] removed 1704 variables 3.7% (44461 remain 18%)
c [simplification-15] removed 10621 irredundant clauses 3.9% (258820 remain 23%)
c [simplification-15] maximum reduction of 4% = max (4%, 4%)
c [simplification-15] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-15] new conflict interval 24000
c [simplification-15] penalized conflict interval 24000 = 1 * 24000
c [simplification-15] new conflict limit 197477
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  257.5   44460   258820    174002    2076   2747 323987   2 33.5 153.1   37
c i  257.7   44459   258820    174375    2349   2749 323988   1 33.5 153.0   37
c i  257.8   44458   258820    174509    2447   2752 323988   1 33.7 153.1   37
c i  257.9   44457   258820    174966    2777   2761 323993   2 33.7 153.3   38
c i  258.0   44456   258820    175122    2876   2761 324002   3 33.9 153.4   38
c i  258.4   44455   258820    176027    3422   2770 324012   1 34.1 153.4   39
c i  259.0   44454   258820    177300    4213   2781 324058   1 34.4 153.4   39
c i  259.1   44453   258820    177466    4328   2783 324064   1 34.4 153.3   39
c -  259.2   44453   258820    177907    2662   2793 324072   2 34.4 153.3   37
c i  259.5   44452   258820    178493    3053   2803 324091   2 34.4 153.2   37
c i  259.8   44408   258820    179105    3446   2813 324108   1 34.7 153.3   38
c i  260.5   44406   258820    180796    4730   2825 324114   1 34.6 153.0   39
c -  261.4   44406   258820    182523    3424   2833 324124   1 35.0 153.1   37
c i  262.4   44405   258820    184295    4811   2847 324136   1 35.0 152.7   39
c i  263.6   44404   258820    185896    6074   2858 324148   1 35.2 152.4   40
c i  263.7   44403   258820    186023    6142   2859 324150   1 35.2 152.4   40
c -  264.5   44403   258820    187309    4219   2876 324162   1 35.3 152.1   38
c i  265.6   44402   258820    189046    5447   2896 324187   1 35.3 151.7   39
c i  266.0   44401   258820    189695    6012   2896 324192   1 35.3 151.5   39
c i  266.4   44400   258820    190261    6397   2900 324192   1 35.4 151.4   39
c i  266.4   44399   258820    190262    6397   2900 324192   1 35.4 151.4   39
c i  267.4   44398   258820    191704    7499   2909 324194   1 35.5 151.5   41
c i  267.9   44397   258820    192422    8046   2911 324201   1 35.5 151.3   41
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  268.3   44397   258820    192945    4966   2913 324201   1 35.5 151.1   37
c i  269.4   44396   258820    194956    6565   2923 324245   1 35.4 150.7   39
c i  269.7   44395   258820    195592    6802   2923 324245   1 35.7 150.7   40
c i  270.0   44394   258820    195931    7068   2925 324249   1 35.7 150.7   40
c i  270.6   44393   258820    196929    7922   2939 324254   2 35.7 150.3   41
c i  270.7   44356   258820    197015    7985   2940 324255   1 35.7 150.3   41
c i  270.7   44355   258820    197066    8019   2941 324267   2 35.7 150.3   41
c i  270.7   44354   258820    197070    8019   2941 324270   2 35.7 150.3   41
c i  271.2   44353   258820    197775    8579   2943 324275   1 35.7 150.1   41
c i  271.6   44352   258820    198487    9176   2946 324286   1 35.7 149.9   42
c i  271.7   44351   258820    198608    9283   2947 324291   1 35.7 149.9   42
c 
c [simplification-16] limit of 198695 conflicts hit after 198696 conflicts
c [ternres-14] limit 47247579 with penalty 0 = 0 + 0
c [ternres-14] all 44351 free variables schedulable
c [ternres-14] 256 ternary resolvents (1 bin, 255 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-30] removed 180 variables
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 33774 probes 76%
c [lift-14] 326 units, 163 impls, 8 eqs in 1 rounds
c [lift-14] 41748 variables remain 95% (2144 retained)
c [lift-14] removed 389 variables
c [cliff-14] limit of 37798063 steps penalty 0 = 0 + 0
c [cliff-14] failed 1, lifted 41
c [unhide-16] limit 9449515 with penalty 0 = 0 + 0
c [unhide-16-36] 0 units, 24 failed, 27647 tauts, 0 hbrs, 50555 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 122 transitive binary clauses
c [transred-14] found 1 units
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 43833 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 590 variables 1% in round 1 in 29654744 steps
c [elim-16-1] backward subsumption/strengthening limit 59309488
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 8140472 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 590 = 1% variables out of 43833
c [bca-15] limit of 10000000 steps
c [bca-15] 72656 out of 86488 literals actually usable 84%
c [bca-15] added 162 blocked clauses in 199191 steps
c [rephase-5] after 198696 conflicts (new increment 40000, next 238696)
c [flushphases] 29 phases reset
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-16] removed 1108 variables 2.5% (43243 remain 17%)
c [simplification-16] removed 6621 irredundant clauses 2.6% (252199 remain 23%)
c [simplification-16] maximum reduction of 3% = max (2%, 3%)
c [simplification-16] geometric conflict interval increment 6000 = 24000 / 4
c [simplification-16] new conflict interval 30000
c [simplification-16] penalized conflict interval 30000 = 1 * 30000
c [simplification-16] new conflict limit 228696
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  278.4   43242   252199    199114    8421   2886 319795   1 35.7 149.7   41
c i  278.8   43241   252199    199705    8904   2892 319798   2 35.6 149.5   41
c i  278.9   43240   252199    199887    9057   2899 319805   2 35.6 149.5   41
c -  279.3   43240   252199    200666    5718   2903 319806   1 35.6 149.4   37
c i  279.7   43239   252199    201288    6291   2903 319806   1 35.5 149.2   38
c i  280.2   43238   252199    202088    6955   2907 319812   1 35.5 149.0   39
c i  280.9   43237   252199    203096    7799   2917 319816   1 35.5 148.8   40
c i  280.9   43236   252199    203097    7799   2917 319816   1 35.5 148.8   40
c i  280.9   43235   252199    203098    7799   2917 319816   1 35.5 148.8   40
c i  280.9   43234   252199    203099    7799   2917 319816   1 35.5 148.8   40
c i  280.9   43233   252199    203100    7799   2917 319816   0 35.5 148.8   40
c i  281.4   43232   252199    203980    8540   2920 319820   2 35.5 148.6   40
c i  281.8   43229   252199    204548    8959   2927 319838   1 35.5 148.5   40
c i  281.8   43228   252199    204577    8987   2927 319838   1 35.5 148.4   40
c i  282.8   43227   252199    206178   10180   2935 319842   1 35.5 148.1   41
c -  283.1   43227   252199    207363    6509   2960 319881   1 35.5 148.1   37
c i  283.3   43226   252199    207776    6881   2961 319881   1 35.5 148.0   39
c i  284.9   43225   252199    210843    9063   2973 319902   1 36.0 147.9   40
c i  285.5   43224   252199    211744    9797   2978 319903   1 36.0 147.7   41
c i  285.6   43223   252199    211895    9927   2979 319904   1 36.0 147.7   41
c i  287.2   43222   252199    214207   11917   2984 319906   1 35.8 147.1   42
c -  287.4   43222   252199    214633    7283   2985 319906   1 35.8 147.0   37
c i  287.6   43221   252199    214889    7512   2986 319906   1 35.8 147.0   38
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  287.6   43220   252199    215050    7655   2987 319906   1 35.7 146.9   39
c i  289.0   43219   252199    217385    9394   3003 319915   1 36.0 146.4   40
c i  289.1   43218   252199    217555    9530   3003 319915   1 36.0 146.4   40
c i  289.2   43217   252199    217652    9594   3003 319915   1 36.0 146.4   40
c i  291.4   43216   252199    221417   12826   3012 319935   2 35.7 145.6   42
c i  291.4   43215   252199    221418   12826   3012 319935   2 35.7 145.6   42
c i  291.6   43214   252199    221806   13115   3012 319935   1 35.7 145.5   42
c -  292.0   43213   252199    222386    8045   3012 319937   1 35.7 145.4   37
c i  292.7   43212   252199    223467    8964   3017 319940   1 35.6 145.1   39
c i  293.4   43211   252199    224527    9867   3022 319941   1 35.6 144.8   40
c i  293.8   43210   252199    225153   10382   3029 319949   1 35.6 144.7   40
c i  295.3   43209   252199    227414   12303   3034 319962   2 35.4 144.3   42
c i  296.4   43208   252199    229057   13592   3046 319974   2 35.3 143.9   42
c 
c [simplification-17] limit of 229694 conflicts hit after 229694 conflicts
c [ternres-15] limit 52786873 with penalty 0 = 0 + 0
c [ternres-15] all 43208 free variables schedulable
c [ternres-15] 283 ternary resolvents (2 bin, 281 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-8] limit 1319671 penalty 3 = 3 + 0
c [gauss-8] extracted 47 xors of average arity 3.0
c [gauss-8] connected 140 occurrences of 122 variables (average 1.1)
c [gauss-8] limit 1319671 penalty 3 = 3 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 101 variables
c [treelook-6] limit 1319671 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 71360 literals 83%
c [treelook-6] scheduling used 1172668 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1319671 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 1373735 steps
c [treelook-6] 71230 literals remain 83%
c [treelook-6] 14839 variables remain to probed next time 34%
c [treelook-6] removed 22 variables, found 8901 hbrs
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 32303 probes 75%
c [lift-15] 136 units, 128 impls, 19 eqs in 1 rounds
c [lift-15] 40367 variables remain 94% (2541 retained)
c [lift-15] removed 177 variables
c [cliff-15] limit of 42229498 steps penalty 0 = 0 + 0
c [cliff-15] failed 0, lifted 41
c [unhide-17] limit 10557374 with penalty 0 = 0 + 0
c [unhide-17-41] 2 units, 28 failed, 15672 tauts, 0 hbrs, 57748 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 61 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 42847 variables 100%
c [block-6] limit of 32991795 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 1 blocked clauses
c [block-6] 1 < 1/1000 * 248500 = 248 considered unsuccessful
c [cce-6] limit of 6598359 steps penalty 4 = 4 + 0
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 91
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 89
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 88
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 87
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 86
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 85
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 84
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 83
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 82
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 81
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 80
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 79
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 78
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 77
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 76
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 75
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 74
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 73
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 72
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 71
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 70
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 69
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 68
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 67
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 66
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 65
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 64
c [cce-6-1] eliminated 3 clauses out of 8 (38%) of length 63
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 62
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 61
c [cce-6-1] eliminated 5 clauses out of 9 (56%) of length 60
c [cce-6-1] eliminated 3 clauses out of 8 (38%) of length 59
c [cce-6-1] eliminated 1 clauses out of 10 (10%) of length 58
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 112 large clauses in 6598360 steps
c [cce-6-1] allowing another 3299180 steps for small clauses
c [cce-6] scheduling 179373 clauses = 146467 binary + 32906 ternary
c [cce-6] tried to eliminate 122 small clauses 0%
c [cce-6] eliminated 24 small clauses 0%
c [cce-6] eliminated 18 binary clauses 0%
c [cce-6] eliminated 6 ternary clauses 0%
c [cce-6-1] eliminated 24 small clauses in 6598360 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 136 covered clauses in round 1
c [cce-6] eliminated 136 covered clauses in TOTAL during 1 rounds
c [cce-6] 136 < 1/1000 * 248496 = 248 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 42847 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 785 variables 2% in round 1 in 29991814 steps
c [elim-17-1] backward subsumption/strengthening limit 59983628
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 8035264 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 785 = 2% variables out of 42847
c [bca-16] limit of 10000000 steps
c [bca-16] 69963 out of 84126 literals actually usable 83%
c [bca-16] added 106 blocked clauses in 194193 steps
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-17] removed 1146 variables 2.7% (42062 remain 17%)
c [simplification-17] removed 5910 irredundant clauses 2.3% (246289 remain 22%)
c [simplification-17] maximum reduction of 3% = max (3%, 2%)
c [simplification-17] geometric conflict interval increment 7500 = 30000 / 4
c [simplification-17] new conflict interval 37500
c [simplification-17] penalized conflict interval 37500 = 1 * 37500
c [simplification-17] new conflict limit 267194
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  305.5   42061   246289    230963   14714   3044 338002   1 35.2 143.4   44
c -  305.6   42061   246289    230980    8729   3045 338002   1 35.2 143.4   39
c i  307.6   42060   246289    234795   11618   3058 338033   2 35.3 143.0   42
c i  307.6   42059   246289    234804   11626   3058 338033   2 35.3 143.0   42
c i  307.6   42058   246289    234825   11646   3058 338033   2 35.3 143.0   42
c i  308.6   42057   246289    236978   13165   3069 338046   1 35.4 142.9   43
c i  308.8   42056   246289    237345   13355   3069 338046   2 35.5 142.9   43
c i  309.7   42055   246289    238748   14186   3073 338055   2 35.6 142.8   44
c i  309.8   42054   246289    239000   14363   3075 338055   1 35.6 142.8   44
c i  309.8   42053   246289    239008   14369   3075 338055   1 35.6 142.8   44
c i  309.9   42052   246289    239177   14456   3075 338055   1 35.6 142.8   44
c -  311.0   42052   246289    241342    9522   3087 338059   2 35.6 142.7   39
c i  312.3   42051   246289    243794   11579   3092 338072   1 35.5 142.4   41
c i  312.5   42050   246289    244046   11767   3092 338073   1 35.5 142.3   42
c i  312.5   42049   246289    244063   11782   3092 338073   1 35.5 142.3   42
c i  312.7   42048   246289    244478   12113   3092 338073   2 35.5 142.3   42
c i  312.7   42047   246289    244488   12120   3092 338073   2 35.5 142.3   42
c i  314.3   42046   246289    247124   14144   3100 338077   1 35.3 141.9   44
c i  314.7   42045   246289    247873   14676   3101 338079   2 35.6 142.2   44
c i  315.5   42044   246289    249230   15386   3116 338084   3 35.8 142.1   45
c i  315.6   42043   246289    249410   15514   3117 338084   1 35.8 142.1   45
c i  315.8   42042   246289    249784   15768   3117 338084   1 35.8 142.0   45
c i  316.6   42041   246289    251572   16689   3122 338085   1 35.9 141.9   46
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  317.0   42041   246289    252514   10362   3131 338096   1 35.9 141.8   39
c i  319.0   42040   246289    256102   13628   3136 338096   1 35.6 141.5   44
c i  319.1   42039   246289    256208   13685   3137 338096   1 35.7 141.5   44
c i  319.1   42038   246289    256237   13686   3137 338096   1 35.7 141.5   44
c i  320.6   42037   246289    259231   15890   3141 338100   1 36.6 141.9   47
c i  320.7   42036   246289    259443   16094   3143 338100   1 36.5 141.9   47
c -  323.3   42036   246289    263843   11155   3159 338108   1 36.6 141.6   39
c 
c [simplification-18] limit of 267942 conflicts hit after 267942 conflicts
c [ternres-16] limit 59288770 with penalty 0 = 0 + 0
c [ternres-16] all 42036 free variables schedulable
c [ternres-16] 100 ternary resolvents (2 bin, 98 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-33] removed 47 variables
c [basicprobe-6] limit 59288770 penalty 0 = 0 + 0
c [basicprobe-6-0] 10625 probes remain 26% after last round
c [basicprobe-6-0] 445 units = 444 failed (100%) + 1 lifted (0%)
c [basicprobe-6-0] removed 517 variables, found 95611 hbrs
c [bate-5] eliminated 280 asymmetric tautologies during probing
c [cgrclsr-6] limit 370554 penalty 4 = 4 + 0
c [cgrclsr-6] all 41498 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 3 variables
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 30997 probes 75%
c [lift-16] 262 units, 132 impls, 7 eqs in 1 rounds
c [lift-16] 38116 variables remain 93% (3020 retained)
c [lift-16] removed 359 variables
c [cliff-16] limit of 47431016 steps penalty 0 = 0 + 0
c [cliff-16] failed 7, lifted 43
c [unhide-18] limit 11857754 with penalty 0 = 0 + 0
c [unhide-18-46] 2 units, 30 failed, 26217 tauts, 0 hbrs, 43556 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 110 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 41057 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 764 variables 2% in round 1 in 30404170 steps
c [elim-18-1] backward subsumption/strengthening limit 60808340
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 7777747 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 764 = 2% variables out of 41057
c [bca-17] limit of 10000000 steps
c [bca-17] 66994 out of 80588 literals actually usable 83%
c [bca-17] added 159 blocked clauses in 185077 steps
c [rephase-6] after 267942 conflicts (new increment 80000, next 347942)
c [flushphases] 15 phases reset
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-18] removed 1743 variables 4.1% (40293 remain 16%)
c [simplification-18] removed 9537 irredundant clauses 3.9% (236752 remain 21%)
c [simplification-18] maximum reduction of 4% = max (4%, 4%)
c [simplification-18] geometric conflict interval increment 7500 = 37500 / 5
c [simplification-18] new conflict interval 45000
c [simplification-18] penalized conflict interval 45000 = 1 * 45000
c [simplification-18] new conflict limit 312942
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  334.9   40292   236752    268588   12710   3089 408237   1 36.6 141.2   43
c R  336.8   40292   236752    272374   14968   3093 408241   1 36.6 140.9   45
c i  340.5   40291   236752    278294   19628   3118 408256   3 36.2 139.8   46
c -  340.5   40291   236752    278338   11664   3118 408256   2 36.2 139.8   40
c i  342.6   40290   236752    281737   14531   3130 408267   1 36.0 139.1   43
c i  345.3   40289   236752    286932   18689   3142 408295   1 35.7 138.3   44
c -  347.1   40289   236752    289840   12434   3150 408297   1 35.5 137.8   40
c i  349.1   40288   236752    292865   14890   3164 408301   2 35.4 137.2   42
c i  349.2   40287   236752    293025   15011   3164 408302   1 35.4 137.2   42
c i  350.4   40286   236752    295012   16439   3177 408309   1 35.4 136.9   43
c i  350.9   40285   236752    295922   17069   3177 408311   1 35.4 136.8   44
c i  351.0   40284   236752    296157   17232   3178 408312   2 35.4 136.8   44
c i  351.2   40283   236752    296442   17439   3180 408319   1 35.3 136.8   44
c i  352.3   40282   236752    298796   19229   3190 408357   4 35.4 136.7   45
c -  354.9   40282   236752    302809   13338   3213 408364   1 35.1 136.1   40
c i  355.5   40281   236752    303976   14261   3214 408366   1 35.0 135.9   42
c i  358.9   40280   236752    309757   18818   3229 408384   1 34.7 134.9   43
c 
c [simplification-19] limit of 313498 conflicts hit after 313499 conflicts
c [ternres-17] limit 67129158 with penalty 0 = 0 + 0
c [ternres-17] all 40280 free variables schedulable
c [ternres-17] 381 ternary resolvents (0 bin, 381 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-34] removed 18 variables
c [simpleprobe-7] all 40275 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 108 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 108 variables, found 61531 hbrs, 59 units
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 29320 probes 73%
c [lift-17] 174 units, 144 impls, 9 eqs in 1 rounds
c [lift-17] 36379 variables remain 91% (3531 retained)
c [lift-17] removed 257 variables
c [cliff-17] limit of 53703326 steps penalty 0 = 0 + 0
c [cliff-17] failed 4, lifted 53
c [unhide-19] limit 13425831 with penalty 0 = 0 + 0
c [unhide-19-52] 3 units, 27 failed, 72989 tauts, 0 hbrs, 62076 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 140 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 39834 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 458 variables 1% in round 1 in 28347063 steps
c [elim-19-1] backward subsumption/strengthening limit 56694126
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 7629339 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 458 = 1% variables out of 39834
c [bca-18] limit of 10000000 steps
c [bca-18] 64576 out of 78754 literals actually usable 82%
c [bca-18] added 136 blocked clauses in 182264 steps
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-19] removed 904 variables 2.2% (39376 remain 16%)
c [simplification-19] removed 5198 irredundant clauses 2.2% (231554 remain 21%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 15000 = 45000 / 3
c [simplification-19] new conflict interval 60000
c [simplification-19] penalized conflict interval 60000 = 1 * 60000
c [simplification-19] new conflict limit 373499
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  369.4   39375   231554    313572   17694   3261 414656   1 34.5 134.4   43
c i  369.5   39374   231554    313728   17812   3261 414656   1 34.4 134.4   43
c -  373.3   39374   231554    320402   13693   3280 414674   1 34.1 133.5   40
c i  373.4   39373   231554    320545   13791   3280 414674   1 34.1 133.5   41
c i  375.4   39372   231554    324959   17110   3288 414676   1 33.8 133.1   42
c i  377.4   39371   231554    328801   20475   3293 414678   1 33.6 132.7   43
c i  378.3   39370   231554    330548   21946   3296 414679   1 33.5 132.5   45
c -  380.3   39370   231554    333837   14543   3313 414684   1 33.3 132.0   40
c i  383.3   39369   231554    339170   19010   3332 414696   1 33.0 131.3   43
c -  388.3   39048   231554    348105   15436   3370 414699   1 32.4 130.2   40
c i  391.3   39047   231554    353385   19475   3413 414710   1 32.1 129.6   42
c i  391.9   39046   231554    354393   20184   3413 414710   1 32.1 129.6   43
c i  392.6   39045   231554    355607   21115   3434 414719   1 32.0 129.5   43
c i  393.1   39044   231554    356721   21866   3433 414722   1 32.0 129.4   43
c i  394.0   39043   231554    358142   22900   3446 414724   1 32.0 129.2   43
c i  394.0   39042   231554    358143   22900   3446 414724   1 32.0 129.2   43
c i  394.5   39041   231554    358950   23453   3470 414732   1 31.9 129.1   43
c i  394.7   39038   231554    359209   23637   3476 414733   1 31.9 129.1   43
c i  394.9   39037   231554    359519   23840   3485 414739   1 31.9 129.0   43
c i  394.9   38977   231554    359598   23886   3493 414742   1 31.9 129.0   43
c i  394.9   38670   231554    359603   23885   3494 414745   1 31.9 129.0   43
c i  394.9   37881   231554    359636   23898   3498 414751   1 31.9 129.0   43
c i  395.1   37658   231554    359889   24056   3515 414754   1 31.9 129.0   43
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  395.1   37356   231554    359918   24064   3518 414756   1 31.9 129.0   43
c i  395.1   35814   231554    359921   24063   3518 414758   1 31.9 129.0   43
c i  395.1   35475   231554    359924   24063   3518 414760   1 31.9 129.0   43
c i  395.1   34599   231554    359931   24067   3518 414762   1 31.9 129.0   43
c i  395.1   31150   231554    359933   24067   3518 414763   1 31.9 129.0   43
c i  395.1   29550   231554    359939   24070   3519 414764   1 31.9 129.0   43
c 0  395.1   27812   231554    359939   24070   3519 414764   1 31.9 129.0   43
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 686 basic ate = 653 trn 95% + 33 lrg 5% in 5 updates
c bcas: 18 count, 3611 added (393 skipped), 4712685 steps
c bkwd: tried 5735477 clauses, 11470953 lits, 2.00 lits/clause
c bkwd: checked 120191527 occs, 20.96 occs/clause, 10.48 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 1 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 6 bces, 11935 removed, 8149051 resolutions, 24380459 steps
c blkd: 13264 blocking literals 3%, 17 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 0 am1, 12205199 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 148480 subsumed
c card: 74923 at-most-one constraints found, average size 4.18
c card: 74923 at-most-one constraints used 100%, average size 4.18
c card: 2587 at-most-two constraints found, average size 4.74
c card: 2542 at-most-two constraints used 98%, average size 4.75
c cces: 6 cces, 17176 eliminated, 17169 ate 100%, 7 abce 0%
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, 2112287 esteps, 145677 csteps
c cgrs: 3 eqs, 1 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: 3387 extracted (3148 ands 93%, 232 xors 7%, 7 ites 0%)
c clff: 17 cliffs, 3407 lifted, 127 failed
c clff: 13194 decisions, 426721723 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3776495 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 198 gcs, 0 rescored clauses, 188 rescored vars
c dcps: 35 decompositions, 10031 equivalent 4%
c deco: 56534 decision-only clauses 16%, 73% reduction
c decs: 2260910 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 48066 flipped 2.126% (in 555 phases)
c elms: 19 elims, 118777 eliminated 45%
c elms: 37 rounds, 1.9 rounds/bve
c elms: 103623 small 87%, 15137 large 13%
c elms: 514383 tried small, 103623 succeeded 20%, 410760 failed 80%
c elms: 53255 subsumed, 102280 strengthened, 2906 blocked
c elms: 31447916 copies, 29598228 resolutions, 23036291 ipos
c elms: 9121022 subchks, 10705698 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 8 extractions, 1589 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 61 binary and 0 ternary equations
c gaus: 0 gc, 29047426 steps, 14523713 extr 50%, 57762 elim 0%
c glue: 31.9 orig avg, 28.2 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 942296 = 228481 simple + 701505 trn 24% + 12310 lrg 74%, 3159 sub 1%
c hght: 129 average, 4.05 height/glue
c ints: 11450 luby (2503516 steps), 0 inout (0 steps)
c lift: 17 phases, 22485 probed (8064 level1 36%, 14421 level2 64%)
c lift: 4712 units, 142 equivalences, 1337 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 358659 clauses, 118.0 length
c lrnd: 142889 uips 40%, 192777 flips 54%
c mega: 0 count, 0 failed, 0 rounds
c mins: 42331076 learned lits, 50% minimized
c mins: 293548 mins 82%, 3043 bin 1%, 5534 size 2%, 56534 deco 16%
c move: moved 358659, 12584 bin 4%, 9417 trn 3%, 0 lrg 0%
c otfs: str 5209 dyn (5177 red, 32 irr) 1280 drv 25%, 3929 rst 75%
c otfs: sub 71 dyn (71 red, 0 irr)
c phas: 21 computed, 131349 set, 28470 pos (22%), 102879 neg (78%)
c prbs: 6 basic, 11079 probed, 1036 failed, 2 lifted
c prbs: 7 simple, 1060211 probed, 939 failed, 1812 eqs
c prbs: 6 treelook, 174 probed, 22 failed, 0 lifted
c prps: 1596539533 props, 653 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c psns: 112298620 searches, 22303413 hits, 20% 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: 35 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 35 arith 100%, 0 double 0%
c rmbd: 44951 removed, 7995 red 18%
c rphs: 6 recomputed phases
c rsts: 11109 restarts 97%, 341 skipped 3%
c rsts: 0 saturating 0%, 2 agile 1%, 339 reuse 99%
c rsts: 31.6 avg interval, 31.6 scaled, 1.0 factor
c rsts: 5630 kept 50.7% average 25.4%
c simp: 19 count (19 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 358659 count (334291 tried 0.9), 69346 sub out of 351838 (19.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: 105633 fixed 40%, 494 its, 728.62 confs/it
c trvs: 11348499843 traversals, 93% srch, 8% simp, 0% lkhd
c trvs: 7.1 search traversals per propagation, 29317.6 per conflict
c trvs: 1.4 search traversals per search visit
c trds: 17 transitive reductions, 2177 removed, 18 failed
c trds: 14803 nodes, 39271 edges, 33857311 steps
c trim: 2946231 words, 11.2 MB
c trnr: 17 count, 34 bin, 13377 trn, 82725742 steps
c unhd: 19 count, 52 rounds, 126032318 steps
c unhd: 9596 non-trivial sccs of average size 2.2
c unhd: 83 units, 82 bin, 0 trn, 1 lrg
c unhd: 7148 failed, 7097 stamp, 0 lits, 18 bin, 18 trn, 1 lrg
c unhd: 377879 tauts, 7013 bin 2%, 20794 trn 6%, 1988 lrg 1%
c unhd: 377879 tauts, 348084 stamp 92%, 320806 red 85%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 617171 str, 82 bin 0%, 7605 trn 1%, 609484 lrg 99%, 591229 red 96%
c vars: 27812 remaining 11% and 234441 removed 89% out of 262253
c vars: 105633 fixed 40%, 118777 eliminated 45%, 10031 equivalent 4%
c vsts: 8291177518 visits, 90% srch, 10% simp, 0% lkhd
c vsts: 5.1 search visits per propagation, 20823.6 per conflict
c wchs: 557887246 pushed, 57340896 enlarged, 275 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    351838 100    214439 100  11005334 100   2510004 100    166519 100
c 
c  0      15970   5         0   0   6537674  59    831606  33     45079  27 
c  1      15463   4         0   0   2773735  25<   603848  24     43781  26 
c  2      70054  20     42689  20   1013766   9    437488  17<    32872  20<
c  3     102434  29     84011  39    297056   3    270938  11     15549   9 
c  4      41870  12<    35140  16<   121318   1    107795   4      7656   5 
c  5      20383   6     17249   8     63400   1     54798   2      4653   3 
c  6      15938   5      8597   4     46609   0     41401   2      3285   2 
c  7      16744   5      6438   3     41994   0     41433   2      2958   2 
c  8      14032   4      5394   3     32923   0     33473   1      2672   2 
c  9      10700   3      4102   2     21979   0     24214   1      2027   1 
c 10      12470   4      4680   2     30336   0     28820   1      2696   2 
c 11      11232   3      4404   2     17754   0     24452   1      2366   1 
c 12       4403   1      1690   1      6580   0      9443   0       886   1 
c 13        145   0        45   0       210   0       295   0        39   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             4.1           4.0           0.7           1.9           2.1
c std             2.8           2.2           1.4           2.4           2.6
c 
c   40.117  10% elim
c   37.815  10% analysis
c   22.866   6% unhide
c   17.346   4% cce
c   15.894   4% gc
c   14.024   4% probe
c   12.854   3% cliff
c   12.277   3% lift
c    7.653   2% bump
c    7.608   2% decomp
c    6.344   2% mincls
c    5.102   1% backward
c    4.398   1% defrag
c    3.456   1% restart
c    3.189   1% decide
c    2.778   1% bca
c    2.570   1% gauss
c    2.481   1% block
c    2.044   1% transred
c    1.458   0% cgrclsr
c    1.216   0% phase
c    0.857   0% card
c    0.724   0% ternres
c    0.388   0% reduce
c    0.123   0% tabularasa
c    0.022   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    5.784   1% probe simple     41%
c    6.098   2% probe basic      43%
c    2.142   1% probe tree-look  15%
c ==================================
c   11.446   3% preprocessing     8%
c  127.941  32% inprocessing     92%
c ==================================
c  139.386  35% simplifying
c  255.720  65% search
c ==================================
c  395.113 100% all
c 
c 2260910 decisions, 5722.2 decisions/sec
c 359939 conflicts, 911.0 conflicts/sec
c 1596539533 propagations, 4.0 megaprops/sec
c 395.1 seconds, 96.1 MB
c launch: done
