c launch: /data/cnf/sc2014/app/pb_300_10_lb_07.cnf.bz2
c host: atom10
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/pb_300_10_lb_07.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/pb_300_10_lb_07.cnf.bz2
c no embedded options
c found 'p cnf 138579 621238' header
c read 138579 variables, 621238 clauses, 1470042 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 118663 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  118663   593745         0       0      0     0  18  0.0   0.0   31
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 5532 at-most-one constraints of average size 3.0
c [card-1] found 148 at-most-two constraints of average size 5.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5679 out of 5680 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 29361 variables
c [simpleprobe-1] all 109218 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 16 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 16 variables, found 7891 hbrs, 0 units
c [unhide-1] limit 259840 based on 519681 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 56196 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 109202 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 17123 variables 16% in round 1 in 41546558 steps
c [elim-1-1] backward subsumption/strengthening limit 83093116
c [elim-1-1] subsumed 0 and strengthened 9 clauses in 7769355 steps
c [elim-1-1] rescheduled 36 variables 0% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 98856 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 17123 = 16% variables out of 109202
c [phase-1] phase bias: 8428 positive 9%, 83651 negative 91%
c [simplification-1] removed 18711 variables 16.9% (92079 remain 78%)
c [simplification-1] removed 161190 irredundant clauses 27.1% (432555 remain 73%)
c [simplification-1] maximum reduction of 27% = max (17%, 27%)
c [simplification-1] large reduction 27% >= 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] 31988, max 63701, min4 31224 at 28%, min10 21781 at 10%
c [cut-width] cut-width based bias -1
c [decision-order] bias -1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    4.6   92079   432555         5       1      0     7  23  1.4 112.9   28
c R    4.6   92079   432555        61      42     15     7  27  4.3 144.9   28
c R    4.7   92079   432555       165     144     17     7   9  5.4 139.3   28
c R    4.9   92079   432555       409     381     18     7   2  5.3 214.7   28
c R    5.3   92079   432555       989     927     20    11   2  6.1 207.3   28
c 
c [simplification-2] limit of 1012 conflicts hit after 1012 conflicts
c [simpleprobe-2] all 92079 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 81188 variables remain 88% (10891 retained)
c [simpleprobe-2] removed 0 variables, found 901 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 47269 literals 26%
c [treelook-1] scheduling used 318961 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304124 steps
c [treelook-1] 47065 literals remain 26%
c [treelook-1] 45471 variables remain to probed next time 49%
c [treelook-1] removed 0 variables, found 144 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6026 probes remain 7% after last round
c [basicprobe-1-0] removed 0 variables, found 1051 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 92079 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 0 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 1228 clauses out of 1228 (100%) of length 11
c [cce-1-1] eliminated 307 clauses out of 307 (100%) of length 10
c [cce-1-1] eliminated 2 clauses out of 8 (25%) of length 6
c [cce-1-1] eliminated 39 clauses out of 913 (4%) of length 5
c [cce-1-1] eliminated 1357 clauses out of 7508 (18%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2933 large clauses in 75931665 steps
c [cce-1-1] allowing another 37965832 steps for small clauses
c [cce-1] scheduling 248932 clauses = 244691 binary + 4241 ternary
c [cce-1] tried to eliminate 33765 small clauses 14%
c [cce-1] eliminated 10393 small clauses 4%
c [cce-1] eliminated 10187 binary clauses 4%
c [cce-1] eliminated 206 ternary clauses 5%
c [cce-1-1] eliminated 10393 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 13326 covered clauses in round 1
c [cce-1] eliminated 13326 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 92079 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 2293 not tried 2% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1580 = 2% variables out of 92079
c [bca-1] limit of 10000000 steps
c [bca-1] 176315 out of 181000 literals actually usable 97%
c [bca-1] added 0 blocked clauses in 354599 steps
c [phase-2] phase bias: 176 positive 99%, 1 negative 1%
c [simplification-2] removed 1580 variables 1.7% (90499 remain 76%)
c [simplification-2] removed 13960 irredundant clauses 3.2% (418595 remain 71%)
c [simplification-2] maximum reduction of 3% = max (2%, 3%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 5000
c [simplification-2] penalized conflict interval 5000 = 1 * 5000
c [simplification-2] new conflict limit 6012
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   16.1   90499   418595      2296    2099    213  9782   3  6.5 210.3   29
c R   17.5   90499   418595      5249    4823    256  9785   4  7.9 211.2   29
c -   17.5   90499   418595      5249    2819    256  9785   4  7.9 211.2   29
c 
c [simplification-3] limit of 6046 conflicts hit after 6046 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 90499 free variables schedulable
c [ternres-1] 1733 ternary resolvents (3 bin, 1730 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 6981 at-most-one constraints of average size 3.4
c [card-2] found 310 at-most-two constraints of average size 4.3
c [card-2] using previous limit 1000000 for elimination
c [card-2] 7291 out of 7291 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 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-1] limit 209297 based on 418595 irredundant clauses
c [cgrclsr-1] all 90499 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 529669 with penalty 0 = 0 + 0
c [lift-1] using 89979 probes 99%
c [lift-1] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-1] 90483 variables remain 100% (16 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 209297 based on 418595 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 1316 tauts, 0 hbrs, 2769 literals
c [transred-1] limit 882783 with penalty 0 = 0 + 0
c [transred-1] removed 24 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 14 clauses out of 906 (2%) of length 5
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 14 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 400314 clauses = 231908 binary + 168406 ternary
c [cce-2] tried to eliminate 1452 small clauses 0%
c [cce-2] eliminated 259 small clauses 0%
c [cce-2] eliminated 218 binary clauses 0%
c [cce-2] eliminated 41 ternary clauses 0%
c [cce-2-1] eliminated 259 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 273 covered clauses in round 1
c [cce-2] eliminated 273 covered clauses in TOTAL during 1 rounds
c [cce-2] 273 < 1/1000 * 418576 = 418 considered unsuccessful
c [elim-3] 2293 variables 3% will be scheduled this time
c [elim-3] scheduled 2293 variables 3%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 2 variables 0% in round 1 in 15000599 steps
c [elim-3-1] backward subsumption/strengthening limit 4999401
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 4999402 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 2 = 0% variables out of 90499
c [elim-3] 2 < 1/1000 * 90499 = 90 considered unsuccessful
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-3] removed 2 variables 0.0% (90497 remain 76%)
c [simplification-3] removed 477 irredundant clauses 0.1% (418118 remain 70%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 25000
c [simplification-3] penalized conflict interval 25000 = 1 * 25000
c [simplification-3] new conflict limit 31046
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   22.3   90497   418118      9211    3997   2050 13465   3  7.7 190.9   29
c R   22.8   90497   418118     11780    6250   2059 13470   6 12.3 190.7   30
c -   23.7   90497   418118     13650    5027   2072 13471   4 11.7 184.0   30
c -   25.3   90497   418118     18429    6070   2099 13480   4 10.8 175.6   30
c -   26.8   90497   418118     23730    7146   2118 13484   4 10.5 170.7   30
c R   27.1   90497   418118     26103    9345   2127 13485   4 10.3 171.1   30
c -   28.4   90497   418118     29670    8220   2146 13499   3 10.2 165.8   30
c 
c [simplification-4] limit of 31138 conflicts hit after 31138 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 90497 free variables schedulable
c [ternres-2] 16 ternary resolvents (1 bin, 15 trn)
c [ternres-2] 52861 variables remain 58% (37636 retained)
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 23724 literals 13%
c [treelook-2] scheduling used 175294 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 189160 steps
c [treelook-2] 23722 literals remain 13%
c [treelook-2] 22101 variables remain to probed next time 24%
c [treelook-2] removed 0 variables, found 1185 hbrs
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 44 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 90497 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [bca-2] limit of 10000000 steps
c [bca-2] 168157 out of 180996 literals actually usable 93%
c [bca-2] added 0 blocked clauses in 346260 steps
c [rephase-1] after 31138 conflicts (new increment 20000, next 51138)
c [flushphases] 1587 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 0 variables 0.0% (90497 remain 76%)
c [simplification-4] removed 30 irredundant clauses 0.0% (418088 remain 70%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 25000
c [simplification-4] new conflict interval 50000
c [simplification-4] penalized conflict interval 50000 = 1 * 50000
c [simplification-4] new conflict limit 81138
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   31.5   90497   418088     36245    9493   2185 14677   5 10.2 159.2   31
c -   33.5   90497   418088     43407   10573   2220 14679   4 11.1 154.1   30
c -   35.3   90497   418088     51128   12015   2252 14686   6 11.1 150.1   30
c R   36.1   90497   418088     57385   17812   2273 14690   6 11.2 148.7   32
c -   36.8   90497   418088     59204   13046   2285 14693   5 11.1 147.0   30
c -   39.2   90497   418088     67894   14451   2314 14700   6 11.0 142.0   30
c -   41.6   90497   418088     76913   15623   2338 14704   4 10.9 137.7   31
c 
c [simplification-5] limit of 81204 conflicts hit after 81205 conflicts
c [ternres-3] limit 6986903 with penalty 0 = 0 + 0
c [ternres-3] 52861 schedulable variables 58%
c [ternres-3] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-2] limit 349345 penalty 1 = 1 + 0
c [cgrclsr-2] all 90497 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 2096071 with penalty 1 = 1 + 0
c [lift-2] using 89962 probes 99%
c [lift-2] 0 units, 1 impls, 0 eqs in 1 rounds
c [lift-2] 90421 variables remain 100% (76 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 60 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 239365 clauses = 231605 binary + 7760 ternary
c [cce-3] tried to eliminate 963 small clauses 0%
c [cce-3] eliminated 310 small clauses 0%
c [cce-3] eliminated 304 binary clauses 0%
c [cce-3] eliminated 6 ternary clauses 0%
c [cce-3-1] eliminated 310 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 310 covered clauses in round 1
c [cce-3] eliminated 310 covered clauses in TOTAL during 1 rounds
c [cce-3] 310 < 1/1000 * 418039 = 418 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 90497 variables 100%
c [elim-4] limit of 69869033 steps penalty 1 = 1 + 0
c [elim-4-1] eliminated 151 variables 0% in round 1 in 33939004 steps
c [elim-4-1] backward subsumption/strengthening limit 35930029
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 7515783 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 151 = 0% variables out of 90497
c [rephase-2] after 81205 conflicts (new increment 40000, next 121205)
c [flushphases] 1326 phases reset
c [phase-5] phase bias: 9 positive 100%, 0 negative 0%
c [simplification-5] removed 151 variables 0.2% (90346 remain 76%)
c [simplification-5] removed 455 irredundant clauses 0.1% (417633 remain 70%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 50000
c [simplification-5] new conflict interval 100000
c [simplification-5] penalized conflict interval 100000 = 1 * 100000
c [simplification-5] new conflict limit 181205
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   47.9   90346   417633     86741   16896   2391 14795   6 11.2 135.2   32
c -   50.6   90346   417633     97071   18214   2431 14800   4 11.3 131.1   32
c -   53.1   90346   417633    107968   19511   2455 14804   6 11.4 127.8   32
c -   54.8   90346   417633    119476   20379   2462 14806   6 12.5 128.0   33
c R   55.7   90346   417633    125030   25670   2470 14806   6 12.8 128.9   34
c -   57.4   90346   417633    131004   21410   2482 14808   4 12.7 127.0   32
c -   60.6   90346   417633    143393   22751   2519 14809   4 12.6 123.7   32
c -   63.5   90346   417633    156266   23989   2539 14812   4 12.6 121.0   32
c -   66.9   90346   417633    169636   25276   2556 14813   5 12.4 117.9   32
c 
c [simplification-6] limit of 181241 conflicts hit after 181241 conflicts
c [ternres-4] limit 13932692 with penalty 0 = 0 + 0
c [ternres-4] all 90346 free variables schedulable
c [ternres-4] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 1741586 penalty 2 = 2 + 0
c [card-3] found 6911 at-most-one constraints of average size 3.4
c [card-3] found 523 at-most-two constraints of average size 4.4
c [card-3] using previous limit 1741586 for elimination
c [card-3] 7433 out of 7434 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 6966346 penalty 1 = 1 + 0
c [basicprobe-2-0] 3891 probes remain 4% after last round
c [basicprobe-2-0] removed 0 variables, found 1944 hbrs
c [bate-1] eliminated 2943 asymmetric tautologies during probing
c [unhide-3] limit 696634 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 2933 tauts, 0 hbrs, 74769 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 41 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 90346 variables 100%
c [elim-5] limit of 278653858 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 115 variables 0% in round 1 in 33546105 steps
c [elim-5-1] backward subsumption/strengthening limit 67092210
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 7273668 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 115 = 0% variables out of 90346
c [rephase-3] after 181241 conflicts (new increment 80000, next 261241)
c [flushphases] 1310 phases reset
c [phase-6] phase bias: 1 positive 12%, 7 negative 88%
c [simplification-6] removed 115 variables 0.1% (90231 remain 76%)
c [simplification-6] removed 5805 irredundant clauses 1.4% (411828 remain 69%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 50000 = 100000 / 2
c [simplification-6] new conflict interval 150000
c [simplification-6] penalized conflict interval 150000 = 1 * 150000
c [simplification-6] new conflict limit 331241
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   73.4   90231   411828    183951   26317   5286 16360   5 12.6 116.1   33
c -   77.0   90231   411828    198657   27909   5306 16360   4 12.5 113.0   33
c -   80.4   90231   411828    214069   29273   5330 16360   7 12.6 110.7   33
c -   84.2   90231   411828    229555   30581   5352 16362   4 12.5 108.0   33
c -   86.4   90231   411828    246179   31741   5377 16362   6 12.8 107.1   34
c -   88.8   90231   411828    262844   32534   5391 16364   4 12.9 106.1   35
c R   89.9   90231   411828    270976   39940   5393 16365   7 12.9 105.7   36
c -   92.3   90231   411828    280081   33676   5408 16368   5 12.9 104.1   34
c -   96.0   90231   411828    297841   34906   5428 16368   5 12.9 102.3   34
c -  100.5   90231   411828    316220   36448   5455 16370   5 12.8 100.0   34
c 
c [simplification-7] limit of 331261 conflicts hit after 331263 conflicts
c [ternres-5] limit 23833778 with penalty 0 = 0 + 0
c [ternres-5] all 90231 free variables schedulable
c [ternres-5] 33 ternary resolvents (1 bin, 32 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 34 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 90231 variables 100%
c [block-3] limit of 59584445 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 90231 variables 100%
c [elim-6] limit of 476675563 steps penalty 0 = 0 + 0
c [elim-6-1] no variable eliminated in round 1 in 33113905 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 90231
c [bca-3] limit of 10000000 steps
c [bca-3] 164723 out of 180464 literals actually usable 91%
c [bca-3] added 0 blocked clauses in 379528 steps
c [rephase-4] after 331263 conflicts (new increment 160000, next 491263)
c [flushphases] 1310 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (90231 remain 76%)
c [simplification-7] removed 22 irredundant clauses 0.0% (411806 remain 69%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 150000
c [simplification-7] new conflict interval 300000
c [simplification-7] penalized conflict interval 300000 = 1 * 300000
c [simplification-7] new conflict limit 631263
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  107.6   90231   411806    336031   37706   5503 16359   6 13.1  98.5   35
c -  111.7   90231   411806    355356   38954   5532 16364   5 13.0  96.7   35
c -  116.2   90231   411806    375281   40469   5560 16365   5 12.9  94.6   35
c -  119.5   90231   411806    396850   41470   5576 16365   5 13.2  93.9   35
c -  124.2   90231   411806    417751   42853   5596 16367   5 13.1  91.9   35
c -  128.8   90231   411806    439340   44322   5633 16372   4 13.1  90.4   35
c -  133.4   90231   411806    461659   45699   5670 16378   5 13.0  89.0   35
c -  138.2   90231   411806    484896   47015   5691 16381   5 13.1  87.5   35
c -  142.8   90231   411806    508056   48323   5714 16387   6 13.1  86.1   35
c -  146.7   90231   411806    531829   49114   5732 16387   9 13.2  85.4   37
c -  151.0   90231   411806    557105   50303   5757 16393  10 13.2  84.6   35
c -  155.3   90231   411806    582554   51833   5783 16401   7 13.1  83.7   35
c R  155.5   90231   411806    583745   52946   5784 16401   7 13.1  83.6   37
c i  156.9   90230   411806    590268   59117   5797 16407   5 13.1  83.2   39
c i  157.6   90221   411806    593011   61693   5803 16411   6 13.1  83.0   39
c i  157.6   90219   411806    593031   61698   5806 16414   6 13.1  83.0   39
c -  160.9   90218   411806    607969   53204   5825 16417   8 13.0  82.2   36
c i  163.1   90217   411806    618096   62688   5840 16425   5 13.0  81.6   39
c i  163.6   90178   411806    620077   64435   5858 16434  11 13.0  81.5   39
c 
c [simplification-8] limit of 631507 conflicts hit after 631507 conflicts
c [ternres-6] limit 43964131 with penalty 0 = 0 + 0
c [ternres-6] all 90099 free variables schedulable
c [ternres-6] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 2198206 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 79435 schedulable variables 88%
c [simpleprobe-3] limit 87928263 penalty 1 = 1 + 0
c [decomp-13] removed 25 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 25 variables, found 6325 hbrs, 1 units
c [cgrclsr-3] limit 1099103 penalty 2 = 2 + 0
c [cgrclsr-3] all 90074 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 5000000 with penalty 2 = 2 + 0
c [lift-3] using 89408 probes 99%
c [lift-3] 2 units, 4 impls, 0 eqs in 1 rounds
c [lift-3] 89850 variables remain 100% (214 retained)
c [lift-3] removed 10 variables
c [cliff-3] limit of 8792826 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 74 transitive binary clauses
c [cce-4] limit of 21982065 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 9 clauses out of 969 (1%) of length 5
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 9 large clauses in 21982066 steps
c [cce-4-1] allowing another 10991033 steps for small clauses
c [cce-4] scheduling 235762 clauses = 227964 binary + 7798 ternary
c [cce-4] tried to eliminate 1390 small clauses 1%
c [cce-4] eliminated 425 small clauses 0%
c [cce-4] eliminated 419 binary clauses 0%
c [cce-4] eliminated 6 ternary clauses 0%
c [cce-4-1] eliminated 425 small clauses in 21982066 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 434 covered clauses in round 1
c [cce-4] eliminated 434 covered clauses in TOTAL during 1 rounds
c [rephase-5] after 631507 conflicts (new increment 320000, next 951507)
c [flushphases] 1310 phases reset
c [phase-8] phase bias: 6 positive 100%, 0 negative 0%
c [simplification-8] removed 35 variables 0.0% (90064 remain 76%)
c [simplification-8] removed 1349 irredundant clauses 0.3% (410457 remain 69%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 300000
c [simplification-8] new conflict interval 600000
c [simplification-8] penalized conflict interval 600000 = 1 * 600000
c [simplification-8] new conflict limit 1231507
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  169.9   90064   410457    636345   53627   5923 22861   8 13.0  80.8   40
c i  172.4   90063   410457    649654   66122   5939 22865   6 12.9  80.1   42
c i  172.4   89991   410457    649679   66131   5942 22869   7 12.9  80.1   42
c i  173.4   89985   410457    654912   70977   5951 22870   5 13.0  79.9   43
c i  174.7   89963   410457    660361   75782   5978 22878  10 12.9  79.7   44
c i  174.7   86936   410457    660362   75782   5978 22878  10 12.9  79.7   44
c 0  174.7   86693   410457    660362   75782   5978 22878  10 12.9  79.7   44
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 2943 basic ate = 2796 trn 95% + 147 lrg 5% in 1 updates
c bcas: 3 count, 0 added (2 skipped), 1080387 steps
c bkwd: tried 1543786 clauses, 3087563 lits, 2.00 lits/clause
c bkwd: checked 20856671 occs, 13.51 occs/clause, 6.76 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 9 large (0% self)
c blkd: 3 bces, 0 removed, 3578909 resolutions, 10014069 steps
c blkd: 582 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 3 count, 0 units, 0 am1, 8906134 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 45269 subsumed
c card: 19424 at-most-one constraints found, average size 3.29
c card: 19424 at-most-one constraints used 100%, average size 3.29
c card: 981 at-most-two constraints found, average size 4.47
c card: 979 at-most-two constraints used 100%, average size 4.47
c cces: 4 cces, 14343 eliminated, 14233 ate 99%, 110 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 3 count, 1657864 esteps, 75754 csteps
c cgrs: 0 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 1500 extracted (1500 ands 100%, 0 xors 0%, 0 ites 0%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 12060 decisions, 23825741 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2091280 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 35 gcs, 0 rescored clauses, 345 rescored vars
c dcps: 13 decompositions, 1588 equivalent 1%
c deco: 20457 decision-only clauses 3%, 58% reduction
c decs: 3176269 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 137332 flipped 4.324% (in 1454 phases)
c elms: 6 elims, 18971 eliminated 14%
c elms: 10 rounds, 1.7 rounds/bve
c elms: 18971 small 100%, 0 large 0%
c elms: 423484 tried small, 18971 succeeded 4%, 404513 failed 96%
c elms: 8043 subsumed, 210 strengthened, 0 blocked
c elms: 9302161 copies, 7012136 resolutions, 15186542 ipos
c elms: 2706459 subchks, 1228258 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10396644 steps, 5198322 extr 50%, 0 elim 0%
c glue: 12.9 orig avg, 12.7 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 24283 = 15117 simple + 8424 trn 62% + 742 lrg 35%, 10 sub 3%
c hght: 80 average, 6.16 height/glue
c ints: 19310 luby (4558682 steps), 0 inout (0 steps)
c lift: 3 phases, 1282 probed (429 level1 33%, 853 level2 67%)
c lift: 2 units, 0 equivalences, 5 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 656084 clauses, 36.4 length
c lrnd: 305893 uips 47%, 274100 flips 42%
c mega: 0 count, 0 failed, 0 rounds
c mins: 23890111 learned lits, 37% minimized
c mins: 631003 mins 96%, 125 bin 0%, 4499 size 1%, 20457 deco 3%
c move: moved 656084, 11128 bin 2%, 3177 trn 0%, 0 lrg 0%
c otfs: str 15708 dyn (15706 red, 2 irr) 4278 drv 27%, 11430 rst 73%
c otfs: sub 23 dyn (23 red, 0 irr)
c phas: 8 computed, 92279 set, 8620 pos (9%), 83659 neg (91%)
c prbs: 2 basic, 4882 probed, 0 failed, 0 lifted
c prbs: 3 simple, 488646 probed, 1 failed, 34 eqs
c prbs: 2 treelook, 206 probed, 0 failed, 0 lifted
c prps: 432319636 props, 134 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c psns: 108834394 searches, 9117916 hits, 8% 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: 43 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 43 arith 100%, 0 double 0%
c rmbd: 2742 removed, 28 red 1%
c rphs: 5 recomputed phases
c rsts: 19139 restarts 99%, 171 skipped 1%
c rsts: 0 saturating 0%, 4 agile 2%, 167 reuse 98%
c rsts: 33.9 avg interval, 33.9 scaled, 1.0 factor
c rsts: 3324 kept 17.4% average 20.2%
c simp: 8 count (8 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 656084 count (322426 tried 0.5), 38361 sub out of 654656 (5.9%)
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: 0 count
c tops: 31327 fixed 23%, 10 its, 66036.20 confs/it
c trvs: 8162786678 traversals, 100% srch, 1% simp, 0% lkhd
c trvs: 19.0 search traversals per propagation, 12300.9 per conflict
c trvs: 1.8 search traversals per search visit
c trds: 6 transitive reductions, 277 removed, 0 failed
c trds: 6886 nodes, 8967 edges, 10894793 steps
c trim: 665699 words, 2.5 MB
c trnr: 6 count, 5 bin, 1846 trn, 51806300 steps
c unhd: 3 count, 3 rounds, 7054769 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 60445 tauts, 474 bin 1%, 333 trn 1%, 24 lrg 0%
c unhd: 60445 tauts, 59614 stamp 99%, 1973 red 3%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 77538 str, 0 bin 0%, 28 trn 0%, 77510 lrg 100%, 77537 red 100%
c vars: 86693 remaining 63% and 51886 removed 37% out of 138579
c vars: 31327 fixed 23%, 18971 eliminated 14%, 1588 equivalent 1%
c vsts: 4624770628 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 10.7 search visits per propagation, 6943.3 per conflict
c wchs: 707139645 pushed, 18061957 enlarged, 62 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    654656 100    537208 100  18242414 100   4436587 100    407276 100
c 
c  0      32848   5         0   0  11385238  62   1500773  34    131405  32 
c  1      42654   7     17286   3   4157421  23<  1002358  23    102827  25 
c  2     163697  25    155713  29   1204963   7    674614  15<    56489  14<
c  3     199933  31<   184298  34<   955827   5    701580  16     64251  16 
c  4     121666  19    108323  20    355664   2    336898   8     31725   8 
c  5      53399   8     48348   9    112903   1    128158   3     11568   3 
c  6      19747   3     13878   3     37282   0     46661   1      4724   1 
c  7       9060   1      4481   1     15168   0     20514   0      2033   0 
c  8       4600   1      1976   0      7202   0      9831   0       882   0 
c  9       3300   1      1318   0      5080   0      7146   0       605   0 
c 10       2839   0      1128   0      4282   0      6077   0       546   0 
c 11        907   0       457   0      1377   0      1967   0       220   0 
c 12          6   0         2   0         7   0        10   0         1   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             3.1           3.2           0.7           1.6           1.6
c std             1.6           1.3           1.1           1.6           1.6
c 
c   15.278   9% analysis
c   12.792   7% elim
c    8.939   5% cce
c    4.347   2% mincls
c    3.855   2% decide
c    3.399   2% bump
c    2.910   2% restart
c    2.524   1% gc
c    2.392   1% probe
c    2.265   1% decomp
c    0.960   1% defrag
c    0.841   0% transred
c    0.765   0% lift
c    0.742   0% card
c    0.728   0% block
c    0.620   0% unhide
c    0.608   0% cliff
c    0.546   0% cgrclsr
c    0.543   0% gauss
c    0.533   0% ternres
c    0.497   0% reduce
c    0.483   0% backward
c    0.413   0% bca
c    0.383   0% phase
c    0.015   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    0.000   0% tabularasa
c ----------------------------------
c    1.606   1% probe simple     67%
c    0.306   0% probe basic      13%
c    0.479   0% probe tree-look  20%
c ==================================
c    4.539   3% preprocessing    14%
c   28.311  16% inprocessing     86%
c ==================================
c   32.850  19% simplifying
c  141.850  81% search
c ==================================
c  174.703 100% all
c 
c 3176269 decisions, 18181.0 decisions/sec
c 660362 conflicts, 3779.9 conflicts/sec
c 432319636 propagations, 2.5 megaprops/sec
c 174.7 seconds, 55.3 MB
c launch: done
