c launch: /data/cnf/sc2014/app/complete-500-0.1-17-98765432150017.cnf.bz2
c host: atom17
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/complete-500-0.1-17-98765432150017.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/complete-500-0.1-17-98765432150017.cnf.bz2
c no embedded options
c found 'p cnf 1000 74812' header
c read 1000 variables, 74812 clauses, 1324194 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 1000 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    1000    74812         0       0      0     0   0  0.0   0.0    7
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 879 at-most-one constraints of average size 4.9
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 879 out of 879 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 1000 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 96 variables remain 10% (904 retained)
c [simpleprobe-1] removed 0 variables, found 1056 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 2820 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1000 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] no variable eliminated in round 1 in 0 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 0 = 0% variables out of 1000
c [phase-1] phase bias: 500 positive 50%, 500 negative 50%
c [simplification-1] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-1] removed 1285 irredundant clauses 1.7% (73527 remain 98%)
c [simplification-1] maximum reduction of 2% = max (0%, 2%)
c [simplification-1] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-1] new conflict interval 6666
c [simplification-1] penalized conflict interval 6666 = 1 * 6666
c [simplification-1] new conflict limit 6666
c [cut-width] 268561, max 775702, min4 22715 at 74%, min10 12123 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    1.5    1000    73527         5       5      0  1056   0 89.2 462.5    7
c R    1.5    1000    73527        29      23      0  1056   0 93.8 358.6    7
c R    1.5    1000    73527        72      55      0  1056   1 85.6 281.3    7
c R    1.5    1000    73527       183     135      0  1056   1 77.1 200.8    7
c R    1.6    1000    73527       435     286      0  1056   2 72.5 145.8    9
c -    2.2    1000    73527      6016    2031      0  1056   6 100.0 137.6    8
c 
c [simplification-2] limit of 6666 conflicts hit after 6667 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 2000 literals 100%
c [treelook-1] scheduling used 185507 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 868715 steps
c [treelook-1] 1998 literals remain 100%
c [treelook-1] 1000 variables remain to probed next time 100%
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 804 probes remain 80% after last round
c [block-1] scheduling all variables this time
c [block-1] scheduled 1000 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] incomplete large round (ATE)
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 49803 clauses = 49803 binary + 0 ternary
c [cce-1] tried to eliminate 732 small clauses 1%
c [cce-1] eliminated 232 small clauses 0%
c [cce-1] eliminated 232 binary clauses 0%
c [cce-1-1] eliminated 232 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 232 covered clauses in round 1
c [cce-1] eliminated 232 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps
c [bca-1] 1133 out of 2002 literals actually usable 57%
c [bca-1] added 0 blocked clauses in 9215 steps
c [simplification-2] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-2] removed 232 irredundant clauses 0.3% (73295 remain 98%)
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 26666
c [simplification-2] penalized conflict interval 26666 = 1 * 26666
c [simplification-2] new conflict limit 33333
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   17.9    1000    73295     12796    2512      0  1288   8 82.5 119.9    8
c -   18.7    1000    73295     21791    3024      0  1288   8 74.5 107.2    8
c -   19.7    1000    73295     32095    3524      0  1288   7 73.5 103.0    8
c 
c [simplification-3] limit of 33333 conflicts hit after 33334 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 1000 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 793 at-most-one constraints of average size 5.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 793 out of 793 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 [simpleprobe-2] 96 schedulable variables 10%
c [simpleprobe-2] limit 2405657 penalty 1 = 1 + 0
c [simpleprobe-2] 121 variables remain 12% (879 retained)
c [simpleprobe-2] removed 0 variables, found 152 hbrs, 0 units
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 1000 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 721697 with penalty 0 = 0 + 0
c [lift-1] using 0 probes 0%
c [lift-1] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-1] 1000 variables remain 100% (0 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 120282 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 3611 literals
c [transred-1] limit 1202828 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 49571 clauses = 49571 binary + 0 ternary
c [cce-2] tried to eliminate 52 small clauses 0%
c [cce-2] eliminated 8 small clauses 0%
c [cce-2] eliminated 8 binary clauses 0%
c [cce-2-1] eliminated 8 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 8 covered clauses in round 1
c [cce-2] eliminated 8 covered clauses in TOTAL during 1 rounds
c [cce-2] 8 < 1/1000 * 73295 = 73 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 1000 variables 100%
c [elim-2] limit of 12028289 steps penalty 1 = 1 + 0
c [elim-2-1] no variable eliminated in round 1 in 0 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 0 = 0% variables out of 1000
c [rephase-1] after 33334 conflicts (new increment 20000, next 53334)
c [flushphases] 0 phases reset
c [simplification-3] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-3] removed 8 irredundant clauses 0.0% (73287 remain 98%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 26666
c [simplification-3] new conflict interval 53332
c [simplification-3] penalized conflict interval 53332 = 1 * 53332
c [simplification-3] new conflict limit 86666
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.5    1000    73287     42981    4014      0  1448   7 69.3  96.7    8
c -   24.6    1000    73287     54496    4517      0  1448   7 70.1  96.7   11
c -   25.9    1000    73287     68416    5014      0  1448   8 69.8  95.3    9
c -   27.5    1000    73287     84478    5515      0  1448   8 69.0  93.1    9
c 
c [simplification-4] limit of 86666 conflicts hit after 86666 conflicts
c [block-2] scheduling all variables this time
c [block-2] scheduled 1000 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] 1147 out of 2002 literals actually usable 57%
c [bca-2] added 0 blocked clauses in 13120 steps
c [rephase-2] after 86666 conflicts (new increment 40000, next 126666)
c [flushphases] 0 phases reset
c [simplification-4] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-4] removed 0 irredundant clauses 0.0% (73287 remain 98%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 53332
c [simplification-4] new conflict interval 106664
c [simplification-4] penalized conflict interval 106664 = 1 * 106664
c [simplification-4] new conflict limit 193330
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   31.0    1000    73287    103247    6010      0  1448   7 67.8  90.4   12
c -   33.1    1000    73287    124427    6509      0  1448   8 66.0  87.2    9
c -   35.1    1000    73287    144311    7023      0  1448   8 65.6  86.4    9
c -   37.3    1000    73287    166284    7518      0  1448   7 64.4  84.5   12
c -   39.8    1000    73287    190871    8035      0  1448   7 64.2  83.6   11
c 
c [simplification-5] limit of 193330 conflicts hit after 193330 conflicts
c [ternres-2] limit 3727177 with penalty 1 = 1 + 0
c [ternres-2] all 1000 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 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 [treelook-2] limit 186358 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1928 literals 96%
c [treelook-2] scheduling used 186597 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 186358 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 981379 steps
c [treelook-2] 1926 literals remain 96%
c [treelook-2] 1000 variables remain to probed next time 100%
c [cgrclsr-2] limit 372717 penalty 1 = 1 + 0
c [cgrclsr-2] all 1000 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 2236306 with penalty 1 = 1 + 0
c [lift-2] using 0 probes 0%
c [lift-2] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-2] 1000 variables remain 100% (0 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-2] limit 1000000 with penalty 1 = 1 + 0
c [transred-2] removed 0 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 49563 clauses = 49563 binary + 0 ternary
c [cce-3] tried to eliminate 55 small clauses 0%
c [cce-3] eliminated 36 small clauses 0%
c [cce-3] eliminated 36 binary clauses 0%
c [cce-3-1] eliminated 36 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 36 covered clauses in round 1
c [cce-3] eliminated 36 covered clauses in TOTAL during 1 rounds
c [cce-3] 36 < 1/1000 * 73287 = 73 considered unsuccessful
c [rephase-3] after 193330 conflicts (new increment 80000, next 273330)
c [flushphases] 0 phases reset
c [simplification-5] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-5] removed 36 irredundant clauses 0.0% (73251 remain 98%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 106664
c [simplification-5] new conflict interval 213328
c [simplification-5] penalized conflict interval 213328 = 1 * 213328
c [simplification-5] new conflict limit 406658
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   43.8    1000    73251    212086    8511      0  1484   7 64.7  84.5   12
c -   46.4    1000    73251    237759    9016      0  1484   7 64.9  84.4    9
c -   49.2    1000    73251    265569    9515      0  1484   8 64.5  83.7   10
c -   52.3    1000    73251    295297   10006      0  1484   7 63.8  82.6   13
c -   55.3    1000    73251    325923   10528      0  1484   7 63.1  81.5   10
c -   58.7    1000    73251    356987   11025      0  1484   7 63.5  81.8   10
c -   62.6    1000    73251    393236   11519      0  1484   8 63.7  81.6   10
c 
c [simplification-6] limit of 406658 conflicts hit after 406658 conflicts
c [card-3] limit 1998459 penalty 2 = 2 + 0
c [card-3] found 793 at-most-one constraints of average size 5.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1998459 for elimination
c [card-3] 793 out of 793 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 799383 with penalty 2 = 2 + 0
c [unhide-3-4] 0 units, 0 failed, 0 tauts, 0 hbrs, 14839 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1000 variables 100%
c [elim-3] limit of 79938366 steps penalty 2 = 2 + 0
c [elim-3-1] no variable eliminated in round 1 in 7898 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 1000
c [rephase-4] after 406658 conflicts (new increment 160000, next 566658)
c [flushphases] 0 phases reset
c [simplification-6] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-6] removed 0 irredundant clauses 0.0% (73251 remain 98%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 213328
c [simplification-6] new conflict interval 426656
c [simplification-6] penalized conflict interval 426656 = 1 * 426656
c [simplification-6] new conflict limit 833314
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   66.7    1000    73251    426138   12018      0  1484   7 63.7  81.6   13
c -   70.6    1000    73251    461808   12519      0  1484   7 63.2  80.9   10
c -   74.3    1000    73251    497883   13016      0  1484   7 62.6  80.1   10
c -   78.3    1000    73251    535331   13529      0  1484   8 61.7  79.0   11
c -   82.3    1000    73251    571589   14008      0  1484   8 60.8  77.9   14
c -   86.3    1000    73251    607481   14516      0  1484   7 60.0  76.8   11
c -   91.2    1000    73251    652199   15025      0  1484   7 60.2  76.9   12
c -   96.1    1000    73251    698501   15516      0  1484   8 60.0  76.6   15
c -  101.2    1000    73251    745106   16011      0  1484   8 59.6  75.9   12
c -  106.0    1000    73251    789345   16515      0  1484   7 59.0  75.1   12
c 
c [simplification-7] limit of 833314 conflicts hit after 833314 conflicts
c [basicprobe-2] limit 17336895 penalty 1 = 1 + 0
c [basicprobe-2-0] 804 sched 80%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-0] fully completed probing
c [block-3] scheduling all variables this time
c [block-3] scheduled 1000 variables 100%
c [block-3] limit of 86684477 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 [bca-3] limit of 10000000 steps
c [bca-3] 1022 out of 2002 literals actually usable 51%
c [bca-3] added 0 blocked clauses in 38720 steps
c [rephase-5] after 833314 conflicts (new increment 320000, next 1153314)
c [flushphases] 0 phases reset
c [simplification-7] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-7] removed 0 irredundant clauses 0.0% (73251 remain 98%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 426656
c [simplification-7] new conflict interval 853312
c [simplification-7] penalized conflict interval 853312 = 1 * 853312
c [simplification-7] new conflict limit 1686626
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  113.7    1000    73251    837255   17016      0  1484   7 58.7  74.7   13
c -  119.3    1000    73251    885280   17518      0  1484   7 59.1  75.2   16
c -  125.0    1000    73251    930035   18026      0  1484   7 59.7  76.0   16
c -  131.1    1000    73251    980011   18529      0  1484   7 60.1  76.5   16
c -  137.7    1000    73251   1032021   19014      0  1484   7 60.5  77.0   13
c -  144.7    1000    73251   1090202   19509      0  1484   7 60.6  77.0   16
c -  151.8    1000    73251   1150489   20033      0  1484   7 60.6  76.8   13
c -  159.1    1000    73251   1210809   20525      0  1484   7 60.5  76.6   13
c -  166.9    1000    73251   1273670   21015      0  1484   7 60.4  76.4   13
c -  174.9    1000    73251   1338009   21514      0  1484   8 60.3  76.1   13
c -  182.6    1000    73251   1401061   22024      0  1484   7 60.0  75.8   17
c -  190.7    1000    73251   1466930   22528      0  1484   7 59.7  75.3   17
c -  199.0    1000    73251   1532821   23019      0  1484   7 59.3  74.8   13
c -  207.2    1000    73251   1596954   23542      0  1484   7 58.9  74.3   13
c -  216.2    1000    73251   1667925   24020      0  1484   8 58.7  73.9   13
c 
c [simplification-8] limit of 1686626 conflicts hit after 1686627 conflicts
c [ternres-3] limit 19141541 with penalty 2 = 2 + 0
c [ternres-3] all 1000 free variables schedulable
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 3828308 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 [cgrclsr-3] limit 1914154 penalty 2 = 2 + 0
c [cgrclsr-3] all 1000 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 5000000 with penalty 2 = 2 + 0
c [lift-3] using 0 probes 0%
c [lift-3] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-3] 1000 variables remain 100% (0 retained)
c [cliff-3] limit of 15313233 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-3] limit 500000 with penalty 2 = 2 + 0
c [transred-3] removed 0 transitive binary clauses
c [cce-4] limit of 38283083 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 19141542 steps for small clauses
c [cce-4] scheduling 49527 clauses = 49527 binary + 0 ternary
c [cce-4] tried to eliminate 123 small clauses 0%
c [cce-4] eliminated 53 small clauses 0%
c [cce-4] eliminated 53 binary clauses 0%
c [cce-4-1] eliminated 53 small clauses in 38283084 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 53 covered clauses in round 1
c [cce-4] eliminated 53 covered clauses in TOTAL during 1 rounds
c [cce-4] 53 < 1/1000 * 73251 = 73 considered unsuccessful
c [rephase-6] after 1686627 conflicts (new increment 640000, next 2326627)
c [flushphases] 0 phases reset
c [simplification-8] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-8] removed 53 irredundant clauses 0.1% (73198 remain 98%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 853312
c [simplification-8] conflict interval soft limit 1000000 reached
c [simplification-8] new conflict interval 1000000
c [simplification-8] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-8] new conflict limit 2686627
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  225.1    1000    73198   1711730   24511      0  1537   8 58.1  73.2   15
c -  230.0    1000    73198   1741871   25026      0  1537   8 57.4  72.3   18
c -  236.2    1000    73198   1772434   25519      0  1537   8 56.7  71.5   24
c -  241.7    1000    73198   1808680   26030      0  1537   8 56.1  70.6   21
c -  247.7    1000    73198   1847430   26525      0  1537   8 55.5  69.9   25
c -  253.3    1000    73198   1881683   27020      0  1537   8 54.9  69.2   26
c -  259.4    1000    73198   1916047   27523      0  1537   8 54.3  68.4   27
c -  265.5    1000    73198   1949742   28042      0  1537   8 53.7  67.7   28
c -  271.2    1000    73198   1983203   28519      0  1537   8 53.1  66.9   28
c -  277.8    1000    73198   2022610   29024      0  1537   8 52.5  66.3   29
c -  284.3    1000    73198   2057627   29524      0  1537   8 52.0  65.5   26
c -  296.9    1000    73198   2133894   30032      0  1537   8 52.1  65.6   26
c -  309.9    1000    73198   2216792   30537      0  1537   8 52.0  65.6   34
c -  321.9    1000    73198   2290324   31028      0  1537   8 51.8  65.3   25
c -  334.6    1000    73198   2361556   31520      0  1537   8 51.4  65.0   23
c -  345.5    1000    73198   2426703   32020      0  1537   8 51.1  64.6   22
c -  356.6    1000    73198   2491491   32514      0  1537   8 50.7  64.3   22
c -  367.9    1000    73198   2556661   33022      0  1537   8 50.4  63.9   22
c -  379.3    1000    73198   2624969   33527      0  1537   8 50.1  63.6   21
c -  388.6    1000    73198   2682882   34017      0  1537   8 49.7  63.2   25
c 
c [simplification-9] limit of 2686627 conflicts hit after 2686629 conflicts
c [rephase-7] after 2686629 conflicts (new increment 1280000, next 3966629)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-9] removed 0 irredundant clauses 0.0% (73198 remain 98%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 1000000
c [simplification-9] new conflict interval 2000000
c [simplification-9] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-9] new conflict limit 4686629
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  400.5    1000    73198   2757032   34520      0  1537   8 50.4  64.3   25
c -  413.3    1000    73198   2841547   35015      0  1537   8 51.2  65.3   25
c -  425.6    1000    73198   2926297   35516      0  1537   7 51.9  66.3   25
c -  439.0    1000    73198   3021130   36016      0  1537   8 52.4  67.0   30
c -  452.9    1000    73198   3121496   36514      0  1537   8 52.9  67.6   25
c -  467.6    1000    73198   3218025   37016      0  1537   8 53.5  68.3   25
c -  481.2    1000    73198   3320584   37533      0  1537   8 53.8  68.7   25
c -  496.1    1000    73198   3430408   38008      0  1537   8 54.2  69.1   26
c -  511.6    1000    73198   3540617   38538      0  1537   8 54.6  69.5   26
c -  527.2    1000    73198   3656754   39014      0  1537   8 54.8  69.7   25
c -  543.5    1000    73198   3774202   39522      0  1537   7 55.0  70.0   26
c -  561.2    1000    73198   3892234   40039      0  1537   7 55.3  70.2   25
c -  578.7    1000    73198   4011806   40517      0  1537   8 55.4  70.4   25
c -  595.1    1000    73198   4129096   41032      0  1537   7 55.5  70.5   25
c -  611.5    1000    73198   4249541   41516      0  1537   7 55.6  70.5   25
c -  631.2    1000    73198   4379239   42027      0  1537   8 55.6  70.5   25
c -  649.6    1000    73198   4506756   42529      0  1537   8 55.7  70.5   25
c -  667.2    1000    73198   4630257   43028      0  1537   7 55.7  70.5   24
c 
c [simplification-10] limit of 4686629 conflicts hit after 4686629 conflicts
c [card-4] limit 16534627 penalty 3 = 3 + 0
c [card-4] found 796 at-most-one constraints of average size 5.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 16534627 for elimination
c [card-4] 796 out of 796 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 121 schedulable variables 12%
c [simpleprobe-3] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-3] 92 variables remain 9% (908 retained)
c [simpleprobe-3] removed 0 variables, found 2910 hbrs, 0 units
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-7] 0 units, 0 failed, 0 tauts, 0 hbrs, 54378 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 1000 variables 100%
c [elim-4] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-4-1] no variable eliminated in round 1 in 5231647 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 1000
c [rephase-8] after 4686629 conflicts (new increment 2560000, next 7246629)
c [flushphases] 0 phases reset
c [simplification-10] removed 0 variables 0.0% (1000 remain 100%)
c [simplification-10] removed 0 irredundant clauses 0.0% (73198 remain 98%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 2000000
c [simplification-10] new conflict interval 4000000
c [simplification-10] penalized conflict interval 4000000 = 1 * 4000000
c [simplification-10] new conflict limit 8686629
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  693.2    1000    73198   4750802   43538      0  4447   8 55.9  70.7   28
c -  712.4    1000    73198   4858137   44030      0  4447   8 56.4  71.4   28
c -  731.4    1000    73198   4977990   44521      0  4447   8 56.6  71.7   28
c -  751.6    1000    73198   5105588   45027      0  4447   8 56.8  71.9   28
c -  771.4    1000    73198   5236374   45514      0  4447   8 56.9  72.0   28
c -  791.3    1000    73198   5366022   46013      0  4447   8 57.0  72.1   27
c -  813.5    1000    73198   5501701   46525      0  4447   8 57.1  72.2   33
c -  837.6    1000    73198   5645748   47030      0  4447   8 57.2  72.3   33
c -  859.1    1000    73198   5784372   47531      0  4447   8 57.2  72.3   27
c -  882.2    1000    73198   5923146   48015      0  4447   8 57.3  72.4   27
c -  903.9    1000    73198   6056498   48521      0  4447   7 57.3  72.4   26
c -  926.0    1000    73198   6192332   49020      0  4447   8 57.2  72.2   26
c -  950.5    1000    73198   6339540   49515      0  4447   8 57.1  72.1   25
c -  974.0    1000    73198   6480439   50016      0  4447   8 57.1  72.0   24
c -  996.0    1000    73198   6615160   50531      0  4447   8 56.9  71.8   24
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 0 added (0 skipped), 61055 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: 3 bces, 0 removed, 4364674 resolutions, 12296772 steps
c blkd: 2 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 22260594 steps
c card: 9 rescheduled, 84 eliminated, 82741 resolved, 80 subsumed
c card: 3261 at-most-one constraints found, average size 4.95
c card: 3261 at-most-one constraints used 100%, average size 4.95
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 329 eliminated, 327 ate 99%, 2 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, 2490996 esteps, 2102024 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: 279 extracted (279 ands 100%, 0 xors 0%, 0 ites 0%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 12243 decisions, 30321193 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1399006 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 32 gcs, 0 rescored clauses, 3438 rescored vars
c dcps: 13 decompositions, 0 equivalent 0%
c deco: 3964275 decision-only clauses 61%, 62% reduction
c decs: 8839582 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 113 flipped 0.001% (in 3 phases)
c elms: 4 elims, 0 eliminated 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 0 subsumed, 0 strengthened, 0 blocked
c elms: 52472 copies, 73455 resolutions, 0 ipos
c elms: 197011 subchks, 1166138 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, 14157066 steps, 7078533 extr 50%, 0 elim 0%
c glue: 56.9 orig avg, 48.8 real avg, 7.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 4118 = 4118 simple + 0 trn 100% + 0 lrg 0%, 0 sub 0%
c hght: 72 average, 1.26 height/glue
c ints: 159496 luby (49025128 steps), 0 inout (0 steps)
c lift: 3 phases, 0 probed (0 level1 0%, 0 level2 0%)
c lift: 0 units, 0 equivalences, 0 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 6536827 clauses, 78.8 length
c lrnd: 1414072 uips 22%, 4440925 flips 68%
c mega: 0 count, 0 failed, 0 rounds
c mins: 515216086 learned lits, 50% minimized
c mins: 2566524 mins 39%, 0 bin 0%, 6028 size 0%, 3964275 deco 61%
c move: moved 6536827, 329 bin 0%, 0 trn 0%, 0 lrg 0%
c otfs: str 438435 dyn (322611 red, 115824 irr) 109824 drv 25%, 328611 rst 75%
c otfs: sub 10692 dyn (10692 red, 0 irr)
c phas: 1 computed, 1000 set, 500 pos (50%), 500 neg (50%)
c prbs: 2 basic, 2000 probed, 0 failed, 0 lifted
c prbs: 3 simple, 6262 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 4 probed, 0 failed, 0 lifted
c prps: 375404396 props, 42 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 41985283 searches, 30137603 hits, 72% 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: 98 count, 0 reset, 10 acts 10%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 98 arith 100%, 0 double 0%
c rmbd: 1285 removed, 0 red 0%
c rphs: 8 recomputed phases
c rsts: 51 restarts 0%, 159445 skipped 100%
c rsts: 159444 saturating 100%, 0 agile 0%, 1 reuse 0%
c rsts: 127626.7 avg interval, 127626.7 scaled, 1.0 factor
c rsts: 27 kept 52.9% average 9.9%
c simp: 10 count (10 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 6536827 count (6006206 tried 0.9), 3892340 sub out of 6536827 (59.5%)
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: 0 fixed 0%, 0 its, 0.00 confs/it
c trvs: 79182633264 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 211.4 search traversals per propagation, 11907.4 per conflict
c trvs: 2.0 search traversals per search visit
c trds: 3 transitive reductions, 0 removed, 0 failed
c trds: 609 nodes, 18103 edges, 2703171 steps
c trim: 167100487 words, 637.4 MB
c trnr: 3 count, 0 bin, 0 trn, 539674 steps
c unhd: 4 count, 7 rounds, 5024284 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: 0 tauts, 0 bin 0%, 0 trn 0%, 0 lrg 0%
c unhd: 0 tauts, 0 stamp 0%, 0 red 0%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 75648 str, 0 bin 0%, 0 trn 0%, 75648 lrg 100%, 62541 red 83%
c vars: 1000 remaining 100% and 0 removed 0% out of 1000
c vars: 0 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 40183066874 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 107.3 search visits per propagation, 6039.9 per conflict
c wchs: 19160422673 pushed, 106494802 enlarged, 340 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   6536827 100   2571598 100  50299605 100  26662518 100   2583744 100
c 
c  0          0   0         0   0         0   0         0   0         0   0 
c  1          5   0         0   0       260   0        62   0         8   0 
c  2       3053   0      2009   0    342239   1    108755   0     11874   0 
c  3     111698   2     60890   2  19803915  39   6134606  23    736813  29 
c  4     506795   8    495221  19  14704739  29<  5686593  21    682118  26 
c  5     968599  15    949581  37   7769070  15   4283745  16<   488285  19<
c  6    1174919  18    534920  21<  3064618   6   2954433  11    257868  10 
c  7    1010968  15<   176493   7   1348691   3   2016406   8    116330   5 
c  8    1082020  17    148285   6   1235852   2   2113696   8    103840   4 
c  9    1196125  18    143438   6   1421852   3   2383945   9    128122   5 
c 10     478159   7     59772   2    602310   1    970870   4     57834   2 
c 11       4486   0       989   0      6059   0      9407   0       652   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             7.0           5.6           4.3           5.4           4.8
c std             1.8           1.5           1.6           2.1           1.8
c 
c   54.963   5% analysis
c   17.098   2% cce
c   13.850   1% bump
c    5.805   1% decide
c    4.352   0% block
c    4.291   0% probe
c    4.225   0% card
c    4.055   0% mincls
c    2.672   0% unhide
c    2.057   0% reduce
c    1.699   0% defrag
c    1.445   0% cliff
c    1.301   0% cgrclsr
c    1.135   0% gc
c    0.827   0% decomp
c    0.633   0% elim
c    0.266   0% transred
c    0.263   0% gauss
c    0.231   0% bca
c    0.197   0% restart
c    0.145   0% lift
c    0.022   0% phase
c    0.010   0% cutwidth
c    0.002   0% ternres
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    3.374   0% probe simple     79%
c    0.433   0% probe basic      10%
c    0.484   0% probe tree-look  11%
c ==================================
c    1.500   0% preprocessing     4%
c   36.274   4% inprocessing     96%
c ==================================
c   37.773   4% simplifying
c  962.106  96% search
c ==================================
c  999.879 100% all
c 
c 8839582 decisions, 8840.7 decisions/sec
c 6646651 conflicts, 6647.5 conflicts/sec
c 375404396 propagations, 0.4 megaprops/sec
c 999.9 seconds, 90.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
