c launch: /data/cnf/sc2014/app/MD5-32-3.cnf.bz2
c host: atom31
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-32-3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-32-3.cnf.bz2
c no embedded options
c found 'p cnf 9527 73634' header
c read 9527 variables, 73634 clauses, 288356 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 9516 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    9516    73369         0       0      0     0   0  0.0   0.0    4
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 123 out of 123 constraints (100%) meet size limits
c [card-1] found 4 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 34 variables
c [simpleprobe-1] all 9493 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 6 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 6 variables, found 344 hbrs, 1 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 9487 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 2763 variables 29% in round 1 in 11933238 steps
c [elim-1-1] backward subsumption/strengthening limit 23866476
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 6725632 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2763 = 29% variables out of 9487
c [phase-1] phase bias: 2130 positive 32%, 4594 negative 68%
c [simplification-1] removed 2792 variables 29.3% (6724 remain 71%)
c [simplification-1] removed 914 irredundant clauses 1.2% (72455 remain 99%)
c [simplification-1] maximum reduction of 29% = max (29%, 1%)
c [simplification-1] large reduction 29% >= 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] 34438, max 55564, min4 33415 at 25%, min10 14899 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    1.0    6724    72455         5       0      1   191   0  2.0  20.3    6
c R    1.0    6724    72455        20       3      9   195   0  1.8  33.6    6
c R    1.0    6724    72455        61      28     22   195   1  2.7  98.2    6
c R    1.0    6724    72455       164      85     44   197   2  3.1 106.6    6
c R    1.0    6724    72455       411     233    112   202   3  3.4 123.9    6
c R    1.1    6724    72455       978     592    219   211   5  3.5 136.1    6
c 
c [simplification-2] limit of 1018 conflicts hit after 1018 conflicts
c [decomp-3] removed 1 variables
c [simpleprobe-2] all 6723 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 3822 variables remain 57% (2901 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 12307 literals 92%
c [treelook-1] scheduling used 300060 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300025 steps
c [treelook-1] 9516 literals remain 71%
c [treelook-1] 6335 variables remain to probed next time 94%
c [treelook-1] removed 0 variables, found 61 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 751 sched 11%, 0 failed, 0 lifted, 36 hbrs
c [basicprobe-1-1] 760 sched 11%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 759 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-3] 760 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-3] fully completed probing
c [basicprobe-1-3] removed 0 variables, found 39 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6723 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 0 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 54 clauses out of 892 (6%) of length 6
c [cce-1-1] eliminated 9217 clauses out of 29008 (32%) of length 5
c [cce-1-1] eliminated 339 clauses out of 24930 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 9610 large clauses in 13380877 steps
c [cce-1-1] allowing another 6690438 steps for small clauses
c [cce-1] scheduling 15495 clauses = 591 binary + 14904 ternary
c [cce-1] tried to eliminate 15495 small clauses 100%
c [cce-1] eliminated 216 small clauses 1%
c [cce-1] eliminated 4 binary clauses 1%
c [cce-1] eliminated 212 ternary clauses 1%
c [cce-1-1] eliminated 216 small clauses in 9289466 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 9826 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 15279 clauses = 587 binary + 14692 ternary
c [cce-1] tried to eliminate 15279 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 9826 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6723 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 29 variables 0% in round 1 in 16772468 steps
c [elim-2-1] backward subsumption/strengthening limit 3227532
c [elim-2-1] subsumed 0 and strengthened 0 clauses in 3227630 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 29 = 0% variables out of 6723
c [bca-1] limit of 10000000 steps
c [bca-1] 11966 out of 13390 literals actually usable 89%
c [bca-1] added 0 blocked clauses in 50574 steps
c [phase-2] phase bias: 20 positive 54%, 17 negative 46%
c [simplification-2] removed 30 variables 0.4% (6694 remain 70%)
c [simplification-2] removed 9857 irredundant clauses 13.6% (62598 remain 85%)
c [simplification-2] maximum reduction of 14% = max (0%, 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 3018
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.6    6694    62598      2280    1494    552   320   8  3.9 176.7    5
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 6694 free variables schedulable
c [ternres-1] 3929 ternary resolvents (36 bin, 3893 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 8 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 8 out of 8 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 10430 xors of average arity 3.4
c [gauss-1] connected 35576 occurrences of 3095 variables (average 11.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 9884 occurrences of 3095 variables (average 3.2)
c [gauss-1] fully completed
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 6694 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 4815 probes 72%
c [lift-1] 0 units, 11 impls, 0 eqs in 1 rounds
c [lift-1] 2952 variables remain 44% (3742 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, 162 tauts, 0 hbrs, 51 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 24 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 51 clauses out of 19751 (0%) of length 5
c [cce-2-1] eliminated 62 clauses out of 24732 (0%) of length 4
c [cce-2-1] completed large round (ACCE)
c [cce-2-1] eliminated 113 large clauses in 17288580 steps
c [cce-2-1] allowing another 8644290 steps for small clauses
c [cce-2] scheduling 935 clauses = 608 binary + 327 ternary
c [cce-2] tried to eliminate 935 small clauses 100%
c [cce-2] eliminated 10 small clauses 1%
c [cce-2] eliminated 5 binary clauses 1%
c [cce-2] eliminated 5 ternary clauses 2%
c [cce-2-1] eliminated 10 small clauses in 8781301 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] completed small and large (ACCE)
c [cce-2-1] eliminated 123 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 925 clauses = 603 binary + 322 ternary
c [cce-2] tried to eliminate 925 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 123 covered clauses in TOTAL during 2 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6694 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] no variable eliminated in round 1 in 16645003 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 6694
c [phase-3] phase bias: 160 positive 62%, 97 negative 38%
c [simplification-3] removed 0 variables 0.0% (6694 remain 70%)
c [simplification-3] removed 126 irredundant clauses 0.2% (62472 remain 85%)
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    4.2    6694    62472      5202    3569   4752   382   7  4.1 243.3    6
c -    4.7    6694    62472      9303    4571   5360   421   7  4.5 258.2    6
c R    5.0    6694    62472     11704    6528   5645   425   9  4.8 282.0    6
c -    5.4    6694    62472     14619    6279   6057   442   6  4.9 284.8    6
c -    6.2    6694    62472     20561    7992   6833   472   7  5.3 292.9    9
c 
c [simplification-4] limit of 23084 conflicts hit after 23084 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 6694 free variables schedulable
c [ternres-2] 1584 ternary resolvents (5 bin, 1579 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5371 literals 40%
c [treelook-2] scheduling used 150018 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150031 steps
c [treelook-2] 3967 literals remain 30%
c [treelook-2] 2428 variables remain to probed next time 36%
c [treelook-2] removed 0 variables, found 8 hbrs
c [transred-2] limit 514750 with penalty 0 = 0 + 0
c [transred-2] removed 10 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 6694 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 99 clauses out of 19574 (1%) of length 5
c [cce-3-1] eliminated 174 clauses out of 24753 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 273 large clauses in 17503995 steps
c [cce-3-1] allowing another 8751997 steps for small clauses
c [cce-3] scheduling 947 clauses = 606 binary + 341 ternary
c [cce-3] tried to eliminate 947 small clauses 100%
c [cce-3] eliminated 1 small clauses 0%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses in 8898015 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 274 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 946 clauses = 605 binary + 341 ternary
c [cce-3] tried to eliminate 946 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 274 covered clauses in TOTAL during 2 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 3794 out of 13390 literals actually usable 28%
c [bca-2] added 0 blocked clauses in 26477 steps
c [rephase-1] after 23084 conflicts (new increment 20000, next 43084)
c [flushphases] 111 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 0 variables 0.0% (6694 remain 70%)
c [simplification-4] removed 274 irredundant clauses 0.4% (62198 remain 85%)
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 63084
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    7.3    6694    62198     25951   12552   8903   493  11  5.7 308.4    7
c -    7.4    6694    62197     26932    9784   9043   497   8  5.7 306.7    7
c -    8.3    6694    62197     34033   11740   9651   521   9  5.8 302.7    7
c -    9.3    6694    62197     41508   13656  10256   536  10  6.0 301.8    7
c -   10.2    6694    62197     49344   15623  10725   556  16  6.3 302.8    7
c -   10.8    6694    62197     56819   17109  11016   560  27  7.0 308.9    7
c R   10.8    6694    62197     57048   17297  11030   561  22  7.0 309.3    8
c 
c [simplification-5] limit of 63128 conflicts hit after 63128 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 6694 free variables schedulable
c [ternres-3] 1095 ternary resolvents (13 bin, 1082 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 3714 xors of average arity 3.0
c [gauss-2] connected 11142 occurrences of 1483 variables (average 7.5)
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 6694 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 486580 with penalty 1 = 1 + 0
c [lift-2] using 1603 probes 24%
c [lift-2-1] found 0 units 6 impls in round 1
c [lift-2] 0 units, 9 impls, 0 eqs in 2 rounds
c [lift-2] 1349 variables remain 20% (5345 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1621934 with penalty 0 = 0 + 0
c [transred-3] removed 6 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 99 clauses out of 19366 (1%) of length 5
c [cce-4-1] eliminated 210 clauses out of 24624 (1%) of length 4
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] eliminated 309 large clauses in 17376205 steps
c [cce-4-1] allowing another 8688102 steps for small clauses
c [cce-4] scheduling 15141 clauses = 606 binary + 14535 ternary
c [cce-4] tried to eliminate 15141 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 11997420 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 311 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 15139 clauses = 606 binary + 14533 ternary
c [cce-4] tried to eliminate 15139 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 311 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 6694 variables 100%
c [elim-4] limit of 16219345 steps penalty 1 = 1 + 0
c [elim-4] incomplete 6 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 6694
c [elim-4] 1 < 1/1000 * 6694 = 6 considered unsuccessful
c [rephase-2] after 63128 conflicts (new increment 40000, next 103128)
c [flushphases] 19 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 1 variables 0.0% (6693 remain 70%)
c [simplification-5] removed 312 irredundant clauses 0.5% (61885 remain 84%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 20000 = 40000 / 2
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] new conflict limit 123128
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   13.6    6693    61885     65677   18975  12596   613  11  7.0 307.1    8
c -   14.8    6693    61885     74888   20984  12971   621  13  7.3 306.5    8
c -   15.9    6693    61885     84564   22919  13351   627  10  7.5 306.6    8
c -   17.2    6693    61885     94858   24981  13722   636  15  7.8 304.7    8
c -   18.8    6693    61885    105633   27069  14096   646  21  8.0 303.9    8
c -   19.6    6693    61885    116171   28729  14258   651  21  9.2 306.9    8
c 
c [simplification-6] limit of 123142 conflicts hit after 123143 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6693 free variables schedulable
c [ternres-4] 555 ternary resolvents (7 bin, 548 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 16 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 19 out of 19 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 1767055 penalty 1 = 1 + 0
c [basicprobe-2-0] 1279 sched 19%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-2-1] 1279 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 1278 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-3] 1278 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-3] fully completed probing
c [basicprobe-2-3] removed 0 variables, found 7 hbrs
c [unhide-3] limit 176705 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 14 tauts, 0 hbrs, 1890 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 6 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 34 clauses out of 19229 (0%) of length 5
c [cce-5-1] eliminated 77 clauses out of 24406 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 111 large clauses in 17541448 steps
c [cce-5-1] allowing another 8770724 steps for small clauses
c [cce-5] scheduling 15157 clauses = 603 binary + 14554 ternary
c [cce-5] tried to eliminate 15157 small clauses 100%
c [cce-5] eliminated 3 small clauses 0%
c [cce-5] eliminated 1 binary clauses 0%
c [cce-5] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 3 small clauses in 12157872 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 114 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 15154 clauses = 602 binary + 14552 ternary
c [cce-5] tried to eliminate 15154 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 114 covered clauses in TOTAL during 2 rounds
c [rephase-3] after 123143 conflicts (new increment 80000, next 203143)
c [flushphases] 4 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-6] removed 114 irredundant clauses 0.2% (61771 remain 84%)
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 243143
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   21.1    6693    61771    124307   36577  14898   668  24  9.7 309.4   11
c -   21.6    6693    61771    127223   30256  15017   670  13  9.7 308.3    9
c -   23.5    6693    61771    139499   32424  15317   676  12  9.6 306.6    9
c -   25.2    6693    61771    152326   34664  15630   683  15  9.8 306.4    9
c -   27.4    6693    61771    165645   36781  15941   689  12  9.8 305.4    9
c -   29.1    6693    61771    179664   39191  16249   691  21 10.1 306.9   10
c -   31.3    6693    61771    193551   41012  16482   693  13 10.5 305.6   10
c -   33.5    6693    61771    208124   43081  16699   693  12 10.7 305.1   10
c -   36.2    6693    61771    223606   45407  16964   699  18 10.7 304.0   10
c -   38.0    6693    61771    238912   47428  17134   699  30 11.4 304.8   10
c 
c [simplification-7] limit of 243143 conflicts hit after 243143 conflicts
c [ternres-5] limit 8492986 with penalty 0 = 0 + 0
c [ternres-5] all 6693 free variables schedulable
c [ternres-5] 467 ternary resolvents (6 bin, 461 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 6693 variables 100%
c [block-3] limit of 21232466 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 47 clauses out of 19128 (0%) of length 5
c [cce-6-1] eliminated 112 clauses out of 24356 (0%) of length 4
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] eliminated 159 large clauses in 17647516 steps
c [cce-6-1] allowing another 8823758 steps for small clauses
c [cce-6] scheduling 1035 clauses = 602 binary + 433 ternary
c [cce-6] tried to eliminate 1035 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 9008318 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 160 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 1034 clauses = 602 binary + 432 ternary
c [cce-6] tried to eliminate 1034 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 160 covered clauses in TOTAL during 2 rounds
c [bca-3] limit of 10000000 steps
c [bca-3] 1404 out of 13388 literals actually usable 10%
c [bca-3] added 0 blocked clauses in 57838 steps
c [rephase-4] after 243143 conflicts (new increment 160000, next 403143)
c [flushphases] 2 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-7] removed 160 irredundant clauses 0.3% (61611 remain 84%)
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 483143
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   40.0    6693    61611    254119   48823  17685   702  24 12.3 306.7   11
c R   41.4    6693    61611    269154   63554  17739   702  30 13.9 308.0   18
c -   41.5    6693    61611    269582   49959  17751   702  17 13.8 307.9   11
c -   44.7    6693    61611    286730   52118  17946   706  12 13.7 305.9   11
c -   47.7    6693    61611    304251   54229  18075   706  13 13.8 304.8   12
c -   50.5    6693    61611    322354   56456  18220   707  28 14.0 304.8   12
c -   53.8    6693    61611    340661   58348  18342   708  17 14.3 304.2   12
c -   57.2    6693    61611    359736   60447  18471   708  18 14.5 303.3   12
c -   60.5    6693    61611    379425   62796  18596   709  27 14.6 302.8   12
c -   63.1    6693    61611    398793   64069  18656   710  23 16.4 303.3   12
c -   66.9    6693    61611    419308   66284  18738   712  22 16.3 302.6   12
c -   71.5    6693    61611    440341   68399  18863   713  12 16.2 301.5   13
c -   75.0    6693    61611    461976   70630  18966   715  22 16.4 301.8   13
c 
c [simplification-8] limit of 483149 conflicts hit after 483150 conflicts
c [ternres-6] limit 20606093 with penalty 0 = 0 + 0
c [ternres-6] all 6693 free variables schedulable
c [ternres-6] 222 ternary resolvents (5 bin, 217 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1030304 penalty 2 = 2 + 0
c [gauss-3] extracted 2818 xors of average arity 3.0
c [gauss-3] connected 8454 occurrences of 1483 variables (average 5.7)
c [gauss-3] limit 1030304 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 3808 schedulable variables 57%
c [simpleprobe-3] limit 41212187 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 515152 penalty 2 = 2 + 0
c [cgrclsr-3] all 6693 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 3090914 with penalty 2 = 2 + 0
c [lift-3] using 364 probes 5%
c [lift-3-1] found 0 units 1 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, 1 impls, 0 eqs in 6 rounds
c [lift-3] 985 variables remain 15% (5708 retained)
c [cliff-3] limit of 4121218 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 47 transitive binary clauses
c [cce-7] limit of 41212187 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 35 clauses out of 19052 (0%) of length 5
c [cce-7-1] eliminated 85 clauses out of 24235 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 120 large clauses in 17591017 steps
c [cce-7-1] allowing another 8795508 steps for small clauses
c [cce-7] scheduling 1062 clauses = 602 binary + 460 ternary
c [cce-7] tried to eliminate 1062 small clauses 100%
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 120 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 1062 clauses = 602 binary + 460 ternary
c [cce-7] tried to eliminate 1062 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 120 covered clauses in TOTAL during 2 rounds
c [elim-5] 6 variables 0% will be scheduled this time
c [elim-5] scheduled 6 variables 0%
c [elim-5] limit of 103030469 steps penalty 2 = 2 + 0
c [elim-5-1] no variable eliminated in round 1 in 88046 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 6693
c [rephase-5] after 483150 conflicts (new increment 320000, next 803150)
c [flushphases] 2 phases reset
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-8] removed 120 irredundant clauses 0.2% (61491 remain 84%)
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 963150
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   80.7    6693    61491    484122   72853  19306   735  22 16.3 301.0   14
c -   84.5    6693    61491    506487   75005  19365   735  31 16.8 300.7   14
c -   87.8    6693    61491    528559   75777  19371   735  30 20.2 301.2   14
c -   90.7    6693    61491    551205   76621  19387   735  23 22.6 302.0   14
c -   93.3    6693    61491    574634   78142  19408   735  23 23.9 303.1   14
c R   93.9    6693    61491    579423   82783  19410   735  27 24.3 303.2   20
c -   98.4    6693    61491    598898   79901  19512   735  16 24.0 302.1   14
c -  103.9    6693    61491    624141   82211  19621   736  13 23.7 301.2   15
c -  108.6    6693    61491    649697   84346  19702   737  15 23.6 300.9   15
c -  114.3    6693    61491    675841   86587  19780   737  15 23.4 300.0   15
c -  118.2    6693    61491    702808   88919  19855   737  30 23.9 300.2   15
c -  124.1    6693    61491    729771   91114  19944   739  30 23.8 299.2   15
c -  130.0    6693    61491    757129   93283  20006   739  26 23.5 298.5   15
c -  136.2    6693    61491    785009   95174  20065   740  25 23.6 297.8   15
c -  142.5    6693    61491    813653   97571  20120   740  28 23.5 297.4   15
c -  145.8    6693    61491    841971   98953  20132   740  27 24.5 298.3   15
c -  152.2    6693    61491    871440  100857  20175   740  23 25.1 297.8   16
c -  159.1    6693    61491    901591  103214  20254   740  26 24.9 297.5   16
c -  166.0    6693    61491    931973  105154  20318   740  27 25.1 297.0   16
c -  172.9    6693    61491    963089  107267  20375   741  27 25.0 296.6   16
c 
c [simplification-9] limit of 963150 conflicts hit after 963150 conflicts
c [ternres-7] limit 49549087 with penalty 0 = 0 + 0
c [ternres-7] all 6693 free variables schedulable
c [ternres-7] 228 ternary resolvents (1 bin, 227 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 10 transitive binary clauses
c [cce-8] limit of 99098175 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 24 clauses out of 18992 (0%) of length 5
c [cce-8-1] eliminated 49 clauses out of 24155 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 73 large clauses in 17668126 steps
c [cce-8-1] allowing another 8834063 steps for small clauses
c [cce-8] scheduling 15197 clauses = 603 binary + 14594 ternary
c [cce-8] tried to eliminate 15197 small clauses 100%
c [cce-8] eliminated 3 small clauses 0%
c [cce-8] eliminated 3 ternary clauses 0%
c [cce-8-1] eliminated 3 small clauses in 12394904 steps
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 76 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 15194 clauses = 603 binary + 14591 ternary
c [cce-8] tried to eliminate 15194 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 76 covered clauses in TOTAL during 2 rounds
c [rephase-6] after 963150 conflicts (new increment 640000, next 1603150)
c [flushphases] 2 phases reset
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-9] removed 76 irredundant clauses 0.1% (61415 remain 84%)
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 1923150
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  180.9    6693    61415    994505  109255  20658   732  16 25.0 296.3   18
c -  188.4    6693    61415   1026561  111531  20703   732  22 24.8 296.0   18
c -  196.6    6693    61415   1059074  113639  20740   732  16 24.7 295.5   18
c -  203.6    6693    61415   1092115  115702  20777   732  35 25.1 295.1   18
c -  209.1    6693    61415   1125566  116470  20783   732  34 27.3 295.5   19
c -  213.9    6693    61415   1158976  117460  20792   732  31 28.5 296.0   18
c -  222.7    6693    61415   1197355  118164  20796   733  30 33.5 296.3   19
c -  231.0    6693    61415   1234191  118881  20797   733  29 36.9 296.7   29
c -  239.9    6693    61415   1269699  120763  20832   734  16 36.8 296.2   19
c -  249.3    6693    61415   1305944  122924  20890   735  18 36.6 295.6   19
c -  259.4    6693    61415   1342879  125399  20948   736  15 36.1 294.9   19
c -  267.4    6693    61415   1379897  127482  20969   736  15 35.9 295.0   19
c -  277.6    6693    61415   1417774  129967  21013   736  21 35.4 294.6   19
c -  287.2    6693    61415   1456408  131932  21054   736  20 35.8 294.4   19
c -  295.3    6693    61415   1495930  133937  21100   739  30 36.6 294.4   19
c -  305.5    6693    61415   1535302  135591  21145   739  27 37.2 294.1   20
c -  316.5    6693    61415   1574824  137626  21188   740  16 36.8 293.8   20
c -  328.9    6693    61415   1615297  140113  21233   741  23 36.4 293.1   20
c -  339.1    6693    61415   1656230  142406  21273   741  16 36.3 293.0   20
c -  350.2    6693    61415   1697500  144732  21321   741  22 35.9 292.8   20
c -  363.7    6693    61415   1739341  147080  21384   741  16 35.5 292.2   20
c -  370.1    6693    61415   1781604  148753  21403   741  31 36.2 292.9   20
c -  377.1    6693    61415   1824285  150140  21405   741  32 37.1 293.3   20
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  391.3    6693    61415   1867410  152332  21460   741  17 36.6 292.8   21
c -  404.4    6693    61415   1911375  154751  21505   741  15 36.4 292.5   21
c 
c [simplification-10] limit of 1923152 conflicts hit after 1923155 conflicts
c [ternres-8] limit 124898357 with penalty 0 = 0 + 0
c [ternres-8] all 6693 free variables schedulable
c [ternres-8] 183 ternary resolvents (2 bin, 181 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 7806147 penalty 3 = 3 + 0
c [card-4] found 3 at-most-one constraints of average size 3.0
c [card-4] found 21 at-most-two constraints of average size 4.0
c [card-4] using previous limit 7806147 for elimination
c [card-4] 24 out of 24 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, 905 tauts, 0 hbrs, 10795 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [cce-9] limit of 249796715 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 13 clauses out of 18950 (0%) of length 5
c [cce-9-1] eliminated 41 clauses out of 24091 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 54 large clauses in 17686905 steps
c [cce-9-1] allowing another 8843452 steps for small clauses
c [cce-9] scheduling 1093 clauses = 604 binary + 489 ternary
c [cce-9] tried to eliminate 1093 small clauses 100%
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 54 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 1093 clauses = 604 binary + 489 ternary
c [cce-9] tried to eliminate 1093 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 54 covered clauses in TOTAL during 2 rounds
c [cce-9] 54 < 1/1000 * 61415 = 61 considered unsuccessful
c [rephase-7] after 1923155 conflicts (new increment 1280000, next 3203155)
c [flushphases] 2 phases reset
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-10] removed 54 irredundant clauses 0.1% (61361 remain 84%)
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 2923155
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  417.1    6693    61361   1955515  156486  21104   741  19 36.2 292.4   23
c -  430.4    6693    61361   2000504  159206  21138   741  27 35.9 292.0   23
c -  445.3    6693    61361   2045652  161484  21187   743  24 35.6 291.5   23
c -  454.2    6693    61361   2091953  163001  21211   743  14 36.3 291.9   23
c -  470.3    6693    61361   2138609  165785  21270   744  24 36.0 291.3   24
c -  484.8    6693    61361   2185017  167746  21302   744  23 35.8 291.0   24
c -  497.8    6693    61361   2232166  169714  21325   744  26 35.8 290.9   24
c -  511.0    6693    61361   2280033  171707  21361   744  30 35.8 290.7   24
c -  526.5    6693    61361   2328500  174223  21404   744  25 35.6 290.5   24
c -  534.8    6693    61361   2378096  175492  21409   744  30 36.8 291.0   24
c -  544.9    6693    61361   2428528  176607  21411   744  34 38.1 291.3   24
c -  555.2    6693    61361   2479452  177498  21416   744  32 39.6 291.7   24
c -  563.5    6693    61361   2529628  178890  21426   745  29 40.3 292.2   23
c -  579.2    6693    61361   2583641  179615  21427   745  29 43.2 292.7   26
c -  597.4    6693    61361   2638972  180200  21427   745  28 46.3 293.1   26
c R  599.1    6693    61361   2647084  187734  21427   745  28 46.6 293.1   39
c -  616.1    6693    61361   2691082  182274  21476   745  15 46.1 292.6   25
c -  634.0    6693    61361   2743897  185021  21528   746  18 45.6 292.2   25
c -  649.5    6693    61361   2797206  187620  21561   746  29 45.4 292.1   25
c -  668.9    6693    61361   2850518  190019  21627   746  24 44.9 291.7   25
c -  683.1    6693    61361   2904889  191801  21655   746  31 45.3 291.7   24
c 
c [simplification-11] limit of 2923155 conflicts hit after 2923155 conflicts
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 6693 free variables schedulable
c [ternres-9] 170 ternary resolvents (5 bin, 165 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 2757146 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5155 literals 39%
c [treelook-3] scheduling used 788033 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2757146 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 577545 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 4 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6693 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] 814 out of 13388 literals actually usable 6%
c [bca-4] added 0 blocked clauses in 213190 steps
c [simplification-11] removed 0 variables 0.0% (6693 remain 70%)
c [simplification-11] removed 0 irredundant clauses 0.0% (61361 remain 84%)
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 4923155
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  701.7    6693    61361   2959266  193980  21852   752  25 45.1 291.5   27
c -  721.5    6693    61361   3014196  196264  21911   752  16 44.7 291.2   27
c -  737.9    6693    61361   3069977  198514  21958   752  17 44.6 291.2   27
c -  758.2    6693    61361   3126134  200992  21992   752  15 44.3 290.7   28
c -  774.2    6693    61361   3185071  203248  22029   754  30 45.0 290.9   27
c -  789.5    6693    61361   3242200  204528  22049   754  16 45.5 291.0   28
c -  810.5    6693    61361   3299987  206955  22123   754  15 45.2 290.7   28
c -  828.1    6693    61361   3358505  209266  22174   754  15 45.2 290.6   28
c -  850.5    6693    61361   3417091  211740  22208   754  16 44.8 290.3   28
c -  869.8    6693    61361   3476427  214076  22246   755  26 44.6 290.1   28
c -  890.1    6693    61361   3535987  216269  22305   755  16 44.5 290.0   29
c -  914.4    6693    61361   3596090  218653  22342   755  16 44.2 289.7   29
c -  935.7    6693    61361   3657262  221254  22406   756  23 44.1 289.5   29
c -  960.2    6693    61361   3718351  223604  22468   756  19 43.7 289.3   29
c -  974.3    6693    61361   3781484  225390  22478   756  27 44.4 289.5   29
c -  991.1    6693    61361   3847193  226559  22481   756  31 45.9 289.8   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), 348079 steps
c bkwd: tried 122473 clauses, 244946 lits, 2.00 lits/clause
c bkwd: checked 5056473 occs, 41.29 occs/clause, 20.64 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 0 removed, 2299223 resolutions, 5005286 steps
c blkd: 4 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 4 units, 0 am1, 11223086 steps
c card: 54 rescheduled, 238 eliminated, 30648 resolved, 3164 subsumed
c card: 9 at-most-one constraints found, average size 3.00
c card: 9 at-most-one constraints used 100%, average size 3.00
c card: 165 at-most-two constraints found, average size 4.00
c card: 165 at-most-two constraints used 100%, average size 4.00
c cces: 9 cces, 11058 eliminated, 11056 ate 100%, 2 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, 815153 esteps, 58248 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: 2298 extracted (90 ands 4%, 2004 xors 87%, 204 ites 9%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 500812 decisions, 9291867 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 361990 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 52 gcs, 0 rescored clauses, 2026 rescored vars
c dcps: 23 decompositions, 25 equivalent 0%
c deco: 90274 decision-only clauses 2%, 47% reduction
c decs: 61938055 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3751765 flipped 6.057% (in 7501 phases)
c elms: 5 elims, 2793 eliminated 29%
c elms: 7 rounds, 1.4 rounds/bve
c elms: 2793 small 100%, 0 large 0%
c elms: 19114 tried small, 2793 succeeded 15%, 16321 failed 85%
c elms: 158 subsumed, 198 strengthened, 1 blocked
c elms: 1488799 copies, 2750408 resolutions, 1920404 ipos
c elms: 49217 subchks, 49300 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 16962 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 8061108 steps, 4030554 extr 50%, 2469025 elim 31%
c glue: 46.8 orig avg, 45.8 real avg, 4.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 644 = 421 simple + 216 trn 65% + 7 lrg 34%, 29 sub 1%
c hght: 290 average, 6.20 height/glue
c ints: 98302 luby (28819470 steps), 0 inout (0 steps)
c lift: 3 phases, 48696 probed (16238 level1 33%, 32458 level2 67%)
c lift: 0 units, 0 equivalences, 21 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3852800 clauses, 88.4 length
c lrnd: 1704817 uips 44%, 1653519 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 340611949 learned lits, 11% minimized
c mins: 3411753 mins 89%, 53 bin 0%, 350720 size 9%, 90274 deco 2%
c move: moved 3852800, 11 bin 0%, 267 trn 0%, 0 lrg 0%
c otfs: str 90512 dyn (89682 red, 830 irr) 27975 drv 31%, 62537 rst 69%
c otfs: sub 470 dyn (469 red, 1 irr)
c phas: 10 computed, 7018 set, 2310 pos (33%), 4708 neg (67%)
c prbs: 2 basic, 16288 probed, 0 failed, 0 lifted
c prbs: 3 simple, 36852 probed, 1 failed, 19 eqs
c prbs: 3 treelook, 9350 probed, 0 failed, 0 lifted
c prps: 960072028 props, 15 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 45766851 searches, 1844164 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: 115 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 115 arith 100%, 0 double 0%
c rmbd: 68 removed, 68 red 100%
c rphs: 7 recomputed phases
c rsts: 91438 restarts 93%, 6864 skipped 7%
c rsts: 0 saturating 0%, 2309 agile 34%, 4555 reuse 66%
c rsts: 42.1 avg interval, 42.1 scaled, 1.0 factor
c rsts: 13484 kept 14.7% average 38.2%
c simp: 11 count (11 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3852800 count (5999524 tried 1.6), 77454 sub out of 3841955 (2.0%)
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: 16 fixed 0%, 0 its, 0.00 confs/it
c trvs: 52295986778 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 54.5 search traversals per propagation, 13472.8 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 9 transitive reductions, 111 removed, 0 failed
c trds: 120082 nodes, 11295 edges, 19701 steps
c trim: 2878128 words, 11.0 MB
c trnr: 9 count, 80 bin, 8353 trn, 30911072 steps
c unhd: 4 count, 6 rounds, 3654724 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: 1165 tauts, 0 bin 0%, 885 trn 76%, 262 lrg 22%
c unhd: 1165 tauts, 18 stamp 2%, 1123 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 12800 str, 0 bin 0%, 90 trn 1%, 12710 lrg 99%, 12690 red 99%
c vars: 6693 remaining 70% and 2834 removed 30% out of 9527
c vars: 16 fixed 0%, 2793 eliminated 29%, 25 equivalent 0%
c vsts: 32113209306 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 33.5 search visits per propagation, 8272.1 per conflict
c wchs: 8408506422 pushed, 13331862 enlarged, 767 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3841955 100   3503211 100 236368079 100  40516947 100   1865347 100
c 
c  0     172476   4         0   0 190419466  81< 24274662  60   1048607  56 
c  1     264677   7    204159   6  26338670  11   4609403  11<   230091  12 
c  2     768521  20    764529  22   7274622   3   3021330   7    138855   7<
c  3     693607  18    687883  20   5114990   2   2711608   7    118035   6 
c  4     476237  12    471325  13   3024252   1   1835019   5     80271   4 
c  5     324417   8<   320344   9<  1566273   1   1121984   3     50759   3 
c  6     232856   6    229695   7    838746   0    707597   2     36425   2 
c  7     176955   5    174241   5    483924   0    480655   1     27458   1 
c  8     139416   4    137051   4    306165   0    347364   1     21352   1 
c  9     112594   3    110337   3    200788   0    263454   1     18114   1 
c 10     170542   4    166243   5    258927   0    386487   1     32161   2 
c 11     154714   4    144553   4    227993   0    367954   1     41050   2 
c 12     146968   4     87766   3    298538   0    370586   1     20989   1 
c 13       7975   0      5085   0     14725   0     18844   0      1180   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.7           0.4           1.4           1.7
c std             3.2           3.0           1.2           2.5           2.9
c 
c   70.882   7% analysis
c   64.826   6% decide
c   12.838   1% bump
c   12.742   1% restart
c   10.951   1% defrag
c    5.764   1% mincls
c    4.133   0% cce
c    2.704   0% elim
c    2.003   0% reduce
c    1.423   0% gc
c    0.989   0% decomp
c    0.837   0% probe
c    0.433   0% cliff
c    0.398   0% block
c    0.297   0% unhide
c    0.276   0% gauss
c    0.269   0% backward
c    0.253   0% ternres
c    0.200   0% card
c    0.191   0% bca
c    0.189   0% phase
c    0.179   0% lift
c    0.143   0% cgrclsr
c    0.018   0% transred
c    0.003   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c    0.000   0% tabularasa
c ----------------------------------
c    0.273   0% probe simple     33%
c    0.209   0% probe basic      25%
c    0.355   0% probe tree-look  42%
c ==================================
c    1.011   0% preprocessing     9%
c   10.122   1% inprocessing     91%
c ==================================
c   11.133   1% simplifying
c  988.887  99% search
c ==================================
c 1000.020 100% all
c 
c 61938055 decisions, 61936.8 decisions/sec
c 3880775 conflicts, 3880.7 conflicts/sec
c 960072028 propagations, 1.0 megaprops/sec
c 1000.0 seconds, 128.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
