c launch: /data/cnf/sc2014/app/MD5-29-5.cnf.bz2
c host: atom19
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-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-29-5.cnf.bz2
c no embedded options
c found 'p cnf 8591 65322' header
c read 8591 variables, 65322 clauses, 254918 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 8581 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    8581    65083         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 2 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] 122 out of 122 constraints (100%) meet size limits
c [card-1] found 4 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 8559 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 14 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 14 variables, found 326 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 8545 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 3055 variables 36% in round 1 in 10641509 steps
c [elim-1-1] backward subsumption/strengthening limit 21283018
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 5207438 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 3055 = 36% variables out of 8545
c [phase-1] phase bias: 1648 positive 30%, 3842 negative 70%
c [simplification-1] removed 3091 variables 36.0% (5490 remain 64%)
c [simplification-1] removed 7416 irredundant clauses 11.4% (57667 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] 28286, max 46953, min4 27452 at 75%, min10 12569 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    5490    57667         5       1      2   158   0  2.0  28.8    5
c R    0.9    5490    57667        21       3     12   158   0  2.2  78.8    5
c R    0.9    5490    57667        63      20     25   160   1  2.6  94.9    5
c R    0.9    5490    57667       166      71     55   162   1  2.9 101.2    5
c R    0.9    5490    57667       415     231    105   165   3  3.3 120.2    5
c R    0.9    5490    57667       989     599    217   175   6  3.6 145.1    5
c 
c [simplification-2] limit of 1014 conflicts hit after 1014 conflicts
c [simpleprobe-2] all 5490 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2097 variables remain 38% (3393 retained)
c [simpleprobe-2] removed 0 variables, found 17 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10980 literals 100%
c [treelook-1] scheduling used 274736 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300004 steps
c [treelook-1] 7985 literals remain 73%
c [treelook-1] 4792 variables remain to probed next time 87%
c [treelook-1] removed 0 variables, found 63 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 596 sched 11%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-1-1] 597 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 19 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5490 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 1 blocked clauses
c [block-1] 1 < 1/1000 * 57667 = 57 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 42 clauses out of 714 (6%) of length 6
c [cce-1-1] eliminated 7373 clauses out of 22975 (32%) of length 5
c [cce-1-1] eliminated 270 clauses out of 19616 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7685 large clauses in 10102446 steps
c [cce-1-1] allowing another 5051223 steps for small clauses
c [cce-1] scheduling 12719 clauses = 457 binary + 12262 ternary
c [cce-1] tried to eliminate 12719 small clauses 100%
c [cce-1] eliminated 212 small clauses 2%
c [cce-1] eliminated 2 binary clauses 0%
c [cce-1] eliminated 210 ternary clauses 2%
c [cce-1-1] eliminated 212 small clauses in 7015164 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7897 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 12507 clauses = 455 binary + 12052 ternary
c [cce-1] tried to eliminate 12507 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 7897 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5490 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 42 variables 1% in round 1 in 12903819 steps
c [elim-2-1] backward subsumption/strengthening limit 7096181
c [elim-2-1] subsumed 0 and strengthened 0 clauses in 3611102 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 42 = 1% variables out of 5490
c [bca-1] limit of 10000000 steps
c [bca-1] 9504 out of 10898 literals actually usable 87%
c [bca-1] added 0 blocked clauses in 39110 steps
c [phase-2] phase bias: 11 positive 58%, 8 negative 42%
c [simplification-2] removed 42 variables 0.8% (5448 remain 63%)
c [simplification-2] removed 7930 irredundant clauses 13.8% (49737 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 3014
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.1    5448    49737      2286    1496    508   274   7  3.9 190.3    4
c 
c [simplification-3] limit of 3018 conflicts hit after 3018 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 5448 free variables schedulable
c [ternres-1] 3254 ternary resolvents (35 bin, 3219 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4 at-most-one constraints of average size 3.0
c [card-2] found 9 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 13 out of 13 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 1 used 100%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 15546 xors of average arity 3.6
c [gauss-1] connected 56424 occurrences of 4582 variables (average 12.3)
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 5448 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 4045 probes 74%
c [lift-1-1] found 0 units 8 impls in round 1
c [lift-1] 0 units, 8 impls, 1 eqs in 2 rounds
c [lift-1] 1403 variables remain 26% (4044 retained)
c [lift-1] removed 1 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 180 tauts, 0 hbrs, 56 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 20 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 36 clauses out of 15578 (0%) of length 5
c [cce-2-1] eliminated 49 clauses out of 19526 (0%) of length 4
c [cce-2-1] completed large round (ACCE)
c [cce-2-1] eliminated 85 large clauses in 13288459 steps
c [cce-2-1] allowing another 6644229 steps for small clauses
c [cce-2] scheduling 750 clauses = 464 binary + 286 ternary
c [cce-2] tried to eliminate 750 small clauses 100%
c [cce-2] eliminated 11 small clauses 1%
c [cce-2] eliminated 5 binary clauses 1%
c [cce-2] eliminated 6 ternary clauses 2%
c [cce-2-1] eliminated 11 small clauses in 6756115 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] completed small and large (ACCE)
c [cce-2-1] eliminated 96 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 739 clauses = 459 binary + 280 ternary
c [cce-2] tried to eliminate 739 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 96 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5447 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 12734496 steps
c [elim-3-1] backward subsumption/strengthening limit 7265504
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 3595990 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 5447
c [elim-3] 2 < 1/1000 * 5447 = 5 considered unsuccessful
c [phase-3] phase bias: 103 positive 70%, 45 negative 30%
c [simplification-3] removed 3 variables 0.1% (5445 remain 63%)
c [simplification-3] removed 99 irredundant clauses 0.2% (49638 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 23018
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    3.7    5445    49638      5210    3582   4046   319   8  4.4 239.4    5
c -    4.1    5445    49637      8954    4317   4600   352   6  4.5 242.2    5
c R    4.2    5445    49637     11703    6494   4918   368  14  4.9 256.1    5
c -    4.6    5445    49636     14407    6026   5317   378   8  4.9 259.6    8
c -    5.2    5445    49636     19955    7693   5795   396   9  5.2 263.9    8
c 
c [simplification-4] limit of 23044 conflicts hit after 23044 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5445 free variables schedulable
c [ternres-2] 1247 ternary resolvents (4 bin, 1243 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-8] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5080 literals 47%
c [treelook-2] scheduling used 150011 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150104 steps
c [treelook-2] 3656 literals remain 34%
c [treelook-2] 3515 variables remain to probed next time 65%
c [treelook-2] removed 0 variables, found 39 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 275 probes 5%
c [lift-2-1] found 0 units 0 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-5] found 0 units 0 impls in round 5
c [lift-2] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-2] 1128 variables remain 21% (4316 retained)
c [transred-2] limit 456249 with penalty 0 = 0 + 0
c [transred-2] removed 22 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5444 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 91 clauses out of 15431 (1%) of length 5
c [cce-3-1] eliminated 175 clauses out of 19543 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 266 large clauses in 13195140 steps
c [cce-3-1] allowing another 6597570 steps for small clauses
c [cce-3] scheduling 12278 clauses = 460 binary + 11818 ternary
c [cce-3] tried to eliminate 12278 small clauses 100%
c [cce-3] eliminated 9 small clauses 0%
c [cce-3] eliminated 9 ternary clauses 0%
c [cce-3-1] eliminated 9 small clauses in 9083723 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 275 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 12269 clauses = 460 binary + 11809 ternary
c [cce-3] tried to eliminate 12269 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 275 covered clauses in TOTAL during 2 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 3050 out of 10890 literals actually usable 28%
c [bca-2] added 0 blocked clauses in 22764 steps
c [rephase-1] after 23044 conflicts (new increment 20000, next 43044)
c [flushphases] 176 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 1 variables 0.0% (5444 remain 63%)
c [simplification-4] removed 276 irredundant clauses 0.6% (49360 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 53044
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    6.3    5444    49360     25973   12834   7491   436  15  5.6 275.9    6
c -    6.3    5444    49360     26036    9389   7495   436  13  5.6 275.9    6
c -    7.2    5444    49360     32849   11203   8043   448   9  5.8 275.5    6
c -    8.0    5444    49360     40014   12937   8524   461  12  6.1 277.8    9
c -    9.0    5444    49360     47812   14826   9026   471  15  6.4 277.2    6
c 
c [simplification-5] limit of 53058 conflicts hit after 53059 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5444 free variables schedulable
c [ternres-3] 613 ternary resolvents (6 bin, 607 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4370 xors of average arity 3.0
c [gauss-2] connected 13110 occurrences of 1393 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 5444 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1236654 with penalty 0 = 0 + 0
c [transred-3] removed 9 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 48 clauses out of 15288 (0%) of length 5
c [cce-4-1] eliminated 122 clauses out of 19374 (1%) of length 4
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] eliminated 170 large clauses in 13415487 steps
c [cce-4-1] allowing another 6707743 steps for small clauses
c [cce-4] scheduling 12294 clauses = 462 binary + 11832 ternary
c [cce-4] tried to eliminate 12294 small clauses 100%
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 170 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 12294 clauses = 462 binary + 11832 ternary
c [cce-4] tried to eliminate 12294 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 170 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5444 variables 100%
c [elim-4] limit of 12366540 steps penalty 1 = 1 + 0
c [elim-4] incomplete 8 not tried 0% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 1 = 0% variables out of 5444
c [elim-4] 1 < 1/1000 * 5444 = 5 considered unsuccessful
c [rephase-2] after 53059 conflicts (new increment 40000, next 93059)
c [flushphases] 95 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 1 variables 0.0% (5443 remain 63%)
c [simplification-5] removed 171 irredundant clauses 0.3% (49189 remain 76%)
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 113059
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   10.6    5443    49189     55390   16361   9924   497  18  7.2 284.1    6
c R   10.7    5443    49189     57053   17904   9985   497  18  7.2 285.4    7
c -   11.7    5443    49189     63742   18024  10280   505  10  7.4 283.8    6
c -   12.9    5443    49189     72703   19801  10611   514  10  7.6 283.1    7
c -   13.9    5443    49189     82303   21682  10997   521  17  8.0 284.8    7
c -   15.4    5443    49189     92450   23549  11372   524  14  8.1 283.4    7
c -   16.8    5443    49189    102863   25371  11655   526  11  8.3 282.3    7
c 
c [simplification-6] limit of 113067 conflicts hit after 113067 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5443 free variables schedulable
c [ternres-4] 522 ternary resolvents (3 bin, 519 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 15 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 17 out of 17 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 1593588 penalty 1 = 1 + 0
c [basicprobe-2-0] 978 sched 18%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-2-1] 979 sched 18%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 5 hbrs
c [lift-3] limit 956152 with penalty 1 = 1 + 0
c [lift-3] using 316 probes 6%
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 1 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 2 impls, 0 eqs in 6 rounds
c [lift-3] 812 variables remain 15% (4631 retained)
c [unhide-3] limit 159358 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 19 tauts, 0 hbrs, 1241 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 10 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 44 clauses out of 15193 (0%) of length 5
c [cce-5-1] eliminated 97 clauses out of 19252 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 141 large clauses in 13195962 steps
c [cce-5-1] allowing another 6597981 steps for small clauses
c [cce-5] scheduling 804 clauses = 462 binary + 342 ternary
c [cce-5] tried to eliminate 804 small clauses 100%
c [cce-5] eliminated 1 small clauses 0%
c [cce-5] eliminated 1 binary clauses 0%
c [cce-5-1] eliminated 1 small clauses in 6733735 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 142 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 803 clauses = 461 binary + 342 ternary
c [cce-5] tried to eliminate 803 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 142 covered clauses in TOTAL during 2 rounds
c [rephase-3] after 113067 conflicts (new increment 80000, next 193067)
c [flushphases] 15 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-6] removed 143 irredundant clauses 0.3% (49046 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 233067
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   18.2    5443    49046    113472   27086  12351   539  24  8.8 285.7    8
c -   19.0    5443    49046    124195   28454  12481   540  20  9.5 288.9    8
c R   19.0    5443    49046    124338   28590  12484   540  20  9.5 288.9    8
c -   20.6    5443    49046    136136   30324  12742   545  22  9.8 286.9    8
c -   22.4    5443    49046    148681   32426  12954   550  20  9.9 285.9    8
c -   24.2    5443    49046    161704   34504  13170   555  24 10.0 284.8    8
c -   26.0    5443    49046    174912   36316  13354   555  24 10.2 283.7   13
c -   27.7    5443    49046    188415   37902  13496   558  13 10.8 283.9   13
c -   30.0    5443    49046    203136   40136  13722   559  17 10.8 283.1    9
c -   32.1    5443    49046    217997   42039  13894   562  24 11.0 282.7    9
c 
c [simplification-7] limit of 233073 conflicts hit after 233073 conflicts
c [ternres-5] limit 7845503 with penalty 0 = 0 + 0
c [ternres-5] all 5443 free variables schedulable
c [ternres-5] 280 ternary resolvents (4 bin, 276 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5443 variables 100%
c [block-3] limit of 19613757 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 21 clauses out of 15129 (0%) of length 5
c [cce-6-1] eliminated 50 clauses out of 19152 (0%) of length 4
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] eliminated 71 large clauses in 13600239 steps
c [cce-6-1] allowing another 6800119 steps for small clauses
c [cce-6] scheduling 12327 clauses = 461 binary + 11866 ternary
c [cce-6] tried to eliminate 12327 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 9482725 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 73 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 12325 clauses = 461 binary + 11864 ternary
c [cce-6] tried to eliminate 12325 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 73 covered clauses in TOTAL during 2 rounds
c [bca-3] limit of 10000000 steps
c [bca-3] 1129 out of 10888 literals actually usable 10%
c [bca-3] added 0 blocked clauses in 61365 steps
c [rephase-4] after 233073 conflicts (new increment 160000, next 393073)
c [flushphases] 9 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-7] removed 73 irredundant clauses 0.1% (48973 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 473073
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.9    5443    48973    233399   43977  14333   564  22 11.1 282.6   10
c -   36.2    5443    48973    248728   45560  14400   566  24 12.1 284.3   10
c -   37.8    5443    48973    264601   46715  14439   566  30 15.2 285.0    9
c -   40.4    5443    48973    281191   48242  14548   568  16 16.2 284.2   10
c -   43.2    5443    48973    298584   50158  14677   570  13 16.5 282.9   10
c -   46.3    5443    48973    316705   52303  14846   570  17 16.4 281.3   10
c -   49.0    5443    48973    335212   54408  14975   573  13 16.2 281.7   10
c -   52.0    5443    48973    354401   56670  15142   577  16 16.2 281.3   10
c -   55.6    5443    48973    374099   58986  15297   578  23 16.1 280.3   11
c -   57.3    5443    48973    393363   60362  15344   578  22 16.9 281.6   11
c -   61.4    5443    48973    414212   62717  15481   578  16 16.7 280.3   11
c -   65.1    5443    48973    435057   64660  15583   578  14 16.7 279.8   11
c -   68.4    5443    48973    456299   66516  15655   580  16 16.8 279.9   11
c 
c [simplification-8] limit of 473081 conflicts hit after 473082 conflicts
c [ternres-6] limit 19027331 with penalty 0 = 0 + 0
c [ternres-6] all 5443 free variables schedulable
c [ternres-6] 212 ternary resolvents (1 bin, 211 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 951366 penalty 2 = 2 + 0
c [gauss-3] extracted 2900 xors of average arity 3.0
c [gauss-3] connected 8700 occurrences of 1257 variables (average 6.9)
c [gauss-3] limit 951366 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2075 schedulable variables 38%
c [simpleprobe-3] limit 38054662 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 60 hbrs, 0 units
c [cgrclsr-3] limit 475683 penalty 2 = 2 + 0
c [cgrclsr-3] all 5443 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-3] limit of 3805466 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 45 transitive binary clauses
c [cce-7] limit of 38054662 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 23 clauses out of 15085 (0%) of length 5
c [cce-7-1] eliminated 47 clauses out of 19108 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 70 large clauses in 13639024 steps
c [cce-7-1] allowing another 6819512 steps for small clauses
c [cce-7] scheduling 824 clauses = 461 binary + 363 ternary
c [cce-7] tried to eliminate 824 small clauses 100%
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 70 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 824 clauses = 461 binary + 363 ternary
c [cce-7] tried to eliminate 824 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 70 covered clauses in TOTAL during 2 rounds
c [elim-5] 8 variables 0% will be scheduled this time
c [elim-5] scheduled 8 variables 0%
c [elim-5] limit of 95136657 steps penalty 2 = 2 + 0
c [elim-5-1] no variable eliminated in round 1 in 100485 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 5443
c [rephase-5] after 473082 conflicts (new increment 320000, next 793082)
c [flushphases] 0 phases reset
c [simplification-8] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-8] removed 70 irredundant clauses 0.1% (48903 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 953082
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   73.3    5443    48903    478371   68704  15953   597  15 16.7 279.1   12
c -   77.6    5443    48903    500968   70937  16056   599  25 16.6 278.4   19
c -   79.9    5443    48903    523515   72696  16077   599  31 17.5 279.8   12
c -   83.3    5443    48903    546615   73577  16084   599  30 21.3 280.4   12
c -   87.3    5443    48903    570996   74307  16090   599  27 26.0 281.1   12
c R   88.1    5443    48903    579429   82589  16100   599  28 26.2 281.5   18
c -   91.7    5443    48903    595371   76242  16174   599  17 25.9 280.7   13
c -   96.7    5443    48903    620416   78357  16246   599  17 25.5 279.9   13
c -  100.9    5443    48903    646066   80222  16297   600  16 26.5 279.9   13
c -  106.2    5443    48903    672235   82550  16372   602  17 26.1 279.3   21
c -  110.3    5443    48903    698515   84546  16427   603  31 26.0 279.5   14
c -  115.3    5443    48903    725545   86059  16478   603  17 27.5 279.5   14
c -  121.0    5443    48903    753292   88477  16561   605  24 27.1 278.7   22
c -  126.7    5443    48903    781104   90378  16633   605  14 26.8 278.2   22
c -  133.1    5443    48903    809746   92680  16699   606  23 26.5 277.7   22
c -  136.3    5443    48903    838387   94386  16721   606  30 27.0 278.7   14
c -  142.1    5443    48903    867558   96071  16781   606  16 27.0 278.4   23
c -  149.0    5443    48903    897702   98366  16850   606  24 26.7 277.6   23
c -  155.6    5443    48903    928170  100449  16912   607  23 26.6 277.1   14
c 
c [simplification-9] limit of 953082 conflicts hit after 953082 conflicts
c [ternres-7] limit 47343214 with penalty 0 = 0 + 0
c [ternres-7] all 5443 free variables schedulable
c [ternres-7] 198 ternary resolvents (1 bin, 197 trn)
c [ternres-7] fully completed ternary resolution
c [lift-4] limit 5000000 with penalty 2 = 2 + 0
c [lift-4] using 237 probes 4%
c [lift-4-1] found 0 units 0 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 0 impls in round 5
c [lift-4] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-4] 575 variables remain 11% (4868 retained)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 9 transitive binary clauses
c [cce-8] limit of 94686428 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 20 clauses out of 15044 (0%) of length 5
c [cce-8-1] eliminated 44 clauses out of 19060 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 64 large clauses in 13548901 steps
c [cce-8-1] allowing another 6774450 steps for small clauses
c [cce-8] scheduling 836 clauses = 462 binary + 374 ternary
c [cce-8] tried to eliminate 836 small clauses 100%
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 64 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 836 clauses = 462 binary + 374 ternary
c [cce-8] tried to eliminate 836 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 64 covered clauses in TOTAL during 2 rounds
c [rephase-6] after 953082 conflicts (new increment 640000, next 1593082)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-9] removed 64 irredundant clauses 0.1% (48839 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 1913082
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  162.9    5443    48839    959057  102523  17149   599  24 26.3 276.8   16
c -  169.2    5443    48839    990400  104456  17190   599  24 26.6 276.7   25
c -  177.1    5443    48839   1022441  106721  17242   599  25 26.3 276.0   25
c -  184.5    5443    48839   1054961  108783  17302   600  26 26.3 275.7   16
c -  191.6    5443    48839   1087829  110694  17350   601  26 26.2 275.3   17
c -  196.0    5443    48839   1121576  112255  17369   601  27 27.5 276.0   17
c -  201.1    5443    48839   1155437  113210  17378   601  33 29.8 276.7   17
c -  206.4    5443    48839   1189920  113924  17381   601  29 32.1 277.4   17
c -  214.9    5443    48839   1229691  114773  17383   601  29 37.7 278.0   18
c R  216.2    5443    48839   1241431  126278  17388   601  29 37.9 278.2   26
c -  222.9    5443    48839   1264952  116490  17429   601  25 37.5 277.7   27
c -  231.4    5443    48839   1301235  118751  17496   602  16 37.0 277.3   17
c -  241.2    5443    48839   1338218  121283  17562   602  17 36.5 276.5   17
c -  248.1    5443    48839   1376364  122980  17588   602  33 37.2 276.6   17
c -  258.3    5443    48839   1414051  125233  17651   603  23 36.8 276.0   28
c -  267.6    5443    48839   1451938  127060  17690   603  16 36.5 275.6   28
c -  275.5    5443    48839   1490557  129119  17729   603  28 36.3 275.7   18
c -  284.5    5443    48839   1529941  131019  17761   604  17 36.5 275.7   18
c -  294.6    5443    48839   1569609  133116  17798   604  15 36.3 275.2   18
c -  306.0    5443    48839   1610167  135460  17826   604  18 36.2 274.7   18
c -  315.1    5443    48839   1650677  137449  17849   605  16 36.0 274.6   29
c -  325.9    5443    48839   1692217  140087  17910   606  25 35.7 274.3   18
c -  338.8    5443    48839   1733742  142176  17951   607  17 35.2 273.8   19
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  345.5    5443    48839   1776264  144062  17968   607  28 35.8 274.2   18
c -  351.7    5443    48839   1819439  145206  17975   607  28 36.8 274.6   18
c -  364.9    5443    48839   1862642  147366  18031   607  16 36.5 274.0   19
c -  377.1    5443    48839   1906359  149583  18065   608  16 36.2 273.6   31
c 
c [simplification-10] limit of 1913082 conflicts hit after 1913082 conflicts
c [ternres-8] limit 118501289 with penalty 0 = 0 + 0
c [ternres-8] all 5443 free variables schedulable
c [ternres-8] 174 ternary resolvents (1 bin, 173 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 7406330 penalty 3 = 3 + 0
c [card-4] found 5 at-most-one constraints of average size 3.0
c [card-4] found 24 at-most-two constraints of average size 4.0
c [card-4] using previous limit 7406330 for elimination
c [card-4] 29 out of 29 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-6] 0 units, 0 failed, 762 tauts, 0 hbrs, 5836 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1 transitive binary clauses
c [cce-9] limit of 237002578 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 5 clauses out of 15014 (0%) of length 5
c [cce-9-1] eliminated 18 clauses out of 19009 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 23 large clauses in 13794806 steps
c [cce-9-1] allowing another 6897403 steps for small clauses
c [cce-9] scheduling 12354 clauses = 465 binary + 11889 ternary
c [cce-9] tried to eliminate 12354 small clauses 100%
c [cce-9] eliminated 1 small clauses 0%
c [cce-9] eliminated 1 binary clauses 0%
c [cce-9-1] eliminated 1 small clauses in 9671470 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 24 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 12353 clauses = 464 binary + 11889 ternary
c [cce-9] tried to eliminate 12353 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 24 covered clauses in TOTAL during 2 rounds
c [cce-9] 24 < 1/1000 * 48838 = 48 considered unsuccessful
c [rephase-7] after 1913082 conflicts (new increment 1280000, next 3193082)
c [flushphases] 0 phases reset
c [simplification-10] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-10] removed 25 irredundant clauses 0.1% (48814 remain 75%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
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 2913082
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  388.9    5443    48814   1950749  151296  17766   604  22 36.2 273.4   21
c -  403.2    5443    48814   1995603  153837  17808   604  25 35.8 272.9   22
c -  416.6    5443    48814   2040736  156140  17841   604  27 35.5 272.6   34
c -  425.7    5443    48814   2086975  157785  17859   604  22 36.0 272.9   21
c -  440.7    5443    48814   2133422  160395  17891   604  21 35.6 272.5   22
c -  454.6    5443    48814   2180143  162386  17929   604  17 35.5 272.1   22
c -  467.2    5443    48814   2227464  164647  17970   604  26 35.3 272.0   22
c -  481.9    5443    48814   2275358  166914  18002   604  17 35.1 271.7   22
c -  498.4    5443    48814   2323797  169497  18040   604  28 34.8 271.3   22
c -  506.7    5443    48814   2373576  170841  18050   604  32 35.9 271.7   21
c -  514.7    5443    48814   2423631  172224  18055   604  31 36.9 272.2   22
c -  523.5    5443    48814   2474118  173159  18058   604  32 38.2 272.6   22
c -  536.1    5443    48814   2528287  173915  18060   604  29 40.3 272.9   21
c -  548.2    5443    48814   2582596  174955  18064   604  27 42.1 273.3   23
c -  558.7    5443    48814   2635178  175978  18065   604  32 43.5 273.7   23
c R  560.9    5443    48814   2647536  187501  18066   604  29 43.8 273.8   38
c -  576.1    5443    48814   2687392  177975  18097   604  18 43.5 273.4   23
c -  594.3    5443    48814   2739758  180293  18124   604  16 43.1 272.9   23
c -  610.4    5443    48814   2792717  182637  18161   605  16 42.7 272.8   24
c -  628.4    5443    48814   2846269  185096  18213   607  22 42.4 272.4   24
c -  643.4    5443    48814   2900636  187485  18246   607  29 42.3 272.4   24
c 
c [simplification-11] limit of 2913084 conflicts hit after 2913085 conflicts
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 5443 free variables schedulable
c [ternres-9] 190 ternary resolvents (1 bin, 189 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 2621001 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 7273 literals 67%
c [treelook-3] scheduling used 870013 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2621001 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 761058 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 5 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5443 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 496 out of 10888 literals actually usable 5%
c [bca-4] added 0 blocked clauses in 201231 steps
c [simplification-11] removed 0 variables 0.0% (5443 remain 63%)
c [simplification-11] removed 0 irredundant clauses 0.0% (48814 remain 75%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] new conflict interval 2000000
c [simplification-11] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-11] new conflict limit 4913085
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  661.3    5443    48814   2955388  189627  18469   611  32 42.3 272.2   26
c -  680.8    5443    48814   3010448  191976  18506   611  24 42.0 271.8   26
c -  697.5    5443    48814   3066414  193674  18531   611  22 42.2 271.7   26
c -  718.0    5443    48814   3122322  195957  18560   611  26 41.9 271.3   26
c -  732.1    5443    48814   3178704  198152  18584   611  25 41.8 271.4   26
c -  745.6    5443    48814   3237303  199682  18595   611  19 42.5 271.6   26
c -  764.2    5443    48814   3295794  201908  18621   611  31 42.7 271.4   26
c -  779.5    5443    48814   3354623  203366  18637   611  18 43.1 271.6   27
c -  800.3    5443    48814   3413189  205863  18664   611  35 42.9 271.3   27
c -  820.8    5443    48814   3471854  207991  18695   611  25 42.6 271.1   27
c -  840.0    5443    48814   3531430  209982  18734   611  19 42.6 271.0   27
c -  863.3    5443    48814   3591464  212481  18761   612  23 42.2 270.7   27
c -  885.0    5443    48814   3652448  214684  18780   612  18 42.1 270.6   27
c -  909.3    5443    48814   3713270  216869  18800   613  18 41.8 270.2   28
c -  923.4    5443    48814   3775270  218779  18816   613  29 42.1 270.4   27
c -  940.9    5443    48814   3842653  219786  18822   613  33 43.4 270.7   27
c -  958.1    5443    48814   3905778  221085  18829   613  15 43.8 270.8   28
c -  983.9    5443    48814   3969237  223758  18851   614  23 43.6 270.5   28
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), 324470 steps
c bkwd: tried 157042 clauses, 314084 lits, 2.00 lits/clause
c bkwd: checked 6342076 occs, 40.38 occs/clause, 20.19 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, 1 removed, 1830090 resolutions, 3980520 steps
c blkd: 3 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 4 units, 1 am1, 10674588 steps
c card: 55 rescheduled, 246 eliminated, 31987 resolved, 3493 subsumed
c card: 13 at-most-one constraints found, average size 3.00
c card: 13 at-most-one constraints used 100%, average size 3.00
c card: 168 at-most-two constraints found, average size 4.00
c card: 168 at-most-two constraints used 100%, average size 4.00
c cces: 9 cces, 8811 eliminated, 8811 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 3 count, 775684 esteps, 60614 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: 2350 extracted (98 ands 4%, 2066 xors 88%, 186 ites 8%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 415392 decisions, 7822208 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 320240 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 52 gcs, 0 rescored clauses, 2099 rescored vars
c dcps: 19 decompositions, 29 equivalent 0%
c deco: 97693 decision-only clauses 2%, 48% reduction
c decs: 59658248 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3643577 flipped 6.107% (in 7710 phases)
c elms: 5 elims, 3100 eliminated 36%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 3100 small 100%, 0 large 0%
c elms: 16747 tried small, 3100 succeeded 19%, 13647 failed 81%
c elms: 269 subsumed, 269 strengthened, 0 blocked
c elms: 1231903 copies, 2256704 resolutions, 1569578 ipos
c elms: 37698 subchks, 33335 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 22816 extracted, 3.4 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7902916 steps, 3951458 extr 50%, 2664749 elim 34%
c glue: 43.5 orig avg, 42.4 real avg, 4.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 608 = 403 simple + 187 trn 66% + 18 lrg 31%, 24 sub 3%
c hght: 270 average, 6.22 height/glue
c ints: 102602 luby (30052278 steps), 0 inout (0 steps)
c lift: 4 phases, 49385 probed (16464 level1 33%, 32921 level2 67%)
c lift: 0 units, 1 equivalences, 10 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3990257 clauses, 81.3 length
c lrnd: 1798116 uips 45%, 1680317 flips 42%
c mega: 0 count, 0 failed, 0 rounds
c mins: 324516634 learned lits, 11% minimized
c mins: 3535297 mins 89%, 30 bin 0%, 357237 size 9%, 97693 deco 2%
c move: moved 3990257, 9 bin 0%, 270 trn 0%, 0 lrg 0%
c otfs: str 87595 dyn (86980 red, 615 irr) 27981 drv 32%, 59614 rst 68%
c otfs: sub 470 dyn (468 red, 2 irr)
c phas: 7 computed, 5657 set, 1762 pos (31%), 3895 neg (69%)
c prbs: 2 basic, 6300 probed, 0 failed, 0 lifted
c prbs: 3 simple, 30385 probed, 5 failed, 23 eqs
c prbs: 3 treelook, 11692 probed, 0 failed, 0 lifted
c prps: 894631741 props, 15 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 47246285 searches, 1855620 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, 1 acts 1%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 117 arith 100%, 0 double 0%
c rmbd: 46 removed, 45 red 98%
c rphs: 7 recomputed phases
c rsts: 94088 restarts 92%, 8514 skipped 8%
c rsts: 0 saturating 0%, 4024 agile 47%, 4490 reuse 53%
c rsts: 42.3 avg interval, 42.3 scaled, 1.0 factor
c rsts: 13778 kept 14.6% average 37.1%
c simp: 11 count (11 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3990257 count (6068265 tried 1.5), 81961 sub out of 3981059 (2.1%)
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: 52839635215 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 59.1 search traversals per propagation, 13147.6 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 9 transitive reductions, 121 removed, 0 failed
c trds: 97744 nodes, 8966 edges, 15140 steps
c trim: 3235841 words, 12.3 MB
c trnr: 9 count, 56 bin, 6634 trn, 26917638 steps
c unhd: 4 count, 6 rounds, 3067604 steps
c unhd: 4 non-trivial sccs of average size 2.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: 1045 tauts, 0 bin 0%, 794 trn 76%, 231 lrg 22%
c unhd: 1045 tauts, 20 stamp 2%, 1001 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 7197 str, 0 bin 0%, 103 trn 1%, 7094 lrg 99%, 7095 red 99%
c vars: 5443 remaining 63% and 3148 removed 37% out of 8591
c vars: 19 fixed 0%, 3100 eliminated 36%, 29 equivalent 0%
c vsts: 32466022444 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 36.3 search visits per propagation, 8077.3 per conflict
c wchs: 8917669820 pushed, 12044107 enlarged, 837 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3981059 100   3622435 100 236156651 100  40779391 100   1956503 100
c 
c  0     169444   4         0   0 189565874  80< 24490805  60   1103928  56 
c  1     266915   7    203379   6  27114915  11   4688331  11<   244940  13 
c  2     812526  20    799937  22   7490100   3   3100811   8    148879   8<
c  3     743908  19    730709  20   5104270   2   2746818   7    130568   7 
c  4     502380  13<   493028  14   2913882   1   1813480   4     84716   4 
c  5     338431   9    332361   9<  1485953   1   1095934   3     51252   3 
c  6     242785   6    238790   7    786430   0    690964   2     36308   2 
c  7     184451   5    181675   5    445889   0    467545   1     27683   1 
c  8     146009   4    143902   4    286596   0    344514   1     21944   1 
c  9     118043   3    116453   3    201108   0    267667   1     18903   1 
c 10     173769   4    171013   5    261990   0    390439   1     33674   2 
c 11     129422   3    119593   3    191143   0    302455   1     33451   2 
c 12     151239   4     90536   2    305487   0    375520   1     20013   1 
c 13       1737   0      1059   0      3014   0      4108   0       244   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.5           4.6           0.4           1.4           1.7
c std             3.1           2.9           1.2           2.4           2.8
c 
c   68.314   7% analysis
c   60.592   6% decide
c   12.507   1% bump
c   11.562   1% defrag
c   11.530   1% restart
c    5.950   1% mincls
c    3.323   0% cce
c    2.315   0% elim
c    2.045   0% reduce
c    1.215   0% gc
c    0.764   0% decomp
c    0.594   0% probe
c    0.358   0% cliff
c    0.345   0% backward
c    0.318   0% block
c    0.275   0% gauss
c    0.233   0% unhide
c    0.214   0% ternres
c    0.192   0% lift
c    0.176   0% card
c    0.164   0% bca
c    0.120   0% cgrclsr
c    0.076   0% phase
c    0.016   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.220   0% probe simple     37%
c    0.065   0% probe basic      11%
c    0.309   0% probe tree-look  52%
c ==================================
c    0.873   0% preprocessing    10%
c    8.288   1% inprocessing     90%
c ==================================
c    9.160   1% simplifying
c  990.834  99% search
c ==================================
c  999.995 100% all
c 
c 59658248 decisions, 59658.6 decisions/sec
c 4018238 conflicts, 4018.3 conflicts/sec
c 894631741 propagations, 0.9 megaprops/sec
c 1000.0 seconds, 107.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
