c launch: /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version ayv 86bf266b9332599f1b876e28a02fe8427aeaa2db
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat Oct 11 12:11:52 CEST 2014
c compiled Sat Oct 11 12:11:52 CEST 2014
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNDBLSCR  -I../yalsat -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT
c -DNLGLDRUPLIG
c Linux cluster2 3.13.0-36-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c no embedded options
c found 'p cnf 167075 6571833' header
c read 167075 variables, 6571833 clauses, 21183250 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 166190 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  166190  6549347         0       0      0     0   1  0.0   0.0  290
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 1637336 based on 6549347 irredundant clauses
c [card-1] found 12136 at-most-one constraints of average size 3.0
c [card-1] found 79 at-most-two constraints of average size 7.7
c [card-1] using previous limit 1637336 for elimination
c [card-1] 12215 out of 12215 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 5689 variables
c [simpleprobe-1] all 161386 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 2500000 penalty 3 = 0 + 3
c [simpleprobe-1] 161386 variables remain 100% (0 retained)
c [simpleprobe-1] removed 0 variables, found 21 hbrs, 0 units
c [unhide-1] limit 3249191 based on 6498382 irredundant clauses
c [unhide-1-1] 3 units, 104 failed, 98559 tauts, 0 hbrs, 9 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 161309 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-1] incomplete 109343 not tried 68% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 22323 = 14% variables out of 161309
c [phase-1] phase bias: 66888 positive 48%, 72098 negative 52%
c [simplification-1] removed 25654 variables 15.6% (138986 remain 84%)
c [simplification-1] removed 491412 irredundant clauses 7.5% (6057935 remain 92%)
c [simplification-1] maximum reduction of 16% = max (16%, 8%)
c [simplification-1] large reduction 16% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 2000 = 2 * 1000
c [simplification-1] new conflict limit 2000
c [cut-width] 322039, max 960982, min4 147484 at 75%, min10 87868 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   14.4  138986  6057935         5       3      0    16   8 21.0 943.8  385
c R   14.4  138986  6057935        20      12      0    16   9  9.1 931.1  385
c R   14.4  138986  6057935        61      47      0    20   8  7.1 902.9  385
c R   14.4  138986  6057935       165     135      4    25   6  7.7 831.4  385
c R   14.6  138986  6057935       414     349      7    28   5  8.6 726.6  385
c R   14.8  138986  6057935      1001     887     18    33   6  9.1 583.2  386
c 
c [simplification-2] limit of 2052 conflicts hit after 2054 conflicts
c [decomp-3] removed 161 variables
c [treelook-1] limit 1514408 based on 6057634 irredundant clauses
c [treelook-1] scheduled 27574 literals 10%
c [treelook-1] scheduling used 1549239 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1514408 based on 6057634 irredundant clauses
c [treelook-1] used 1606396 steps
c [treelook-1] 27542 literals remain 10%
c [treelook-1] 26355 variables remain to probed next time 19%
c [decomp-4] removed 1 variables
c [treelook-1] removed 1 variables, found 277 hbrs
c [basicprobe-1] limit 12115266 based on 6057633 irredundant clauses
c [basicprobe-1-0] 8270 probes remain 6% after last round
c [basicprobe-1-0] removed 0 variables, found 7326 hbrs
c [unhide-2] limit 3028816 based on 6057633 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 2472 tauts, 0 hbrs, 1972 literals
c [elim-2] 109206 variables 79% will be scheduled this time
c [elim-2] scheduled 109206 variables 79%
c [elim-2] limit of 6057458 steps based on 6057458 irredundant clauses
c [elim-2] incomplete 107303 not tried 77% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 138824
c [phase-2] phase bias: 392 positive 70%, 170 negative 30%
c [simplification-2] removed 162 variables 0.1% (138824 remain 84%)
c [simplification-2] removed 477 irredundant clauses 0.0% (6057458 remain 92%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 40000 = 2 * 20000
c [simplification-2] new conflict limit 42054
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   24.7  138824  6057458      2325    2119     24  4427   5  9.4 422.2  384
c -   26.0  138824  6057458      4778    2461     45  4442   7 10.0 282.7  385
c R   26.2  138824  6057458      5304    2973     48  4442   7 10.0 272.6  385
c -   27.7  138824  6057458      8153    3179     64  4452   5 10.1 202.0  385
c R   29.3  138824  6057458     11920    6715     84  4460   7 10.3 163.6  386
c -   29.5  138824  6057458     12167    3945     85  4460   6 10.3 160.3  385
c -   31.9  138824  6057458     16628    4736    101  4464   6 10.4 125.1  385
c -   34.6  138824  6057458     21719    5608    116  4470   7 10.3 102.1  385
c R   36.4  138824  6057458     26390   10090    124  4477   7 10.9  93.9  386
c -   36.8  138824  6057458     27118    6296    127  4478   8 10.8  91.3  385
c -   40.0  138824  6057458     33182    7096    149  4483   7 10.9  78.2  385
c -   43.4  138824  6057458     39909    7979    165  4484   6 10.9  69.0  385
c 
c [simplification-3] limit of 42174 conflicts hit after 42175 conflicts
c [card-2] limit 1514364 based on 6057458 irredundant clauses
c [card-2] found 5235 at-most-one constraints of average size 3.3
c [card-2] found 87 at-most-two constraints of average size 9.0
c [card-2] using previous limit 1514364 for elimination
c [card-2] 5322 out of 5322 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 224 variables
c [simpleprobe-2] all 138600 free variables schedulable
c [simpleprobe-2] limit 4992674 penalty 4 = 1 + 3
c [decomp-6] removed 3 variables
c [simpleprobe-2] 138597 variables remain 100% (0 retained)
c [simpleprobe-2] removed 3 variables, found 181 hbrs, 0 units
c [rephase-1] after 42175 conflicts (new increment 20000, next 62175)
c [flushphases] 128259 phases reset
c [phase-3] phase bias: 90 positive 97%, 3 negative 3%
c [simplification-3] removed 227 variables 0.2% (138597 remain 83%)
c [simplification-3] removed 227 irredundant clauses 0.0% (6057231 remain 92%)
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 40000
c [simplification-3] penalized conflict interval 80000 = 2 * 40000
c [simplification-3] new conflict limit 122175
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   54.3  138597  6057231     47197    8829    160  4384   5 10.9  61.0  386
c -   57.5  138597  6057231     54989    9638    170  4386   8 11.2  57.5  386
c R   59.0  138597  6057231     57895   12248    173  4387   6 11.1  56.2  386
c -   62.0  138597  6057231     63479   10563    188  4389   6 11.1  52.5  386
c -   66.5  138597  6057231     72406   11473    205  4394   6 11.0  48.0  386
c -   71.2  138597  6057231     81845   12408    219  4397   7 11.0  44.6  386
c -   76.2  138597  6057231     91895   13327    228  4404   7 11.0  41.7  386
c -   81.5  138597  6057231    102297   14185    236  4406   6 11.1  39.2  386
c -   87.3  138597  6057231    113904   15161    247  4408   7 11.0  37.3  386
c 
c [simplification-4] limit of 122225 conflicts hit after 122226 conflicts
c [treelook-2] limit 1514307 based on 6057231 irredundant clauses
c [treelook-2] scheduled 28872 literals 10%
c [treelook-2] scheduling used 1525518 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1514307 based on 6057231 irredundant clauses
c [treelook-2] used 1622969 steps
c [treelook-2] 28626 literals remain 10%
c [treelook-2] 11311 variables remain to probed next time 8%
c [decomp-8] removed 1 variables
c [treelook-2] removed 1 variables, found 286 hbrs
c [unhide-3] limit 3028615 based on 6057231 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 4099 tauts, 0 hbrs, 13790 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 138596 variables 100%
c [elim-3] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-3] incomplete 106858 not tried 77% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 395 = 0% variables out of 138596
c [rephase-2] after 122226 conflicts (new increment 40000, next 162226)
c [flushphases] 127989 phases reset
c [phase-4] phase bias: 315 positive 48%, 346 negative 52%
c [simplification-4] removed 396 variables 0.3% (138201 remain 83%)
c [simplification-4] removed 5179 irredundant clauses 0.1% (6052052 remain 92%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 40000
c [simplification-4] new conflict interval 80000
c [simplification-4] penalized conflict interval 160000 = 2 * 80000
c [simplification-4] new conflict limit 282226
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  102.2  138201  6052052    125403   15995    264  4512   6 11.1  36.4  387
c R  102.5  138201  6052052    126063   16619    264  4512   6 11.1  36.3  387
c -  108.4  138201  6052052    137465   16880    276  4513   7 11.1  34.6  387
c -  115.1  138201  6052052    150278   17859    287  4516   8 11.1  33.1  387
c -  121.8  138201  6052052    163425   18844    298  4519   6 11.1  31.8  387
c -  128.5  138201  6052052    177037   19792    311  4519   7 11.2  30.7  387
c -  135.5  138201  6052052    191254   20723    318  4519   8 11.2  29.9  387
c -  143.0  138201  6052052    206006   21740    332  4520   8 11.3  28.9  387
c -  150.9  138201  6052052    221460   22740    338  4521   8 11.3  28.2  387
c -  159.4  138201  6052052    237757   23836    350  4525   9 11.3  27.4  387
c -  164.9  138201  6052052    253893   24719    357  4526   6 11.3  27.2  387
c -  171.3  138201  6052052    270951   25605    366  4526  11 11.3  26.9  387
c R  171.9  138201  6052052    272630   27159    366  4526   6 11.3  26.9  388
c 
c [simplification-5] limit of 282264 conflicts hit after 282265 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 79938053 with penalty 3 = 0 + 3
c [ternres-1] all 138201 free variables schedulable
c [ternres-1] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-1] 126482 variables remain 92% (11719 retained)
c [gauss-1] limit 3197522 penalty 3 = 0 + 3
c [gauss-1] extracted 35 xors of average arity 3.0
c [gauss-1] connected 105 occurrences of 105 variables (average 1.0)
c [gauss-1] limit 3197522 penalty 3 = 0 + 3
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 6 variables
c [cgrclsr-1] limit 3026021 based on 6052043 irredundant clauses
c [cgrclsr-1] all 138195 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 2500000 with penalty 3 = 0 + 3
c [lift-1] using 133702 probes 97%
c [lift-1] 0 units, 1 impls, 1 eqs in 1 rounds
c [lift-1] 138147 variables remain 100% (47 retained)
c [lift-1] removed 1 variables
c [cliff-1] limit of 12500000 steps penalty 3 = 0 + 3
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 6052042 based on 6052042 irredundant clauses
c [transred-1] removed 847 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 138194 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1000000000 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 9550 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 319752212 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 14 clauses out of 201 (7%) of length 25
c [cce-1-1] eliminated 6 clauses out of 756 (1%) of length 24
c [cce-1-1] eliminated 37 clauses out of 2733 (1%) of length 23
c [cce-1-1] eliminated 92 clauses out of 1670 (6%) of length 22
c [cce-1-1] eliminated 95 clauses out of 814 (12%) of length 21
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 19
c [cce-1-1] eliminated 84 clauses out of 233 (36%) of length 18
c [cce-1-1] eliminated 47 clauses out of 189 (25%) of length 17
c [cce-1-1] eliminated 21 clauses out of 80 (26%) of length 16
c [cce-1-1] eliminated 4 clauses out of 15 (27%) of length 15
c [cce-1-1] eliminated 1 clauses out of 1181 (0%) of length 12
c [cce-1-1] eliminated 132 clauses out of 752 (18%) of length 11
c [cce-1-1] eliminated 7 clauses out of 3759 (0%) of length 10
c [cce-1-1] eliminated 9 clauses out of 15679 (0%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 552 large clauses in 319752213 steps
c [cce-1-1] allowing another 159876106 steps for small clauses
c [cce-1] scheduling 337829 clauses = 324080 binary + 13749 ternary
c [cce-1] tried to eliminate 5009 small clauses 1%
c [cce-1] eliminated 1412 small clauses 0%
c [cce-1] eliminated 1408 binary clauses 0%
c [cce-1] eliminated 4 ternary clauses 0%
c [cce-1-1] eliminated 1412 small clauses in 319752213 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1964 covered clauses in round 1
c [cce-1] eliminated 1964 covered clauses in TOTAL during 1 rounds
c [cce-1] 1964 < 1/1000 * 6041824 = 6041 considered unsuccessful
c [elim-4] 106666 variables 77% will be scheduled this time
c [elim-4] scheduled 106666 variables 77%
c [elim-4] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-4] incomplete 94449 not tried 68% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 384 = 0% variables out of 138194
c [bca-1] limit of 10000000 steps
c [bca-1] 272951 out of 275622 literals actually usable 99%
c [bca-1] added 8292 blocked clauses in 754669 steps
c [rephase-3] after 282265 conflicts (new increment 80000, next 362265)
c [flushphases] 127639 phases reset
c [phase-5] phase bias: 1011 positive 88%, 143 negative 12%
c [simplification-5] removed 391 variables 0.3% (137810 remain 83%)
c [simplification-5] removed 15589 irredundant clauses 0.3% (6036463 remain 92%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 80000
c [simplification-5] new conflict interval 160000
c [simplification-5] penalized conflict interval 320000 = 2 * 160000
c [simplification-5] new conflict limit 602265
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  207.6  137810  6036463    288484   26567   8725 15072   6 11.4  26.3  390
c -  216.7  137810  6036463    306557   27555   8730 15072   7 11.4  25.7  389
c -  225.9  137810  6036463    325143   28605   8740 15072   8 11.4  25.2  389
c -  235.4  137810  6036463    344470   29628   8754 15074   7 11.4  24.8  389
c -  245.9  137810  6036463    364474   30673   8763 15075   6 11.4  24.3  389
c -  256.2  137810  6036463    385102   31761   8769 15075   9 11.4  23.9  389
c -  265.4  137810  6036463    406011   32741   8782 15079   7 11.4  23.6  389
c -  276.4  137810  6036463    427271   33802   8790 15081   6 11.5  23.3  389
c -  288.1  137810  6036463    449139   34846   8796 15083  11 11.5  23.0  389
c -  299.3  137810  6036463    471756   35941   8802 15084   7 11.5  22.7  389
c -  312.0  137810  6036463    495124   37000   8808 15084   6 11.5  22.4  389
c -  323.8  137810  6036463    519223   38160   8818 15085  10 11.5  22.3  390
c -  333.3  137810  6036463    543850   39177   8824 15085   8 11.5  22.1  390
c -  343.3  137810  6036463    569436   40600   8843 15088   7 11.4  21.9  390
c R  349.8  137810  6036463    586378   56122   8846 15088   9 11.4  21.8  393
c -  355.1  137810  6036463    595021   41643   8850 15089   7 11.4  21.7  390
c 
c [simplification-6] limit of 602299 conflicts hit after 602300 conflicts
c [ternres-2] limit 25000000 with penalty 3 = 0 + 3
c [ternres-2] 126129 schedulable variables 92%
c [ternres-2] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-2] 122458 variables remain 89% (15352 retained)
c [card-3] limit 4235123 penalty 5 = 2 + 3
c [card-3] found 5067 at-most-one constraints of average size 3.3
c [card-3] found 106 at-most-two constraints of average size 8.4
c [card-3] using previous limit 4235123 for elimination
c [card-3] 5171 out of 5173 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 27 variables
c [basicprobe-2] limit 12072884 based on 6036442 irredundant clauses
c [basicprobe-2-0] 6799 probes remain 5% after last round
c [basicprobe-2-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1 variables, found 6664 hbrs
c [bate-1] eliminated 466 asymmetric tautologies during probing
c [lift-2] limit 2500000 with penalty 3 = 0 + 3
c [lift-2] using 133218 probes 97%
c [lift-2] 0 units, 2 impls, 11 eqs in 1 rounds
c [lift-2] 137686 variables remain 100% (85 retained)
c [lift-2] removed 11 variables
c [transred-2] limit 6035963 based on 6035963 irredundant clauses
c [transred-2] removed 1211 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 137771 variables 100%
c [block-2] limit of 100000000 steps penalty 3 = 0 + 3
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 146 blocked clauses
c [block-2] 146 < 1/1000 * 6035389 = 6035 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 137771 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-5] incomplete 98115 not tried 71% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 85 = 0% variables out of 137771
c [elim-5] 85 < 1/1000 * 137771 = 137 considered unsuccessful
c [bca-2] limit of 10000000 steps
c [bca-2] 272520 out of 275374 literals actually usable 99%
c [bca-2] added 102 blocked clauses in 768084 steps
c [rephase-4] after 602300 conflicts (new increment 160000, next 762300)
c [flushphases] 127545 phases reset
c [phase-6] phase bias: 565 positive 63%, 330 negative 37%
c [simplification-6] removed 124 variables 0.1% (137686 remain 83%)
c [simplification-6] removed 1328 irredundant clauses 0.0% (6035135 remain 92%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 160000
c [simplification-6] new conflict interval 320000
c [simplification-6] penalized conflict interval 640000 = 2 * 320000
c [simplification-6] new conflict limit 1242300
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  385.6  137686  6035135    620786   42819   8988 21284   6 11.4  21.5  390
c -  399.0  137686  6035135    647212   43939   8996 21284   6 11.5  21.3  390
c -  413.5  137686  6035135    674089   45026   9005 21287   7 11.5  21.1  390
c -  427.6  137686  6035135    701911   46394   9013 21287  11 11.5  21.0  390
c -  442.7  137686  6035135    730073   47533   9018 21288   6 11.5  20.8  391
c -  458.6  137686  6035135    758614   48676   9030 21288   7 11.5  20.7  391
c -  474.7  137686  6035135    788337   49974   9040 21288   6 11.5  20.5  391
c -  491.4  137686  6035135    818145   51142   9052 21290   6 11.5  20.4  391
c -  504.0  137686  6035135    848496   52261   9057 21290   9 11.5  20.3  391
c -  520.0  137686  6035135    879105   53378   9066 21290   6 11.5  20.2  391
c -  537.8  137686  6035135    910708   54605   9073 21291   8 11.6  20.1  391
c -  555.4  137686  6035135    942713   55812   9078 21293   8 11.6  20.0  391
c -  572.9  137686  6035135    975102   56961   9088 21293  10 11.6  19.9  391
c -  591.6  137686  6035135   1008375   58133   9092 21296   6 11.6  19.8  391
c -  610.2  137686  6035135   1042368   59348   9096 21296   8 11.6  19.7  391
c -  624.8  137686  6035135   1077298   60546   9098 21300   9 11.6  19.7  391
c -  639.0  137686  6035135   1112594   61596   9101 21301  12 11.6  19.6  391
c -  651.0  137686  6035135   1147361   62651   9102 21302  11 11.6  19.6  391
c -  665.9  137686  6035135   1184011   63798   9108 21303  11 11.5  19.5  391
c -  679.2  137686  6035135   1220770   64944   9112 21303   8 11.5  19.4  391
c 
c [simplification-7] limit of 1242336 conflicts hit after 1242337 conflicts
c [ternres-3] limit 25000000 with penalty 3 = 0 + 3
c [ternres-3] 122349 schedulable variables 89%
c [ternres-3] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-3] 118747 variables remain 86% (18939 retained)
c [gauss-2] limit 3125000 penalty 4 = 1 + 3
c [gauss-2] extracted 30 xors of average arity 3.0
c [gauss-2] connected 89 occurrences of 87 variables (average 1.0)
c [gauss-2] limit 3125000 penalty 4 = 1 + 3
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 216 variables
c [simpleprobe-3] all 137470 free variables schedulable
c [simpleprobe-3] limit 25000000 penalty 3 = 0 + 3
c [decomp-12] removed 25 variables
c [simpleprobe-3] 106097 variables remain 77% (31348 retained)
c [simpleprobe-3] removed 25 variables, found 3856 hbrs, 0 units
c [cgrclsr-2] limit 3017462 based on 6034924 irredundant clauses
c [cgrclsr-2] all 137445 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 2500000 with penalty 3 = 0 + 3
c [lift-3] using 132789 probes 97%
c [lift-3] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-3] 137318 variables remain 100% (127 retained)
c [cliff-2] limit of 12069848 steps based on 6034924 irredundant clauses
c [cliff-2] failed 0, lifted 0
c [unhide-4] limit 3017462 based on 6034924 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 9055 tauts, 0 hbrs, 23275 literals
c [transred-3] limit 6034712 based on 6034712 irredundant clauses
c [transred-3] removed 1332 transitive binary clauses
c [cce-2] limit of 69209694 steps penalty 4 = 1 + 3
c [cce-2-1] eliminated 4 clauses out of 195 (2%) of length 25
c [cce-2-1] eliminated 1 clauses out of 752 (0%) of length 24
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 5 large clauses in 69209695 steps
c [cce-2-1] allowing another 34604847 steps for small clauses
c [cce-2] scheduling 338494 clauses = 321118 binary + 17376 ternary
c [cce-2] tried to eliminate 942 small clauses 0%
c [cce-2] eliminated 280 small clauses 0%
c [cce-2] eliminated 271 binary clauses 0%
c [cce-2] eliminated 9 ternary clauses 0%
c [cce-2-1] eliminated 280 small clauses in 69209695 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 285 covered clauses in round 1
c [cce-2] eliminated 285 covered clauses in TOTAL during 1 rounds
c [cce-2] 285 < 1/1000 * 6034183 = 6034 considered unsuccessful
c [bca-3] limit of 10000000 steps
c [bca-3] 271936 out of 274892 literals actually usable 99%
c [bca-3] added 66 blocked clauses in 796432 steps
c [rephase-5] after 1242337 conflicts (new increment 320000, next 1562337)
c [flushphases] 127321 phases reset
c [phase-7] phase bias: 282 positive 37%, 475 negative 63%
c [simplification-7] removed 241 variables 0.2% (137445 remain 83%)
c [simplification-7] removed 1237 irredundant clauses 0.0% (6033898 remain 92%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 320000
c [simplification-7] new conflict interval 640000
c [simplification-7] penalized conflict interval 1280000 = 2 * 640000
c [simplification-7] new conflict limit 2522337
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  715.7  137445  6033898   1263515   66115   9116 20383   8 11.5  19.4  393
c -  730.8  137445  6033898   1301091   67287   9122 20383  10 11.5  19.4  394
c -  745.3  137445  6033898   1338935   68614   9124 20384   8 11.5  19.3  394
c -  762.9  137445  6033898   1378822   70094   9130 20384   7 11.5  19.3  394
c -  779.2  137445  6033898   1418234   71351   9135 20385   8 11.5  19.2  394
c -  796.2  137445  6033898   1458509   72604   9142 20386   9 11.5  19.2  394
c -  814.6  137445  6033898   1499602   74135   9153 20388   7 11.4  19.1  394
c -  831.9  137445  6033898   1540716   75353   9157 20388   7 11.4  19.1  394
c -  850.3  137445  6033898   1582340   76563   9158 20388   9 11.5  19.1  394
c -  868.7  137445  6033898   1625478   78150   9167 20390  11 11.4  19.0  394
c -  884.8  137445  6033898   1667847   79414   9185 20392  11 11.4  19.0  394
c -  900.8  137445  6033898   1710434   80548   9202 20395   7 11.4  18.9  394
c i  904.1  137444  6033898   1717581   86537   9226 20403   7 11.3  18.9  397
c i  915.7  137417  6033898   1744127  110355   9258 20412   9 11.3  18.9  399
c -  920.9  137329  6033898   1756323   82544   9263 20413   8 11.3  18.8  394
c i  925.6  137328  6033898   1768924   94102   9297 20425   5 11.3  18.8  398
c -  938.6  137238  6033898   1801452   84518   9320 20427  12 11.3  18.8  394
c i  940.1  137237  6033898   1805427   88113   9330 20430   7 11.3  18.8  396
c i  944.2  137144  6033898   1815752   97478   9355 20440   8 11.2  18.7  398
c i  945.2  137036  6033898   1817952   99432   9373 20446   8 11.2  18.7  398
c i  952.6  136946  6033898   1835428  115082   9397 20452   8 11.2  18.7  400
c i  953.4  136755  6033898   1837017  116369   9421 20460   6 11.2  18.7  400
c i  953.5  136705  6033898   1837043  116384   9425 20461   6 11.2  18.7  400
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  953.6  136614  6033898   1837207  116497   9431 20464   7 11.2  18.7  400
c i  953.6  136611  6033898   1837322  116571   9439 20468   7 11.2  18.7  400
c i  953.7  136520  6033898   1837417  116644   9446 20471   7 11.2  18.7  400
c i  953.7  136366  6033898   1837422  116645   9446 20473   7 11.2  18.7  400
c i  953.7  136172  6033898   1837424  116645   9446 20474   6 11.2  18.7  400
c i  953.7  136000  6033898   1837425  116645   9446 20474   6 11.2  18.7  400
c 0  953.7  135290  6033898   1837425  116645   9446 20474   6 11.2  18.7  400
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 466 basic ate = 157 trn 34% + 309 lrg 66% in 1 updates
c bcas: 3 count, 8460 added (12033 skipped), 2319185 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 2 bces, 9696 removed, 54744775 resolutions, 135383224 steps
c blkd: 2743 blocking literals 1%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 3 count, 0 units, 0 am1, 12959391 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 56797 subsumed
c card: 22438 at-most-one constraints found, average size 3.16
c card: 22438 at-most-one constraints used 100%, average size 3.16
c card: 272 at-most-two constraints found, average size 8.40
c card: 270 at-most-two constraints used 99%, average size 8.40
c cces: 2 cces, 2249 eliminated, 2206 ate 98%, 43 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 2 count, 6043615 esteps, 9271 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: 332 extracted (331 ands 100%, 1 xors 0%, 0 ites 0%)
c clff: 2 cliffs, 0 lifted, 0 failed
c clff: 9673 decisions, 24576476 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 27755083 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 29 gcs, 0 rescored clauses, 965 rescored vars
c dcps: 12 decompositions, 3930 equivalent 2%
c deco: 3312 decision-only clauses 0%, 54% reduction
c decs: 2856610 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 0 flipped 0.000% (in 0 phases)
c elms: 5 elims, 23187 eliminated 14%
c elms: 5 rounds, 1.0 rounds/bve
c elms: 12463 small 54%, 10724 large 46%
c elms: 13742 tried small, 12463 succeeded 91%, 1279 failed 9%
c elms: 25780 subsumed, 6616 strengthened, 0 blocked
c elms: 6423178 copies, 6162887 resolutions, 178762 ipos
c elms: 17516411 subchks, 1788202 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 2 extractions, 65 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12648868 steps, 6324434 extr 50%, 261 elim 0%
c glue: 11.2 orig avg, 11.2 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 19997 = 4058 simple + 15823 trn 20% + 116 lrg 79%, 1007 sub 1%
c hght: 19 average, 1.67 height/glue
c ints: 49150 luby (13246479 steps), 0 inout (0 steps)
c lift: 3 phases, 772 probed (258 level1 33%, 514 level2 67%)
c lift: 0 units, 12 equivalences, 3 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1834987 clauses, 25.5 length
c lrnd: 584466 uips 32%, 1144136 flips 62%
c mega: 0 count, 0 failed, 0 rounds
c mins: 46803958 learned lits, 31% minimized
c mins: 1812667 mins 99%, 169 bin 0%, 18839 size 1%, 3312 deco 0%
c move: moved 1834987, 2299 bin 0%, 12693 trn 1%, 0 lrg 0%
c otfs: str 7212 dyn (7146 red, 66 irr) 2438 drv 34%, 4774 rst 66%
c otfs: sub 40 dyn (40 red, 0 irr)
c phas: 7 computed, 143108 set, 69543 pos (49%), 73565 neg (51%)
c prbs: 2 basic, 5166 probed, 1 failed, 0 lifted
c prbs: 3 simple, 135595 probed, 0 failed, 26 eqs
c prbs: 2 treelook, 277 probed, 0 failed, 0 lifted
c prps: 1170801622 props, 409 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 66539492 searches, 8509494 hits, 13% 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: 76 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 76 arith 100%, 0 double 0%
c rmbd: 1205 removed, 388 red 32%
c rphs: 5 recomputed phases
c rsts: 30336 restarts 62%, 18814 skipped 38%
c rsts: 18440 saturating 98%, 0 agile 0%, 374 reuse 2%
c rsts: 59.4 avg interval, 59.4 scaled, 1.0 factor
c rsts: 12384 kept 40.8% average 18.8%
c simp: 7 count (7 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 1834987 count (871387 tried 0.5), 135268 sub out of 1833753 (7.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 0 count
c tops: 4668 fixed 3%, 15 its, 122495.00 confs/it
c trvs: 121606054410 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 103.9 search traversals per propagation, 66151.5 per conflict
c trvs: 1.5 search traversals per search visit
c trds: 3 transitive reductions, 3390 removed, 0 failed
c trds: 196987 nodes, 239614 edges, 18123274 steps
c trim: 881411 words, 3.4 MB
c trnr: 3 count, 0 bin, 77 trn, 129938054 steps
c unhd: 4 count, 4 rounds, 36701560 steps
c unhd: 378 non-trivial sccs of average size 2.2
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 104 failed, 91 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 114185 tauts, 121 bin 0%, 8294 trn 7%, 6477 lrg 6%
c unhd: 114185 tauts, 99293 stamp 87%, 15772 red 14%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 39046 str, 3 bin 0%, 1257 trn 3%, 37786 lrg 97%, 37145 red 95%
c vars: 135290 remaining 81% and 31785 removed 19% out of 167075
c vars: 4668 fixed 3%, 23187 eliminated 14%, 3930 equivalent 2%
c vsts: 79119018035 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 67.6 search visits per propagation, 43028.4 per conflict
c wchs: 4255593393 pushed, 41263850 enlarged, 53 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   1833753 100   1576595 100  41682307 100  15513569 100    725138 100
c 
c  0      47344   3         0   0  28322857  68   8198844  53    355875  49 
c  1      78294   4     35303   2   8904476  21<  2974373  19<   158117  22<
c  2     401137  22    380254  24   2022747   5   1358476   9     62505   9 
c  3     649999  35<   588355  37<  1466803   4   1576244  10     70289  10 
c  4     504068  27    436568  28    751458   2   1084446   7     57365   8 
c  5     143925   8    129503   8    201063   0    302391   2     19689   3 
c  6       8830   0      6565   0     12675   0     18489   0      1286   0 
c  7        156   0        47   0       228   0       306   0        12   0 
c  8          0   0         0   0         0   0         0   0         0   0 
c  9          0   0         0   0         0   0         0   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   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.5           1.1           1.1
c std             1.1           1.0           0.9           1.4           1.5
c 
c   26.036   3% analysis
c   24.129   3% decomp
c   23.625   2% gc
c   15.674   2% probe
c   14.239   1% defrag
c   13.697   1% elim
c   11.635   1% cce
c    7.895   1% bump
c    6.844   1% unhide
c    6.407   1% block
c    5.959   1% lift
c    5.595   1% mincls
c    5.556   1% transred
c    5.341   1% reduce
c    4.034   0% phase
c    3.996   0% cgrclsr
c    3.818   0% bca
c    2.341   0% decide
c    2.227   0% gauss
c    1.427   0% card
c    1.270   0% ternres
c    1.064   0% restart
c    0.455   0% cliff
c    0.129   0% cutwidth
c    0.000   0% backward
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    9.277   1% probe simple     59%
c    0.624   0% probe basic       4%
c    5.773   1% probe tree-look  37%
c ==================================
c   14.274   1% preprocessing    14%
c   89.444   9% inprocessing     86%
c ==================================
c  103.719  11% simplifying
c  849.971  89% search
c ==================================
c  953.693 100% all
c 
c 2856610 decisions, 2995.3 decisions/sec
c 1837425 conflicts, 1926.6 conflicts/sec
c 1170801622 propagations, 1.2 megaprops/sec
c 953.7 seconds, 635.6 MB
c launch: done
