c launch: /data/cnf/sc2014/app/MD5-29-4.cnf.bz2
c host: atom02
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/MD5-29-4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-29-4.cnf.bz2
c no embedded options
c found 'p cnf 8590 65312' header
c read 8590 variables, 65312 clauses, 254884 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 8580 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    8580    65073         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 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 123 out of 123 constraints (100%) meet size limits
c [card-1] found 3 units
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 0 used 0%
c [card-1] exported 0 binary clauses, 0.0 per/constraint
c [decomp-1] removed 30 variables
c [simpleprobe-1] all 8560 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 8 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 8 variables, found 327 hbrs, 2 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 64 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8552 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 3036 variables 36% in round 1 in 10632206 steps
c [elim-1-1] backward subsumption/strengthening limit 21264412
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 5182238 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 3036 = 36% variables out of 8552
c [phase-1] phase bias: 1654 positive 30%, 3862 negative 70%
c [simplification-1] removed 3064 variables 35.7% (5516 remain 64%)
c [simplification-1] removed 7370 irredundant clauses 11.3% (57703 remain 89%)
c [simplification-1] maximum reduction of 36% = max (36%, 11%)
c [simplification-1] large reduction 36% >= 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] 28059, max 46544, min4 26796 at 75%, min10 11867 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.9    5516    57703         5       1      1   159   0  2.5  23.7    5
c R    0.9    5516    57703        20       2     13   159   0  2.1  61.1    5
c R    0.9    5516    57703        61      16     31   161   1  2.3  88.8    5
c R    0.9    5516    57703       164      65     58   167   1  2.8 102.3    5
c R    0.9    5516    57703       414     221    103   173   4  3.4 119.9    5
c R    1.0    5516    57703       981     573    213   182   6  3.5 152.7    5
c 
c [simplification-2] limit of 1026 conflicts hit after 1026 conflicts
c [simpleprobe-2] all 5516 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2453 variables remain 44% (3063 retained)
c [simpleprobe-2] removed 0 variables, found 21 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 11032 literals 100%
c [treelook-1] scheduling used 275042 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300190 steps
c [treelook-1] 8137 literals remain 74%
c [treelook-1] 5471 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 51 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 614 sched 11%, 0 failed, 0 lifted, 25 hbrs
c [basicprobe-1-1] 624 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 625 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 26 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5516 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 0 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 28 clauses out of 651 (4%) of length 6
c [cce-1-1] eliminated 7500 clauses out of 23015 (33%) of length 5
c [cce-1-1] eliminated 279 clauses out of 19584 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7807 large clauses in 9989036 steps
c [cce-1-1] allowing another 4994518 steps for small clauses
c [cce-1] scheduling 705 clauses = 472 binary + 233 ternary
c [cce-1] tried to eliminate 705 small clauses 100%
c [cce-1] eliminated 21 small clauses 3%
c [cce-1] eliminated 9 binary clauses 2%
c [cce-1] eliminated 12 ternary clauses 5%
c [cce-1-1] eliminated 21 small clauses in 5069789 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7828 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 684 clauses = 463 binary + 221 ternary
c [cce-1] tried to eliminate 684 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 7828 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5516 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 56 variables 1% in round 1 in 12859417 steps
c [elim-2-1] backward subsumption/strengthening limit 7140583
c [elim-2-1] subsumed 0 and strengthened 0 clauses in 3583639 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 56 = 1% variables out of 5516
c [bca-1] limit of 10000000 steps
c [bca-1] 9362 out of 10922 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 38519 steps
c [phase-2] phase bias: 9 positive 69%, 4 negative 31%
c [simplification-2] removed 56 variables 1.0% (5460 remain 64%)
c [simplification-2] removed 7967 irredundant clauses 13.8% (49736 remain 76%)
c [simplification-2] maximum reduction of 14% = max (1%, 14%)
c [simplification-2] large reduction 14% >= 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 3026
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.1    5460    49736      2278    1455    429   235   7  3.9 213.2    4
c 
c [simplification-3] limit of 3028 conflicts hit after 3028 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 5460 free variables schedulable
c [ternres-1] 3260 ternary resolvents (37 bin, 3223 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 7 at-most-one constraints of average size 3.0
c [card-2] found 10 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 17 out of 17 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 0 used 0%
c [card-2] exported 0 binary clauses, 0.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 15398 xors of average arity 3.6
c [gauss-1] connected 55640 occurrences of 4491 variables (average 12.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 5460 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 4055 probes 74%
c [lift-1-1] found 0 units 13 impls in round 1
c [lift-1] 0 units, 13 impls, 0 eqs in 2 rounds
c [lift-1] 1405 variables remain 26% (4055 retained)
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, 163 tauts, 0 hbrs, 42 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 9 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 36 clauses out of 15506 (0%) of length 5
c [cce-2-1] eliminated 100 clauses out of 19530 (1%) of length 4
c [cce-2-1] completed large round (ACCE)
c [cce-2-1] eliminated 136 large clauses in 13087409 steps
c [cce-2-1] allowing another 6543704 steps for small clauses
c [cce-2] scheduling 12493 clauses = 457 binary + 12036 ternary
c [cce-2] tried to eliminate 12493 small clauses 100%
c [cce-2] eliminated 76 small clauses 1%
c [cce-2] eliminated 6 binary clauses 1%
c [cce-2] eliminated 70 ternary clauses 1%
c [cce-2-1] eliminated 76 small clauses in 8917763 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] completed small and large (ACCE)
c [cce-2-1] eliminated 212 covered clauses in round 1
c [cce-2-2] completed large round (ACCE)
c [cce-2-2] allowing another 0 steps for small clauses
c [cce-2] scheduling 12417 clauses = 451 binary + 11966 ternary
c [cce-2] tried to eliminate 12417 small clauses 100%
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 212 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5460 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 2 variables 0% in round 1 in 12617020 steps
c [elim-3-1] backward subsumption/strengthening limit 7382980
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 3558453 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 2 = 0% variables out of 5460
c [elim-3] 2 < 1/1000 * 5460 = 5 considered unsuccessful
c [phase-3] phase bias: 118 positive 74%, 42 negative 26%
c [simplification-3] removed 2 variables 0.0% (5458 remain 64%)
c [simplification-3] removed 216 irredundant clauses 0.4% (49520 remain 76%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] new conflict limit 23028
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    3.7    5458    49520      5199    3573   4010   292   9  4.3 236.7    5
c -    4.1    5458    49520      8738    4231   4520   320   8  4.6 243.0    5
c R    4.3    5458    49520     11691    6560   4884   333  11  5.0 258.7    5
c -    4.6    5458    49520     14029    5958   5112   344  11  5.1 259.9    8
c -    5.3    5458    49520     20004    7710   5780   367   9  5.3 261.3    8
c 
c [simplification-4] limit of 23046 conflicts hit after 23046 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5458 free variables schedulable
c [ternres-2] 1260 ternary resolvents (3 bin, 1257 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5432 literals 50%
c [treelook-2] scheduling used 150039 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150142 steps
c [treelook-2] 3913 literals remain 36%
c [treelook-2] 2842 variables remain to probed next time 52%
c [treelook-2] removed 0 variables, found 16 hbrs
c [transred-2] limit 445185 with penalty 0 = 0 + 0
c [transred-2] removed 9 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5458 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 101 clauses out of 15348 (1%) of length 5
c [cce-3-1] eliminated 202 clauses out of 19502 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 303 large clauses in 13245805 steps
c [cce-3-1] allowing another 6622902 steps for small clauses
c [cce-3] scheduling 12437 clauses = 452 binary + 11985 ternary
c [cce-3] tried to eliminate 12437 small clauses 100%
c [cce-3] eliminated 2 small clauses 0%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3] eliminated 1 ternary clauses 0%
c [cce-3-1] eliminated 2 small clauses in 9096557 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 305 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 0 steps for small clauses
c [cce-3] scheduling 12435 clauses = 451 binary + 11984 ternary
c [cce-3] tried to eliminate 12435 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 305 covered clauses in TOTAL during 2 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 2902 out of 10918 literals actually usable 27%
c [bca-2] added 0 blocked clauses in 21840 steps
c [rephase-1] after 23046 conflicts (new increment 20000, next 43046)
c [flushphases] 187 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-4] removed 305 irredundant clauses 0.6% (49215 remain 76%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] new conflict limit 53046
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    6.3    5458    49215     25950   12808   7529   389  16  5.7 274.4    6
c -    6.4    5458    49215     26113    9433   7548   389  13  5.7 274.0    6
c -    7.2    5458    49215     33231   11372   8223   411  12  5.9 274.5    6
c -    8.1    5458    49215     40594   13191   8785   435  10  6.1 277.1    9
c -    9.1    5458    49215     48420   15094   9292   442  15  6.2 279.7    6
c 
c [simplification-5] limit of 53074 conflicts hit after 53075 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5458 free variables schedulable
c [ternres-3] 777 ternary resolvents (6 bin, 771 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4460 xors of average arity 3.0
c [gauss-2] connected 13380 occurrences of 1435 variables (average 9.3)
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 [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 5458 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 370822 with penalty 1 = 1 + 0
c [lift-2] using 503 probes 9%
c [lift-2-1] found 0 units 2 impls in round 1
c [lift-2-2] found 0 units 0 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] 0 units, 2 impls, 0 eqs in 5 rounds
c [lift-2] 902 variables remain 17% (4556 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1236073 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 54 clauses out of 15187 (0%) of length 5
c [cce-4-1] eliminated 108 clauses out of 19320 (1%) of length 4
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] eliminated 162 large clauses in 13062307 steps
c [cce-4-1] allowing another 6531153 steps for small clauses
c [cce-4] scheduling 733 clauses = 452 binary + 281 ternary
c [cce-4] tried to eliminate 733 small clauses 100%
c [cce-4] eliminated 6 small clauses 1%
c [cce-4] eliminated 6 ternary clauses 2%
c [cce-4-1] eliminated 6 small clauses in 6650004 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 168 covered clauses in round 1
c [cce-4-2] completed large round (ACCE)
c [cce-4-2] allowing another 0 steps for small clauses
c [cce-4] scheduling 727 clauses = 452 binary + 275 ternary
c [cce-4] tried to eliminate 727 small clauses 100%
c [cce-4-2] completed small round (ACCE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 168 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5458 variables 100%
c [elim-4] limit of 12360735 steps penalty 1 = 1 + 0
c [elim-4-1] no variable eliminated in round 1 in 12322460 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 5458
c [rephase-2] after 53075 conflicts (new increment 40000, next 93075)
c [flushphases] 29 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-5] removed 168 irredundant clauses 0.3% (49046 remain 75%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] new conflict limit 113075
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   10.7    5458    49046     55868   16563  10305   467  18  7.1 284.8    6
c R   10.8    5458    49046     57024   17665  10326   467  20  7.4 285.5    7
c -   11.8    5458    49046     64526   18448  10683   476  14  7.4 283.3    6
c -   12.9    5458    49046     73762   20552  11048   484  17  7.6 283.0    7
c -   13.9    5458    49046     82742   22092  11273   488  20  8.2 283.9    7
c -   15.3    5458    49046     92907   24094  11632   492  15  8.3 282.5    7
c -   16.8    5458    49046    103208   25761  11936   497  13  8.4 282.3    7
c 
c [simplification-6] limit of 113077 conflicts hit after 113077 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5458 free variables schedulable
c [ternres-4] 457 ternary resolvents (5 bin, 452 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 9 at-most-one constraints of average size 3.0
c [card-3] found 12 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 21 out of 21 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 1575929 penalty 1 = 1 + 0
c [basicprobe-2-0] 1019 sched 19%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-2-1] 1020 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 7 hbrs
c [unhide-3] limit 157592 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 15 tauts, 0 hbrs, 1892 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 4 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 42 clauses out of 15082 (0%) of length 5
c [cce-5-1] eliminated 83 clauses out of 19230 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 125 large clauses in 13342985 steps
c [cce-5-1] allowing another 6671492 steps for small clauses
c [cce-5] scheduling 750 clauses = 453 binary + 297 ternary
c [cce-5] tried to eliminate 750 small clauses 100%
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 125 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 0 steps for small clauses
c [cce-5] scheduling 750 clauses = 453 binary + 297 ternary
c [cce-5] tried to eliminate 750 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 125 covered clauses in TOTAL during 2 rounds
c [rephase-3] after 113077 conflicts (new increment 80000, next 193077)
c [flushphases] 5 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-6] removed 125 irredundant clauses 0.3% (48921 remain 75%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] new conflict limit 233077
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   18.1    5458    48921    113987   27522  12590   511  19  9.0 285.0    8
c R   18.8    5458    48921    124336   37581  12686   512  24  9.8 287.3   10
c -   18.9    5458    48921    124611   28844  12691   512  17  9.8 287.1    8
c -   20.6    5458    48921    137025   31010  13025   516  14  9.9 285.4    8
c -   22.3    5458    48921    149683   33142  13300   517  26 10.1 284.9    8
c -   24.1    5458    48921    162627   34998  13541   518  13 10.2 284.0    8
c -   25.9    5458    48921    176229   37102  13746   523  22 10.3 283.8    8
c -   27.8    5458    48921    190046   38960  13922   526  14 10.7 283.5   13
c -   30.0    5458    48921    204645   41047  14113   528  20 10.8 282.6    9
c -   32.2    5458    48921    219468   42946  14258   530  16 11.0 282.3    9
c 
c [simplification-7] limit of 233079 conflicts hit after 233080 conflicts
c [ternres-5] limit 7848533 with penalty 0 = 0 + 0
c [ternres-5] all 5458 free variables schedulable
c [ternres-5] 357 ternary resolvents (3 bin, 354 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5458 variables 100%
c [block-3] limit of 19621333 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 31 clauses out of 15010 (0%) of length 5
c [cce-6-1] eliminated 76 clauses out of 19143 (0%) of length 4
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] eliminated 107 large clauses in 13437490 steps
c [cce-6-1] allowing another 6718745 steps for small clauses
c [cce-6] scheduling 12482 clauses = 453 binary + 12029 ternary
c [cce-6] tried to eliminate 12482 small clauses 100%
c [cce-6] eliminated 2 small clauses 0%
c [cce-6] eliminated 2 ternary clauses 0%
c [cce-6-1] eliminated 2 small clauses in 9408411 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 109 covered clauses in round 1
c [cce-6-2] completed large round (ACCE)
c [cce-6-2] allowing another 0 steps for small clauses
c [cce-6] scheduling 12480 clauses = 453 binary + 12027 ternary
c [cce-6] tried to eliminate 12480 small clauses 100%
c [cce-6-2] completed small round (ACCE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 109 covered clauses in TOTAL during 2 rounds
c [bca-3] limit of 10000000 steps
c [bca-3] 1038 out of 10918 literals actually usable 10%
c [bca-3] added 0 blocked clauses in 60522 steps
c [rephase-4] after 233080 conflicts (new increment 160000, next 393080)
c [flushphases] 3 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-7] removed 109 irredundant clauses 0.2% (48812 remain 75%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] new conflict limit 473080
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.9    5458    48812    234793   44926  14726   535  26 11.3 282.2   10
c -   36.3    5458    48812    249930   46230  14776   535  23 13.4 283.4   10
c -   37.7    5458    48812    265614   47651  14831   535  26 14.6 284.3    9
c R   38.0    5458    48812    269179   51050  14839   535  30 15.1 284.5   12
c -   40.4    5458    48812    282544   49456  15021   537  13 14.9 283.3   16
c -   43.2    5458    48812    299996   51533  15158   537  18 14.8 282.8   10
c -   46.3    5458    48812    318004   53741  15288   537  24 14.7 281.5   16
c -   49.1    5458    48812    336073   55415  15403   537  20 14.9 281.4   17
c -   52.3    5458    48812    355113   57527  15520   540  15 14.8 280.8   11
c -   55.8    5458    48812    374812   59870  15662   540  22 14.7 279.8   11
c -   57.8    5458    48812    394006   61031  15691   540  16 16.2 280.8   11
c -   61.9    5458    48812    414597   63206  15815   542  16 16.1 279.3   11
c -   65.5    5458    48812    435787   65539  15918   545  19 16.0 278.6   18
c -   68.7    5458    48812    456987   67310  16023   545  14 16.1 278.4   11
c 
c [simplification-8] limit of 473080 conflicts hit after 473081 conflicts
c [ternres-6] limit 19104408 with penalty 0 = 0 + 0
c [ternres-6] all 5458 free variables schedulable
c [ternres-6] 252 ternary resolvents (3 bin, 249 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 955220 penalty 2 = 2 + 0
c [gauss-3] extracted 2990 xors of average arity 3.0
c [gauss-3] connected 8970 occurrences of 1352 variables (average 6.6)
c [gauss-3] limit 955220 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2418 schedulable variables 44%
c [simpleprobe-3] limit 38208817 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 21 hbrs, 0 units
c [cgrclsr-3] limit 477610 penalty 2 = 2 + 0
c [cgrclsr-3] all 5458 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 2865661 with penalty 2 = 2 + 0
c [lift-3] using 282 probes 5%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 1 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, 1 impls, 0 eqs in 6 rounds
c [lift-3] 620 variables remain 11% (4838 retained)
c [cliff-3] limit of 3820881 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 18 transitive binary clauses
c [cce-7] limit of 38208817 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 20 clauses out of 14964 (0%) of length 5
c [cce-7-1] eliminated 37 clauses out of 19064 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 57 large clauses in 13323403 steps
c [cce-7-1] allowing another 6661701 steps for small clauses
c [cce-7] scheduling 12493 clauses = 453 binary + 12040 ternary
c [cce-7] tried to eliminate 12493 small clauses 100%
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 57 covered clauses in round 1
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] allowing another 0 steps for small clauses
c [cce-7] scheduling 12493 clauses = 453 binary + 12040 ternary
c [cce-7] tried to eliminate 12493 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 57 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5458 variables 100%
c [elim-5] limit of 95522042 steps penalty 2 = 2 + 0
c [elim-5-1] no variable eliminated in round 1 in 12145278 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 5458
c [rephase-5] after 473081 conflicts (new increment 320000, next 793081)
c [flushphases] 0 phases reset
c [simplification-8] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-8] removed 58 irredundant clauses 0.1% (48754 remain 75%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 240000
c [simplification-8] new conflict interval 480000
c [simplification-8] penalized conflict interval 480000 = 1 * 480000
c [simplification-8] new conflict limit 953081
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   74.2    5458    48754    478959   69407  16347   552  19 16.0 277.9   19
c -   78.5    5458    48754    501553   71771  16418   553  26 16.1 277.1   13
c -   81.0    5458    48754    524400   73319  16439   553  29 18.1 278.0   12
c -   83.4    5458    48754    546954   74365  16461   553  27 19.3 278.8   13
c -   85.9    5458    48754    570326   75939  16480   553  25 20.1 280.1   13
c R   86.8    5458    48754    579508   84869  16485   553  29 20.9 280.5   20
c -   90.3    5458    48754    594511   77601  16545   553  17 20.7 279.7   21
c -   95.4    5458    48754    619640   79830  16616   553  16 20.5 278.9   21
c -  100.2    5458    48754    644977   81848  16662   553  16 20.4 278.5   13
c -  105.5    5458    48754    671163   83931  16707   554  19 20.9 277.8   21
c -  109.9    5458    48754    697431   85805  16743   554  30 21.5 277.7   13
c -  115.5    5458    48754    724361   87292  16787   554  18 22.5 277.1   14
c -  121.7    5458    48754    752152   89818  16858   554  23 22.2 276.5   22
c -  127.3    5458    48754    779868   91556  16928   555  14 22.4 276.0   14
c -  133.9    5458    48754    808669   94016  16993   556  21 22.3 275.3   23
c -  137.1    5458    48754    837108   95470  17024   556  25 22.9 276.3   14
c -  142.8    5458    48754    866283   97149  17054   556  16 23.3 276.0   23
c -  150.0    5458    48754    896432   99433  17121   556  19 23.1 275.3   23
c -  156.8    5458    48754    926886  101380  17179   556  16 23.2 274.9   15
c 
c [simplification-9] limit of 953081 conflicts hit after 953081 conflicts
c [ternres-7] limit 47234683 with penalty 0 = 0 + 0
c [ternres-7] all 5458 free variables schedulable
c [ternres-7] 155 ternary resolvents (2 bin, 153 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 5 transitive binary clauses
c [cce-8] limit of 94469366 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 16 clauses out of 14927 (0%) of length 5
c [cce-8-1] eliminated 24 clauses out of 19034 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 40 large clauses in 13638762 steps
c [cce-8-1] allowing another 6819381 steps for small clauses
c [cce-8] scheduling 776 clauses = 453 binary + 323 ternary
c [cce-8] tried to eliminate 776 small clauses 100%
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 40 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 776 clauses = 453 binary + 323 ternary
c [cce-8] tried to eliminate 776 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 40 covered clauses in TOTAL during 2 rounds
c [cce-8] 40 < 1/1000 * 48754 = 48 considered unsuccessful
c [rephase-6] after 953081 conflicts (new increment 640000, next 1593081)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-9] removed 40 irredundant clauses 0.1% (48714 remain 75%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 480000
c [simplification-9] new conflict interval 960000
c [simplification-9] penalized conflict interval 960000 = 1 * 960000
c [simplification-9] new conflict limit 1913081
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  164.2    5458    48714    958089  103739  17397   553  23 23.0 274.6   16
c -  170.3    5458    48714    989426  105244  17432   553  17 24.2 274.6   16
c -  178.2    5458    48714   1021694  107597  17494   553  23 24.0 274.0   17
c -  185.6    5458    48714   1054153  109636  17557   553  24 23.9 273.8   17
c -  192.7    5458    48714   1087363  111957  17611   556  34 24.1 273.5   17
c -  197.3    5458    48714   1120691  112982  17622   556  31 25.6 274.1   16
c -  205.0    5458    48714   1156430  113850  17623   556  33 29.2 274.6   16
c -  209.6    5458    48714   1190520  114833  17627   556  26 30.6 275.2   17
c -  216.5    5458    48714   1226307  115697  17631   556  31 33.1 275.6   18
c -  225.4    5458    48714   1261872  117136  17669   556  16 33.8 275.3   17
c -  233.5    5458    48714   1298156  119511  17718   557  24 33.5 275.0   17
c -  243.8    5458    48714   1334784  121793  17763   557  27 33.1 274.2   17
c -  251.1    5458    48714   1371604  123640  17799   557  18 32.9 274.4   18
c -  259.5    5458    48714   1410346  125453  17819   558  35 33.9 274.2   17
c -  268.7    5458    48714   1451699  126175  17825   558  35 36.9 274.5   18
c -  276.4    5458    48714   1490436  127910  17853   559  30 37.3 274.5   18
c -  285.5    5458    48714   1529682  129338  17890   561  19 37.9 274.4   18
c -  295.4    5458    48714   1569551  131733  17940   561  15 37.4 274.2   18
c -  307.3    5458    48714   1609986  134206  17996   561  19 37.0 273.5   29
c -  316.8    5458    48714   1650780  136328  18045   561  17 36.9 273.4   18
c -  327.8    5458    48714   1692211  138893  18097   561  22 36.5 273.2   19
c -  340.2    5458    48714   1733776  141033  18137   561  18 36.0 272.6   19
c -  347.5    5458    48714   1776597  143338  18167   561  28 36.3 273.0   18
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  356.4    5458    48714   1821604  144380  18180   561  34 38.3 273.4   18
c -  368.8    5458    48714   1865148  146329  18222   561  24 38.4 273.1   19
c -  380.9    5458    48714   1908492  148250  18260   561  14 38.0 272.9   19
c 
c [simplification-10] limit of 1913083 conflicts hit after 1913083 conflicts
c [ternres-8] limit 121641146 with penalty 0 = 0 + 0
c [ternres-8] all 5458 free variables schedulable
c [ternres-8] 191 ternary resolvents (9 bin, 182 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 7602571 penalty 3 = 3 + 0
c [card-4] found 10 at-most-one constraints of average size 3.0
c [card-4] found 23 at-most-two constraints of average size 4.1
c [card-4] using previous limit 7602571 for elimination
c [card-4] 32 out of 33 constraints (97%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 714 tauts, 0 hbrs, 4123 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 0 transitive binary clauses
c [rephase-7] after 1913083 conflicts (new increment 1280000, next 3193083)
c [flushphases] 0 phases reset
c [simplification-10] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-10] removed 0 irredundant clauses 0.0% (48714 remain 75%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
c [simplification-10] new conflict interval 1920000
c [simplification-10] penalized conflict interval 1920000 = 1 * 1920000
c [simplification-10] new conflict limit 3833083
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  392.6    5458    48714   1952881  150193  18001   564  16 37.9 272.8   33
c -  406.5    5458    48714   1997862  152697  18039   564  24 37.5 272.3   21
c -  420.4    5458    48714   2043245  155055  18075   564  15 37.1 271.9   22
c -  428.9    5458    48714   2089725  157169  18098   564  29 37.6 272.3   21
c -  444.0    5458    48714   2135707  159166  18141   564  19 37.3 271.8   22
c -  458.3    5458    48714   2182557  161492  18175   564  16 37.0 271.5   22
c -  471.2    5458    48714   2230376  163577  18210   564  18 37.0 271.3   35
c -  486.2    5458    48714   2278258  166026  18244   564  21 36.7 271.0   35
c -  500.1    5458    48714   2326438  168143  18268   564  26 36.5 270.8   22
c -  510.0    5458    48714   2376824  169172  18272   564  33 38.2 271.2   21
c -  520.8    5458    48714   2429166  170204  18275   564  31 40.3 271.5   21
c -  533.0    5458    48714   2481601  171041  18281   564  28 42.2 271.9   23
c -  541.5    5458    48714   2532353  172106  18289   564  28 43.2 272.4   21
c -  552.2    5458    48714   2584953  173213  18293   564  32 44.7 272.8   21
c -  563.0    5458    48714   2637953  173996  18294   564  30 46.2 273.3   22
c R  564.6    5458    48714   2648142  183738  18294   564  28 46.4 273.3   35
c -  580.3    5458    48714   2689752  175936  18330   564  17 45.9 272.9   23
c -  597.7    5458    48714   2742456  178595  18376   565  26 45.5 272.5   23
c -  613.5    5458    48714   2795635  180873  18416   565  27 45.3 272.4   23
c -  631.8    5458    48714   2848915  183131  18456   565  18 44.9 272.0   24
c -  644.9    5458    48714   2903013  185154  18484   565  28 44.9 272.0   24
c -  663.0    5458    48714   2957930  187139  18511   565  20 44.9 271.8   24
c -  682.4    5458    48714   3013060  189499  18547   565  17 44.6 271.4   24
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  699.9    5458    48714   3068685  191969  18583   565  20 44.3 271.4   24
c -  719.4    5458    48714   3124859  194393  18616   565  28 44.0 271.1   24
c -  734.8    5458    48714   3182384  196442  18640   566  34 44.4 271.0   24
c -  755.6    5458    48714   3244848  197148  18641   566  36 46.4 271.3   26
c -  773.6    5458    48714   3302435  198796  18660   566  24 46.4 271.2   25
c -  792.7    5458    48714   3360478  200922  18691   566  14 46.2 271.0   25
c -  812.7    5458    48714   3419458  203206  18717   567  17 46.0 270.8   25
c -  830.3    5458    48714   3479036  205518  18739   567  32 46.1 270.7   25
c -  850.0    5458    48714   3539687  207108  18754   567  16 46.4 270.6   25
c -  873.3    5458    48714   3599607  209435  18784   567  17 46.0 270.3   25
c -  894.7    5458    48714   3660490  211897  18809   567  26 45.8 270.1   25
c -  918.8    5458    48714   3721529  214271  18845   567  17 45.5 269.7   26
c -  931.5    5458    48714   3783392  215953  18861   567  26 45.8 270.0   25
c 
c [simplification-11] limit of 3833083 conflicts hit after 3833084 conflicts
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 5458 free variables schedulable
c [ternres-9] 279 ternary resolvents (7 bin, 272 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 3883351 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5921 literals 54%
c [treelook-3] scheduling used 984194 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3883351 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 630974 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 5 hbrs
c [block-4] scheduling all variables this time
c [block-4] scheduled 5458 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 [cce-9] limit of 310668156 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 24 clauses out of 14886 (0%) of length 5
c [cce-9-1] eliminated 52 clauses out of 19011 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 76 large clauses in 13582163 steps
c [cce-9-1] allowing another 6791081 steps for small clauses
c [cce-9] scheduling 12510 clauses = 457 binary + 12053 ternary
c [cce-9] tried to eliminate 12510 small clauses 100%
c [cce-9] eliminated 4 small clauses 0%
c [cce-9] eliminated 3 binary clauses 1%
c [cce-9] eliminated 1 ternary clauses 0%
c [cce-9-1] eliminated 4 small clauses in 9615830 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 80 covered clauses in round 1
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] allowing another 0 steps for small clauses
c [cce-9] scheduling 12506 clauses = 454 binary + 12052 ternary
c [cce-9] tried to eliminate 12506 small clauses 100%
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 0 covered clauses in round 2
c [cce-9] eliminated 80 covered clauses in TOTAL during 2 rounds
c [bca-4] limit of 10000000 steps
c [bca-4] 430 out of 10918 literals actually usable 4%
c [bca-4] added 0 blocked clauses in 264359 steps
c [rephase-8] after 3833084 conflicts (new increment 2560000, next 6393084)
c [flushphases] 0 phases reset
c [simplification-11] removed 0 variables 0.0% (5458 remain 64%)
c [simplification-11] removed 80 irredundant clauses 0.2% (48634 remain 75%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1920000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] new conflict limit 4833084
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  944.9    5458    48634   3847258  217507  19137   582  27 46.6 270.5   29
c -  964.1    5458    48634   3911189  218829  19149   583  16 47.2 270.6   29
c -  989.2    5458    48634   3974360  221331  19179   583  25 46.8 270.3   29
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: 4 count, 0 added (0 skipped), 385240 steps
c bkwd: tried 156959 clauses, 313918 lits, 2.00 lits/clause
c bkwd: checked 6303005 occs, 40.16 occs/clause, 20.08 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: 4 bces, 0 removed, 1845282 resolutions, 3990868 steps
c blkd: 1 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 3 units, 0 am1, 12336016 steps
c card: 60 rescheduled, 255 eliminated, 45348 resolved, 3241 subsumed
c card: 29 at-most-one constraints found, average size 3.00
c card: 29 at-most-one constraints used 100%, average size 3.00
c card: 165 at-most-two constraints found, average size 4.01
c card: 164 at-most-two constraints used 99%, average size 4.01
c cces: 9 cces, 8924 eliminated, 8923 ate 100%, 1 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: 3 count, 777628 esteps, 63036 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: 2308 extracted (94 ands 4%, 2000 xors 87%, 214 ites 9%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 409567 decisions, 7768628 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 320196 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 52 gcs, 0 rescored clauses, 2091 rescored vars
c dcps: 20 decompositions, 23 equivalent 0%
c deco: 109055 decision-only clauses 3%, 47% reduction
c decs: 57668228 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3502966 flipped 6.074% (in 7454 phases)
c elms: 5 elims, 3094 eliminated 36%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 3094 small 100%, 0 large 0%
c elms: 20002 tried small, 3094 succeeded 15%, 16908 failed 85%
c elms: 349 subsumed, 302 strengthened, 0 blocked
c elms: 1525898 copies, 2832971 resolutions, 1904843 ipos
c elms: 45297 subchks, 40817 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 22848 extracted, 3.4 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7910680 steps, 3955340 extr 50%, 2727749 elim 34%
c glue: 46.7 orig avg, 45.6 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 538 = 369 simple + 161 trn 69% + 8 lrg 30%, 24 sub 1%
c hght: 270 average, 5.79 height/glue
c ints: 102396 luby (30003043 steps), 0 inout (0 steps)
c lift: 3 phases, 45445 probed (15152 level1 33%, 30293 level2 67%)
c lift: 0 units, 0 equivalences, 16 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3975746 clauses, 88.0 length
c lrnd: 1760485 uips 44%, 1718376 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 350056243 learned lits, 12% minimized
c mins: 3522317 mins 89%, 29 bin 0%, 344345 size 9%, 109055 deco 3%
c move: moved 3975746, 19 bin 0%, 134 trn 0%, 0 lrg 0%
c otfs: str 89204 dyn (88553 red, 651 irr) 27527 drv 31%, 61677 rst 69%
c otfs: sub 456 dyn (455 red, 1 irr)
c phas: 7 computed, 5689 set, 1781 pos (31%), 3908 neg (69%)
c prbs: 2 basic, 7804 probed, 0 failed, 0 lifted
c prbs: 3 simple, 31099 probed, 2 failed, 17 eqs
c prbs: 3 treelook, 10335 probed, 0 failed, 0 lifted
c prps: 901292278 props, 16 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 47957796 searches, 1895071 hits, 4% 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: 117 count, 0 reset, 2 acts 2%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 117 arith 100%, 0 double 0%
c rmbd: 50 removed, 50 red 100%
c rphs: 8 recomputed phases
c rsts: 90936 restarts 89%, 11460 skipped 11%
c rsts: 0 saturating 0%, 7218 agile 63%, 4242 reuse 37%
c rsts: 43.6 avg interval, 43.6 scaled, 1.0 factor
c rsts: 13187 kept 14.5% average 36.7%
c simp: 11 count (11 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3975746 count (6394901 tried 1.6), 89287 sub out of 3966491 (2.3%)
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: 15 fixed 0%, 0 its, 0.00 confs/it
c trvs: 53505111446 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 59.4 search traversals per propagation, 13363.0 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 8 transitive reductions, 51 removed, 0 failed
c trds: 87102 nodes, 7508 edges, 10800 steps
c trim: 3342480 words, 12.8 MB
c trnr: 9 count, 75 bin, 6913 trn, 29014108 steps
c unhd: 4 count, 6 rounds, 3015670 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: 976 tauts, 0 bin 0%, 756 trn 77%, 207 lrg 21%
c unhd: 976 tauts, 13 stamp 1%, 934 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6121 str, 0 bin 0%, 82 trn 1%, 6039 lrg 99%, 6023 red 98%
c vars: 5458 remaining 64% and 3132 removed 36% out of 8590
c vars: 15 fixed 0%, 3094 eliminated 36%, 23 equivalent 0%
c vsts: 32888043444 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 36.5 search visits per propagation, 8213.0 per conflict
c wchs: 8968511372 pushed, 11780614 enlarged, 811 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3966491 100   3622656 100 239930155 100  43327412 100   1961002 100
c 
c  0     166650   4         0   0 191350269  80< 25963974  60   1091264  56 
c  1     260244   7    197334   5  27377338  11   4948695  11<   240897  12 
c  2     784321  20    774914  21   8046506   3   3320347   8    152166   8<
c  3     723199  18    713734  20   5792697   2   3007763   7    136343   7 
c  4     490913  12    484629  13   3158233   1   1913643   4     86432   4 
c  5     334883   8<   330679   9<  1547899   1   1131017   3     52095   3 
c  6     245502   6    243075   7    862598   0    738397   2     37811   2 
c  7     189321   5    187807   5    492630   0    502731   1     28655   1 
c  8     151659   4    150583   4    291394   0    357846   1     22611   1 
c  9     124236   3    123362   3    197829   0    277623   1     19432   1 
c 10     186720   5    185261   5    264310   0    413534   1     34930   2 
c 11     134986   3    125309   3    198818   0    317641   1     34930   2 
c 12     173505   4    105727   3    349037   0    433381   1     23362   1 
c 13        352   0       242   0       597   0       820   0        74   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             4.6           4.7           0.4           1.4           1.7
c std             3.2           3.0           1.2           2.4           2.8
c 
c   70.035   7% analysis
c   58.524   6% decide
c   12.966   1% bump
c   11.132   1% defrag
c   11.129   1% restart
c    5.987   1% mincls
c    3.499   0% cce
c    2.725   0% elim
c    2.054   0% reduce
c    1.619   0% gc
c    1.010   0% decomp
c    0.806   0% probe
c    0.381   0% block
c    0.357   0% cliff
c    0.343   0% backward
c    0.280   0% gauss
c    0.246   0% bca
c    0.227   0% ternres
c    0.219   0% unhide
c    0.210   0% card
c    0.145   0% lift
c    0.120   0% cgrclsr
c    0.075   0% phase
c    0.011   0% transred
c    0.002   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.223   0% probe simple     28%
c    0.085   0% probe basic      11%
c    0.497   0% probe tree-look  62%
c ==================================
c    0.890   0% preprocessing     9%
c    9.363   1% inprocessing     91%
c ==================================
c   10.252   1% simplifying
c  989.800  99% search
c ==================================
c 1000.052 100% all
c 
c 57668228 decisions, 57665.2 decisions/sec
c 4003273 conflicts, 4003.1 conflicts/sec
c 901292278 propagations, 0.9 megaprops/sec
c 1000.1 seconds, 128.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
