c launch: /data/cnf/sc2014/app/006-23-80.cnf.bz2
c host: atom06
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/006-23-80.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/006-23-80.cnf.bz2
c no embedded options
c found 'p cnf 4288 132592' header
c read 4288 variables, 132592 clauses, 873647 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 3829 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    3829    76353         0       0      0     0   0  0.0   0.0    4
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 3 at-most-one constraints of average size 3.0
c [card-1] found 7 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 10 constraints (90%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 611 variables
c [simpleprobe-1] all 3677 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 91 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 91 variables, found 9 hbrs, 39 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 664 tauts, 0 hbrs, 21 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3586 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 143 variables 4% in round 1 in 4149715 steps
c [elim-1-1] backward subsumption/strengthening limit 8299430
c [elim-1-1] subsumed 3931 and strengthened 1897 clauses in 8299570 steps
c [elim-1-1] rescheduled 2661 variables 74% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 1407068 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 143 = 4% variables out of 3586
c [phase-1] phase bias: 1411 positive 41%, 2032 negative 59%
c [simplification-1] removed 359 variables 9.4% (3443 remain 90%)
c [simplification-1] removed 10543 irredundant clauses 13.8% (65810 remain 86%)
c [simplification-1] maximum reduction of 14% = max (9%, 14%)
c [simplification-1] large reduction 14% >= 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] 8842, max 11970, min4 8898 at 70%, min10 7726 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    0.8    3443    65810        20      13      1     5   1  3.5  17.3    5
c R    0.8    3443    65810        60      38      3     5   1  3.6  61.8    5
c R    0.8    3443    65810       162     122      6     5   1  4.2  90.6    5
c R    0.8    3443    65810       410     334     14     5   2  4.6 109.5    5
c R    0.9    3443    65810       983     810     27     8   4  4.7 194.2    5
c 
c [simplification-2] limit of 1006 conflicts hit after 1006 conflicts
c [simpleprobe-2] all 3443 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1121 variables remain 33% (2322 retained)
c [simpleprobe-2] removed 0 variables, found 3 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6886 literals 100%
c [treelook-1] scheduling used 283165 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300171 steps
c [treelook-1] 5634 literals remain 82%
c [treelook-1] 3430 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 16 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 388 sched 11%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-1-1] 398 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 16 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3443 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 61 blocked clauses
c [block-1] 61 < 1/1000 * 65810 = 65 considered unsuccessful
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 998 clauses out of 18278 (5%) of length 7
c [cce-1-1] eliminated 578 clauses out of 22444 (3%) of length 6
c [cce-1-1] eliminated 1987 clauses out of 13056 (15%) of length 5
c [cce-1-1] eliminated 251 clauses out of 7068 (4%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 3814 large clauses in 36606098 steps
c [cce-1-1] allowing another 18303049 steps for small clauses
c [cce-1] scheduling 695 clauses = 257 binary + 438 ternary
c [cce-1] tried to eliminate 695 small clauses 100%
c [cce-1] eliminated 43 small clauses 6%
c [cce-1] eliminated 4 binary clauses 2%
c [cce-1] eliminated 39 ternary clauses 9%
c [cce-1-1] eliminated 43 small clauses in 18442011 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3857 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 652 clauses = 253 binary + 399 ternary
c [cce-1] tried to eliminate 652 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 3857 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3443 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 1043 not tried 30% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 18 = 1% variables out of 3443
c [bca-1] limit of 10000000 steps
c [bca-1] 5216 out of 6852 literals actually usable 76%
c [bca-1] added 0 blocked clauses in 35226 steps
c [phase-2] phase bias: 17 positive 22%, 59 negative 78%
c [simplification-2] removed 18 variables 0.5% (3425 remain 89%)
c [simplification-2] removed 4313 irredundant clauses 6.6% (61497 remain 81%)
c [simplification-2] maximum reduction of 7% = max (1%, 7%)
c [simplification-2] large reduction 7% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 3006
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.4    3425    61497      2283    1933     92    33   6  5.0 243.9    5
c 
c [simplification-3] limit of 3008 conflicts hit after 3010 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 3425 free variables schedulable
c [ternres-1] 187 ternary resolvents (17 bin, 170 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 4 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4 out of 4 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 3889 xors of average arity 4.9
c [gauss-1] connected 18967 occurrences of 825 variables (average 23.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 3 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 3422 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 1489 probes 44%
c [lift-1-1] found 1 units 14 impls in round 1
c [lift-1-2] found 0 units 10 impls in round 2
c [lift-1] 2 units, 34 impls, 4 eqs in 3 rounds
c [lift-1] 1932 variables remain 57% (1484 retained)
c [lift-1] removed 6 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 51 tauts, 0 hbrs, 59 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 11 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 3 clauses out of 17364 (0%) of length 7
c [cce-2-1] eliminated 8 clauses out of 21268 (0%) of length 6
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] eliminated 11 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 4461 clauses = 268 binary + 4193 ternary
c [cce-2] tried to eliminate 4461 small clauses 100%
c [cce-2] eliminated 1043 small clauses 23%
c [cce-2] eliminated 5 binary clauses 2%
c [cce-2] eliminated 1038 ternary clauses 25%
c [cce-2-1] eliminated 1043 small clauses in 16326920 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] eliminated 1054 covered clauses in round 1
c [cce-2-2] eliminated 21 clauses out of 11156 (0%) of length 5
c [cce-2-2] eliminated 20 clauses out of 6812 (0%) of length 4
c [cce-2-2] completed large round (ACCE)
c [cce-2-2] eliminated 41 large clauses in 10935232 steps
c [cce-2-2] allowing another 5467616 steps for small clauses
c [cce-2] scheduling 3418 clauses = 263 binary + 3155 ternary
c [cce-2] tried to eliminate 3418 small clauses 100%
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] completed small and large (ACCE)
c [cce-2-2] eliminated 41 covered clauses in round 2
c [cce-2-3] completed large round (ACCE)
c [cce-2-3] allowing another 0 steps for small clauses
c [cce-2] scheduling 3418 clauses = 263 binary + 3155 ternary
c [cce-2] tried to eliminate 3418 small clauses 100%
c [cce-2-3] completed small round (ACCE)
c [cce-2-3] eliminated 0 covered clauses in round 3
c [cce-2] eliminated 1095 covered clauses in TOTAL during 3 rounds
c [elim-3] 1043 variables 31% will be scheduled this time
c [elim-3] scheduled 1043 variables 31%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 373 not tried 11% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 3416
c [phase-3] phase bias: 21 positive 68%, 10 negative 32%
c [simplification-3] removed 9 variables 0.3% (3416 remain 89%)
c [simplification-3] removed 1129 irredundant clauses 1.8% (60368 remain 79%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] new conflict limit 9676
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    4.2    3416    60368      5204    4466   1225    61   6  5.3 327.4    5
c -    4.3    3416    60368      5613    2796   1236    61   6  5.3 324.4    5
c 
c [simplification-4] limit of 9680 conflicts hit after 9680 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3416 free variables schedulable
c [ternres-2] 65 ternary resolvents (6 bin, 59 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3657 literals 54%
c [treelook-2] scheduling used 150020 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150557 steps
c [treelook-2] 3016 literals remain 44%
c [treelook-2] 2766 variables remain to probed next time 81%
c [treelook-2] removed 0 variables, found 10 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 34 probes 1%
c [lift-2-1] found 0 units 0 impls in round 1
c [lift-2-2] found 0 units 2 impls in round 2
c [lift-2-3] found 0 units 0 impls in round 3
c [lift-2-4] found 0 units 0 impls in round 4
c [lift-2-5] found 0 units 0 impls in round 5
c [lift-2] 0 units, 2 impls, 0 eqs in 6 rounds
c [lift-2] 1898 variables remain 56% (1518 retained)
c [transred-2] limit 137644 with penalty 0 = 0 + 0
c [transred-2] removed 2 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3416 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 [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 43 clauses out of 21347 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 43 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 682 clauses = 269 binary + 413 ternary
c [cce-3] tried to eliminate 682 small clauses 100%
c [cce-3] eliminated 3 small clauses 0%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 3 small clauses in 15188693 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 46 covered clauses in round 1
c [cce-3-2] eliminated 2 clauses out of 11186 (0%) of length 5
c [cce-3-2] eliminated 19 clauses out of 6790 (0%) of length 4
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 21 large clauses in 10979467 steps
c [cce-3-2] allowing another 5489733 steps for small clauses
c [cce-3] scheduling 679 clauses = 268 binary + 411 ternary
c [cce-3] tried to eliminate 679 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 21 covered clauses in round 2
c [cce-3-3] completed large round (ACCE)
c [cce-3-3] allowing another 0 steps for small clauses
c [cce-3] scheduling 679 clauses = 268 binary + 411 ternary
c [cce-3] tried to eliminate 679 small clauses 100%
c [cce-3-3] completed small round (ACCE)
c [cce-3-3] eliminated 0 covered clauses in round 3
c [cce-3] eliminated 67 covered clauses in TOTAL during 3 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 2268 out of 6834 literals actually usable 33%
c [bca-2] added 0 blocked clauses in 20846 steps
c [phase-4] phase bias: 1 positive 50%, 1 negative 50%
c [simplification-4] removed 0 variables 0.0% (3416 remain 89%)
c [simplification-4] removed 67 irredundant clauses 0.1% (60301 remain 79%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] new conflict limit 36346
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -    5.8    3416    60301      9680    3808   1396    84   6  5.4 330.8    4
c R    5.9    3416    60301     11684    5588   1445    88  10  5.7 334.2    5
c -    6.1    3416    60301     14343    4922   1506    90   8  5.8 319.0    5
c -    6.5    3416    60301     19490    5960   1644    96   9  6.2 304.1    8
c -    6.9    3416    60301     25279    7178   1772   104  16  6.8 302.7    8
c R    6.9    3416    60301     25925    7775   1782   104  18  7.1 302.9    9
c -    7.4    3416    60301     31460    8195   1910   113  11  7.2 292.5    8
c 
c [simplification-5] limit of 36396 conflicts hit after 36397 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3416 free variables schedulable
c [ternres-3] 59 ternary resolvents (4 bin, 55 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1537 xors of average arity 4.7
c [gauss-2] connected 7157 occurrences of 446 variables (average 16.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 3414 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 1, lifted 0
c [transred-3] limit 521309 with penalty 0 = 0 + 0
c [transred-3] removed 9 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 19 clauses out of 21375 (0%) of length 6
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 19 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 739 clauses = 288 binary + 451 ternary
c [cce-4] tried to eliminate 739 small clauses 100%
c [cce-4] eliminated 4 small clauses 1%
c [cce-4] eliminated 4 ternary clauses 1%
c [cce-4-1] eliminated 10 small clauses in 15212995 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 29 covered clauses in round 1
c [cce-4-2] eliminated 18 clauses out of 11221 (0%) of length 5
c [cce-4-2] eliminated 50 clauses out of 6718 (1%) of length 4
c [cce-4-2] completed large round (ACCE)
c [cce-4-2] eliminated 68 large clauses in 10891917 steps
c [cce-4-2] allowing another 5445958 steps for small clauses
c [cce-4] scheduling 735 clauses = 288 binary + 447 ternary
c [cce-4] tried to eliminate 735 small clauses 100%
c [cce-4-2] completed small round (ACCE)
c [cce-4-2] eliminated 68 covered clauses in round 2
c [cce-4-3] completed large round (ACCE)
c [cce-4-3] allowing another 0 steps for small clauses
c [cce-4] scheduling 735 clauses = 288 binary + 447 ternary
c [cce-4] tried to eliminate 735 small clauses 100%
c [cce-4-3] completed small round (ACCE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 97 covered clauses in TOTAL during 3 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3413 variables 100%
c [elim-4] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-4] incomplete 1569 not tried 46% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 1 = 0% variables out of 3413
c [elim-4] 1 < 1/1000 * 3413 = 3 considered unsuccessful
c [rephase-1] after 36397 conflicts (new increment 20000, next 56397)
c [flushphases] 4 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 4 variables 0.1% (3412 remain 89%)
c [simplification-5] removed 124 irredundant clauses 0.2% (60177 remain 79%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 26666
c [simplification-5] new conflict interval 53332
c [simplification-5] penalized conflict interval 53332 = 1 * 53332
c [simplification-5] new conflict limit 89729
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -    9.4    3412    60177     38274    9374   2049   123  11  7.4 289.5    6
c -   10.0    3412    60177     45671   10546   2199   124  10  7.6 282.6    9
c -   10.5    3412    60177     53470   11689   2300   131  12  7.9 287.9    9
c R   10.7    3412    60177     56983   14973   2332   131  18  8.3 288.8   10
c -   11.2    3412    60177     61856   12888   2413   133  11  8.3 284.8   10
c -   12.0    3412    60177     70814   14166   2567   136   9  8.5 285.2   10
c -   12.9    3412    60177     80379   15417   2708   137  15  8.6 286.6   10
c 
c [simplification-6] limit of 89759 conflicts hit after 89759 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 3412 free variables schedulable
c [ternres-4] 94 ternary resolvents (6 bin, 88 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] found 9 at-most-two constraints of average size 4.1
c [card-3] using previous limit 500000 for elimination
c [card-3] 10 out of 10 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1 variables
c [basicprobe-2] limit 729422 penalty 1 = 1 + 0
c [basicprobe-2-0] 508 sched 15%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-2-1] 510 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 15 hbrs
c [bate-1] eliminated 7 asymmetric tautologies during probing
c [lift-3] limit 437653 with penalty 1 = 1 + 0
c [lift-3] using 229 probes 7%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 2 impls in round 2
c [lift-3-3] found 0 units 0 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 2 impls, 0 eqs in 6 rounds
c [lift-3] 1669 variables remain 49% (1742 retained)
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 0
c [unhide-3] limit 72942 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 50 tauts, 0 hbrs, 1088 literals
c [transred-4] limit 1458844 with penalty 0 = 0 + 0
c [transred-4] removed 7 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 10 clauses out of 21474 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 10 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 3471 clauses = 294 binary + 3177 ternary
c [cce-5] tried to eliminate 3471 small clauses 100%
c [cce-5] eliminated 5 small clauses 0%
c [cce-5] eliminated 5 ternary clauses 0%
c [cce-5-1] eliminated 5 small clauses in 16159857 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 15 covered clauses in round 1
c [cce-5-2] eliminated 20 clauses out of 11188 (0%) of length 5
c [cce-5-2] eliminated 53 clauses out of 6639 (1%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 73 large clauses in 10775002 steps
c [cce-5-2] allowing another 5387501 steps for small clauses
c [cce-5] scheduling 3466 clauses = 294 binary + 3172 ternary
c [cce-5] tried to eliminate 3466 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 73 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 0 steps for small clauses
c [cce-5] scheduling 3466 clauses = 294 binary + 3172 ternary
c [cce-5] tried to eliminate 3466 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 88 covered clauses in TOTAL during 3 rounds
c [rephase-2] after 89759 conflicts (new increment 40000, next 129759)
c [flushphases] 0 phases reset
c [simplification-6] removed 1 variables 0.0% (3411 remain 89%)
c [simplification-6] removed 100 irredundant clauses 0.2% (60077 remain 79%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 53332
c [simplification-6] new conflict interval 106664
c [simplification-6] penalized conflict interval 106664 = 1 * 106664
c [simplification-6] new conflict limit 196423
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.1    3411    60077     90448   16676   2892   157  13  8.9 283.7    7
c -   16.1    3411    60077    100844   17852   3009   158   9  9.1 283.8   10
c -   16.9    3411    60077    111891   19313   3096   160  22  9.7 287.6   10
c -   17.6    3411    60077    122466   20051   3123   161  33 12.9 290.5   10
c -   18.5    3411    60077    133548   20638   3168   161   9 15.0 289.9   11
c -   19.7    3411    60077    146381   22305   3280   161  18 14.9 287.3   11
c -   21.0    3411    60077    159110   23229   3375   162  12 15.2 286.9    7
c -   22.5    3411    60077    173123   24877   3506   162  17 15.0 286.4    7
c -   23.6    3411    60077    186787   25840   3578   162  15 15.3 286.6    7
c 
c [simplification-7] limit of 196431 conflicts hit after 196431 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 3411 free variables schedulable
c [ternres-5] 51 ternary resolvents (7 bin, 44 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3411 variables 100%
c [block-3] limit of 12500000 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 [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 13 clauses out of 21612 (0%) of length 6
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 13 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 803 clauses = 294 binary + 509 ternary
c [cce-6] tried to eliminate 803 small clauses 100%
c [cce-6] eliminated 4 small clauses 0%
c [cce-6] eliminated 4 ternary clauses 1%
c [cce-6-1] eliminated 4 small clauses in 15246743 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 17 covered clauses in round 1
c [cce-6-2] eliminated 6 clauses out of 11160 (0%) of length 5
c [cce-6-2] eliminated 26 clauses out of 6593 (0%) of length 4
c [cce-6-2] completed large round (ACCE)
c [cce-6-2] eliminated 32 large clauses in 10952466 steps
c [cce-6-2] allowing another 5476233 steps for small clauses
c [cce-6] scheduling 799 clauses = 294 binary + 505 ternary
c [cce-6] tried to eliminate 799 small clauses 100%
c [cce-6-2] completed small round (ACCE)
c [cce-6-2] eliminated 32 covered clauses in round 2
c [cce-6-3] completed large round (ACCE)
c [cce-6-3] allowing another 0 steps for small clauses
c [cce-6] scheduling 799 clauses = 294 binary + 505 ternary
c [cce-6] tried to eliminate 799 small clauses 100%
c [cce-6-3] completed small round (ACCE)
c [cce-6-3] eliminated 0 covered clauses in round 3
c [cce-6] eliminated 49 covered clauses in TOTAL during 3 rounds
c [cce-6] 49 < 1/1000 * 60077 = 60 considered unsuccessful
c [bca-3] limit of 10000000 steps
c [bca-3] 107 out of 6824 literals actually usable 2%
c [bca-3] added 0 blocked clauses in 35725 steps
c [rephase-3] after 196431 conflicts (new increment 80000, next 276431)
c [flushphases] 0 phases reset
c [simplification-7] removed 0 variables 0.0% (3411 remain 89%)
c [simplification-7] removed 49 irredundant clauses 0.1% (60028 remain 79%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 106664
c [simplification-7] new conflict interval 213328
c [simplification-7] penalized conflict interval 213328 = 1 * 213328
c [simplification-7] new conflict limit 409759
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   26.3    3411    60028    201566   27173   3742   168  14 15.3 283.8   12
c -   28.0    3411    60028    216793   28510   3839   170  14 15.3 282.8   12
c -   29.5    3411    60028    232673   30121   3937   170  18 15.4 282.2    8
c -   30.6    3411    60028    248207   31198   3972   170  35 17.3 284.4   13
c -   32.2    3411    60028    263762   31760   3973   170  36 22.4 285.4    8
c -   33.8    3411    60028    279656   32113   3991   170  19 25.1 286.1    8
c -   35.7    3411    60028    297488   33436   4084   172  16 24.6 284.7   13
c -   38.0    3411    60028    315817   34782   4174   172  12 24.1 282.6   13
c -   39.9    3411    60028    334448   36055   4267   172  13 24.0 283.1   13
c -   42.2    3411    60028    353751   37406   4357   172  13 23.8 282.8   13
c -   44.8    3411    60028    373750   38828   4454   174  19 23.4 280.2   14
c -   46.3    3411    60028    393483   40034   4474   174  33 24.8 281.5    9
c 
c [simplification-8] limit of 409765 conflicts hit after 409765 conflicts
c [ternres-6] limit 9934764 with penalty 0 = 0 + 0
c [ternres-6] all 3411 free variables schedulable
c [ternres-6] 26 ternary resolvents (2 bin, 24 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 134 xors of average arity 3.0
c [gauss-3] connected 402 occurrences of 62 variables (average 6.5)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1112 schedulable variables 33%
c [simpleprobe-3] limit 19869528 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 15 hbrs, 0 units
c [cgrclsr-3] limit 248369 penalty 2 = 2 + 0
c [cgrclsr-3] all 3411 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-4] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-4] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 9 transitive binary clauses
c [elim-5] 372 variables 11% will be scheduled this time
c [elim-5] scheduled 372 variables 11%
c [elim-5] limit of 49673821 steps penalty 2 = 2 + 0
c [elim-5-1] no variable eliminated in round 1 in 27326335 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 3411
c [rephase-4] after 409765 conflicts (new increment 160000, next 569765)
c [flushphases] 0 phases reset
c [simplification-8] removed 0 variables 0.0% (3411 remain 89%)
c [simplification-8] removed 8 irredundant clauses 0.0% (60020 remain 79%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 213328
c [simplification-8] new conflict interval 426656
c [simplification-8] penalized conflict interval 426656 = 1 * 426656
c [simplification-8] new conflict limit 836421
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   49.0    3411    60020    413142   40488   4522   184  15 26.3 281.7   15
c -   51.7    3411    60020    434397   41828   4598   184  16 26.1 280.4   14
c -   54.0    3411    60020    456126   43120   4660   184  18 25.9 279.8    9
c -   56.8    3411    60020    478275   44345   4745   184  15 25.5 278.7   15
c -   59.9    3411    60020    501124   45875   4811   184  20 25.3 277.2   15
c -   61.9    3411    60020    523552   46729   4825   184  37 27.5 278.0   10
c -   64.4    3411    60020    546474   47364   4829   184  35 30.9 278.7   10
c -   66.9    3411    60020    569370   47939   4832   184  40 32.7 279.4   10
c -   70.0    3411    60020    592672   48472   4832   184  41 34.4 280.1   10
c -   72.9    3411    60020    616605   49007   4832   184  40 36.2 280.8   10
c -   76.0    3411    60020    640904   49516   4832   184  41 37.6 281.5   10
c -   79.3    3411    60020    665884   50106   4832   184  35 39.3 282.2   16
c -   82.7    3411    60020    691373   50628   4833   184  38 41.3 282.9   16
c -   86.3    3411    60020    717426   51097   4833   184  38 43.8 283.6   16
c -   90.2    3411    60020    743922   51615   4833   184  36 45.7 284.3   11
c -   94.6    3411    60020    771314   52141   4833   184  38 47.9 285.0   11
c -   98.6    3411    60020    798668   52623   4833   184  37 49.2 285.8   11
c -  102.5    3411    60020    826825   53192   4835   184  39 50.8 286.5   11
c 
c [simplification-9] limit of 836421 conflicts hit after 836422 conflicts
c [ternres-7] limit 30412039 with penalty 0 = 0 + 0
c [ternres-7] all 3411 free variables schedulable
c [ternres-7] 21 ternary resolvents (1 bin, 20 trn)
c [ternres-7] fully completed ternary resolution
c [lift-4] limit 4561805 with penalty 2 = 2 + 0
c [lift-4] using 262 probes 8%
c [lift-4-1] found 0 units 0 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 0 impls in round 5
c [lift-4] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-4] 1407 variables remain 41% (2004 retained)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [cce-7] limit of 30412039 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 7 clauses out of 21856 (0%) of length 6
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 7 large clauses in 30412040 steps
c [cce-7-1] allowing another 15206020 steps for small clauses
c [cce-7] scheduling 3497 clauses = 297 binary + 3200 ternary
c [cce-7] tried to eliminate 3497 small clauses 100%
c [cce-7] eliminated 5 small clauses 0%
c [cce-7] eliminated 5 ternary clauses 0%
c [cce-7-1] eliminated 5 small clauses in 16400726 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 12 covered clauses in round 1
c [cce-7-2] eliminated 9 clauses out of 11158 (0%) of length 5
c [cce-7-2] eliminated 20 clauses out of 6571 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 29 large clauses in 10932022 steps
c [cce-7-2] allowing another 5466011 steps for small clauses
c [cce-7] scheduling 3492 clauses = 297 binary + 3195 ternary
c [cce-7] tried to eliminate 3492 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 29 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 0 steps for small clauses
c [cce-7] scheduling 3492 clauses = 297 binary + 3195 ternary
c [cce-7] tried to eliminate 3492 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 41 covered clauses in TOTAL during 3 rounds
c [cce-7] 41 < 1/1000 * 60020 = 60 considered unsuccessful
c [rephase-5] after 836422 conflicts (new increment 320000, next 1156422)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (3411 remain 89%)
c [simplification-9] removed 41 irredundant clauses 0.1% (59979 remain 79%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 426656
c [simplification-9] new conflict interval 853312
c [simplification-9] penalized conflict interval 853312 = 1 * 853312
c [simplification-9] new conflict limit 1689734
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  106.6    3411    59979    855738   54049   4871   184  37 51.7 287.7   11
c -  110.6    3411    59979    885549   54791   4918   184  17 51.4 286.4   18
c -  114.6    3411    59979    916906   56311   4967   184  38 52.0 285.8   11
c -  119.4    3411    59979    948820   56900   4968   184  37 55.2 286.4   11
c -  123.6    3411    59979    980438   57284   4974   184  34 57.5 287.1   11
c -  128.3    3411    59979   1012569   58274   5054   184  17 56.6 285.1   18
c -  132.1    3411    59979   1045307   59500   5090   184  36 56.6 284.7   11
c -  136.3    3411    59979   1078130   60098   5122   184  17 56.9 284.2   12
c -  140.0    3411    59979   1111625   61185   5146   184  36 57.2 284.7   12
c -  144.0    3411    59979   1146596   62016   5153   184  35 58.9 285.5   12
c -  149.3    3411    59979   1181711   62577   5159   184  36 60.8 286.0   12
c -  154.2    3411    59979   1216917   63076   5161   184  37 62.3 286.6   12
c -  159.2    3411    59979   1252416   63599   5161   184  35 63.6 287.1   18
c -  164.7    3411    59979   1288748   64149   5161   184  34 65.0 287.7   18
c -  169.5    3411    59979   1325020   64660   5164   184  36 65.9 288.2   19
c -  174.9    3411    59979   1362679   65138   5164   184  36 67.4 288.8   19
c -  180.6    3411    59979   1400638   65634   5164   184  35 68.6 289.3   19
c -  186.7    3411    59979   1439866   66121   5165   184  38 70.2 289.9   19
c -  192.4    3411    59979   1478656   66671   5165   184  35 71.1 290.5   12
c -  197.0    3411    59979   1517867   67334   5171   184  40 71.9 291.2   12
c -  203.1    3411    59979   1557701   67874   5171   184  37 72.6 291.7   19
c -  209.0    3411    59979   1598370   68415   5174   184  36 73.7 292.3   19
c -  217.5    3411    59979   1641972   68933   5176   184  38 75.9 292.9   19
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  226.9    3411    59979   1686743   69352   5176   184  38 78.2 293.5   19
c 
c [simplification-10] limit of 1689734 conflicts hit after 1689736 conflicts
c [ternres-8] limit 79345113 with penalty 0 = 0 + 0
c [ternres-8] all 3411 free variables schedulable
c [ternres-8] 2 ternary resolvents (1 bin, 1 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4959069 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 10 at-most-two constraints of average size 4.1
c [card-4] using previous limit 4959069 for elimination
c [card-4] 12 out of 12 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 2 at-most-one constraints, 2 used 100%
c [card-4] exported 2 binary clauses, 1.0 per/constraint
c [unhide-4] limit 1983627 with penalty 3 = 3 + 0
c [unhide-4-8] 0 units, 0 failed, 199 tauts, 0 hbrs, 13677 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 0 transitive binary clauses
c [rephase-6] after 1689736 conflicts (new increment 640000, next 2329736)
c [flushphases] 0 phases reset
c [simplification-10] removed 0 variables 0.0% (3411 remain 89%)
c [simplification-10] removed 1 irredundant clauses 0.0% (59978 remain 79%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 853312
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] new conflict limit 2689736
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  233.1    3411    59978   1728530   70041   5057   181  39 78.7 294.1   13
c -  240.7    3411    59978   1771369   70568   5059   181  40 79.7 294.9   13
c -  249.1    3411    59978   1814779   71074   5060   181  40 80.9 295.6   19
c -  257.2    3411    59978   1858417   71621   5061   181  38 81.9 296.4   19
c -  266.4    3411    59978   1906271   72103   5062   181  37 84.2 297.1   19
c -  274.9    3411    59978   1951737   72642   5063   181  40 85.5 297.9   19
c -  283.2    3411    59978   1997108   73188   5063   181  41 86.4 298.6   19
c -  292.0    3411    59978   2043184   73709   5063   181  41 87.3 299.3   19
c -  300.8    3411    59978   2089036   74204   5063   181  38 88.0 300.1   19
c -  310.2    3411    59978   2135212   74738   5063   181  41 88.5 300.8   19
c -  319.8    3411    59978   2182384   75199   5064   181  41 89.2 301.5   19
c -  329.4    3411    59978   2230086   75727   5064   181  39 90.0 302.3   20
c -  339.6    3411    59978   2279043   76247   5065   181  40 90.8 303.0   20
c -  350.1    3411    59978   2328743   76742   5065   181  40 91.7 303.8   19
c -  361.1    3411    59978   2378889   77302   5065   181  40 92.6 304.5   20
c -  371.1    3411    59978   2428666   77787   5065   181  42 93.2 305.2   20
c -  382.4    3411    59978   2480109   78313   5065   181  42 94.0 306.0   20
c -  392.9    3411    59978   2530689   78768   5065   181  41 94.4 306.7   20
c -  404.3    3411    59978   2582588   79258   5065   181  41 95.1 307.4   20
c -  415.0    3411    59978   2634769   79816   5065   181  41 95.6 308.2   15
c -  427.3    3411    59978   2688110   80373   5065   181  41 96.4 308.9   15
c 
c [simplification-11] limit of 2689736 conflicts hit after 2689738 conflicts
c [ternres-9] limit 164905609 with penalty 0 = 0 + 0
c [ternres-9] all 3411 free variables schedulable
c [ternres-9] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 2061320 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5584 literals 82%
c [treelook-3] scheduling used 538120 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2061320 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1281370 steps
c [treelook-3] fully completed tree based probing
c [cliff-5] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-5] failed 0, lifted 0
c [block-4] scheduling all variables this time
c [block-4] scheduled 3411 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 15 out of 6824 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 81987 steps
c [rephase-7] after 2689738 conflicts (new increment 1280000, next 3969738)
c [flushphases] 0 phases reset
c [simplification-11] removed 0 variables 0.0% (3411 remain 89%)
c [simplification-11] removed 0 irredundant clauses 0.0% (59978 remain 79%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] new conflict interval 2000000
c [simplification-11] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-11] new conflict limit 4689738
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  437.5    3411    59978   2741162   81945   5161   181  25 95.1 305.1   15
c -  444.8    3411    59978   2793907   82594   5166   181  32 94.8 305.8   13
c -  454.4    3411    59978   2848669   83230   5166   181  33 95.1 306.4   20
c -  463.5    3411    59978   2902449   83727   5167   181  36 95.0 307.1   20
c -  472.9    3411    59978   2957186   84318   5167   181  35 94.9 307.7   20
c -  482.1    3411    59978   3012002   84844   5167   181  35 94.8 308.4   20
c -  492.6    3411    59978   3068205   85328   5167   181  35 95.0 309.0   20
c -  502.7    3411    59978   3126065   85981   5171   181  39 95.6 309.6   15
c -  513.0    3411    59978   3184990   86677   5182   181  34 96.0 309.6   15
c -  519.7    3411    59978   3243636   87648   5199   181  31 96.0 310.4   15
c -  528.8    3411    59978   3302014   88463   5227   181  36 95.7 309.3   15
c -  537.6    3411    59978   3360459   88966   5228   181  37 95.6 309.9   15
c -  549.9    3411    59978   3420569   89476   5229   181  37 95.8 310.4   23
c -  558.4    3411    59978   3479980   90089   5229   181  34 95.7 310.9   23
c -  568.0    3411    59978   3540189   90537   5229   181  38 95.6 311.4   23
c -  578.2    3411    59978   3600379   91078   5229   181  37 95.5 311.9   16
c -  591.7    3411    59978   3662351   91552   5229   181  37 95.7 312.4   16
c -  603.2    3411    59978   3723988   91997   5229   181  36 95.7 312.9   16
c -  617.2    3411    59978   3786311   92559   5229   181  38 95.7 313.4   16
c -  632.3    3411    59978   3850068   93081   5230   181  37 95.9 313.9   25
c -  644.6    3411    59978   3913349   93541   5230   181  36 95.9 314.4   25
c -  659.5    3411    59978   3977491   94082   5230   181  34 96.0 314.9   26
c -  673.2    3411    59978   4042088   94590   5230   181  38 96.1 315.4   25
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  688.0    3411    59978   4107364   95093   5230   181  38 96.2 315.9   26
c -  701.3    3411    59978   4172841   95594   5230   181  36 96.2 316.3   26
c -  715.4    3411    59978   4239182   96112   5230   181  38 96.3 316.8   26
c -  730.5    3411    59978   4305406   96632   5230   181  38 96.3 317.3   26
c -  746.0    3411    59978   4372203   97057   5230   181  37 96.3 317.8   26
c -  761.8    3411    59978   4440808   97618   5231   181  36 96.5 318.3   25
c -  778.2    3411    59978   4509054   98141   5231   181  36 96.6 318.7   25
c -  795.5    3411    59978   4578035   98565   5231   181  36 96.7 319.2   25
c -  813.0    3411    59978   4648186   99182   5231   181  36 96.9 319.7   26
c 
c [simplification-12] limit of 4689738 conflicts hit after 4689738 conflicts
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3411 free variables schedulable
c [ternres-10] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 5274 xors of average arity 5.1
c [gauss-4] connected 26878 occurrences of 1062 variables (average 25.3)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] connected 5159 occurrences of 1062 variables (average 4.9)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 3411 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [transred-9] limit 1000000 with penalty 1 = 1 + 0
c [transred-9] removed 0 transitive binary clauses
c [cce-8] limit of 166196228 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 5 clauses out of 21929 (0%) of length 6
c [cce-8-1] eliminated 4 clauses out of 11156 (0%) of length 5
c [cce-8-1] eliminated 7 clauses out of 6548 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 16 large clauses in 43600911 steps
c [cce-8-1] allowing another 21800455 steps for small clauses
c [cce-8] scheduling 3503 clauses = 300 binary + 3203 ternary
c [cce-8] tried to eliminate 3503 small clauses 100%
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 16 covered clauses in round 1
c [cce-8-2] completed large round (ACCE)
c [cce-8-2] allowing another 0 steps for small clauses
c [cce-8] scheduling 3503 clauses = 300 binary + 3203 ternary
c [cce-8] tried to eliminate 3503 small clauses 100%
c [cce-8-2] completed small round (ACCE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 16 covered clauses in TOTAL during 2 rounds
c [cce-8] 16 < 1/1000 * 59978 = 59 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 3411 variables 100%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6-1] eliminated 1 variables 0% in round 1 in 48021188 steps
c [elim-6-1] backward subsumption/strengthening limit 51978812
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 9538629 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 1 = 0% variables out of 3411
c [elim-6] 1 < 1/1000 * 3411 = 3 considered unsuccessful
c [rephase-8] after 4689738 conflicts (new increment 2560000, next 7249738)
c [flushphases] 0 phases reset
c [simplification-12] removed 1 variables 0.0% (3410 remain 89%)
c [simplification-12] removed 17 irredundant clauses 0.0% (59961 remain 79%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 2000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 5689738
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  827.7    3410    59961   4717639  100161   5264   180  24 96.5 318.2   28
c -  837.0    3410    59961   4787168  101552   5293   180  32 95.9 317.6   18
c -  850.1    3410    59961   4856633  102197   5313   180  21 95.4 316.7   28
c -  862.4    3410    59961   4928360  103376   5331   180  38 95.4 316.3   16
c -  879.7    3410    59961   5001802  104009   5332   180  36 95.8 316.9   25
c -  897.3    3410    59961   5075350  104495   5332   180  37 96.2 317.4   25
c -  909.3    3410    59961   5147769  105064   5335   180  36 96.3 318.0   25
c -  927.3    3410    59961   5219965  105543   5335   180  37 96.3 318.5   16
c -  944.9    3410    59961   5292719  106111   5335   180  37 96.3 319.0   25
c -  963.3    3410    59961   5367299  106635   5335   180  36 96.5 319.5   25
c -  982.4    3410    59961   5441329  107159   5335   180  37 96.5 320.0   25
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 7 basic ate = 6 trn 86% + 1 lrg 14% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 173784 steps
c bkwd: tried 107736 clauses, 209918 lits, 1.95 lits/clause
c bkwd: checked 8435194 occs, 78.30 occs/clause, 40.18 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 3931 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 1894 large (1% self)
c blkd: 4 bces, 61 removed, 3053913 resolutions, 6336692 steps
c blkd: 12 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 2 am1, 9622292 steps
c card: 1 rescheduled, 7 eliminated, 9711 resolved, 3082 subsumed
c card: 6 at-most-one constraints found, average size 3.00
c card: 6 at-most-one constraints used 100%, average size 3.00
c card: 30 at-most-two constraints found, average size 4.10
c card: 29 at-most-two constraints used 97%, average size 4.10
c cces: 8 cces, 5304 eliminated, 5304 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 1548371 esteps, 32918 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: 774 extracted (41 ands 5%, 522 xors 67%, 211 ites 27%)
c clff: 5 cliffs, 0 lifted, 1 failed
c clff: 966846 decisions, 20063985 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1006239 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 60 gcs, 0 rescored clauses, 2874 rescored vars
c dcps: 19 decompositions, 180 equivalent 4%
c deco: 320006 decision-only clauses 6%, 47% reduction
c decs: 21323370 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 739341 flipped 3.467% (in 1812 phases)
c elms: 6 elims, 163 eliminated 4%
c elms: 8 rounds, 1.3 rounds/bve
c elms: 163 small 100%, 0 large 0%
c elms: 2135 tried small, 163 succeeded 8%, 1972 failed 92%
c elms: 1756 subsumed, 1507 strengthened, 3 blocked
c elms: 1316059 copies, 3218764 resolutions, 600354 ipos
c elms: 217319 subchks, 144922 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 10834 extracted, 4.9 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 19500316 steps, 9750158 extr 50%, 442242 elim 2%
c glue: 96.5 orig avg, 94.1 real avg, 7.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 124 = 27 simple + 90 trn 22% + 7 lrg 73%, 51 sub 6%
c hght: 320 average, 3.32 height/glue
c ints: 131071 luby (40501279 steps), 0 inout (0 steps)
c lift: 4 phases, 39913 probed (13310 level1 33%, 26603 level2 67%)
c lift: 2 units, 4 equivalences, 38 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5464639 clauses, 206.5 length
c lrnd: 1676224 uips 31%, 3424064 flips 63%
c mega: 0 count, 0 failed, 0 rounds
c mins: 1128676760 learned lits, 10% minimized
c mins: 4953434 mins 91%, 34 bin 0%, 191165 size 3%, 320006 deco 6%
c move: moved 5464639, 10 bin 0%, 1313 trn 0%, 0 lrg 0%
c otfs: str 228981 dyn (227340 red, 1641 irr) 50165 drv 22%, 178816 rst 78%
c otfs: sub 865 dyn (865 red, 0 irr)
c phas: 5 computed, 3552 set, 1450 pos (41%), 2102 neg (59%)
c prbs: 2 basic, 3608 probed, 0 failed, 0 lifted
c prbs: 3 simple, 14600 probed, 39 failed, 84 eqs
c prbs: 3 treelook, 7477 probed, 0 failed, 0 lifted
c prps: 692004749 props, 32 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 35131820 searches, 951809 hits, 3% 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: 139 count, 0 reset, 2 acts 1%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 139 arith 100%, 0 double 0%
c rmbd: 29 removed, 18 red 62%
c rphs: 8 recomputed phases
c rsts: 22480 restarts 17%, 108591 skipped 83%
c rsts: 1 saturating 0%, 106534 agile 98%, 2056 reuse 2%
c rsts: 247.8 avg interval, 247.8 scaled, 1.0 factor
c rsts: 4616 kept 20.5% average 49.1%
c simp: 12 count (12 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 5464639 count (18246990 tried 3.3), 214784 sub out of 5462887 (3.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: 535 fixed 12%, 0 its, 0.00 confs/it
c trvs: 67337121444 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 97.4 search traversals per propagation, 12206.4 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 9 transitive reductions, 40 removed, 0 failed
c trds: 60948 nodes, 3948 edges, 5984 steps
c trim: 8883646 words, 33.9 MB
c trnr: 10 count, 44 bin, 482 trn, 9442923 steps
c unhd: 4 count, 8 rounds, 2867172 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: 964 tauts, 0 bin 0%, 656 trn 68%, 303 lrg 31%
c unhd: 964 tauts, 5 stamp 1%, 508 red 53%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 14845 str, 0 bin 0%, 27 trn 0%, 14818 lrg 100%, 14784 red 100%
c vars: 3410 remaining 80% and 878 removed 20% out of 4288
c vars: 535 fixed 12%, 163 eliminated 4%, 180 equivalent 4%
c vsts: 40954058314 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 59.2 search visits per propagation, 7422.4 per conflict
c wchs: 12441969703 pushed, 6788898 enlarged, 214 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   5462887 100   5066852 100 286516639 100  90583250 100   2783857 100
c 
c  0      38242   1         0   0  90388054  32  20176184  22    426266  15 
c  1      82796   2     34000   1 100932326  35  24140394  27    536682  19 
c  2     276626   5    249374   5  39490475  14< 12815780  14    403098  14 
c  3     349484   6    344970   7  22197094   8   9178984  10<   376924  14 
c  4     370695   7    364320   7  15069449   5   7544542   8    258308   9<
c  5     427122   8    419607   8   7570673   3   4609405   5    159705   6 
c  6     459907   8    452244   9   3757272   1   2773934   3    103879   4 
c  7     471661   9    463629   9   2027789   1   1847783   2     72459   3 
c  8     467782   9<   459460   9<  1224564   0   1395784   2     56743   2 
c  9     457202   8    449243   9    851998   0   1161602   1     51728   2 
c 10     873715  16    858349  17   1229038   0   2007179   2    112678   4 
c 11     771035  14    729468  14    985062   0   1863898   2    183190   7 
c 12     415866   8    241626   5    791615   0   1065985   1     42051   2 
c 13        754   0       562   0      1230   0      1796   0       146   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.6           7.6           1.5           2.6           3.6
c std             3.1           3.0           1.8           2.9           3.4
c 
c  140.412  14% analysis
c   27.168   3% bump
c   19.993   2% decide
c    7.442   1% cce
c    3.971   0% mincls
c    2.893   0% elim
c    2.443   0% reduce
c    1.638   0% gc
c    1.616   0% restart
c    1.498   0% defrag
c    1.130   0% cliff
c    0.795   0% decomp
c    0.566   0% backward
c    0.566   0% probe
c    0.460   0% block
c    0.381   0% gauss
c    0.344   0% cgrclsr
c    0.330   0% unhide
c    0.194   0% lift
c    0.143   0% card
c    0.088   0% bca
c    0.060   0% ternres
c    0.048   0% phase
c    0.010   0% transred
c    0.003   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    0.327   0% probe simple     58%
c    0.060   0% probe basic      11%
c    0.178   0% probe tree-look  32%
c ==================================
c    0.801   0% preprocessing     5%
c   14.208   1% inprocessing     95%
c ==================================
c   15.009   2% simplifying
c  984.964  98% search
c ==================================
c  999.973 100% all
c 
c 21323370 decisions, 21323.9 decisions/sec
c 5514804 conflicts, 5515.0 conflicts/sec
c 692004749 propagations, 0.7 megaprops/sec
c 1000.0 seconds, 140.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
