c launch: /data/cnf/sc2014/app/MD5-28-5.cnf.bz2
c host: atom04
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-28-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-28-5.cnf.bz2
c no embedded options
c found 'p cnf 8279 62533' header
c read 8279 variables, 62533 clauses, 243687 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 8270 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    8270    62320         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 4 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] 124 out of 124 constraints (100%) meet size limits
c [card-1] found 5 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 32 variables
c [simpleprobe-1] all 8247 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 15 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 15 variables, found 331 hbrs, 5 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 8232 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 3168 variables 38% in round 1 in 10417875 steps
c [elim-1-1] backward subsumption/strengthening limit 20835750
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 4613650 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 3168 = 38% variables out of 8232
c [phase-1] phase bias: 1526 positive 30%, 3538 negative 70%
c [simplification-1] removed 3206 variables 38.8% (5064 remain 61%)
c [simplification-1] removed 10155 irredundant clauses 16.3% (52165 remain 84%)
c [simplification-1] maximum reduction of 39% = max (39%, 16%)
c [simplification-1] large reduction 39% >= 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] 26327, max 44043, min4 26032 at 25%, min10 10451 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    5064    52165         5       3      0   148   0  3.3  30.5    4
c R    0.8    5064    52165        20       4     13   148   0  2.2  77.4    4
c R    0.9    5064    52165        61      14     26   153   0  2.4  69.4    4
c R    0.9    5064    52165       165      57     64   157   1  2.7  85.2    4
c R    0.9    5064    52165       410     194    117   164   3  3.1 102.0    4
c R    0.9    5064    52165       983     548    246   173   6  3.4 132.0    4
c 
c [simplification-2] limit of 1028 conflicts hit after 1028 conflicts
c [simpleprobe-2] all 5064 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2082 variables remain 41% (2982 retained)
c [simpleprobe-2] removed 0 variables, found 25 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10128 literals 100%
c [treelook-1] scheduling used 249347 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300003 steps
c [treelook-1] 7105 literals remain 70%
c [treelook-1] 3982 variables remain to probed next time 79%
c [treelook-1] removed 0 variables, found 73 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 604 sched 12%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-1-1] 608 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 22 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5064 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 8 blocked clauses
c [block-1] 8 < 1/1000 * 52165 = 52 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 45 clauses out of 660 (7%) of length 6
c [cce-1-1] eliminated 6752 clauses out of 20508 (33%) of length 5
c [cce-1-1] eliminated 277 clauses out of 17880 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7074 large clauses in 8773447 steps
c [cce-1-1] allowing another 4386723 steps for small clauses
c [cce-1] scheduling 11757 clauses = 454 binary + 11303 ternary
c [cce-1] tried to eliminate 11757 small clauses 100%
c [cce-1] eliminated 225 small clauses 2%
c [cce-1] eliminated 5 binary clauses 1%
c [cce-1] eliminated 220 ternary clauses 2%
c [cce-1-1] eliminated 225 small clauses in 6129104 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7299 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 11532 clauses = 449 binary + 11083 ternary
c [cce-1] tried to eliminate 11532 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 7299 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5064 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 32 variables 1% in round 1 in 11183572 steps
c [elim-2-1] backward subsumption/strengthening limit 8816428
c [elim-2-1] subsumed 0 and strengthened 0 clauses in 3142776 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 32 = 1% variables out of 5064
c [bca-1] limit of 10000000 steps
c [bca-1] 8695 out of 10066 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 35604 steps
c [phase-2] phase bias: 34 positive 72%, 13 negative 28%
c [simplification-2] removed 32 variables 0.6% (5032 remain 61%)
c [simplification-2] removed 7347 irredundant clauses 14.1% (44818 remain 72%)
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 3028
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.0    5032    44818      2297    1475    562   272   7  3.9 176.4    4
c 
c [simplification-3] limit of 3030 conflicts hit after 3030 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 5032 free variables schedulable
c [ternres-1] 3047 ternary resolvents (30 bin, 3017 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 at-most-one constraints of average size 3.0
c [card-2] found 6 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 7 out of 7 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 16205 xors of average arity 3.7
c [gauss-1] connected 59416 occurrences of 4694 variables (average 12.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 2 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 5030 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 3782 probes 75%
c [lift-1-1] found 0 units 5 impls in round 1
c [lift-1] 0 units, 5 impls, 0 eqs in 2 rounds
c [lift-1] 1248 variables remain 25% (3782 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, 142 tauts, 0 hbrs, 67 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 40 clauses out of 13726 (0%) of length 5
c [cce-2-1] eliminated 47 clauses out of 17730 (0%) of length 4
c [cce-2-1] completed large round (ACCE)
c [cce-2-1] eliminated 87 large clauses in 11539641 steps
c [cce-2-1] allowing another 5769820 steps for small clauses
c [cce-2] scheduling 746 clauses = 444 binary + 302 ternary
c [cce-2] tried to eliminate 746 small clauses 100%
c [cce-2] eliminated 8 small clauses 1%
c [cce-2] eliminated 1 binary clauses 0%
c [cce-2] eliminated 7 ternary clauses 2%
c [cce-2-1] eliminated 8 small clauses in 5876097 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] completed small and large (ACCE)
c [cce-2-1] eliminated 95 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 738 clauses = 443 binary + 295 ternary
c [cce-2] tried to eliminate 738 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 95 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5030 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] no variable eliminated in round 1 in 11064608 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 5030
c [phase-3] phase bias: 116 positive 74%, 40 negative 26%
c [simplification-3] removed 2 variables 0.0% (5030 remain 61%)
c [simplification-3] removed 103 irredundant clauses 0.2% (44715 remain 72%)
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 23030
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    3.3    5030    44715      5231    3572   3883   319   9  4.3 222.3    4
c -    3.8    5030    44715      8964    4337   4453   341   7  4.5 247.3    4
c R    4.0    5030    44715     11706    6568   4751   347  11  4.9 265.4    7
c -    4.3    5030    44715     14283    6048   5107   358   8  5.0 263.2    7
c -    5.0    5030    44715     20128    7815   5729   378  10  5.4 265.4    7
c 
c [simplification-4] limit of 23050 conflicts hit after 23051 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5030 free variables schedulable
c [ternres-2] 1306 ternary resolvents (8 bin, 1298 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 4787 literals 48%
c [treelook-2] scheduling used 150010 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150192 steps
c [treelook-2] 3338 literals remain 33%
c [treelook-2] 2688 variables remain to probed next time 53%
c [treelook-2] removed 0 variables, found 24 hbrs
c [transred-2] limit 475222 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5030 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 76 clauses out of 13597 (1%) of length 5
c [cce-3-1] eliminated 147 clauses out of 17727 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 223 large clauses in 11774808 steps
c [cce-3-1] allowing another 5887404 steps for small clauses
c [cce-3] scheduling 760 clauses = 446 binary + 314 ternary
c [cce-3] tried to eliminate 760 small clauses 100%
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 223 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 760 clauses = 446 binary + 314 ternary
c [cce-3] tried to eliminate 760 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 223 covered clauses in TOTAL during 2 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 2368 out of 10062 literals actually usable 24%
c [bca-2] added 0 blocked clauses in 19550 steps
c [rephase-1] after 23051 conflicts (new increment 20000, next 43051)
c [flushphases] 109 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 0 variables 0.0% (5030 remain 61%)
c [simplification-4] removed 223 irredundant clauses 0.5% (44492 remain 71%)
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 40000
c [simplification-4] penalized conflict interval 40000 = 1 * 40000
c [simplification-4] new conflict limit 63051
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    5.9    5030    44492     25937   12726   7525   416  14  5.9 275.9    6
c -    6.0    5030    44492     26138    9390   7544   417  10  5.9 275.7    5
c -    6.8    5030    44492     33273   11424   8168   433  11  6.0 271.4    5
c -    7.6    5030    44492     40246   13065   8615   446   9  6.2 273.6    8
c -    8.6    5030    44492     48258   15169   9131   457  16  6.4 272.1    6
c -    9.1    5030    44492     56057   16876   9449   465  18  6.9 278.5    6
c R    9.2    5030    44492     56997   17746   9491   465  20  7.0 279.0    6
c 
c [simplification-5] limit of 63065 conflicts hit after 63065 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5030 free variables schedulable
c [ternres-3] 688 ternary resolvents (2 bin, 686 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4083 xors of average arity 3.0
c [gauss-2] connected 12249 occurrences of 1300 variables (average 9.4)
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 5030 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 457759 with penalty 1 = 1 + 0
c [lift-2] using 520 probes 10%
c [lift-2-1] found 0 units 4 impls in round 1
c [lift-2-2] found 0 units 1 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, 5 impls, 0 eqs in 5 rounds
c [lift-2] 728 variables remain 14% (4302 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1525863 with penalty 0 = 0 + 0
c [transred-3] removed 7 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 60 clauses out of 13452 (0%) of length 5
c [cce-4-1] eliminated 135 clauses out of 17604 (1%) of length 4
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] eliminated 195 large clauses in 11542014 steps
c [cce-4-1] allowing another 5771007 steps for small clauses
c [cce-4] scheduling 11387 clauses = 447 binary + 10940 ternary
c [cce-4] tried to eliminate 11387 small clauses 100%
c [cce-4] eliminated 2 small clauses 0%
c [cce-4] eliminated 2 ternary clauses 0%
c [cce-4-1] eliminated 2 small clauses in 8102208 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 197 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 11385 clauses = 447 binary + 10938 ternary
c [cce-4] tried to eliminate 11385 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 197 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5030 variables 100%
c [elim-4] limit of 15258638 steps penalty 1 = 1 + 0
c [elim-4-1] no variable eliminated in round 1 in 10819690 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 5030
c [rephase-2] after 63065 conflicts (new increment 40000, next 103065)
c [flushphases] 6 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 0 variables 0.0% (5030 remain 61%)
c [simplification-5] removed 197 irredundant clauses 0.4% (44295 remain 71%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 40000
c [simplification-5] new conflict interval 80000
c [simplification-5] penalized conflict interval 80000 = 1 * 80000
c [simplification-5] new conflict limit 143065
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   11.3    5030    44295     64625   18625  10572   499  12  7.1 277.0    6
c -   12.5    5030    44295     73710   20620  10912   500  17  7.3 276.5    6
c -   13.5    5030    44295     82999   22311  11185   503  20  7.8 276.9    7
c -   14.8    5030    44295     93256   24407  11544   506  20  8.0 274.4   11
c -   16.3    5030    44295    103406   26040  11791   509  11  8.4 273.6   11
c -   17.1    5030    44295    114057   27735  11973   510  22  9.4 275.8    7
c R   17.8    5030    44295    124297   37653  12079   511  27 10.1 278.8   10
c -   17.9    5030    44295    124870   29187  12097   511  14 10.1 278.5    7
c -   19.6    5030    44295    136995   31243  12371   516  15 10.1 276.5   11
c 
c [simplification-6] limit of 143067 conflicts hit after 143067 conflicts
c [ternres-4] limit 4179869 with penalty 0 = 0 + 0
c [ternres-4] all 5030 free variables schedulable
c [ternres-4] 384 ternary resolvents (4 bin, 380 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 522483 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 16 at-most-two constraints of average size 4.0
c [card-3] using previous limit 522483 for elimination
c [card-3] 16 out of 16 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 2089934 penalty 1 = 1 + 0
c [basicprobe-2-0] 973 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-1] 976 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 3 hbrs
c [unhide-3] limit 208993 with penalty 2 = 2 + 0
c [unhide-3-4] 0 units, 0 failed, 520 tauts, 0 hbrs, 1693 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 43 clauses out of 13348 (0%) of length 5
c [cce-5-1] eliminated 91 clauses out of 17463 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 134 large clauses in 11808236 steps
c [cce-5-1] allowing another 5904118 steps for small clauses
c [cce-5] scheduling 11421 clauses = 451 binary + 10970 ternary
c [cce-5] tried to eliminate 11421 small clauses 100%
c [cce-5] eliminated 2 small clauses 0%
c [cce-5] eliminated 2 binary clauses 0%
c [cce-5-1] eliminated 2 small clauses in 8275862 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 136 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 11419 clauses = 449 binary + 10970 ternary
c [cce-5] tried to eliminate 11419 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 136 covered clauses in TOTAL during 2 rounds
c [rephase-3] after 143067 conflicts (new increment 80000, next 223067)
c [flushphases] 0 phases reset
c [simplification-6] removed 0 variables 0.0% (5030 remain 61%)
c [simplification-6] removed 136 irredundant clauses 0.3% (44159 remain 71%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 80000
c [simplification-6] new conflict interval 160000
c [simplification-6] penalized conflict interval 160000 = 1 * 160000
c [simplification-6] new conflict limit 303067
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   21.8    5030    44159    149585   33259  12605   523  22 10.3 275.6    8
c -   23.6    5030    44159    162151   34864  12787   530  18 10.4 274.8   13
c -   25.5    5030    44159    175624   36973  12975   532  23 10.6 274.2   13
c -   27.2    5030    44159    189172   38572  13124   534  15 11.3 273.6   13
c -   29.4    5030    44159    203697   40718  13261   536  21 11.4 272.4    8
c -   31.5    5030    44159    218457   42659  13417   536  23 11.5 271.9   14
c -   33.7    5030    44159    233775   44585  13574   537  23 11.7 271.3    9
c -   35.0    5030    44159    248959   46022  13610   538  29 13.3 272.4    9
c -   36.8    5030    44159    264746   46858  13615   538  31 18.2 273.0    9
c R   37.3    5030    44159    269120   50890  13617   538  28 19.5 273.2   14
c -   39.4    5030    44159    281409   48375  13727   538  15 19.2 272.0    9
c -   42.3    5030    44159    298833   50371  13864   538  16 19.1 271.0    9
c 
c [simplification-7] limit of 303071 conflicts hit after 303071 conflicts
c [ternres-5] limit 10848370 with penalty 0 = 0 + 0
c [ternres-5] all 5030 free variables schedulable
c [ternres-5] 267 ternary resolvents (0 bin, 267 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 0 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5030 variables 100%
c [block-3] limit of 27120925 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 24 clauses out of 13280 (0%) of length 5
c [cce-6-1] eliminated 46 clauses out of 17382 (0%) of length 4
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] eliminated 70 large clauses in 11878737 steps
c [cce-6-1] allowing another 5939368 steps for small clauses
c [cce-6] scheduling 806 clauses = 449 binary + 357 ternary
c [cce-6] tried to eliminate 806 small clauses 100%
c [cce-6] eliminated 1 small clauses 0%
c [cce-6] eliminated 1 ternary clauses 0%
c [cce-6-1] eliminated 1 small clauses in 6085343 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 71 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 805 clauses = 449 binary + 356 ternary
c [cce-6] tried to eliminate 805 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 71 covered clauses in TOTAL during 2 rounds
c [bca-3] limit of 10000000 steps
c [bca-3] 570 out of 10062 literals actually usable 6%
c [bca-3] added 0 blocked clauses in 56825 steps
c [rephase-4] after 303071 conflicts (new increment 160000, next 463071)
c [flushphases] 0 phases reset
c [simplification-7] removed 0 variables 0.0% (5030 remain 61%)
c [simplification-7] removed 71 irredundant clauses 0.2% (44088 remain 71%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 160000
c [simplification-7] new conflict interval 320000
c [simplification-7] penalized conflict interval 320000 = 1 * 320000
c [simplification-7] new conflict limit 623071
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   45.9    5030    44088    316907   52630  14259   539  21 18.7 269.8   16
c -   48.4    5030    44088    334892   54174  14356   539  15 19.3 269.6   16
c -   51.5    5030    44088    353767   56179  14444   540  16 19.1 269.1   16
c -   55.2    5030    44088    373403   58361  14580   542  19 18.8 267.9   17
c -   56.8    5030    44088    392855   59999  14619   542  28 19.5 269.0   10
c -   60.6    5030    44088    413107   61878  14713   545  14 19.2 267.6   17
c -   64.4    5030    44088    434234   64082  14830   548  15 19.0 267.2   17
c -   67.4    5030    44088    455352   65776  14887   548  20 19.5 267.2   11
c -   71.3    5030    44088    477395   67981  14981   548  14 19.3 266.7   11
c -   75.7    5030    44088    500207   70334  15100   549  24 19.1 266.0   11
c -   77.9    5030    44088    522735   71774  15135   549  26 20.4 267.0   11
c -   80.4    5030    44088    545664   72988  15155   549  29 22.4 267.9   11
c -   83.9    5030    44088    569789   73788  15160   549  31 27.0 268.5   11
c -   88.2    5030    44088    594014   75060  15216   551  16 28.6 268.1   12
c -   93.2    5030    44088    619006   77160  15298   553  14 28.1 267.5   12
c 
c [simplification-8] limit of 623075 conflicts hit after 623076 conflicts
c [ternres-6] limit 27045126 with penalty 0 = 0 + 0
c [ternres-6] all 5030 free variables schedulable
c [ternres-6] 235 ternary resolvents (3 bin, 232 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1352256 penalty 2 = 2 + 0
c [gauss-3] extracted 4132 xors of average arity 3.0
c [gauss-3] connected 12396 occurrences of 1300 variables (average 9.5)
c [gauss-3] limit 1352256 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2068 schedulable variables 41%
c [simpleprobe-3] limit 54090253 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 53 hbrs, 0 units
c [cgrclsr-3] limit 676128 penalty 2 = 2 + 0
c [cgrclsr-3] all 5030 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 4056769 with penalty 2 = 2 + 0
c [lift-3] using 195 probes 4%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 0 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, 0 impls, 0 eqs in 6 rounds
c [lift-3] 533 variables remain 11% (4497 retained)
c [cliff-3] limit of 5409025 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [cce-7] limit of 54090253 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 10 clauses out of 13245 (0%) of length 5
c [cce-7-1] eliminated 22 clauses out of 17338 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 32 large clauses in 11800489 steps
c [cce-7-1] allowing another 5900244 steps for small clauses
c [cce-7] scheduling 814 clauses = 449 binary + 365 ternary
c [cce-7] tried to eliminate 814 small clauses 100%
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 32 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 814 clauses = 449 binary + 365 ternary
c [cce-7] tried to eliminate 814 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 32 covered clauses in TOTAL during 2 rounds
c [cce-7] 32 < 1/1000 * 44088 = 44 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5030 variables 100%
c [elim-5] limit of 135225634 steps penalty 2 = 2 + 0
c [elim-5-1] eliminated 1 variables 0% in round 1 in 10656930 steps
c [elim-5-1] backward subsumption/strengthening limit 21313860
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 2995557 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1 = 0% variables out of 5030
c [elim-5] 1 < 1/1000 * 5030 = 5 considered unsuccessful
c [rephase-5] after 623076 conflicts (new increment 320000, next 943076)
c [flushphases] 0 phases reset
c [simplification-8] removed 1 variables 0.0% (5029 remain 61%)
c [simplification-8] removed 32 irredundant clauses 0.1% (44056 remain 71%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 320000
c [simplification-8] new conflict interval 640000
c [simplification-8] penalized conflict interval 640000 = 1 * 640000
c [simplification-8] new conflict limit 1263076
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   99.1    5029    44056    644582   79305  15596   610  14 27.7 267.3   13
c -  104.4    5029    44056    670780   81584  15696   611  15 27.2 266.5   21
c -  108.6    5029    44056    697287   83668  15745   611  28 27.2 266.5   13
c -  114.1    5029    44056    723999   85469  15811   613  16 27.0 266.0   21
c -  120.0    5029    44056    751840   88014  15894   615  22 26.6 265.3   14
c -  125.4    5029    44056    779621   89870  15971   616  15 26.4 265.0   22
c -  131.8    5029    44056    808231   92156  16019   616  16 26.1 264.2   14
c -  134.9    5029    44056    837030   93681  16037   616  31 27.4 265.1   14
c -  140.3    5029    44056    866084   95236  16081   616  22 27.6 265.0   14
c -  147.3    5029    44056    896277   97484  16145   616  17 27.3 264.2   23
c -  153.8    5029    44056    926973   99731  16223   616  14 27.0 263.8   23
c -  160.5    5029    44056    958152  102061  16279   617  26 26.8 263.5   14
c -  166.4    5029    44056    989369  103689  16322   617  14 27.2 263.4   15
c -  174.2    5029    44056   1021585  106089  16386   617  24 26.9 262.9   24
c -  181.4    5029    44056   1054063  108226  16424   617  28 26.9 262.7   15
c -  188.5    5029    44056   1086684  110035  16462   617  29 26.7 262.4   15
c -  192.9    5029    44056   1120261  111528  16490   618  26 27.8 263.3   15
c -  197.1    5029    44056   1153950  112887  16495   618  29 28.9 264.0   15
c -  201.1    5029    44056   1188255  114178  16513   618  31 29.9 264.6   15
c -  206.0    5029    44056   1224076  115516  16531   618  31 31.3 265.0   14
c -  213.9    5029    44056   1260131  117057  16561   618  15 32.0 264.6   25
c 
c [simplification-9] limit of 1263078 conflicts hit after 1263078 conflicts
c [ternres-7] limit 66340216 with penalty 0 = 0 + 0
c [ternres-7] all 5029 free variables schedulable
c [ternres-7] 198 ternary resolvents (2 bin, 196 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 1000000 with penalty 1 = 1 + 0
c [transred-6] removed 42 transitive binary clauses
c [rephase-6] after 1263078 conflicts (new increment 640000, next 1903078)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (5029 remain 61%)
c [simplification-9] removed 0 irredundant clauses 0.0% (44056 remain 71%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 640000
c [simplification-9] new conflict interval 1280000
c [simplification-9] penalized conflict interval 1280000 = 1 * 1280000
c [simplification-9] new conflict limit 2543078
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  222.5    5029    44056   1296337  119376  16805   578  27 31.6 264.3   18
c -  232.4    5029    44056   1332875  121477  16871   580  16 31.3 263.7   18
c -  239.7    5029    44056   1369746  123367  16904   580  15 31.1 263.7   18
c -  250.3    5029    44056   1407553  125710  16961   581  15 30.8 263.1   28
c -  259.3    5029    44056   1446042  127982  17012   581  25 30.9 262.8   18
c -  267.9    5029    44056   1484476  130036  17053   581  28 30.9 262.7   18
c -  275.1    5029    44056   1523297  131217  17057   581  16 31.5 262.8   18
c -  285.1    5029    44056   1563082  133444  17109   583  26 31.3 262.5   18
c -  296.4    5029    44056   1603212  135562  17154   583  16 31.1 262.0   19
c -  305.9    5029    44056   1644090  137705  17176   583  19 31.1 261.9   19
c -  318.0    5029    44056   1685458  140272  17223   583  27 30.8 261.5   19
c -  328.5    5029    44056   1726752  141921  17262   583  18 30.8 261.3   19
c -  336.5    5029    44056   1769199  143847  17291   583  31 31.3 261.4   19
c -  343.0    5029    44056   1812243  145021  17293   583  30 32.7 261.9   18
c -  355.4    5029    44056   1855914  146798  17324   584  16 33.0 261.6   19
c -  367.9    5029    44056   1899717  148895  17352   584  15 33.0 261.2   20
c -  379.0    5029    44056   1945001  150941  17383   584  30 33.5 261.0   19
c -  393.4    5029    44056   1989596  153019  17426   584  19 33.2 260.5   20
c -  406.7    5029    44056   2034894  155192  17464   584  18 33.0 260.2   20
c -  416.2    5029    44056   2080899  157493  17482   585  29 33.2 260.4   20
c -  429.8    5029    44056   2127103  159661  17513   585  21 33.0 260.1   32
c -  443.1    5029    44056   2174052  161741  17552   585  29 33.2 259.9   20
c -  456.4    5029    44056   2225894  162359  17554   585  35 35.8 260.2   19
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  468.6    5029    44056   2274385  164227  17584   585  32 36.4 260.2   20
c -  485.3    5029    44056   2322666  166602  17621   585  26 36.1 259.8   21
c -  492.8    5029    44056   2372065  167963  17661   585  29 36.8 260.2   21
c -  501.1    5029    44056   2422844  169370  17689   585  29 37.6 260.5   19
c -  511.1    5029    44056   2476346  170611  17699   585  30 39.3 260.8   19
c -  519.3    5029    44056   2528134  172007  17705   585  33 40.3 261.2   20
c 
c [simplification-10] limit of 2543080 conflicts hit after 2543080 conflicts
c [ternres-8] limit 171940645 with penalty 0 = 0 + 0
c [ternres-8] all 5029 free variables schedulable
c [ternres-8] 227 ternary resolvents (6 bin, 221 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 10746290 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 20 at-most-two constraints of average size 4.0
c [card-4] using previous limit 10746290 for elimination
c [card-4] 22 out of 22 constraints (100%) 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-7] 0 units, 0 failed, 364 tauts, 0 hbrs, 45537 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2 transitive binary clauses
c [cce-8] limit of 171940645 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 18 clauses out of 13218 (0%) of length 5
c [cce-8-1] eliminated 49 clauses out of 17312 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 67 large clauses in 12012859 steps
c [cce-8-1] allowing another 6006429 steps for small clauses
c [cce-8] scheduling 825 clauses = 451 binary + 374 ternary
c [cce-8] tried to eliminate 825 small clauses 100%
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 67 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 825 clauses = 451 binary + 374 ternary
c [cce-8] tried to eliminate 825 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 67 covered clauses in TOTAL during 2 rounds
c [rephase-7] after 2543080 conflicts (new increment 1280000, next 3823080)
c [flushphases] 0 phases reset
c [simplification-10] removed 0 variables 0.0% (5029 remain 61%)
c [simplification-10] removed 67 irredundant clauses 0.2% (43989 remain 71%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 1280000
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 3543080
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  530.0    5029    43989   2581099  173228  17711   576  31 41.5 261.7   22
c -  544.3    5029    43989   2637447  174007  17714   576  30 43.6 262.1   22
c R  546.1    5029    43989   2648358  183765  17714   576  27 44.0 262.1   36
c -  562.2    5029    43989   2689965  175978  17745   576  15 43.6 261.6   24
c -  579.8    5029    43989   2742382  178455  17773   576  25 43.2 261.3   24
c -  595.9    5029    43989   2795205  180501  17801   576  23 43.0 261.1   24
c -  614.4    5029    43989   2848680  182866  17834   576  16 42.6 260.7   24
c -  628.7    5029    43989   2902644  185238  17867   576  28 42.4 260.8   24
c -  646.5    5029    43989   2957077  187329  17893   576  17 42.2 260.5   25
c -  666.1    5029    43989   3012141  189740  17919   576  26 42.0 260.1   25
c -  683.7    5029    43989   3067789  191972  17948   576  35 41.9 260.0   25
c -  702.9    5029    43989   3123754  194315  17980   576  24 41.7 259.7   25
c -  717.3    5029    43989   3181004  196158  17999   576  33 42.0 259.7   24
c -  729.0    5029    43989   3239781  197100  18006   576  33 42.8 259.9   24
c -  745.9    5029    43989   3300372  198091  18017   576  19 43.7 260.0   25
c -  764.5    5029    43989   3358487  200385  18054   576  23 43.6 259.9   25
c -  784.3    5029    43989   3417169  202756  18085   577  33 43.4 259.7   25
c -  799.6    5029    43989   3476477  204403  18101   578  32 43.6 259.7   25
c -  819.0    5029    43989   3537320  205968  18119   578  18 43.9 259.6   26
c 
c [simplification-11] limit of 3543080 conflicts hit after 3543081 conflicts
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 5029 free variables schedulable
c [ternres-9] 163 ternary resolvents (2 bin, 161 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 3387233 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5621 literals 56%
c [treelook-3] scheduling used 829231 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3387233 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 610028 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 4 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5029 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 541957331 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 7 clauses out of 13194 (0%) of length 5
c [cce-9-1] eliminated 11 clauses out of 17265 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 18 large clauses in 12081830 steps
c [cce-9-1] allowing another 6040915 steps for small clauses
c [cce-9] scheduling 828 clauses = 451 binary + 377 ternary
c [cce-9] tried to eliminate 828 small clauses 100%
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 18 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 828 clauses = 451 binary + 377 ternary
c [cce-9] tried to eliminate 828 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 18 covered clauses in TOTAL during 2 rounds
c [cce-9] 18 < 1/1000 * 43989 = 43 considered unsuccessful
c [bca-4] limit of 10000000 steps
c [bca-4] 83 out of 10060 literals actually usable 1%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 211670 steps
c [simplification-11] removed 0 variables 0.0% (5029 remain 61%)
c [simplification-11] removed 18 irredundant clauses 0.0% (43971 remain 71%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
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 4543081
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  843.4    5029    43971   3597325  208366  18300   583  18 43.6 259.2   28
c -  864.3    5029    43971   3657924  210659  18327   583  16 43.3 259.1   28
c -  887.2    5029    43971   3718766  212916  18344   583  22 43.1 258.8   28
c -  900.8    5029    43971   3780808  214771  18354   583  32 43.4 259.1   27
c -  912.1    5029    43971   3843637  216001  18359   583  34 44.0 259.5   27
c -  927.6    5029    43971   3909192  217105  18362   583  33 44.9 259.7   26
c -  950.7    5029    43971   3973396  219180  18386   583  28 45.0 259.5   28
c -  973.1    5029    43971   4037080  220949  18402   583  16 45.0 259.3   28
c -  997.2    5029    43971   4101318  223240  18437   583  18 44.8 259.1   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), 323649 steps
c bkwd: tried 141039 clauses, 282078 lits, 2.00 lits/clause
c bkwd: checked 5495467 occs, 38.96 occs/clause, 19.48 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, 8 removed, 1654793 resolutions, 3594851 steps
c blkd: 12 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 5 units, 0 am1, 13727320 steps
c card: 58 rescheduled, 236 eliminated, 29253 resolved, 4246 subsumed
c card: 7 at-most-one constraints found, average size 3.00
c card: 7 at-most-one constraints used 100%, average size 3.00
c card: 162 at-most-two constraints found, average size 4.00
c card: 162 at-most-two constraints used 100%, average size 4.00
c cces: 9 cces, 8138 eliminated, 8135 ate 100%, 3 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, 976239 esteps, 77852 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: 2923 extracted (138 ands 5%, 2509 xors 86%, 276 ites 9%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 441958 decisions, 9574053 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 306220 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 2146 rescored vars
c dcps: 19 decompositions, 30 equivalent 0%
c deco: 113136 decision-only clauses 3%, 48% reduction
c decs: 56022622 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3414110 flipped 6.094% (in 7569 phases)
c elms: 5 elims, 3201 eliminated 39%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 3201 small 100%, 0 large 0%
c elms: 19119 tried small, 3201 succeeded 17%, 15918 failed 83%
c elms: 401 subsumed, 308 strengthened, 0 blocked
c elms: 1411590 copies, 2589202 resolutions, 1779194 ipos
c elms: 38914 subchks, 33645 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 24420 extracted, 3.4 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8705144 steps, 4352572 extr 50%, 2647645 elim 30%
c glue: 44.7 orig avg, 43.7 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 609 = 409 simple + 185 trn 67% + 15 lrg 30%, 34 sub 2%
c hght: 259 average, 5.79 height/glue
c ints: 105887 luby (31126896 steps), 0 inout (0 steps)
c lift: 3 phases, 45131 probed (15046 level1 33%, 30085 level2 67%)
c lift: 0 units, 0 equivalences, 10 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4079953 clauses, 85.2 length
c lrnd: 1802543 uips 44%, 1772531 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 347417367 learned lits, 11% minimized
c mins: 3628157 mins 89%, 22 bin 0%, 338638 size 8%, 113136 deco 3%
c move: moved 4079953, 8 bin 0%, 272 trn 0%, 0 lrg 0%
c otfs: str 93488 dyn (92940 red, 548 irr) 27966 drv 30%, 65522 rst 70%
c otfs: sub 414 dyn (414 red, 0 irr)
c phas: 5 computed, 5267 set, 1676 pos (32%), 3591 neg (68%)
c prbs: 2 basic, 6322 probed, 0 failed, 0 lifted
c prbs: 3 simple, 29338 probed, 5 failed, 28 eqs
c prbs: 3 treelook, 10093 probed, 0 failed, 0 lifted
c prps: 862185394 props, 15 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 51701426 searches, 2107770 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: 119 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 119 arith 100%, 0 double 0%
c rmbd: 61 removed, 61 red 100%
c rphs: 7 recomputed phases
c rsts: 92278 restarts 87%, 13609 skipped 13%
c rsts: 0 saturating 0%, 9419 agile 69%, 4190 reuse 31%
c rsts: 44.0 avg interval, 44.0 scaled, 1.0 factor
c rsts: 13219 kept 14.3% average 36.2%
c simp: 11 count (11 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 4079953 count (6663226 tried 1.6), 92881 sub out of 4070730 (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: 19 fixed 0%, 0 its, 0.00 confs/it
c trvs: 54061167494 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 62.7 search traversals per propagation, 13157.5 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 8 transitive reductions, 73 removed, 0 failed
c trds: 80262 nodes, 7621 edges, 12376 steps
c trim: 3286557 words, 12.5 MB
c trnr: 9 count, 57 bin, 6458 trn, 27608410 steps
c unhd: 4 count, 7 rounds, 3962260 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: 1110 tauts, 2 bin 0%, 838 trn 75%, 250 lrg 23%
c unhd: 1110 tauts, 20 stamp 2%, 1068 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 47361 str, 0 bin 0%, 89 trn 0%, 47272 lrg 100%, 47268 red 100%
c vars: 5029 remaining 61% and 3250 removed 39% out of 8279
c vars: 19 fixed 0%, 3201 eliminated 39%, 30 equivalent 0%
c vsts: 33158548735 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 38.5 search visits per propagation, 8069.2 per conflict
c wchs: 9376066673 pushed, 11619730 enlarged, 845 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   4070730 100   3743625 100 238319343 100  43852179 100   2060683 100
c 
c  0     166636   4         0   0 190041512  80< 26164332  60   1136454  55 
c  1     260944   6    198528   5  27128681  11   5040145  11<   258499  13 
c  2     801141  20    797043  21   8393956   4   3497488   8    168290   8<
c  3     737107  18    732563  20   5735678   2   3061357   7    143540   7 
c  4     505931  12    502594  13   2928370   1   1876315   4     87978   4 
c  5     354130   9<   351934   9<  1528751   1   1154397   3     54569   3 
c  6     263160   6    261932   7    797612   0    735150   2     39326   2 
c  7     205413   5    204799   5    457842   0    509045   1     30315   1 
c  8     164608   4    164124   4    294998   0    379929   1     25046   1 
c  9     133500   3    133063   4    206701   0    296992   1     22292   1 
c 10     191789   5    189710   5    270050   0    429940   1     40493   2 
c 11     105148   3     96910   3    158568   0    250245   1     29468   1 
c 12     181189   4    110393   3    376565   0    456775   1     24402   1 
c 13         34   0        32   0        59   0        69   0        11   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           2.9           1.2           2.4           2.8
c 
c   70.127   7% analysis
c   56.550   6% decide
c   13.041   1% bump
c   11.404   1% defrag
c   10.699   1% restart
c    6.218   1% mincls
c    2.870   0% cce
c    2.549   0% elim
c    2.114   0% reduce
c    1.122   0% gc
c    0.710   0% decomp
c    0.570   0% unhide
c    0.522   0% probe
c    0.432   0% cliff
c    0.301   0% backward
c    0.282   0% block
c    0.278   0% gauss
c    0.216   0% ternres
c    0.216   0% card
c    0.137   0% lift
c    0.113   0% cgrclsr
c    0.072   0% bca
c    0.037   0% phase
c    0.013   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.199   0% probe simple     38%
c    0.062   0% probe basic      12%
c    0.260   0% probe tree-look  50%
c ==================================
c    0.843   0% preprocessing     9%
c    8.218   1% inprocessing     91%
c ==================================
c    9.062   1% simplifying
c  990.963  99% search
c ==================================
c 1000.028 100% all
c 
c 56022622 decisions, 56021.1 decisions/sec
c 4107919 conflicts, 4107.8 conflicts/sec
c 862185394 propagations, 0.9 megaprops/sec
c 1000.0 seconds, 119.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
