c launch: /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c host: atom29
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/manol-pipe-g10bid_i.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c no embedded options
c found 'p cnf 266405 792175' header
c read 266405 variables, 792175 clauses, 1848407 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 266404 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  266404   792174         0       0      0     0   0  0.0   0.0   44
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 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 266404 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 7402 variables
c [simpleprobe-1] 91633 variables remain 35% (167369 retained)
c [simpleprobe-1] removed 7402 variables, found 953 hbrs, 86 units
c [unhide-1] limit 385024 based on 770048 irredundant clauses
c [unhide-1-1] 0 units, 83 failed, 201 tauts, 0 hbrs, 171 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 257663 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 220121 variables 85% in round 1 in 60611768 steps
c [elim-1-1] backward subsumption/strengthening limit 121223536
c [elim-1-1] subsumed 692 and strengthened 1264 clauses in 121226315 steps
c [elim-1-1] rescheduled 1574 variables 1% by backward subsumption
c [elim-1-2] eliminated 48 variables 0% in round 2 in 926972 steps
c [elim-1-2] backward subsumption/strengthening limit 1853944
c [elim-1-2] subsumed 3 and strengthened 6 clauses in 1854122 steps
c [elim-1-2] rescheduled 36 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 12690 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 220267 = 85% variables out of 257663
c [phase-1] phase bias: 11667 positive 31%, 25729 negative 69%
c [simplification-1] removed 229008 variables 86.0% (37396 remain 14%)
c [simplification-1] removed 513549 irredundant clauses 64.8% (278625 remain 35%)
c [simplification-1] maximum reduction of 86% = max (86%, 65%)
c [simplification-1] large reduction 86% >= 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] 155138, max 243507, min4 115281 at 75%, min10 49087 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number variables 37396 drops below limit 66601
c [tabula-rasa-1] number clauses 278625 drops below limit 396087
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 37396 phases reset fully
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
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 9349 and clause limit 139312
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   10.7   37396   278625         5       2      0    33   1  2.0 185.7   37
c R   10.7   37396   278625        20       9      5    36   5  2.1 145.1   37
c i   10.7   37395   278625        25      10      8    36   5  2.0 143.6   37
c i   10.7   37391   278625        33      15      9    37   7  2.6 125.2   37
c R   10.7   37389   278625        61      28     14    40   7  3.4  97.4   37
c i   10.7   37388   278625        96      48     18    42   8  3.9  87.4   37
c i   10.7   37364   278625       104      50     20    45   8  3.6  84.9   37
c i   10.7   37363   278625       135      69     24    51   9  3.6  80.7   37
c i   10.7   37308   278625       137      70     24    51   9  3.6  79.9   37
c i   10.7   37304   278625       138      70     24    51   8  3.6  79.6   37
c R   10.7   37244   278625       165      89     28    54   9  3.7  76.3   37
c i   10.7   37243   278625       172      93     30    54   9  3.7  74.9   37
c i   10.7   37237   278625       184      97     34    56   9  3.7  73.6   37
c i   10.7   37218   278625       185      97     34    56   9  3.6  73.6   37
c R   10.8   37141   278625       413     263     54    66   7  4.7 305.6   37
c i   10.8   37140   278625       447     287     55    68   7  4.7 297.9   37
c i   10.8   37139   278625       452     288     55    68   7  4.7 297.6   37
c i   10.8   37048   278625       453     288     55    68   7  4.6 297.5   37
c i   11.0   37038   278625       671     427     70    74   5  4.9 601.4   37
c i   11.0   37035   278625       673     427     70    75   5  4.8 599.6   37
c i   11.0   37023   278625       692     443     72    75   4  5.0 585.2   37
c i   11.0   37015   278625       693     443     72    75   4  5.0 582.6   37
c i   11.0   37010   278625       806     503     82    78   5  4.8 567.2   37
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   11.0   37009   278625       836     523     84    78   4  4.8 555.6   37
c i   11.0   37008   278625       837     523     84    78   4  4.8 555.4   37
c R   11.0   37005   278625       992     622     89    79   6  4.8 539.8   37
c 
c [simplification-2] limit of 1401 conflicts hit after 1401 conflicts
c [decomp-3] removed 562 variables
c [simpleprobe-2] 12911 schedulable variables 35%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 12946 variables remain 35% (23885 retained)
c [simpleprobe-2] removed 3 variables, found 45 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24672 literals 33%
c [treelook-1] scheduling used 300018 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 343445 steps
c [treelook-1] 24645 literals remain 33%
c [treelook-1] 21067 variables remain to probed next time 57%
c [decomp-5] removed 5 variables
c [treelook-1] removed 9 variables, found 128 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 14469 probes remain 40% after last round
c [basicprobe-1-0] 179 units = 157 failed (88%) + 22 lifted (12%)
c [basicprobe-1-0] removed 959 variables, found 1278 hbrs
c [unhide-2] limit 135895 based on 271790 irredundant clauses
c [unhide-2-2] 11 units, 109 failed, 77 tauts, 0 hbrs, 4246 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 35623 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 7236 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 5 clauses out of 97 (5%) of length 23
c [cce-1-1] eliminated 8 clauses out of 80 (10%) of length 22
c [cce-1-1] eliminated 14 clauses out of 109 (13%) of length 21
c [cce-1-1] eliminated 12 clauses out of 121 (10%) of length 20
c [cce-1-1] eliminated 23 clauses out of 187 (12%) of length 19
c [cce-1-1] eliminated 16 clauses out of 280 (6%) of length 18
c [cce-1-1] eliminated 24 clauses out of 381 (6%) of length 17
c [cce-1-1] eliminated 70 clauses out of 443 (16%) of length 16
c [cce-1-1] eliminated 89 clauses out of 368 (24%) of length 15
c [cce-1-1] eliminated 128 clauses out of 508 (25%) of length 14
c [cce-1-1] eliminated 210 clauses out of 658 (32%) of length 13
c [cce-1-1] eliminated 270 clauses out of 1046 (26%) of length 12
c [cce-1-1] eliminated 362 clauses out of 1844 (20%) of length 11
c [cce-1-1] eliminated 609 clauses out of 2601 (23%) of length 10
c [cce-1-1] eliminated 925 clauses out of 4483 (21%) of length 9
c [cce-1-1] eliminated 1549 clauses out of 7548 (21%) of length 8
c [cce-1-1] eliminated 2623 clauses out of 15281 (17%) of length 7
c [cce-1-1] eliminated 2953 clauses out of 34295 (9%) of length 6
c [cce-1-1] eliminated 2468 clauses out of 23826 (10%) of length 5
c [cce-1-1] eliminated 2110 clauses out of 28413 (7%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 14468 large clauses in 226009830 steps
c [cce-1-1] allowing another 113004915 steps for small clauses
c [cce-1] scheduling 51896 clauses = 31988 binary + 19908 ternary
c [cce-1] tried to eliminate 51896 small clauses 100%
c [cce-1] eliminated 2143 small clauses 4%
c [cce-1] eliminated 1485 binary clauses 5%
c [cce-1] eliminated 658 ternary clauses 3%
c [cce-1-1] eliminated 2143 small clauses in 156285751 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 16611 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 49753 clauses = 30503 binary + 19250 ternary
c [cce-1] tried to eliminate 49753 small clauses 100%
c [cce-1] eliminated 707 small clauses 1%
c [cce-1] eliminated 404 binary clauses 1%
c [cce-1] eliminated 303 ternary clauses 2%
c [cce-1-2] eliminated 707 small clauses in 33757289 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 707 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 0 steps for small clauses
c [cce-1] scheduling 49046 clauses = 30099 binary + 18947 ternary
c [cce-1] tried to eliminate 49046 small clauses 100%
c [cce-1] eliminated 350 small clauses 1%
c [cce-1] eliminated 141 binary clauses 0%
c [cce-1] eliminated 209 ternary clauses 1%
c [cce-1-3] eliminated 350 small clauses in 48999819 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 350 covered clauses in round 3
c [cce-1-4] completed large round (ACCE)
c [cce-1-4] allowing another 0 steps for small clauses
c [cce-1] scheduling 48696 clauses = 29958 binary + 18738 ternary
c [cce-1] tried to eliminate 48696 small clauses 100%
c [cce-1] eliminated 43 small clauses 0%
c [cce-1] eliminated 13 binary clauses 0%
c [cce-1] eliminated 30 ternary clauses 0%
c [cce-1-4] eliminated 43 small clauses in 47998135 steps
c [cce-1-4] completed small round (ACCE)
c [cce-1-4] eliminated 43 covered clauses in round 4
c [cce-1-5] completed large round (ACCE)
c [cce-1-5] allowing another 0 steps for small clauses
c [cce-1] scheduling 48653 clauses = 29945 binary + 18708 ternary
c [cce-1] tried to eliminate 12829 small clauses 26%
c [cce-1] eliminated 3 small clauses 0%
c [cce-1] eliminated 1 binary clauses 0%
c [cce-1] eliminated 2 ternary clauses 0%
c [cce-1-5] eliminated 3 small clauses in 12959007 steps
c [cce-1-5] incomplete small round (ACCE)
c [cce-1-5] eliminated 3 covered clauses in round 5
c [cce-1] eliminated 17714 covered clauses in TOTAL during 5 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 35287 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 3916 not tried 11% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 6667 = 19% variables out of 35287
c [bca-1] limit of 10000000 steps
c [bca-1] 54286 out of 57242 literals actually usable 95%
c [bca-1] added 368 blocked clauses in 174132 steps
c [phase-3] phase bias: 121 positive 66%, 61 negative 34%
c [simplification-2] removed 8385 variables 22.7% (28620 remain 11%)
c [simplification-2] removed 65601 irredundant clauses 23.5% (213024 remain 27%)
c [simplification-2] maximum reduction of 24% = max (23%, 24%)
c [simplification-2] large reduction 24% >= 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 3401
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   24.9   28619   213024      1415     738   1625  2246   4  6.0 512.5   33
c i   24.9   28616   213024      1519     793   1637  2251   5  5.9 498.5   33
c i   24.9   28614   213024      1520     793   1637  2251   5  5.9 498.4   33
c i   25.0   28609   213024      1866    1014   1655  2257   7  5.9 475.6   33
c i   25.0   28608   213024      1987    1129   1655  2258   9  6.4 472.2   33
c i   25.0   28603   213024      2020    1147   1656  2258   8  6.3 468.4   33
c R   25.0   28602   213024      2311    1309   1686  2268   9  6.3 456.7   34
c i   25.1   28601   213023      3438    2068   1727  2287   9  7.1 390.9   34
c i   25.1   28600   213023      3439    2068   1727  2287   9  7.1 390.8   34
c 
c [simplification-3] limit of 3609 conflicts hit after 3609 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 28588 free variables schedulable
c [ternres-1] 6075 ternary resolvents (261 bin, 5814 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 152 at-most-one constraints of average size 3.3
c [card-2] found 43 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 195 out of 195 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 18500 xors of average arity 3.0
c [gauss-1] connected 55395 occurrences of 6103 variables (average 9.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 75 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 18936 literals 33%
c [treelook-2] scheduling used 300064 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 332770 steps
c [treelook-2] 18867 literals remain 33%
c [treelook-2] 11763 variables remain to probed next time 41%
c [decomp-7] removed 2 variables
c [treelook-2] removed 3 variables, found 457 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 28510 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 2 variables
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 23014 probes 81%
c [lift-1] 46 units, 20 impls, 7 eqs in 1 rounds
c [lift-1] 27575 variables remain 97% (872 retained)
c [lift-1] removed 61 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 80, lifted 66
c [unhide-3] limit 105819 based on 211639 irredundant clauses
c [unhide-3-3] 1 units, 5 failed, 459 tauts, 0 hbrs, 2325 literals
c [transred-1] limit 206772 based on 206772 irredundant clauses
c [transred-1] removed 214 transitive binary clauses
c [transred-1] found 5 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 28139 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 1736 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 27
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 25
c [cce-2-1] eliminated 16 clauses out of 26 (62%) of length 24
c [cce-2-1] eliminated 7 clauses out of 39 (18%) of length 23
c [cce-2-1] eliminated 13 clauses out of 74 (18%) of length 22
c [cce-2-1] eliminated 11 clauses out of 82 (13%) of length 21
c [cce-2-1] eliminated 29 clauses out of 165 (18%) of length 20
c [cce-2-1] eliminated 36 clauses out of 217 (17%) of length 19
c [cce-2-1] eliminated 52 clauses out of 333 (16%) of length 18
c [cce-2-1] eliminated 71 clauses out of 442 (16%) of length 17
c [cce-2-1] eliminated 83 clauses out of 527 (16%) of length 16
c [cce-2-1] eliminated 101 clauses out of 593 (17%) of length 15
c [cce-2-1] eliminated 123 clauses out of 709 (17%) of length 14
c [cce-2-1] eliminated 201 clauses out of 951 (21%) of length 13
c [cce-2-1] eliminated 353 clauses out of 1554 (23%) of length 12
c [cce-2-1] eliminated 6 clauses out of 2287 (0%) of length 11
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] eliminated 1106 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 41472 clauses = 24116 binary + 17356 ternary
c [cce-2] tried to eliminate 16128 small clauses 39%
c [cce-2] eliminated 249 small clauses 1%
c [cce-2] eliminated 168 binary clauses 1%
c [cce-2] eliminated 81 ternary clauses 0%
c [cce-2-1] eliminated 249 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ACCE)
c [cce-2-1] eliminated 1355 covered clauses in round 1
c [cce-2] eliminated 1355 covered clauses in TOTAL during 1 rounds
c [elim-3] 3724 variables 13% will be scheduled this time
c [elim-3] scheduled 3724 variables 13%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 2182 not tried 8% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 109 = 0% variables out of 27878
c [bca-2] limit of 10000000 steps
c [bca-2] 50508 out of 55540 literals actually usable 91%
c [bca-2] added 14 blocked clauses in 157626 steps
c [phase-4] phase bias: 16 positive 27%, 43 negative 73%
c [simplification-3] removed 819 variables 2.9% (27769 remain 10%)
c [simplification-3] removed 9767 irredundant clauses 4.6% (203256 remain 26%)
c [simplification-3] maximum reduction of 5% = max (3%, 5%)
c [simplification-3] large reduction 5% >= 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 5609
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   29.5   27769   203256      5263    3491   6591  2566   8  7.6 356.8   34
c 
c [simplification-4] limit of 5619 conflicts hit after 5623 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 27769 free variables schedulable
c [ternres-2] 368 ternary resolvents (2 bin, 366 trn)
c [ternres-2] 14402 variables remain 52% (13367 retained)
c [decomp-8] removed 78 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 11195 sched 41%, 68 failed, 5 lifted, 763 hbrs
c [decomp-9] removed 138 variables
c [basicprobe-2-1] 14348 probes remain 52% after last round
c [basicprobe-2-1] 73 units = 68 failed (93%) + 5 lifted (7%)
c [basicprobe-2-1] removed 138 variables, found 768 hbrs
c [bate-1] eliminated 155 asymmetric tautologies during probing
c [cgrclsr-2] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-2] all 27553 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 1 variables
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 21607 probes 78%
c [lift-2] 3 units, 7 impls, 1 eqs in 1 rounds
c [lift-2] 25690 variables remain 93% (1857 retained)
c [lift-2] removed 5 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 13, lifted 6
c [unhide-4] limit 100755 based on 201510 irredundant clauses
c [unhide-4-4] 0 units, 2 failed, 589 tauts, 0 hbrs, 2771 literals
c [transred-2] limit 221778 with penalty 0 = 0 + 0
c [transred-2] removed 89 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 27518 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1543 blocked clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-3-1] eliminated 1 clauses out of 21 (5%) of length 24
c [cce-3-1] eliminated 1 clauses out of 389 (0%) of length 16
c [cce-3-1] eliminated 2 clauses out of 489 (0%) of length 15
c [cce-3-1] eliminated 2 clauses out of 583 (0%) of length 14
c [cce-3-1] eliminated 2 clauses out of 725 (0%) of length 13
c [cce-3-1] eliminated 5 clauses out of 1227 (0%) of length 12
c [cce-3-1] eliminated 314 clauses out of 2156 (15%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 329 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 40538 clauses = 23355 binary + 17183 ternary
c [cce-3] tried to eliminate 18335 small clauses 45%
c [cce-3] eliminated 152 small clauses 0%
c [cce-3] eliminated 69 binary clauses 0%
c [cce-3] eliminated 83 ternary clauses 0%
c [cce-3-1] eliminated 152 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 481 covered clauses in round 1
c [cce-3] eliminated 481 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 27277 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 2860 not tried 10% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 726 = 3% variables out of 27277
c [bca-3] limit of 10000000 steps
c [bca-3] 47529 out of 53104 literals actually usable 90%
c [bca-3] added 75 blocked clauses in 150978 steps
c [phase-5] phase bias: 10 positive 29%, 25 negative 71%
c [simplification-4] removed 1218 variables 4.4% (26551 remain 10%)
c [simplification-4] removed 5883 irredundant clauses 2.9% (197373 remain 25%)
c [simplification-4] maximum reduction of 4% = max (4%, 3%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 24000
c [simplification-4] penalized conflict interval 24000 = 1 * 24000
c [simplification-4] new conflict limit 29623
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   33.9   26551   197372      7568    2923   5759  2268   6  7.7 316.8   34
c R   34.4   26551   197372     11796    6114   5911  2278  12  9.9 290.1   34
c -   34.5   26551   197372     12383    3994   5959  2281   8  9.7 280.3   34
c -   35.2   26551   197372     17985    5109   6177  2309   9  9.1 251.2   34
c -   35.8   26551   197372     24639    6641   6366  2325  12  9.7 233.7   34
c R   35.9   26551   197372     26145    7891   6366  2325  11  9.6 238.6   34
c 
c [simplification-5] limit of 29731 conflicts hit after 29732 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 13737 schedulable variables 52%
c [ternres-3] 692 ternary resolvents (18 bin, 674 trn)
c [ternres-3] 246 variables remain 1% (26305 retained)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 9070 xors of average arity 3.0
c [gauss-2] connected 27199 occurrences of 5009 variables (average 5.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 18 variables
c [simpleprobe-3] 9350 schedulable variables 35%
c [simpleprobe-3] limit 3683596 penalty 0 = 0 + 0
c [decomp-11] removed 1 variables
c [simpleprobe-3] 9374 variables remain 35% (17158 retained)
c [simpleprobe-3] removed 1 variables, found 44 hbrs, 0 units
c [cgrclsr-3] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-3] all 26532 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 552539 with penalty 0 = 0 + 0
c [lift-3] using 19800 probes 75%
c [lift-3] 4 units, 6 impls, 0 eqs in 1 rounds
c [lift-3] 23704 variables remain 89% (2823 retained)
c [lift-3] removed 5 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 7, lifted 3
c [unhide-5] limit 184179 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 0 failed, 223 tauts, 0 hbrs, 3144 literals
c [transred-3] limit 920899 with penalty 0 = 0 + 0
c [transred-3] removed 165 transitive binary clauses
c [transred-3] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 26511 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 27 blocked clauses
c [block-4] 27 < 1/1000 * 196838 = 196 considered unsuccessful
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 26
c [cce-4-1] eliminated 4 clauses out of 66 (6%) of length 22
c [cce-4-1] eliminated 4 clauses out of 75 (5%) of length 21
c [cce-4-1] eliminated 2 clauses out of 165 (1%) of length 20
c [cce-4-1] eliminated 4 clauses out of 236 (2%) of length 19
c [cce-4-1] eliminated 7 clauses out of 313 (2%) of length 18
c [cce-4-1] eliminated 20 clauses out of 386 (5%) of length 17
c [cce-4-1] eliminated 73 clauses out of 507 (14%) of length 16
c [cce-4-1] eliminated 70 clauses out of 595 (12%) of length 15
c [cce-4-1] eliminated 54 clauses out of 670 (8%) of length 14
c [cce-4-1] eliminated 69 clauses out of 817 (8%) of length 13
c [cce-4-1] eliminated 107 clauses out of 1337 (8%) of length 12
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 416 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 39610 clauses = 22702 binary + 16908 ternary
c [cce-4] tried to eliminate 17164 small clauses 43%
c [cce-4] eliminated 61 small clauses 0%
c [cce-4] eliminated 23 binary clauses 0%
c [cce-4] eliminated 38 ternary clauses 0%
c [cce-4-1] eliminated 61 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 477 covered clauses in round 1
c [cce-4] eliminated 477 covered clauses in TOTAL during 1 rounds
c [elim-5] 2146 variables 8% will be scheduled this time
c [elim-5] scheduled 2146 variables 8%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] incomplete 1365 not tried 5% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 15 = 0% variables out of 26511
c [elim-5] 15 < 1/1000 * 26511 = 26 considered unsuccessful
c [bca-4] limit of 10000000 steps
c [bca-4] 44703 out of 52994 literals actually usable 84%
c [bca-4] added 9 blocked clauses in 149036 steps
c [rephase-1] after 29732 conflicts (new increment 20000, next 49732)
c [flushphases] 820 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 55 variables 0.2% (26496 remain 10%)
c [simplification-5] removed 1151 irredundant clauses 0.6% (196221 remain 25%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-5] new conflict interval 36000
c [simplification-5] penalized conflict interval 36000 = 1 * 36000
c [simplification-5] new conflict limit 65732
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   40.1   26496   196221     31553    7681   7159  2425   8  9.3 227.2   34
c -   41.0   26496   196221     39394    9011   7415  2449  10  9.2 212.0   34
c -   42.2   26496   196220     48196   10688   7684  2466  10  9.0 205.2   34
c -   42.7   26496   196220     56723   12090   7782  2468  14  9.2 208.6   34
c R   42.8   26496   196220     57468   12709   7792  2468  15  9.3 208.7   35
c 
c [simplification-6] limit of 65812 conflicts hit after 65813 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 245 schedulable variables 1%
c [ternres-4] 2347 ternary resolvents (36 bin, 2311 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 169 at-most-one constraints of average size 3.3
c [card-3] found 71 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 240 out of 240 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 15 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15710 literals 30%
c [treelook-3] scheduling used 300129 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 326139 steps
c [treelook-3] 15608 literals remain 29%
c [treelook-3] 8701 variables remain to probed next time 33%
c [treelook-3] removed 0 variables, found 106 hbrs
c [lift-4] limit 1188688 with penalty 0 = 0 + 0
c [lift-4] using 18775 probes 71%
c [lift-4] 1 units, 11 impls, 4 eqs in 1 rounds
c [lift-4] 22009 variables remain 83% (4467 retained)
c [lift-4] removed 5 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 10, lifted 1
c [unhide-6] limit 396229 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 0 failed, 713 tauts, 0 hbrs, 13398 literals
c [transred-4] limit 1981147 with penalty 0 = 0 + 0
c [transred-4] removed 107 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 623 (0%) of length 14
c [cce-5-1] eliminated 28 clauses out of 739 (4%) of length 13
c [cce-5-1] eliminated 18 clauses out of 1213 (1%) of length 12
c [cce-5-1] eliminated 8 clauses out of 1961 (0%) of length 11
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 55 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 78616 clauses = 22605 binary + 56011 ternary
c [cce-5] tried to eliminate 13207 small clauses 17%
c [cce-5] eliminated 161 small clauses 0%
c [cce-5] eliminated 16 binary clauses 0%
c [cce-5] eliminated 145 ternary clauses 0%
c [cce-5-1] eliminated 161 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 216 covered clauses in round 1
c [cce-5] eliminated 216 covered clauses in TOTAL during 1 rounds
c [bca-5] limit of 10000000 steps
c [bca-5] 41882 out of 52916 literals actually usable 79%
c [bca-5] added 11 blocked clauses in 148667 steps
c [rephase-2] after 65813 conflicts (new increment 40000, next 105813)
c [flushphases] 476 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 39 variables 0.1% (26457 remain 10%)
c [simplification-6] removed 716 irredundant clauses 0.4% (195504 remain 25%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 36000
c [simplification-6] new conflict interval 72000
c [simplification-6] penalized conflict interval 72000 = 1 * 72000
c [simplification-6] new conflict limit 137813
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   46.7   26457   195504     66711   13415   9923  2536   9  9.2 196.1   35
c -   48.2   26457   195504     77492   15189  10211  2547   8  9.2 192.2   35
c -   49.5   26457   195504     88478   16925  10548  2555  11  9.3 189.0   35
c -   51.1   26457   195504    100486   19049  10892  2570  10  9.3 183.9   35
c -   52.3   26457   195504    111792   20461  11102  2575  12  9.5 185.1   35
c -   53.3   26457   195504    124240   21928  11187  2576  16 12.7 183.7   35
c R   53.4   26457   195504    125089   22625  11195  2576  16 12.8 183.6   36
c i   54.3   26456   195504    130941   27370  11310  2582   9 12.6 181.7   37
c -   55.2   26455   195504    137634   23731  11465  2589   9 12.7 178.4   36
c 
c [simplification-7] limit of 137911 conflicts hit after 137912 conflicts
c [ternres-5] limit 4351127 with penalty 0 = 0 + 0
c [ternres-5] all 26455 free variables schedulable
c [ternres-5] 455 ternary resolvents (27 bin, 428 trn)
c [ternres-5] 11640 variables remain 44% (14815 retained)
c [decomp-14] removed 9 variables
c [basicprobe-3] limit 4351127 penalty 0 = 0 + 0
c [basicprobe-3-0] 13797 sched 52%, 2 failed, 0 lifted, 234 hbrs
c [decomp-15] removed 4 variables
c [basicprobe-3-1] 14338 sched 54%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-3-2] 4580 probes remain 17% after last round
c [basicprobe-3-2] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 4 variables, found 242 hbrs
c [bate-2] eliminated 53 asymmetric tautologies during probing
c [cgrclsr-4] limit 217556 penalty 1 = 1 + 0
c [cgrclsr-4] all 26444 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-5] limit 2610676 with penalty 0 = 0 + 0
c [lift-5] using 17157 probes 65%
c [lift-5] 0 units, 17 impls, 3 eqs in 1 rounds
c [lift-5] 18513 variables remain 70% (7928 retained)
c [lift-5] removed 3 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 0, lifted 0
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 125 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 26441 variables 100%
c [block-5] limit of 25000000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 255 blocked clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 710 (0%) of length 13
c [cce-6-1] eliminated 2 clauses out of 1191 (0%) of length 12
c [cce-6-1] eliminated 2 clauses out of 1951 (0%) of length 11
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 5 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 39494 clauses = 22520 binary + 16974 ternary
c [cce-6] tried to eliminate 14735 small clauses 37%
c [cce-6] eliminated 70 small clauses 0%
c [cce-6] eliminated 27 binary clauses 0%
c [cce-6] eliminated 43 ternary clauses 0%
c [cce-6-1] eliminated 70 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 75 covered clauses in round 1
c [cce-6] eliminated 75 covered clauses in TOTAL during 1 rounds
c [cce-6] 75 < 1/1000 * 195083 = 195 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 26406 variables 100%
c [elim-6] limit of 43511277 steps penalty 1 = 1 + 0
c [elim-6] incomplete 1485 not tried 6% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 263 = 1% variables out of 26406
c [bca-6] limit of 10000000 steps
c [bca-6] 40631 out of 52288 literals actually usable 78%
c [bca-6] added 9 blocked clauses in 150488 steps
c [rephase-3] after 137912 conflicts (new increment 80000, next 217912)
c [flushphases] 301 phases reset
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 312 variables 1.2% (26143 remain 10%)
c [simplification-7] removed 1025 irredundant clauses 0.5% (194479 remain 25%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 36000 = 72000 / 2
c [simplification-7] new conflict interval 108000
c [simplification-7] penalized conflict interval 108000 = 1 * 108000
c [simplification-7] new conflict limit 245912
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   61.7   26143   194478    152474   25652  11665  2568   8 12.3 175.6   36
c i   63.1   26142   194478    161766   33101  11893  2572  10 12.1 175.6   37
c -   63.8   26140   194478    167100   27691  11989  2575  10 12.0 173.9   36
c -   65.4   26140   194478    181969   29569  12230  2584  14 12.2 172.0   36
c i   65.6   26139   194478    183390   30723  12270  2585   9 12.2 171.8   36
c -   67.9   26136   194478    198270   31878  12612  2594   9 11.9 168.4   36
c -   70.7   26136   194478    214956   34246  12906  2617  10 11.8 170.3   36
c -   73.4   26136   194478    232392   36718  13237  2623  13 11.6 168.9   36
c 
c [simplification-8] limit of 246076 conflicts hit after 246076 conflicts
c [ternres-6] limit 8426201 with penalty 0 = 0 + 0
c [ternres-6] 11514 schedulable variables 44%
c [ternres-6] 1882 ternary resolvents (58 bin, 1824 trn)
c [ternres-6] 3 variables remain 0% (26133 retained)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 4266 xors of average arity 3.0
c [gauss-3] connected 12794 occurrences of 3304 variables (average 3.9)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 12 variables
c [simpleprobe-4] 9217 schedulable variables 35%
c [simpleprobe-4] limit 33704807 penalty 0 = 0 + 0
c [decomp-18] removed 26 variables
c [simpleprobe-4] 181 variables remain 1% (25917 retained)
c [simpleprobe-4] removed 26 variables, found 494 hbrs, 0 units
c [lift-6] limit 5055721 with penalty 0 = 0 + 0
c [lift-6] using 13535 probes 52%
c [lift-6] 9 units, 20 impls, 8 eqs in 1 rounds
c [lift-6] 13195 variables remain 51% (12883 retained)
c [lift-6] removed 20 variables
c [unhide-7] limit 842620 with penalty 1 = 1 + 0
c [unhide-7-7] 0 units, 0 failed, 350 tauts, 0 hbrs, 36839 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 300 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 26078 variables 100%
c [block-6] limit of 84262019 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 256 blocked clauses
c [elim-7] 1347 variables 5% will be scheduled this time
c [elim-7] scheduled 1347 variables 5%
c [elim-7] limit of 168524038 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 56 variables 0% in round 1 in 118921637 steps
c [elim-7-1] backward subsumption/strengthening limit 49602401
c [elim-7-1] subsumed 47 and strengthened 1632 clauses in 25563738 steps
c [elim-7-1] rescheduled 959 variables 4% by backward subsumption
c [elim-7-2] eliminated 15 variables 0% in round 2 in 23374612 steps
c [elim-7-2] backward subsumption/strengthening limit 664051
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 664134 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 71 = 0% variables out of 26047
c [bca-7] limit of 10000000 steps
c [bca-7] 37495 out of 51954 literals actually usable 72%
c [bca-7] added 15 blocked clauses in 165845 steps
c [rephase-4] after 246076 conflicts (new increment 160000, next 406076)
c [flushphases] 183 phases reset
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 160 variables 0.6% (25976 remain 10%)
c [simplification-8] removed 1540 irredundant clauses 0.8% (192938 remain 24%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 54000 = 108000 / 2
c [simplification-8] new conflict interval 162000
c [simplification-8] penalized conflict interval 162000 = 1 * 162000
c [simplification-8] new conflict limit 408076
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   78.8   25976   192938    248730   37809  14522  2873  18 11.8 167.9   38
c -   80.4   25976   192938    266971   39824  14723  2873  13 13.1 170.6   38
c R   80.8   25976   192938    270585   43000  14758  2873  12 13.2 170.8   39
c i   82.2   25975   192938    279333   50306  14879  2881   9 13.0 169.4   40
c i   82.2   25946   192938    279334   50306  14879  2881   9 13.0 169.4   40
c i   82.9   25875   192938    284160   53943  15067  2902   7 12.9 168.9   40
c -   83.5   25875   192938    286638   42470  15156  2914  12 12.9 169.1   38
c i   83.6   25874   192938    287858   43451  15190  2917   9 12.9 169.0   38
c i   85.1   25873   192938    298375   52253  15425  2959   9 12.8 169.3   40
c i   85.4   25869   192938    299600   53186  15459  2965   8 12.8 169.7   40
c i   85.6   25856   192938    300734   54044  15513  2971   7 12.7 169.3   40
c i   86.1   25855   192938    303726   56306  15611  2990  10 12.7 169.0   40
c i   86.6   25844   192938    305954   58031  15673  2998   7 12.7 168.7   40
c i   86.7   25840   192938    306828   58747  15702  2999   9 12.7 168.8   40
c -   86.8   25833   192938    307687   45474  15714  3000  12 12.7 168.8   38
c i   88.3   25832   192938    316280   52084  15983  3047   9 12.5 170.7   39
c -   89.9   25829   192938    330383   48381  16179  3076   9 12.5 172.2   38
c -   94.2   25829   192937    353259   52128  16775  3144  13 12.2 175.2   38
c i   95.5   25828   192937    360482   58173  16933  3170  10 12.1 174.9   39
c i   95.5   25805   192937    360574   58251  16936  3170  11 12.1 174.9   39
c -   99.1   25801   192937    376695   55780  17375  3235  10 12.0 176.8   50
c i  100.1   25800   192937    395788   71595  17489  3242   8 11.9 178.0   54
c -  100.9   25795   192937    398908   58085  17567  3256  11 11.9 178.2   39
c 
c [simplification-9] limit of 408812 conflicts hit after 408812 conflicts
c [ternres-7] limit 15200636 with penalty 0 = 0 + 0
c [ternres-7] 2 schedulable variables 0%
c [ternres-7] 1901 ternary resolvents (34 bin, 1867 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-19] removed 676 variables
c [lift-7] limit 9120381 with penalty 0 = 0 + 0
c [lift-7] using 8314 probes 33%
c [lift-7] 48 units, 50 impls, 64 eqs in 1 rounds
c [lift-7] 7089 variables remain 28% (18088 retained)
c [lift-7] removed 123 variables
c [cliff-6] limit of 6080254 steps penalty 1 = 1 + 0
c [cliff-6] failed 1, lifted 0
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 460 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 25176 variables 100%
c [block-7] limit of 152006361 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 6531 blocked clauses
c [cce-7] limit of 15200636 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 11 clauses out of 47 (23%) of length 22
c [cce-7-1] eliminated 35 clauses out of 79 (44%) of length 21
c [cce-7-1] eliminated 51 clauses out of 207 (25%) of length 20
c [cce-7-1] eliminated 65 clauses out of 237 (27%) of length 19
c [cce-7-1] eliminated 83 clauses out of 336 (25%) of length 18
c [cce-7-1] eliminated 100 clauses out of 381 (26%) of length 17
c [cce-7-1] eliminated 115 clauses out of 427 (27%) of length 16
c [cce-7-1] eliminated 119 clauses out of 515 (23%) of length 15
c [cce-7-1] eliminated 101 clauses out of 551 (18%) of length 14
c [cce-7-1] eliminated 66 clauses out of 612 (11%) of length 13
c [cce-7-1] eliminated 52 clauses out of 1026 (5%) of length 12
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 798 large clauses in 15200646 steps
c [cce-7-1] allowing another 7600323 steps for small clauses
c [cce-7] scheduling 73902 clauses = 20923 binary + 52979 ternary
c [cce-7] tried to eliminate 6245 small clauses 8%
c [cce-7] eliminated 232 small clauses 0%
c [cce-7] eliminated 97 binary clauses 0%
c [cce-7] eliminated 135 ternary clauses 0%
c [cce-7-1] eliminated 232 small clauses in 15200637 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1030 covered clauses in round 1
c [cce-7] eliminated 1030 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 24460 variables 100%
c [elim-8] limit of 304012723 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 1951 variables 8% in round 1 in 229116972 steps
c [elim-8-1] backward subsumption/strengthening limit 74895751
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 14662949 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1954 = 8% variables out of 24460
c [bca-8] limit of 10000000 steps
c [bca-8] 28757 out of 45014 literals actually usable 64%
c [bca-8] added 154 blocked clauses in 140652 steps
c [rephase-5] after 408812 conflicts (new increment 320000, next 728812)
c [flushphases] 109 phases reset
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 3289 variables 12.8% (22506 remain 8%)
c [simplification-9] removed 25683 irredundant clauses 13.3% (167254 remain 21%)
c [simplification-9] maximum reduction of 13% = max (13%, 13%)
c [simplification-9] large reduction 13% >= 5% limit
c [simplification-9] new conflict interval 4088 = min (408812/100, 162000)
c [simplification-9] penalized conflict interval 4088 = 1 * 4088
c [simplification-9] new conflict limit 412900
c 
c [simplification-10] limit of 412914 conflicts hit after 412915 conflicts
c [ternres-8] limit 15442096 with penalty 0 = 0 + 0
c [ternres-8] all 22506 free variables schedulable
c [ternres-8] 6176 ternary resolvents (666 bin, 5510 trn)
c [ternres-8] 10 variables remain 0% (22496 retained)
c [card-4] limit 965131 penalty 3 = 3 + 0
c [card-4] found 209 at-most-one constraints of average size 3.2
c [card-4] found 179 at-most-two constraints of average size 4.0
c [card-4] using previous limit 965131 for elimination
c [card-4] 386 out of 388 constraints (99%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-20] removed 85 variables
c [treelook-4] limit 386052 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 15232 literals 34%
c [treelook-4] scheduling used 386066 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 386052 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 388246 steps
c [treelook-4] 14781 literals remain 33%
c [treelook-4] 6494 variables remain to probed next time 29%
c [treelook-4] removed 4 variables, found 147 hbrs
c [cgrclsr-5] limit 386052 penalty 2 = 2 + 0
c [cgrclsr-5] all 22417 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [cgrclsr-5] removed 7 variables
c [lift-8] limit 9265258 with penalty 0 = 0 + 0
c [lift-8] using 2288 probes 10%
c [lift-8-1] found 21 units 13 impls in round 1
c [lift-8-2] found 1 units 12 impls in round 2
c [lift-8-3] found 1 units 16 impls in round 3
c [lift-8] 23 units, 42 impls, 17 eqs in 4 rounds
c [lift-8] 4017 variables remain 18% (18349 retained)
c [lift-8] removed 44 variables
c [cliff-7] limit of 12353677 steps penalty 0 = 0 + 0
c [cliff-7] failed 9, lifted 4
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 395 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 22348 variables 100%
c [block-8] limit of 154420968 steps penalty 0 = 0 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 271 blocked clauses
c [cce-8] limit of 30884193 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 40 (2%) of length 22
c [cce-8-1] eliminated 1 clauses out of 46 (2%) of length 21
c [cce-8-1] eliminated 1 clauses out of 178 (1%) of length 19
c [cce-8-1] eliminated 4 clauses out of 260 (2%) of length 18
c [cce-8-1] eliminated 5 clauses out of 296 (2%) of length 17
c [cce-8-1] eliminated 5 clauses out of 324 (2%) of length 16
c [cce-8-1] eliminated 16 clauses out of 413 (4%) of length 15
c [cce-8-1] eliminated 24 clauses out of 472 (5%) of length 14
c [cce-8-1] eliminated 52 clauses out of 610 (9%) of length 13
c [cce-8-1] eliminated 58 clauses out of 989 (6%) of length 12
c [cce-8-1] eliminated 87 clauses out of 1602 (5%) of length 11
c [cce-8-1] eliminated 131 clauses out of 2493 (5%) of length 10
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 385 large clauses in 30884194 steps
c [cce-8-1] allowing another 15442097 steps for small clauses
c [cce-8] scheduling 66218 clauses = 18946 binary + 47272 ternary
c [cce-8] tried to eliminate 15511 small clauses 23%
c [cce-8] eliminated 380 small clauses 1%
c [cce-8] eliminated 73 binary clauses 0%
c [cce-8] eliminated 307 ternary clauses 1%
c [cce-8-1] eliminated 380 small clauses in 30884194 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 765 covered clauses in round 1
c [cce-8] eliminated 765 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 22305 variables 100%
c [elim-9] limit of 308841936 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 122 variables 1% in round 1 in 118036934 steps
c [elim-9-1] backward subsumption/strengthening limit 190805002
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 14236962 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 122 = 1% variables out of 22305
c [bca-9] limit of 10000000 steps
c [bca-9] 27800 out of 44368 literals actually usable 63%
c [bca-9] added 81 blocked clauses in 139640 steps
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 323 variables 1.4% (22183 remain 8%)
c [simplification-10] removed 2627 irredundant clauses 1.6% (164627 remain 21%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 54000 = 162000 / 3
c [simplification-10] new conflict interval 216000
c [simplification-10] penalized conflict interval 216000 = 1 * 216000
c [simplification-10] new conflict limit 628915
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  118.6   22183   164627    432540   49736  18803  4064  10 11.7 180.8   38
c i  119.7   22182   164627    438147   54368  18944  4076   7 11.7 181.0   38
c -  122.6   22182   164627    457525   52928  19316  4104  11 11.6 181.8   37
c i  122.9   22181   164627    458958   54084  19340  4107   9 11.6 182.5   38
c i  123.5   22173   164627    461864   56426  19417  4117   9 11.6 182.5   38
c i  123.6   22171   164627    462037   56553  19421  4118  10 11.6 182.4   38
c i  123.6   22170   164627    462038   56553  19421  4118  10 11.6 182.4   38
c i  125.8   22166   164627    472986   65352  19761  4151  10 11.5 182.3   39
c i  127.1   22165   164627    481476   72134  19997  4166   9 11.4 182.4   39
c -  127.7   22164   164627    484316   57068  20065  4171  10 11.4 182.0   37
c i  127.8   22163   164627    484828   57475  20080  4171   9 11.4 181.9   38
c i  128.7   22162   164627    488271   60215  20176  4186   8 11.4 182.3   38
c i  130.6   22160   164627    497552   67965  20407  4212   8 11.3 183.1   39
c i  131.0   22158   164627    499757   69738  20472  4221   9 11.3 182.9   39
c -  131.9   22158   164627    510165   60695  20578  4229  15 11.3 183.8   49
c -  134.4   22158   164627    535139   63843  20891  4250  12 11.3 185.7   38
c -  135.9   22158   164627    561586   66777  21059  4266  13 11.4 186.6   39
c R  137.0   22158   164627    581995   84865  21120  4267  18 11.5 186.4   44
c -  138.0   22158   164627    585667   68280  21218  4275   8 11.5 186.1   39
c i  139.7   22157   164627    593922   75098  21354  4282  11 11.4 186.4   40
c -  144.1   22157   164627    613885   71804  21757  4327   9 11.4 186.2   39
c 
c [simplification-11] limit of 629519 conflicts hit after 629521 conflicts
c [ternres-9] limit 24818815 with penalty 0 = 0 + 0
c [ternres-9] 10 schedulable variables 0%
c [ternres-9] 2910 ternary resolvents (71 bin, 2839 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-22] removed 168 variables
c [basicprobe-4] limit 24818815 penalty 0 = 0 + 0
c [basicprobe-4-0] 3850 sched 17%, 7 failed, 4 lifted, 396 hbrs
c [decomp-23] removed 27 variables
c [basicprobe-4-1] 11515 sched 52%, 15 failed, 0 lifted, 705 hbrs
c [decomp-24] removed 36 variables
c [basicprobe-4-2] 11506 sched 52%, 1 failed, 0 lifted, 74 hbrs
c [decomp-25] removed 3 variables
c [basicprobe-4-3] 11498 sched 52%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-4-4] 11498 sched 52%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-5] 11498 sched 52%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 11498 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 27 units = 23 failed (85%) + 4 lifted (15%)
c [basicprobe-4-6] removed 66 variables, found 1190 hbrs
c [bate-3] eliminated 161 asymmetric tautologies during probing
c [lift-9] limit 14891289 with penalty 0 = 0 + 0
c [lift-9] using 98 probes 0%
c [lift-9-1] found 0 units 8 impls in round 1
c [lift-9-2] found 0 units 4 impls in round 2
c [lift-9-3] found 0 units 2 impls in round 3
c [lift-9-4] found 0 units 2 impls in round 4
c [lift-9-5] found 0 units 1 impls in round 5
c [lift-9] 0 units, 17 impls, 5 eqs in 6 rounds
c [lift-9] 3875 variables remain 18% (18069 retained)
c [lift-9] removed 5 variables
c [cliff-8] limit of 19855052 steps penalty 0 = 0 + 0
c [cliff-8] failed 0, lifted 0
c [unhide-8] limit 1240940 with penalty 2 = 2 + 0
c [unhide-8-8] 0 units, 0 failed, 4980 tauts, 0 hbrs, 35483 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 356 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 21944 variables 100%
c [block-9] limit of 248188153 steps penalty 0 = 0 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 756 blocked clauses
c [cce-9] limit of 49637630 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 5 clauses out of 15 (33%) of length 24
c [cce-9-1] eliminated 8 clauses out of 25 (32%) of length 23
c [cce-9-1] eliminated 8 clauses out of 35 (23%) of length 22
c [cce-9-1] eliminated 2 clauses out of 47 (4%) of length 21
c [cce-9-1] eliminated 3 clauses out of 142 (2%) of length 20
c [cce-9-1] eliminated 9 clauses out of 172 (5%) of length 19
c [cce-9-1] eliminated 14 clauses out of 216 (6%) of length 18
c [cce-9-1] eliminated 15 clauses out of 251 (6%) of length 17
c [cce-9-1] eliminated 21 clauses out of 276 (8%) of length 16
c [cce-9-1] eliminated 82 clauses out of 391 (21%) of length 15
c [cce-9-1] eliminated 46 clauses out of 407 (11%) of length 14
c [cce-9-1] eliminated 34 clauses out of 515 (7%) of length 13
c [cce-9-1] eliminated 83 clauses out of 921 (9%) of length 12
c [cce-9-1] eliminated 52 clauses out of 1485 (4%) of length 11
c [cce-9-1] eliminated 244 clauses out of 2208 (11%) of length 10
c [cce-9-1] eliminated 559 clauses out of 3907 (14%) of length 9
c [cce-9-1] eliminated 259 clauses out of 5765 (4%) of length 8
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 1444 large clauses in 49637631 steps
c [cce-9-1] allowing another 24818815 steps for small clauses
c [cce-9] scheduling 64735 clauses = 18551 binary + 46184 ternary
c [cce-9] tried to eliminate 22968 small clauses 35%
c [cce-9] eliminated 809 small clauses 1%
c [cce-9] eliminated 195 binary clauses 1%
c [cce-9] eliminated 614 ternary clauses 1%
c [cce-9-1] eliminated 809 small clauses in 49637631 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2253 covered clauses in round 1
c [cce-9] eliminated 2253 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 21884 variables 100%
c [elim-10] limit of 496376307 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 817 variables 4% in round 1 in 129873726 steps
c [elim-10-1] backward subsumption/strengthening limit 259747452
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 13268012 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 817 = 4% variables out of 21884
c [bca-10] limit of 10000000 steps
c [bca-10] 23651 out of 42136 literals actually usable 56%
c [bca-10] added 193 blocked clauses in 155218 steps
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-11] removed 1090 variables 4.9% (21067 remain 8%)
c [simplification-11] removed 9550 irredundant clauses 5.8% (155077 remain 20%)
c [simplification-11] maximum reduction of 6% = max (5%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] new conflict interval 6295 = min (629521/100, 216000)
c [simplification-11] penalized conflict interval 6295 = 1 * 6295
c [simplification-11] new conflict limit 635816
c 
c [simplification-12] limit of 635818 conflicts hit after 635818 conflicts
c [ternres-10] limit 25013452 with penalty 0 = 0 + 0
c [ternres-10] all 21067 free variables schedulable
c [ternres-10] 4480 ternary resolvents (357 bin, 4123 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 625336 penalty 3 = 3 + 0
c [gauss-4] extracted 3559 xors of average arity 3.0
c [gauss-4] connected 10653 occurrences of 2739 variables (average 3.9)
c [gauss-4] limit 625336 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-29] removed 40 variables
c [simpleprobe-5] 107 schedulable variables 1%
c [simpleprobe-5] limit 100053808 penalty 0 = 0 + 0
c [decomp-30] removed 13 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 13 variables, found 2004 hbrs, 4 units
c [cgrclsr-6] limit 1250672 penalty 1 = 1 + 0
c [cgrclsr-6] all 21014 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 3 variables
c [lift-10] limit 15008071 with penalty 0 = 0 + 0
c [lift-10] using 53 probes 0%
c [lift-10-1] found 0 units 1 impls in round 1
c [lift-10-2] found 0 units 1 impls in round 2
c [lift-10-3] found 5 units 1 impls in round 3
c [lift-10-4] found 0 units 1 impls in round 4
c [lift-10-5] found 0 units 1 impls in round 5
c [lift-10] 5 units, 5 impls, 0 eqs in 6 rounds
c [lift-10] 3622 variables remain 17% (17384 retained)
c [lift-10] removed 5 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 744 transitive binary clauses
c [transred-10] found 2 units
c [block-10] scheduling all variables this time
c [block-10] scheduled 21004 variables 100%
c [block-10] limit of 250134520 steps penalty 0 = 0 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 15 blocked clauses
c [block-10] 15 < 1/1000 * 154893 = 154 considered unsuccessful
c [cce-10] limit of 50026904 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 26
c [cce-10-1] eliminated 3 clauses out of 153 (2%) of length 20
c [cce-10-1] eliminated 1 clauses out of 181 (1%) of length 19
c [cce-10-1] eliminated 3 clauses out of 228 (1%) of length 18
c [cce-10-1] eliminated 2 clauses out of 268 (1%) of length 17
c [cce-10-1] eliminated 2 clauses out of 279 (1%) of length 16
c [cce-10-1] eliminated 5 clauses out of 327 (2%) of length 15
c [cce-10-1] eliminated 13 clauses out of 396 (3%) of length 14
c [cce-10-1] eliminated 13 clauses out of 516 (3%) of length 13
c [cce-10-1] eliminated 23 clauses out of 884 (3%) of length 12
c [cce-10-1] eliminated 31 clauses out of 1500 (2%) of length 11
c [cce-10-1] eliminated 68 clauses out of 2117 (3%) of length 10
c [cce-10-1] eliminated 98 clauses out of 3443 (3%) of length 9
c [cce-10-1] eliminated 94 clauses out of 5408 (2%) of length 8
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 357 large clauses in 50026905 steps
c [cce-10-1] allowing another 25013452 steps for small clauses
c [cce-10] scheduling 61136 clauses = 17585 binary + 43551 ternary
c [cce-10] tried to eliminate 24909 small clauses 41%
c [cce-10] eliminated 537 small clauses 1%
c [cce-10] eliminated 93 binary clauses 1%
c [cce-10] eliminated 444 ternary clauses 1%
c [cce-10-1] eliminated 537 small clauses in 50026905 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 894 covered clauses in round 1
c [cce-10] eliminated 894 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 21003 variables 100%
c [elim-11] limit of 500269041 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 126 variables 1% in round 1 in 95338004 steps
c [elim-11-1] backward subsumption/strengthening limit 190676008
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 13000331 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 126 = 1% variables out of 21003
c [bca-11] limit of 10000000 steps
c [bca-11] 23085 out of 41756 literals actually usable 55%
c [bca-11] added 50 blocked clauses in 157720 steps
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-12] removed 190 variables 0.9% (20877 remain 8%)
c [simplification-12] removed 1787 irredundant clauses 1.2% (153290 remain 19%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 108000 = 216000 / 2
c [simplification-12] new conflict interval 324000
c [simplification-12] penalized conflict interval 324000 = 1 * 324000
c [simplification-12] new conflict limit 959818
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  164.0   20877   153290    645794   70227  24516  5671   9 11.3 185.3   40
c -  170.4   20877   153290    675558   74189  25145  5709   9 11.2 183.9   40
c -  174.4   20877   153290    705128   77729  25585  5732  15 11.2 183.9   40
c -  180.8   20877   153290    735311   81443  26174  5768  10 11.1 182.1   40
c -  186.8   20877   153290    765677   84833  26652  5791   8 11.1 181.1   53
c i  191.0   20876   153290    782132   98713  26978  5815   5 11.1 180.4   55
c -  194.4   20872   153290    797356   88825  27258  5835  12 11.1 179.7   53
c -  199.7   20872   153290    829139   92281  27656  5856  20 11.1 179.2   53
c -  204.4   20872   153290    860063   95317  28004  5872  12 11.0 178.6   41
c -  212.3   20872   153290    892941   99219  28481  5911  11 11.0 176.9   41
c i  213.1   20871   153290    896163  101925  28521  5911   9 11.0 176.8   43
c -  220.1   20871   153290    925646  102712  28931  5937  11 10.9 175.4   41
c i  223.1   20870   153290    938571  113846  29096  5944  12 10.9 175.0   58
c i  224.3   20869   153290    942619  117346  29170  5946   9 10.9 174.7   58
c i  227.4   20868   153290    953780  127235  29307  5955   8 10.9 174.1   59
c -  228.8   20868   153290    959095  106503  29377  5959  15 10.9 173.8   55
c 
c [simplification-13] limit of 960312 conflicts hit after 960312 conflicts
c [ternres-11] limit 44619593 with penalty 0 = 0 + 0
c [ternres-11] all 20868 free variables schedulable
c [ternres-11] 5474 ternary resolvents (149 bin, 5325 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-31] removed 84 variables
c [treelook-5] limit 2230979 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 18900 literals 45%
c [treelook-5] scheduling used 689082 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2230979 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2261159 steps
c [treelook-5] 18178 literals remain 44%
c [treelook-5] 5970 variables remain to probed next time 29%
c [decomp-32] removed 9 variables
c [treelook-5] removed 15 variables, found 820 hbrs
c [cgrclsr-7] limit 4461959 penalty 0 = 0 + 0
c [cgrclsr-7] all 20778 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [cgrclsr-7] removed 16 variables
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 90 probes 0%
c [lift-11-1] found 0 units 4 impls in round 1
c [lift-11-2] found 0 units 2 impls in round 2
c [lift-11-3] found 1 units 1 impls in round 3
c [lift-11-4] found 0 units 2 impls in round 4
c [lift-11-5] found 1 units 3 impls in round 5
c [lift-11] 2 units, 12 impls, 3 eqs in 6 rounds
c [lift-11] 3488 variables remain 17% (17269 retained)
c [lift-11] removed 5 variables
c [cliff-9] limit of 17847837 steps penalty 1 = 1 + 0
c [cliff-9] failed 5, lifted 1
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 787 transitive binary clauses
c [cce-11] limit of 89239187 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 27
c [cce-11-1] eliminated 1 clauses out of 18 (6%) of length 24
c [cce-11-1] eliminated 5 clauses out of 43 (12%) of length 22
c [cce-11-1] eliminated 9 clauses out of 60 (15%) of length 21
c [cce-11-1] eliminated 4 clauses out of 154 (3%) of length 20
c [cce-11-1] eliminated 20 clauses out of 181 (11%) of length 19
c [cce-11-1] eliminated 15 clauses out of 237 (6%) of length 18
c [cce-11-1] eliminated 30 clauses out of 251 (12%) of length 17
c [cce-11-1] eliminated 23 clauses out of 284 (8%) of length 16
c [cce-11-1] eliminated 12 clauses out of 318 (4%) of length 15
c [cce-11-1] eliminated 12 clauses out of 383 (3%) of length 14
c [cce-11-1] eliminated 16 clauses out of 517 (3%) of length 13
c [cce-11-1] eliminated 24 clauses out of 875 (3%) of length 12
c [cce-11-1] eliminated 26 clauses out of 1464 (2%) of length 11
c [cce-11-1] eliminated 53 clauses out of 2079 (3%) of length 10
c [cce-11-1] eliminated 61 clauses out of 3354 (2%) of length 9
c [cce-11-1] eliminated 312 clauses out of 5272 (6%) of length 8
c [cce-11-1] eliminated 553 clauses out of 10472 (5%) of length 7
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 1178 large clauses in 89239188 steps
c [cce-11-1] allowing another 44619594 steps for small clauses
c [cce-11] scheduling 60082 clauses = 17277 binary + 42805 ternary
c [cce-11] tried to eliminate 41077 small clauses 68%
c [cce-11] eliminated 841 small clauses 1%
c [cce-11] eliminated 168 binary clauses 1%
c [cce-11] eliminated 673 ternary clauses 2%
c [cce-11-1] eliminated 982 small clauses in 89239188 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 2160 covered clauses in round 1
c [cce-11] eliminated 2160 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 20743 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 476 variables 2% in round 1 in 104674941 steps
c [elim-12-1] backward subsumption/strengthening limit 209349882
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 12531574 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 476 = 2% variables out of 20743
c [bca-12] limit of 10000000 steps
c [bca-12] 21617 out of 40536 literals actually usable 53%
c [bca-12] added 114 blocked clauses in 173721 steps
c [rephase-6] after 960312 conflicts (new increment 640000, next 1600312)
c [flushphases] 87 phases reset
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-13] removed 601 variables 2.9% (20267 remain 8%)
c [simplification-13] removed 4863 irredundant clauses 3.2% (148427 remain 19%)
c [simplification-13] maximum reduction of 3% = max (3%, 3%)
c [simplification-13] geometric conflict interval increment 81000 = 324000 / 4
c [simplification-13] new conflict interval 405000
c [simplification-13] penalized conflict interval 405000 = 1 * 405000
c [simplification-13] new conflict limit 1365312
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  242.8   20267   148427    993601  105126  32715  6317  10 10.9 172.4   43
c i  249.8   20266   148427   1021944  129895  32996  6341  12 10.9 171.2   48
c -  251.2   20265   148427   1027647  108445  33062  6346  12 10.8 170.9   43
c i  254.4   20264   148427   1044486  122952  33224  6359   8 10.9 170.5   47
c i  254.5   20085   148427   1044886  123228  33244  6364  11 10.9 170.4   47
c i  255.1   20079   148427   1047717  125666  33285  6373   7 10.9 170.4   48
c i  256.5   20072   148427   1053229  130422  33383  6386   9 10.9 170.1   48
c i  257.5   20068   148427   1056310  133082  33433  6392   9 10.9 169.8   49
c -  258.8   20066   148427   1062595  111685  33508  6404  12 10.9 169.6   43
c i  259.7   20065   148427   1065487  114141  33559  6413   9 10.9 169.5   59
c i  261.8   20061   148427   1074374  121958  33673  6428  11 10.9 169.1   60
c i  262.6   20060   148427   1077312  124558  33711  6434  12 10.9 168.9   60
c i  263.1   20056   148427   1079615  126590  33745  6442  10 10.9 168.8   61
c i  263.1   20055   148427   1079672  126629  33749  6445  10 10.9 168.8   61
c i  263.5   20045   148427   1080924  127688  33765  6449  11 10.9 168.9   61
c i  263.6   20038   148427   1081260  127888  33774  6450  11 10.9 168.8   61
c i  263.6   19813   148427   1081331  127941  33777  6450  10 10.9 168.8   61
c i  263.6   19790   148427   1081403  127983  33783  6452  12 10.9 168.8   61
c i  263.6   19695   148427   1081430  127992  33789  6456  12 10.9 168.8   61
c i  263.6   19127   148427   1081431  127992  33789  6456  12 10.9 168.8   61
c i  263.6   19123   148427   1081432  127992  33789  6456  12 10.9 168.8   61
c 0  263.6   19080   148427   1081432  127992  33789  6456  12 10.9 168.8   61
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 369 basic ate = 41 trn 11% + 328 lrg 89% in 3 updates
c bcas: 12 count, 1093 added (176 skipped), 1863723 steps
c bkwd: tried 1185802 clauses, 2370033 lits, 2.00 lits/clause
c bkwd: checked 125414653 occs, 105.76 occs/clause, 52.92 occs/lit
c bkwd: subsumed 9 binary, 5 ternary, 728 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 2902 large (0% self)
c blkd: 10 bces, 18626 removed, 13505229 resolutions, 34796630 steps
c blkd: 9338 blocking literals 2%, 1724 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 7438070 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1870 subsumed
c card: 532 at-most-one constraints found, average size 3.26
c card: 532 at-most-one constraints used 100%, average size 3.26
c card: 293 at-most-two constraints found, average size 4.03
c card: 291 at-most-two constraints used 99%, average size 4.03
c cces: 11 cces, 27279 eliminated, 24280 ate 89%, 2999 abce 11%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 7 count, 6916525 esteps, 366143 csteps
c cgrs: 12 eqs, 2 units
c cgrs: 7 matched (5 ands 71%, 2 xors 29%, 0 ites 0%)
c cgrs: 1 simplified (0 ands 0%, 1 xors 100%, 0 ites 0%)
c cgrs: 12820 extracted (2348 ands 18%, 9631 xors 75%, 841 ites 7%)
c clff: 9 cliffs, 81 lifted, 125 failed
c clff: 1599438 decisions, 106141614 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2640582 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 114 gcs, 0 rescored clauses, 539 rescored vars
c dcps: 32 decompositions, 5761 equivalent 2%
c deco: 9348 decision-only clauses 1%, 55% reduction
c decs: 11583656 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 364393 flipped 3.146% (in 2214 phases)
c elms: 12 elims, 233231 eliminated 88%
c elms: 21 rounds, 1.8 rounds/bve
c elms: 216520 small 93%, 14987 large 6%
c elms: 304514 tried small, 216520 succeeded 71%, 87994 failed 29%
c elms: 9158 subsumed, 7088 strengthened, 7544 blocked
c elms: 10805596 copies, 19130701 resolutions, 6191625 ipos
c elms: 8003351 subchks, 7358125 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 35395 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 8256936 steps, 4128468 extr 50%, 4165211 elim 50%
c glue: 10.9 orig avg, 10.6 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 14204 = 3540 simple + 9865 trn 25% + 799 lrg 69%, 1758 sub 6%
c hght: 169 average, 15.55 height/glue
c ints: 32677 luby (8530796 steps), 0 inout (0 steps)
c lift: 11 phases, 162505 probed (54227 level1 33%, 108278 level2 67%)
c lift: 141 units, 112 equivalences, 207 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1024626 clauses, 23.9 length
c lrnd: 336006 uips 33%, 441739 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 24505374 learned lits, 19% minimized
c mins: 973979 mins 95%, 515 bin 0%, 40784 size 4%, 9348 deco 1%
c move: moved 1024626, 5618 bin 1%, 12578 trn 1%, 0 lrg 0%
c otfs: str 113516 dyn (113115 red, 401 irr) 56806 drv 50%, 56710 rst 50%
c otfs: sub 1952 dyn (1947 red, 5 irr)
c phas: 14 computed, 37672 set, 11814 pos (31%), 25858 neg (69%)
c prbs: 4 basic, 255830 probed, 250 failed, 31 lifted
c prbs: 5 simple, 466802 probed, 91 failed, 187 eqs
c prbs: 5 treelook, 1353 probed, 12 failed, 0 lifted
c prps: 370187668 props, 31 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c psns: 25909556 searches, 3951154 hits, 15% 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: 51 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 51 arith 100%, 0 double 0%
c rmbd: 788 removed, 489 red 62%
c rphs: 6 recomputed phases
c rsts: 31942 restarts 98%, 735 skipped 2%
c rsts: 0 saturating 0%, 0 agile 0%, 735 reuse 100%
c rsts: 33.3 avg interval, 33.3 scaled, 1.0 factor
c rsts: 8390 kept 26.3% average 24.9%
c simp: 13 count (13 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 1024626 count (607727 tried 0.6), 101188 sub out of 1014825 (10.0%)
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: 1 count
c tops: 8333 fixed 3%, 80 its, 13517.90 confs/it
c trvs: 9320768791 traversals, 98% srch, 3% simp, 0% lkhd
c trvs: 25.5 search traversals per propagation, 8466.9 per conflict
c trvs: 1.7 search traversals per search visit
c trds: 11 transitive reductions, 3742 removed, 8 failed
c trds: 527860 nodes, 257309 edges, 2702864 steps
c trim: 1246525 words, 4.8 MB
c trnr: 11 count, 1679 bin, 31081 trn, 144658535 steps
c unhd: 8 count, 8 rounds, 15950870 steps
c unhd: 516 non-trivial sccs of average size 2.1
c unhd: 13 units, 13 bin, 0 trn, 0 lrg
c unhd: 199 failed, 198 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 7592 tauts, 102 bin 1%, 4184 trn 55%, 2162 lrg 28%
c unhd: 7592 tauts, 1144 stamp 15%, 6908 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 98377 str, 13 bin 0%, 642 trn 1%, 97722 lrg 99%, 86347 red 88%
c vars: 19080 remaining 7% and 247325 removed 93% out of 266405
c vars: 8333 fixed 3%, 233231 eliminated 88%, 5761 equivalent 2%
c vsts: 5442265522 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 14.7 search visits per propagation, 4880.5 per conflict
c wchs: 1258510802 pushed, 30423496 enlarged, 180 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   1014825 100    737866 100  33940785 100   4818527 100    473451 100
c 
c  0     131139  13         0   0  26345760  78<  1865961  39    163526  35 
c  1     109922  11     62958   9   4347175  13    757701  16     91047  19 
c  2     273256  27    243496  33   1696980   5    880647  18<    99800  21<
c  3     255005  25<   221149  30<   956201   3    702832  15     63629  13 
c  4     142872  14    122508  17    371823   1    353319   7     29124   6 
c  5      58632   6     52121   7    131598   0    140988   3     11262   2 
c  6      23567   2     21221   3     49546   0     62937   1      7870   2 
c  7       8547   1      7377   1     19037   0     24375   1      3540   1 
c  8       3963   0      3063   0      9140   0     12038   0      2003   0 
c  9       1983   0      1310   0      4062   0      5309   0       789   0 
c 10       2595   0      1238   0      4776   0      5719   0       420   0 
c 11       3227   0      1368   0      4529   0      6482   0       430   0 
c 12        117   0        57   0       158   0       219   0        11   0 
c 13          0   0         0   0         0   0         0   0         0   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             2.6           3.0           0.4           1.6           1.6
c std             1.7           1.4           0.9           1.7           1.7
c 
c   27.864  11% cce
c   26.337  10% elim
c   16.444   6% decide
c   15.459   6% analysis
c    7.139   3% gc
c    6.079   2% backward
c    6.076   2% probe
c    4.603   2% decomp
c    3.765   1% cliff
c    3.304   1% block
c    2.744   1% restart
c    2.732   1% mincls
c    2.659   1% lift
c    2.277   1% defrag
c    2.248   1% bump
c    1.769   1% unhide
c    1.380   1% ternres
c    1.331   1% bca
c    1.189   0% cgrclsr
c    0.800   0% gauss
c    0.620   0% card
c    0.526   0% reduce
c    0.481   0% phase
c    0.272   0% transred
c    0.042   0% tabularasa
c    0.016   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    2.538   1% probe simple     42%
c    2.415   1% probe basic      40%
c    1.124   0% probe tree-look  18%
c ==================================
c   10.651   4% preprocessing    13%
c   69.916  27% inprocessing     87%
c ==================================
c   80.567  31% simplifying
c  183.076  69% search
c ==================================
c  263.648 100% all
c 
c 11583656 decisions, 43936.1 decisions/sec
c 1081432 conflicts, 4101.8 conflicts/sec
c 370187668 propagations, 1.4 megaprops/sec
c 263.6 seconds, 100.3 MB
c launch: done
