c launch: /data/cnf/sc2014/app/hitag2-7-60-0-0xe8fa35372ed37e2-80.cnf.bz2
c host: atom11
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/hitag2-7-60-0-0xe8fa35372ed37e2-80.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hitag2-7-60-0-0xe8fa35372ed37e2-80.cnf.bz2
c no embedded options
c found 'p cnf 2262 29727' header
c read 2262 variables, 29727 clauses, 174405 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 2187 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    2187    29659         0       0      0     0   0  0.0   0.0    2
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 225 variables
c [simpleprobe-1] all 2030 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 294 variables remain 14% (1736 retained)
c [simpleprobe-1] removed 0 variables, found 219 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 4966 tauts, 0 hbrs, 7305 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 2030 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 405 variables 20% in round 1 in 3400851 steps
c [elim-1-1] backward subsumption/strengthening limit 6801702
c [elim-1-1] subsumed 357 and strengthened 914 clauses in 6802316 steps
c [elim-1-1] rescheduled 257 variables 13% by backward subsumption
c [elim-1-2] eliminated 35 variables 2% in round 2 in 479769 steps
c [elim-1-2] backward subsumption/strengthening limit 959538
c [elim-1-2] subsumed 5 and strengthened 39 clauses in 959954 steps
c [elim-1-2] rescheduled 55 variables 3% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 42605 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 440 = 22% variables out of 2030
c [phase-1] phase bias: 296 positive 19%, 1294 negative 81%
c [simplification-1] removed 597 variables 27.3% (1590 remain 73%)
c [simplification-1] removed 9155 irredundant clauses 30.9% (20504 remain 69%)
c [simplification-1] maximum reduction of 31% = max (27%, 31%)
c [simplification-1] large reduction 31% >= 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] 14629, max 23010, min4 10494 at 75%, min10 4093 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.6    1590    20504         6       6      0   108   0  4.2  31.6    2
c R    0.6    1590    20504        21      18      0   108   1  8.8  29.8    2
c R    0.6    1590    20504        63      55      1   108   3 12.8  28.3    2
c R    0.6    1590    20504       168     145      5   108   7 10.4  26.9    2
c R    0.6    1590    20501       420     365     16   110  14 12.1  25.5    2
c R    0.7    1590    20499       996     878     47   111  22 12.7  23.6    3
c 
c [simplification-2] limit of 1006 conflicts hit after 1007 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 3180 literals 100%
c [treelook-1] scheduling used 61441 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 301039 steps
c [treelook-1] 3009 literals remain 95%
c [treelook-1] 1589 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 43 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1117 sched 71%, 19 failed, 0 lifted, 112 hbrs
c [decomp-5] removed 19 variables
c [basicprobe-1-1] 1080 sched 69%, 1 failed, 0 lifted, 28 hbrs
c [decomp-6] removed 1 variables
c [basicprobe-1-2] 1070 sched 68%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-3] 1068 sched 68%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-3] fully completed probing
c [basicprobe-1-3] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-1-3] removed 20 variables, found 142 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 1570 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 755 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 445 clauses out of 9088 (5%) of length 7
c [cce-1-1] eliminated 1045 clauses out of 1984 (53%) of length 6
c [cce-1-1] eliminated 1597 clauses out of 3081 (52%) of length 5
c [cce-1-1] eliminated 474 clauses out of 1985 (24%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 3561 large clauses in 33748281 steps
c [cce-1-1] allowing another 16874140 steps for small clauses
c [cce-1] scheduling 3172 clauses = 2669 binary + 503 ternary
c [cce-1] tried to eliminate 3172 small clauses 100%
c [cce-1] eliminated 34 small clauses 1%
c [cce-1] eliminated 31 binary clauses 1%
c [cce-1] eliminated 3 ternary clauses 1%
c [cce-1-1] eliminated 34 small clauses in 19108629 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3595 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 3138 clauses = 2638 binary + 500 ternary
c [cce-1] tried to eliminate 3138 small clauses 100%
c [cce-1] eliminated 128 small clauses 4%
c [cce-1] eliminated 128 binary clauses 5%
c [cce-1-2] eliminated 128 small clauses in 2186003 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 128 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 0 steps for small clauses
c [cce-1] scheduling 3010 clauses = 2510 binary + 500 ternary
c [cce-1] tried to eliminate 3010 small clauses 100%
c [cce-1] eliminated 26 small clauses 1%
c [cce-1] eliminated 26 binary clauses 1%
c [cce-1-3] eliminated 26 small clauses in 2157487 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 26 covered clauses in round 3
c [cce-1-4] completed large round (ACCE)
c [cce-1-4] allowing another 0 steps for small clauses
c [cce-1] scheduling 2984 clauses = 2484 binary + 500 ternary
c [cce-1] tried to eliminate 2984 small clauses 100%
c [cce-1-4] completed small round (ACCE)
c [cce-1-4] eliminated 0 covered clauses in round 4
c [cce-1] eliminated 3749 covered clauses in TOTAL during 4 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 1564 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 408 variables 26% in round 1 in 2882323 steps
c [elim-2-1] backward subsumption/strengthening limit 5764646
c [elim-2-1] subsumed 0 and strengthened 137 clauses in 5765462 steps
c [elim-2-1] rescheduled 177 variables 11% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 91745 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 408 = 26% variables out of 1564
c [bca-1] limit of 10000000 steps
c [bca-1] 1576 out of 2314 literals actually usable 68%
c [bca-1] added 2 blocked clauses in 6441 steps
c [phase-2] phase bias: 2 positive 50%, 2 negative 50%
c [simplification-2] removed 434 variables 27.3% (1156 remain 53%)
c [simplification-2] removed 6042 irredundant clauses 29.5% (14457 remain 49%)
c [simplification-2] maximum reduction of 29% = max (27%, 29%)
c [simplification-2] large reduction 29% >= 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 3007
c [tabula-rasa-1] number clauses 14457 drops below limit 14829
c [flush-cache] 0 binary, 0 ternary, 367 large
c [flushphases] 1156 phases reset fully
c [phase-3] phase bias: 40 positive 43%, 53 negative 57%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] conflict limit 20000 does not change
c [tabula-rasa-1] new variable limit 289 and clause limit 7228
c 
c [simplification-3] limit of 3007 conflicts hit after 3009 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 1156 free variables schedulable
c [ternres-1] 201 ternary resolvents (0 bin, 201 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 2 out of 2 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 851 xors of average arity 6.1
c [gauss-1] connected 5149 occurrences of 69 variables (average 74.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [simpleprobe-2] 146 schedulable variables 13%
c [simpleprobe-2] limit 1000000 penalty 1 = 1 + 0
c [decomp-9] removed 1 variables
c [simpleprobe-2] 133 variables remain 12% (1022 retained)
c [simpleprobe-2] removed 1 variables, found 3 hbrs, 1 units
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 1155 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 620 probes 54%
c [lift-1-1] found 5 units 2 impls in round 1
c [lift-1] 5 units, 2 impls, 0 eqs in 2 rounds
c [lift-1] 530 variables remain 46% (620 retained)
c [lift-1] removed 5 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 6, lifted 0
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 14 tauts, 0 hbrs, 1426 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 15 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1144 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 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-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 33 (3%) of length 8
c [cce-2-1] eliminated 33 clauses out of 8389 (0%) of length 7
c [cce-2-1] eliminated 4 clauses out of 710 (1%) of length 6
c [cce-2-1] eliminated 36 clauses out of 1193 (3%) of length 5
c [cce-2-1] eliminated 23 clauses out of 1782 (1%) of length 4
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] eliminated 97 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 1963 clauses = 1497 binary + 466 ternary
c [cce-2] tried to eliminate 1963 small clauses 100%
c [cce-2] eliminated 77 small clauses 4%
c [cce-2] eliminated 73 binary clauses 5%
c [cce-2] eliminated 4 ternary clauses 1%
c [cce-2-1] eliminated 77 small clauses in 16647784 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] eliminated 174 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 1886 clauses = 1424 binary + 462 ternary
c [cce-2] tried to eliminate 1886 small clauses 100%
c [cce-2] eliminated 2 small clauses 0%
c [cce-2] eliminated 2 binary clauses 0%
c [cce-2-2] eliminated 2 small clauses in 1602675 steps
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] eliminated 2 covered clauses in round 2
c [cce-2-3] completed large round (ACCE)
c [cce-2-3] allowing another 0 steps for small clauses
c [cce-2] scheduling 1884 clauses = 1422 binary + 462 ternary
c [cce-2] tried to eliminate 1884 small clauses 100%
c [cce-2-3] completed small round (ACCE)
c [cce-2-3] eliminated 0 covered clauses in round 3
c [cce-2] eliminated 176 covered clauses in TOTAL during 3 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1144 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 304 variables 27% in round 1 in 15912468 steps
c [elim-3-1] backward subsumption/strengthening limit 4087532
c [elim-3-1] subsumed 4 and strengthened 37 clauses in 4087755 steps
c [elim-3] incomplete 92 not tried 8% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 304 = 27% variables out of 1144
c [bca-2] limit of 10000000 steps
c [bca-2] 1036 out of 1682 literals actually usable 62%
c [bca-2] added 3 blocked clauses in 5817 steps
c [phase-4] phase bias: 10 positive 59%, 7 negative 41%
c [simplification-3] removed 316 variables 27.3% (840 remain 38%)
c [simplification-3] removed 1154 irredundant clauses 8.0% (13297 remain 45%)
c [simplification-3] maximum reduction of 27% = max (27%, 8%)
c [simplification-3] large reduction 27% >= 5% limit
c [simplification-3] new conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] new conflict limit 5009
c 
c [simplification-4] limit of 5009 conflicts hit after 5011 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 840 free variables schedulable
c [ternres-2] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 828 xors of average arity 6.3
c [gauss-2] connected 5180 occurrences of 64 variables (average 80.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 12 probes 1%
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] 333 variables remain 40% (507 retained)
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 0, lifted 0
c [transred-2] limit 100000 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 8352 (0%) of length 7
c [cce-3-1] eliminated 12 clauses out of 1106 (1%) of length 5
c [cce-3-1] eliminated 13 clauses out of 1702 (1%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 26 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 1138 clauses = 788 binary + 350 ternary
c [cce-3] tried to eliminate 1138 small clauses 100%
c [cce-3] eliminated 3 small clauses 0%
c [cce-3] eliminated 3 binary clauses 0%
c [cce-3-1] eliminated 3 small clauses in 16197506 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 29 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 1135 clauses = 785 binary + 350 ternary
c [cce-3] tried to eliminate 1135 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 29 covered clauses in TOTAL during 2 rounds
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 840 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 36 not tried 4% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 5 = 1% variables out of 840
c [bca-3] limit of 10000000 steps
c [bca-3] 946 out of 1672 literals actually usable 57%
c [bca-3] added 0 blocked clauses in 7111 steps
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 5 variables 0.6% (835 remain 38%)
c [simplification-4] removed 58 irredundant clauses 0.4% (13239 remain 45%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
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 35011
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -    4.7     835    13239      7186    2320    240   146  36 15.1  21.5    2
c -    4.9     835    13239     11334    3011    246   146  36 14.8  20.6    2
c -    5.3     835    13239     16017    3698    251   146  35 14.2  19.8    2
c /    5.7     835    13237     21318    4395    253   146  37 13.9  19.3    3
c /    5.8     835    13237     21934    2906    254   146  37 13.9  19.2    2
c /    5.9     835    13237     24568    3006    256   146  37 13.8  19.0    2
c -    6.1     835    13237     27157    3115    259   146  36 13.6  18.8    2
c -    6.4     835    13237     31112    3731    259   146  36 13.6  18.6    3
c 
c [simplification-5] limit of 35011 conflicts hit after 35012 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 835 free variables schedulable
c [ternres-3] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-3] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1669 literals 100%
c [treelook-2] scheduling used 63196 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 153793 steps
c [treelook-2] 1593 literals remain 95%
c [treelook-2] 834 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 17 hbrs
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 835 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [transred-3] limit 826501 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 835 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 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-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1062 (0%) of length 5
c [cce-4-1] eliminated 2 clauses out of 1697 (0%) of length 4
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 3 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 1074 clauses = 775 binary + 299 ternary
c [cce-4] tried to eliminate 1074 small clauses 100%
c [cce-4] eliminated 7 small clauses 1%
c [cce-4] eliminated 7 ternary clauses 2%
c [cce-4-1] eliminated 7 small clauses in 16176801 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 10 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 1067 clauses = 775 binary + 292 ternary
c [cce-4] tried to eliminate 1067 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 10 covered clauses in TOTAL during 2 rounds
c [cce-4] 10 < 1/1000 * 13237 = 13 considered unsuccessful
c [elim-5] 36 variables 4% will be scheduled this time
c [elim-5] scheduled 36 variables 4%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] incomplete 27 not tried 3% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 835
c [rephase-1] after 35012 conflicts (new increment 20000, next 55012)
c [flushphases] 65 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 0 variables 0.0% (835 remain 38%)
c [simplification-5] removed 15 irredundant clauses 0.1% (13222 remain 45%)
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 95012
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -    7.7     835    13222     35562    4362    289   160  34 13.4  18.4    2
c /    8.1     835    13222     40660    5020    292   160  35 13.5  18.3    2
c /    8.1     835    13222     41308    3543    294   160  35 13.5  18.3    2
c /    8.3     835    13222     43990    3648    295   160  35 13.5  18.2    2
c -    8.5     835    13222     46683    3730    297   160  35 13.4  18.1    3
c -    8.8     835    13222     50836    4305    300   160  36 13.4  18.0    3
c -    9.2     835    13222     55576    4917    303   160  35 13.4  17.9    3
c /    9.6     835    13222     60904    5533    306   160  36 13.4  17.8    3
c -    9.7     835    13222     61539    4042    306   160  36 13.4  17.8    3
c -   10.0     835    13222     65720    4612    308   160  36 13.3  17.7    3
c -   10.4     835    13222     70392    5214    309   160  36 13.3  17.6    2
c -   10.9     835    13222     75757    5821    310   160  35 13.3  17.5    3
c -   11.4     835    13222     81819    6461    312   160  35 13.2  17.4    3
c -   12.0     835    13222     88732    7065    314   160  36 13.2  17.2    3
c 
c [simplification-6] limit of 95012 conflicts hit after 95014 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 835 free variables schedulable
c [ternres-4] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] found 1 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 2 out of 2 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 432 xors of average arity 5.7
c [gauss-3] connected 2472 occurrences of 48 variables (average 51.5)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 2611835 penalty 0 = 0 + 0
c [basicprobe-2-0] 424 sched 51%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-2-1] 429 sched 51%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 23 hbrs
c [lift-3] limit 783550 with penalty 1 = 1 + 0
c [lift-3] using 12 probes 1%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 0 impls in round 2
c [lift-3-3] found 0 units 0 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-3] 316 variables remain 38% (519 retained)
c [cliff-3] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-3] failed 0, lifted 0
c [unhide-3] limit 130591 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 3 tauts, 0 hbrs, 3290 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 702 out of 1672 literals actually usable 42%
c [bca-4] added 0 blocked clauses in 14809 steps
c [rephase-2] after 95014 conflicts (new increment 40000, next 135014)
c [flushphases] 47 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (835 remain 38%)
c [simplification-6] removed 0 irredundant clauses 0.0% (13222 remain 45%)
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 215014
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   13.0     835    13222     96211    7655    348   182  37 13.1  17.1    3
c -   13.8     835    13222    104051    8217    348   182  36 13.2  17.2    4
c -   14.6     835    13221    112608    8782    348   182  37 13.3  17.2    4
c -   15.5     835    13221    121975    9364    350   182  37 13.3  17.2    4
c -   16.5     835    13220    131840    9963    352   182  36 13.3  17.2    4
c /   17.7     835    13220    142552   10531    353   182  38 13.4  17.2    4
c /   17.7     835    13220    142552    5024    353   182  38 13.4  17.2    3
c /   17.9     835    13220    145285    5046    353   182  37 13.4  17.2    3
c -   18.1     835    13220    148035    5052    354   182  37 13.4  17.2    3
c -   18.4     835    13220    152157    5592    354   182  37 13.4  17.1    3
c -   18.9     835    13220    157044    6110    356   182  37 13.4  17.1    3
c /   19.3     835    13220    162507    6644    358   182  37 13.4  17.1    3
c /   19.4     835    13220    163155    5153    359   182  37 13.4  17.1    3
c /   19.6     835    13220    165738    5169    359   182  36 13.4  17.1    3
c -   19.8     835    13220    168364    5197    360   182  36 13.4  17.1    3
c -   20.2     835    13220    172498    5716    361   182  37 13.4  17.1    3
c -   20.6     835    13220    177249    6247    361   182  37 13.4  17.1    3
c /   21.1     835    13220    182754    6776    362   182  36 13.4  17.0    3
c -   21.2     835    13220    183427    5279    362   182  36 13.4  17.0    3
c -   21.5     835    13220    187495    5825    362   182  37 13.4  17.0    3
c -   21.9     835    13220    192096    6362    362   182  36 13.4  17.0    3
c -   22.4     835    13220    197346    6900    362   182  37 13.4  16.9    3
c -   23.0     835    13220    203434    7450    362   182  37 13.3  16.9    3
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.7     835    13219    210201    8011    363   182  37 13.3  16.8    2
c 
c [simplification-7] limit of 215014 conflicts hit after 215015 conflicts
c [ternres-5] limit 6853865 with penalty 0 = 0 + 0
c [ternres-5] all 835 free variables schedulable
c [ternres-5] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 94 schedulable variables 11%
c [simpleprobe-3] limit 27415460 penalty 0 = 0 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 12 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 6 transitive binary clauses
c [cce-5] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 7500000 steps for small clauses
c [cce-5] scheduling 1178 clauses = 778 binary + 400 ternary
c [cce-5] tried to eliminate 1178 small clauses 100%
c [cce-5] eliminated 35 small clauses 3%
c [cce-5] eliminated 34 binary clauses 4%
c [cce-5] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 35 small clauses in 8819591 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 35 covered clauses in round 1
c [cce-5-2] eliminated 3 clauses out of 915 (0%) of length 5
c [cce-5-2] eliminated 19 clauses out of 1817 (1%) of length 4
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] eliminated 22 large clauses in 5609853 steps
c [cce-5-2] allowing another 2804926 steps for small clauses
c [cce-5] scheduling 1143 clauses = 744 binary + 399 ternary
c [cce-5] tried to eliminate 1143 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 22 covered clauses in round 2
c [cce-5-3] completed large round (ACCE)
c [cce-5-3] allowing another 0 steps for small clauses
c [cce-5] scheduling 1143 clauses = 744 binary + 399 ternary
c [cce-5] tried to eliminate 1143 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 57 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 835 variables 100%
c [elim-6] limit of 68538650 steps penalty 1 = 1 + 0
c [elim-6] incomplete 8 not tried 1% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 158 = 19% variables out of 835
c [rephase-3] after 215015 conflicts (new increment 80000, next 295015)
c [flushphases] 27 phases reset
c [phase-8] phase bias: 6 positive 60%, 4 negative 40%
c [simplification-7] removed 158 variables 18.9% (677 remain 31%)
c [simplification-7] removed 473 irredundant clauses 3.6% (12746 remain 43%)
c [simplification-7] maximum reduction of 19% = max (19%, 4%)
c [simplification-7] large reduction 19% >= 5% limit
c [simplification-7] new conflict interval 2150 = min (215015/100, 120000)
c [simplification-7] penalized conflict interval 2150 = 1 * 2150
c [simplification-7] new conflict limit 217165
c 
c [simplification-8] limit of 217165 conflicts hit after 217166 conflicts
c [ternres-6] limit 6925280 with penalty 0 = 0 + 0
c [ternres-6] all 677 free variables schedulable
c [ternres-6] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-6] fully completed ternary resolution
c [cgrclsr-3] limit 173132 penalty 2 = 2 + 0
c [cgrclsr-3] all 677 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 677 variables 100%
c [block-4] limit of 17313200 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 609 (0%) of length 6
c [cce-6-1] eliminated 7 clauses out of 864 (1%) of length 5
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 8 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 721 clauses = 429 binary + 292 ternary
c [cce-6] tried to eliminate 721 small clauses 100%
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 8 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 721 clauses = 429 binary + 292 ternary
c [cce-6] tried to eliminate 721 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 8 covered clauses in TOTAL during 2 rounds
c [cce-6] 8 < 1/1000 * 12746 = 12 considered unsuccessful
c [elim-7] 8 variables 1% will be scheduled this time
c [elim-7] scheduled 8 variables 1%
c [elim-7] limit of 138505602 steps penalty 0 = 0 + 0
c [elim-7-1] no variable eliminated in round 1 in 44091096 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 677
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 0 variables 0.0% (677 remain 31%)
c [simplification-8] removed 13 irredundant clauses 0.1% (12733 remain 43%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 120000
c [simplification-8] new conflict interval 240000
c [simplification-8] penalized conflict interval 240000 = 1 * 240000
c [simplification-8] new conflict limit 457166
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   26.8     677    12733    220174    8314    328   103  39 13.3  16.9    2
c -   27.4     677    12733    227270    8936    333   103  39 13.3  16.9    4
c -   28.2     677    12733    235239    9569    337   103  38 13.3  16.9    3
c -   28.9     677    12733    243482   10192    339   103  39 13.3  16.9    4
c -   29.9     677    12733    252674   10810    341   103  39 13.3  16.9    4
c /   31.0     677    12733    262977   11452    342   103  40 13.3  16.9    3
c -   31.0     677    12733    262977    5949    342   103  40 13.3  16.9    2
c -   31.3     677    12733    266844    6488    342   103  40 13.3  16.9    4
c -   31.7     677    12733    271427    7045    343   103  39 13.3  16.9    4
c -   32.2     677    12733    276681    7602    345   103  39 13.3  16.8    4
c -   32.7     677    12733    282613    8138    345   103  39 13.3  16.8    4
c -   33.3     677    12733    289416    8709    346   103  39 13.3  16.8    4
c -   34.1     677    12733    296940    9286    346   103  39 13.2  16.7    4
c -   34.9     677    12733    304830    9858    349   103  39 13.2  16.7    4
c -   35.7     677    12733    313469   10389    351   103  38 13.2  16.7    3
c -   36.7     677    12733    322806   10962    352   103  39 13.3  16.7    4
c -   37.7     677    12733    332867   11520    353   103  40 13.2  16.7    4
c -   38.8     677    12733    342615   12073    353   103  40 13.3  16.7    4
c -   40.0     677    12733    353913   12618    353   103  39 13.3  16.8    4
c -   41.3     677    12733    365478   13180    354   103  39 13.3  16.7    4
c -   42.8     677    12733    377878   13749    354   103  38 13.3  16.7    5
c -   44.4     677    12733    391453   14307    354   103  39 13.3  16.7    5
c -   46.0     677    12733    405645   14897    355   103  39 13.3  16.7    5
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   47.8     677    12733    420147   15506    356   103  39 13.3  16.6    5
c -   49.8     677    12733    435435   16149    357   103  38 13.3  16.6    6
c -   51.9     677    12733    451758   16757    357   103  38 13.2  16.5    6
c 
c [simplification-9] limit of 457166 conflicts hit after 457166 conflicts
c [ternres-7] limit 17614838 with penalty 0 = 0 + 0
c [ternres-7] all 677 free variables schedulable
c [ternres-7] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 880741 penalty 2 = 2 + 0
c [gauss-4] extracted 396 xors of average arity 5.6
c [gauss-4] connected 2220 occurrences of 45 variables (average 49.3)
c [gauss-4] limit 880741 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [lift-4] limit 2642225 with penalty 2 = 2 + 0
c [lift-4] using 9 probes 1%
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] 235 variables remain 35% (442 retained)
c [cliff-4] limit of 3522967 steps penalty 2 = 2 + 0
c [cliff-4] failed 0, lifted 0
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2 transitive binary clauses
c [bca-5] limit of 10000000 steps
c [bca-5] 456 out of 1356 literals actually usable 34%
c [bca-5] added 0 blocked clauses in 23431 steps
c [rephase-4] after 457166 conflicts (new increment 160000, next 617166)
c [flushphases] 26 phases reset
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 0 variables 0.0% (677 remain 31%)
c [simplification-9] removed 0 irredundant clauses 0.0% (12733 remain 43%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 240000
c [simplification-9] new conflict interval 480000
c [simplification-9] penalized conflict interval 480000 = 1 * 480000
c [simplification-9] new conflict limit 937166
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   54.2     677    12733    468357   17372    372   120  39 13.2  16.5    6
c -   56.4     677    12733    485938   17993    372   120  38 13.3  16.6    6
c -   58.9     677    12733    503947   18659    373   120  40 13.3  16.6    6
c -   61.4     677    12733    522607   19296    374   120  41 13.3  16.5    5
c -   64.2     677    12733    542161   20001    374   120  39 13.3  16.5    7
c -   67.1     677    12733    562187   20700    376   120  39 13.2  16.5    7
c -   70.1     677    12733    583251   21365    376   120  39 13.2  16.4    7
c /   73.2     677    12733    604297   22053    377   120  38 13.2  16.4    7
c /   73.2     677    12733    604299    8546    377   120  38 13.2  16.4    5
c /   73.4     677    12733    606772    8569    377   120  38 13.2  16.4    5
c -   73.6     677    12733    609425    8598    377   120  38 13.2  16.4    5
c -   74.0     677    12733    613419    9137    377   120  39 13.2  16.4    5
c -   74.5     677    12733    618325    9671    377   120  38 13.2  16.4    5
c /   74.9     677    12733    623489   10232    377   120  39 13.2  16.4    5
c /   75.0     677    12733    624076    8738    377   120  40 13.2  16.4    5
c /   75.2     677    12733    626646    8762    377   120  38 13.2  16.4    5
c -   75.4     677    12733    629163    8776    377   120  38 13.2  16.4    5
c -   75.8     677    12733    633003    9324    377   120  39 13.1  16.4    2
c -   76.2     677    12733    637711    9849    377   120  39 13.1  16.3    3
c /   76.7     677    12733    643095   10399    377   120  39 13.1  16.3    3
c -   76.8     677    12733    643716    8905    378   120  39 13.1  16.3    3
c -   77.2     677    12733    647551    9436    378   120  41 13.1  16.3    3
c -   77.6     677    12733    652051    9968    378   120  39 13.1  16.3    2
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   78.1     677    12733    657266   10510    378   120  39 13.1  16.3    2
c -   78.7     677    12733    663267   11048    378   120  39 13.1  16.3    4
c -   79.3     677    12733    669913   11591    378   120  39 13.1  16.3    4
c -   80.1     677    12733    677370   12145    378   120  39 13.1  16.3    4
c -   81.1     677    12733    685495   12710    378   120  40 13.1  16.2    3
c -   81.9     677    12733    693504   13257    378   120  40 13.1  16.2    3
c -   83.0     677    12733    702960   13828    382   120  39 13.1  16.2    4
c -   84.3     677    12733    713435   14376    382   120  40 13.0  16.2    4
c /   85.5     677    12733    724445   14939    382   120  39 13.0  16.1    4
c /   85.5     677    12733    724445    9439    382   120  39 13.0  16.1    4
c /   85.8     677    12733    727075    9465    382   120  39 13.0  16.1    4
c -   86.0     677    12733    729737    9487    382   120  40 13.0  16.1    4
c -   86.4     677    12733    733701   10014    382   120  39 13.0  16.1    4
c -   86.8     677    12733    738202   10544    382   120  39 13.0  16.1    4
c /   87.3     677    12733    743584   11101    382   120  39 13.0  16.1    4
c /   87.4     677    12733    744234    9603    382   120  40 13.0  16.1    4
c /   87.6     677    12733    746924    9621    382   120  39 13.0  16.1    4
c -   87.9     677    12733    749600    9650    383   120  39 13.0  16.1    4
c -   88.3     677    12733    753758   10181    383   120  38 13.0  16.1    4
c -   88.7     677    12733    758375   10734    383   120  38 13.0  16.1    4
c /   89.3     677    12733    763756   11273    383   120  38 13.0  16.1    4
c -   89.3     677    12733    764436    9776    383   120  38 13.0  16.1    4
c -   89.7     677    12733    768371   10341    384   120  39 13.0  16.1    4
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   90.2     677    12733    772998   10904    384   120  39 13.0  16.0    4
c -   90.7     677    12733    778332   11441    384   120  39 12.9  16.0    4
c -   91.3     677    12733    784560   11986    385   120  40 12.9  16.0    4
c -   92.0     677    12733    791301   12526    385   120  39 12.9  16.0    4
c -   92.8     677    12733    798766   13074    385   120  38 12.9  16.0    4
c -   93.7     677    12733    806753   13650    385   120  39 12.9  16.0    4
c -   94.7     677    12733    815702   14201    385   120  38 12.9  16.0    3
c -   95.9     677    12733    825248   14780    385   120  39 12.9  16.0    4
c -   97.1     677    12733    835512   15395    385   120  39 12.9  15.9    4
c /   98.5     677    12733    846685   15982    386   120  39 12.9  15.9    5
c -   98.5     677    12733    846687   10470    386   120  39 12.9  15.9    4
c -   98.9     677    12733    850686   11012    386   120  39 12.9  15.9    2
c -   99.4     677    12733    855317   11565    386   120  39 12.9  15.9    3
c -   99.9     677    12733    860374   12101    386   120  40 12.9  15.9    4
c -  100.5     677    12733    866180   12653    387   120  40 12.9  15.9    4
c -  101.2     677    12733    872825   13222    387   120  39 12.8  15.9    3
c -  102.0     677    12733    880210   13760    388   120  39 12.8  15.9    3
c -  102.9     677    12733    888233   14305    388   120  40 12.8  15.9    4
c -  103.8     677    12733    897103   14851    388   120  40 12.8  15.9    4
c -  104.9     677    12733    906362   15410    389   120  39 12.8  15.8    3
c -  106.1     677    12733    916567   16014    391   120  39 12.8  15.8    5
c -  107.4     677    12733    927327   16575    391   120  40 12.8  15.8    5
c 
c [simplification-10] limit of 937166 conflicts hit after 937169 conflicts
c [ternres-8] limit 40644273 with penalty 0 = 0 + 0
c [ternres-8] all 677 free variables schedulable
c [ternres-8] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2540267 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2540267 for elimination
c [card-4] 1 out of 1 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-3] limit 508053 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1353 literals 100%
c [treelook-3] scheduling used 116521 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 508053 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 509239 steps
c [treelook-3] 930 literals remain 69%
c [treelook-3] 543 variables remain to probed next time 80%
c [treelook-3] removed 0 variables, found 21 hbrs
c [unhide-4] limit 1016106 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 3 tauts, 0 hbrs, 3846 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [cce-7] limit of 40644273 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 700 (0%) of length 5
c [cce-7-1] eliminated 9 clauses out of 1962 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 11 large clauses in 30716920 steps
c [cce-7-1] allowing another 15358460 steps for small clauses
c [cce-7] scheduling 773 clauses = 436 binary + 337 ternary
c [cce-7] tried to eliminate 773 small clauses 100%
c [cce-7] eliminated 26 small clauses 3%
c [cce-7] eliminated 26 binary clauses 6%
c [cce-7-1] eliminated 26 small clauses in 16338176 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 37 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 747 clauses = 410 binary + 337 ternary
c [cce-7] tried to eliminate 747 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 37 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 677 variables 100%
c [elim-8] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-8-1] eliminated 125 variables 18% in round 1 in 138216319 steps
c [elim-8-1] backward subsumption/strengthening limit 261783681
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 5900642 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 125 = 18% variables out of 677
c [rephase-5] after 937169 conflicts (new increment 320000, next 1257169)
c [flushphases] 18 phases reset
c [phase-11] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-10] removed 125 variables 18.5% (552 remain 25%)
c [simplification-10] removed 365 irredundant clauses 2.9% (12368 remain 42%)
c [simplification-10] maximum reduction of 18% = max (18%, 3%)
c [simplification-10] large reduction 18% >= 5% limit
c [simplification-10] new conflict interval 9371 = min (937169/100, 480000)
c [simplification-10] penalized conflict interval 9371 = 1 * 9371
c [simplification-10] new conflict limit 946540
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  111.7     552    12368    943653   16122    342    22  40 12.8  15.8    5
c 
c [simplification-11] limit of 946540 conflicts hit after 946541 conflicts
c [ternres-9] limit 41096862 with penalty 0 = 0 + 0
c [ternres-9] all 552 free variables schedulable
c [ternres-9] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 0 transitive binary clauses
c [cce-8] limit of 82193725 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 7 clauses out of 652 (1%) of length 5
c [cce-8-1] eliminated 5 clauses out of 2028 (0%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 12 large clauses in 30473906 steps
c [cce-8-1] allowing another 15236953 steps for small clauses
c [cce-8] scheduling 510 clauses = 152 binary + 358 ternary
c [cce-8] tried to eliminate 510 small clauses 100%
c [cce-8] eliminated 3 small clauses 1%
c [cce-8] eliminated 3 ternary clauses 1%
c [cce-8-1] eliminated 3 small clauses in 15847856 steps
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 15 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 507 clauses = 152 binary + 355 ternary
c [cce-8] tried to eliminate 507 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 15 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 552 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9-1] no variable eliminated in round 1 in 43074849 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 0 = 0% variables out of 552
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-11] removed 0 variables 0.0% (552 remain 25%)
c [simplification-11] removed 15 irredundant clauses 0.1% (12353 remain 42%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 480000
c [simplification-11] new conflict interval 960000
c [simplification-11] penalized conflict interval 960000 = 1 * 960000
c [simplification-11] new conflict limit 1906541
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  114.1     552    12353    955188   16743    364    22  41 12.8  15.8    5
c -  115.5     552    12353    967527   17350    364    22  40 12.8  15.8    5
c -  117.2     552    12353    981979   17919    365    22  41 12.8  15.8    5
c -  119.0     552    12353    996641   18545    365    22  42 12.8  15.8    4
c -  120.8     552    12353   1011518   19228    365    22  41 12.8  15.8    6
c -  122.7     552    12353   1026672   19896    366    22  42 12.8  15.7    6
c -  124.9     552    12353   1042750   20547    366    22  40 12.8  15.7    6
c -  127.3     552    12353   1060367   21196    367    22  40 12.7  15.7    6
c -  129.8     552    12353   1078477   21832    367    22  41 12.7  15.7    6
c -  132.3     552    12353   1096928   22513    368    22  41 12.7  15.6    6
c -  134.9     552    12353   1115991   23220    369    22  40 12.7  15.6    5
c -  138.1     552    12353   1136104   23958    371    22  41 12.6  15.6    7
c -  141.3     552    12353   1157000   24672    371    22  41 12.6  15.5    7
c -  144.5     552    12353   1178108   25329    371    22  41 12.6  15.5    7
c /  147.8     552    12353   1200028   26028    371    22  41 12.6  15.4    7
c -  147.8     552    12353   1200028   12522    371    22  41 12.6  15.4    5
c -  148.2     552    12353   1204106   13061    372    22  41 12.5  15.4    5
c -  148.7     552    12353   1208817   13609    373    22  42 12.5  15.4    5
c -  149.2     552    12353   1214267   14187    374    22  42 12.5  15.4    5
c -  150.0     552    12353   1220460   14754    374    22  42 12.5  15.4    5
c -  150.8     552    12353   1227552   15302    374    22  41 12.5  15.4    5
c -  151.6     552    12353   1235198   15860    374    22  42 12.5  15.4    5
c -  152.6     552    12353   1243543   16426    374    22  42 12.5  15.4    3
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  153.8     552    12353   1252930   16995    374    22  43 12.5  15.3    3
c -  155.0     552    12353   1262789   17542    374    22  41 12.5  15.3    5
c -  156.3     552    12353   1273036   18132    375    22  41 12.5  15.3    5
c -  157.7     552    12353   1284221   18717    375    22  42 12.5  15.3    3
c -  159.3     552    12353   1296409   19308    375    22  41 12.4  15.3    5
c -  160.9     552    12353   1308986   19877    375    22  40 12.4  15.3    5
c -  162.8     552    12353   1323124   20493    375    22  41 12.4  15.2    5
c -  164.6     552    12353   1336855   21103    375    22  41 12.4  15.2    4
c -  166.6     552    12353   1351556   21706    375    22  42 12.4  15.2    6
c -  168.8     552    12353   1367059   22369    376    22  40 12.3  15.1    6
c -  171.1     552    12353   1383335   23044    376    22  41 12.3  15.1    6
c -  173.4     552    12353   1399574   23722    376    22  42 12.3  15.1    6
c -  176.0     552    12353   1417082   24347    378    22  42 12.3  15.1    7
c -  178.7     552    12353   1435206   25009    379    22  42 12.3  15.1    6
c -  181.7     552    12353   1454244   25669    380    22  40 12.3  15.1    7
c -  184.9     552    12353   1473521   26358    380    22  41 12.3  15.0    7
c -  188.1     552    12353   1493799   27059    381    22  40 12.2  15.0    7
c -  191.6     552    12353   1515017   27743    381    22  41 12.2  15.0    5
c -  195.4     552    12353   1536913   28469    381    22  42 12.2  14.9    8
c -  199.2     552    12353   1559789   29183    381    22  41 12.2  14.9    8
c -  203.0     552    12353   1582668   29848    381    22  42 12.2  14.9    8
c -  207.1     552    12353   1606830   30498    382    22  42 12.1  14.8    8
c -  211.1     552    12353   1631179   31168    384    22  42 12.1  14.8    7
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  215.7     552    12353   1656677   31853    384    22  40 12.1  14.8    8
c -  220.5     552    12353   1682494   32609    385    22  41 12.1  14.7    8
c -  224.9     552    12353   1708390   33364    385    22  41 12.0  14.7    8
c -  230.1     552    12353   1735350   34141    385    22  41 12.0  14.7    9
c -  235.7     552    12353   1764260   34861    385    22  42 12.0  14.6    7
c -  241.2     552    12353   1792964   35515    386    22  41 12.0  14.6   10
c -  247.0     552    12353   1822426   36249    387    23  42 11.9  14.5   10
c -  252.8     552    12353   1853180   37111    389    23  41 11.9  14.5    7
c -  258.4     552    12353   1882195   37813    391    23  41 11.9  14.5   11
c 
c [simplification-12] limit of 1906541 conflicts hit after 1906542 conflicts
c [ternres-10] limit 107435579 with penalty 0 = 0 + 0
c [ternres-10] all 552 free variables schedulable
c [ternres-10] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-10] fully completed ternary resolution
c [basicprobe-3] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 117 sched 21%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 118 sched 21%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 552 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [block-5] scheduling all variables this time
c [block-5] scheduled 552 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-9] limit of 214871159 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 640 (0%) of length 5
c [cce-9-1] eliminated 3 clauses out of 2026 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 5 large clauses in 29943453 steps
c [cce-9-1] allowing another 14971726 steps for small clauses
c [cce-9] scheduling 418 clauses = 152 binary + 266 ternary
c [cce-9] tried to eliminate 418 small clauses 100%
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 5 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 418 clauses = 152 binary + 266 ternary
c [cce-9] tried to eliminate 418 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 5 covered clauses in TOTAL during 2 rounds
c [cce-9] 5 < 1/1000 * 12353 = 12 considered unsuccessful
c [rephase-6] after 1906542 conflicts (new increment 640000, next 2546542)
c [flushphases] 13 phases reset
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-12] removed 0 variables 0.0% (552 remain 25%)
c [simplification-12] removed 5 irredundant clauses 0.0% (12348 remain 42%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 960000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 2906542
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  264.7     552    12348   1911926   38561    397    24  40 11.9  14.5   11
c -  270.8     552    12348   1943141   39353    400    24  41 11.9  14.5   11
c -  276.9     552    12348   1975363   40139    402    24  41 11.9  14.5   11
c -  283.5     552    12348   2008101   40994    402    24  41 11.9  14.5   11
c -  290.1     552    12348   2041014   41807    402    24  40 11.9  14.6   11
c -  297.2     552    12348   2075728   42541    403    24  41 11.9  14.6    8
c -  303.9     552    12348   2109971   43286    403    24  41 12.0  14.6   12
c -  311.3     552    12348   2146301   44014    404    24  42 11.9  14.6   12
c -  318.8     552    12348   2182387   44706    405    24  41 12.0  14.6    9
c -  326.4     552    12348   2218706   45409    405    24  42 12.0  14.6   13
c -  334.7     552    12348   2256323   46129    405    24  41 12.0  14.6    9
c -  342.9     552    12348   2294998   46845    406    24  41 12.0  14.6   13
c -  352.0     552    12348   2334876   47556    406    24  41 12.0  14.6   13
c -  361.2     552    12348   2375155   48317    406    24  41 12.0  14.5   13
c -  370.7     552    12348   2416742   49098    407    24  41 11.9  14.5   12
c -  380.0     552    12348   2458760   49892    407    24  41 11.9  14.5   13
c -  389.3     552    12348   2501664   50610    407    24  40 11.9  14.5   13
c -  398.9     552    12348   2545037   51362    408    24  41 11.9  14.5   13
c -  408.7     552    12348   2589645   52218    410    24  40 11.9  14.5   13
c /  420.1     552    12348   2633700   53189    411    24  41 11.9  14.5   14
c /  420.2     552    12348   2633700   23678    411    24  41 11.9  14.5   10
c /  420.5     552    12348   2636294   23738    411    24  41 11.9  14.5   10
c -  420.8     552    12348   2638982   23781    411    24  41 11.9  14.5   10
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  421.4     552    12348   2642934   24303    411    24  41 11.9  14.5   11
c -  422.0     552    12348   2647692   24847    411    24  41 11.9  14.5   11
c /  422.8     552    12348   2653110   25402    411    24  41 11.9  14.5   11
c /  422.9     552    12348   2653804   23908    411    24  40 11.9  14.5   10
c /  423.2     552    12348   2656461   23945    411    24  40 11.9  14.5   10
c -  423.6     552    12348   2659124   23979    411    24  41 11.9  14.5   10
c -  424.1     552    12348   2663134   24528    411    24  40 11.9  14.5   10
c -  424.7     552    12348   2667854   25085    411    24  40 11.9  14.5   11
c /  425.5     552    12348   2673338   25632    411    24  41 11.9  14.4   11
c -  425.6     552    12348   2674008   24138    411    24  41 11.9  14.4   10
c -  426.1     552    12348   2678083   24677    411    24  41 11.9  14.4   10
c -  426.8     552    12348   2682818   25211    411    24  41 11.9  14.4   10
c -  427.6     552    12348   2688174   25778    411    24  41 11.9  14.4   11
c -  428.4     552    12348   2694088   26364    411    24  41 11.9  14.4   11
c -  429.4     552    12348   2700818   26950    411    24  40 11.9  14.4   11
c -  430.5     552    12348   2708240   27567    411    24  42 11.9  14.4   11
c -  431.8     552    12348   2716781   28190    411    24  41 11.9  14.4   11
c -  433.2     552    12348   2725870   28819    411    24  41 11.9  14.4   11
c -  434.7     552    12348   2735463   29396    411    24  42 11.9  14.4   11
c -  436.4     552    12348   2745547   30001    411    24  41 11.9  14.4   11
c /  438.1     552    12348   2756389   30598    412    24  41 11.9  14.4   11
c /  438.1     552    12348   2756391   25093    412    24  41 11.9  14.4   10
c /  438.5     552    12348   2759096   25110    412    24  41 11.9  14.4   10
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  438.9     552    12348   2761811   25143    412    24  41 11.9  14.4   10
c -  439.6     552    12348   2765892   25678    412    24  41 11.9  14.4   10
c -  440.3     552    12348   2770678   26210    412    24  41 11.9  14.4   10
c /  441.1     552    12348   2776140   26754    412    24  40 11.9  14.4   11
c /  441.2     552    12348   2776855   25265    412    24  41 11.9  14.4   10
c /  441.6     552    12348   2779567   25278    412    24  41 11.9  14.4   10
c -  442.0     552    12348   2782290   25306    412    24  41 11.9  14.4   10
c -  442.6     552    12348   2786408   25831    412    24  41 11.9  14.4   10
c -  443.3     552    12348   2791078   26374    412    24  40 11.9  14.4   11
c /  444.1     552    12348   2796376   26930    412    24  41 11.9  14.4   11
c -  444.2     552    12348   2797062   25436    412    24  40 11.9  14.4   10
c -  444.7     552    12348   2801039   25973    412    24  41 11.9  14.4   10
c -  445.4     552    12348   2805646   26528    412    24  40 11.8  14.4   10
c -  446.2     552    12348   2810995   27059    412    24  43 11.8  14.4   11
c -  447.1     552    12348   2817025   27601    413    24  42 11.9  14.4   11
c -  448.2     552    12348   2823891   28132    413    24  41 11.8  14.4   11
c -  449.4     552    12348   2831446   28670    413    24  41 11.8  14.4   11
c -  450.7     552    12348   2839462   29225    413    24  40 11.8  14.4   11
c -  452.2     552    12348   2848227   29787    413    24  41 11.8  14.4   11
c -  453.8     552    12348   2857496   30374    413    24  41 11.8  14.4   11
c -  455.7     552    12348   2868230   30975    413    24  41 11.8  14.4   11
c /  457.6     552    12348   2879165   31531    413    24  41 11.8  14.4   11
c -  457.6     552    12348   2879167   26030    413    24  41 11.8  14.4   10
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  458.4     552    12348   2884621   27057    413    24  41 11.8  14.4   11
c -  459.2     552    12348   2889827   27604    413    24  41 11.8  14.4   11
c -  460.1     552    12348   2895983   28144    413    24  41 11.8  14.4   11
c -  461.2     552    12348   2902805   28688    413    24  40 11.8  14.4   11
c 
c [simplification-13] limit of 2906542 conflicts hit after 2906543 conflicts
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 552 free variables schedulable
c [ternres-11] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-5] limit 5058250 penalty 3 = 3 + 0
c [gauss-5] extracted 1899 xors of average arity 6.6
c [gauss-5] connected 12533 occurrences of 88 variables (average 142.4)
c [gauss-5] limit 5058250 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [lift-5] limit 2500000 with penalty 3 = 3 + 0
c [lift-5] using 10 probes 2%
c [lift-5-1] found 0 units 0 impls in round 1
c [lift-5-2] found 0 units 0 impls in round 2
c [lift-5-3] found 0 units 0 impls in round 3
c [lift-5-4] found 0 units 0 impls in round 4
c [lift-5-5] found 0 units 0 impls in round 5
c [lift-5] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-5] 170 variables remain 31% (382 retained)
c [cliff-5] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-5] failed 0, lifted 0
c [transred-10] limit 1000000 with penalty 1 = 1 + 0
c [transred-10] removed 1 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 552 variables 100%
c [elim-10] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-10-1] no variable eliminated in round 1 in 46861095 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 0 = 0% variables out of 552
c [bca-6] limit of 10000000 steps
c [bca-6] 272 out of 1106 literals actually usable 25%
c [bca-6] added 0 blocked clauses in 33536 steps
c [rephase-7] after 2906543 conflicts (new increment 1280000, next 4186543)
c [flushphases] 13 phases reset
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-13] removed 0 variables 0.0% (552 remain 25%)
c [simplification-13] removed 1 irredundant clauses 0.0% (12347 remain 42%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] new conflict limit 3906543
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  463.1     552    12347   2909915   29237    417    23  40 11.8  14.4    5
c -  464.2     552    12347   2917481   29827    417    23  40 11.8  14.4    7
c -  465.4     552    12347   2925826   30401    417    23  40 11.8  14.4    7
c -  466.7     552    12347   2934796   30985    417    23  41 11.8  14.4    7
c -  468.1     552    12347   2944317   31559    417    23  40 11.9  14.4    7
c -  469.7     552    12347   2954470   32149    418    23  41 11.9  14.4    7
c -  471.4     552    12347   2965583   32730    418    23  41 11.9  14.4    5
c -  473.2     552    12347   2977273   33301    418    23  42 11.9  14.4    5
c -  475.1     552    12347   2989787   33916    418    23  41 11.9  14.4    8
c -  477.2     552    12347   3002845   34519    418    23  40 11.9  14.4    8
c -  479.4     552    12347   3016816   35096    418    23  39 11.9  14.4    6
c -  481.9     552    12347   3031762   35717    418    23  40 11.9  14.4    9
c -  484.3     552    12347   3046872   36299    419    23  40 11.9  14.5    8
c -  486.8     552    12347   3062685   36877    419    23  41 11.9  14.5    8
c -  489.7     552    12347   3079645   37507    419    23  41 11.9  14.5    6
c -  492.8     552    12347   3097255   38129    419    23  41 11.9  14.5    8
c -  496.0     552    12347   3115635   38730    421    23  41 11.9  14.5    9
c -  499.4     552    12347   3135110   39359    422    23  41 11.9  14.5    9
c -  503.1     552    12347   3154874   40040    422    23  40 11.9  14.5    9
c -  507.0     552    12347   3175808   40644    422    23  40 11.9  14.5    9
c -  510.6     552    12347   3196361   41235    422    23  40 11.9  14.5    9
c /  514.4     552    12347   3217749   41824    422    23  40 11.9  14.5    7
c /  514.4     552    12347   3217749   28323    422    23  40 11.9  14.5    6
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c /  514.7     552    12347   3220355   28342    422    23  41 11.9  14.5    6
c -  515.1     552    12347   3223001   28353    422    23  41 11.9  14.5    6
c -  515.6     552    12347   3226889   28871    422    23  42 11.9  14.5    6
c -  516.3     552    12347   3231404   29393    422    23  40 11.9  14.5    6
c /  517.0     552    12347   3236790   29930    422    23  40 11.9  14.5    6
c /  517.1     552    12347   3237457   28436    422    23  41 11.9  14.5    6
c /  517.5     552    12347   3240020   28462    422    23  40 11.9  14.5    6
c -  517.8     552    12347   3242523   28471    422    23  40 11.9  14.5    6
c -  518.3     552    12347   3246623   28992    422    23  40 11.9  14.5    6
c -  519.0     552    12347   3251069   29536    422    23  40 11.9  14.5    6
c /  519.7     552    12347   3256411   30056    422    23  40 11.9  14.5    6
c -  519.8     552    12347   3257043   28562    422    23  40 11.9  14.5    6
c -  520.4     552    12347   3260953   29096    422    23  41 11.9  14.5    6
c -  521.0     552    12347   3265561   29631    422    23  40 11.9  14.5    6
c -  521.8     552    12347   3270925   30167    422    23  42 11.9  14.5    6
c -  522.7     552    12347   3277006   30711    422    23  41 11.9  14.5    6
c -  523.6     552    12347   3283674   31252    422    23  41 11.9  14.5    6
c -  524.8     552    12347   3291228   31835    423    23  40 11.9  14.5    6
c -  526.1     552    12347   3299522   32415    424    23  40 11.9  14.5    6
c -  527.4     552    12347   3308365   32997    424    23  40 11.9  14.5    9
c -  529.0     552    12347   3317783   33563    424    23  40 11.9  14.5    9
c -  530.6     552    12347   3327799   34116    424    23  41 11.9  14.5    9
c /  532.2     552    12347   3338387   34656    424    23  41 11.9  14.5    9
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c /  532.2     552    12347   3338387   29155    424    23  41 11.9  14.5    9
c /  532.6     552    12347   3341036   29183    424    23  42 11.9  14.5    9
c -  533.0     552    12347   3343653   29185    424    23  42 11.9  14.5    9
c -  533.5     552    12347   3347631   29703    424    23  40 11.9  14.5    9
c -  534.2     552    12347   3352293   30231    425    23  40 11.9  14.5    9
c /  535.0     552    12347   3357692   30756    425    23  41 11.9  14.5    9
c /  535.1     552    12347   3358383   29264    425    23  41 11.9  14.5    9
c /  535.5     552    12347   3360968   29284    425    23  41 11.9  14.5    9
c -  535.9     552    12347   3363628   29297    425    23  41 11.9  14.5    9
c -  536.5     552    12347   3367686   29832    425    23  40 11.9  14.5    9
c -  537.2     552    12347   3372462   30347    425    23  40 11.9  14.5    9
c /  538.0     552    12347   3377949   30886    425    23  39 11.9  14.5    9
c -  538.1     552    12347   3378673   29395    425    23  40 11.9  14.5    9
c -  538.7     552    12347   3382787   29904    425    23  40 11.9  14.5    9
c -  539.4     552    12347   3387562   30425    425    23  41 11.9  14.4    9
c -  540.2     552    12347   3393011   30965    425    23  41 11.9  14.4    9
c -  541.1     552    12347   3399216   31483    425    23  41 11.9  14.4    9
c -  542.2     552    12347   3406016   32037    425    23  41 11.9  14.4    9
c -  543.3     552    12347   3413489   32591    425    23  41 11.9  14.4    9
c -  544.6     552    12347   3421572   33187    426    23  41 11.9  14.4    9
c -  545.9     552    12347   3429987   33723    426    23  41 11.9  14.4    9
c -  547.3     552    12347   3438663   34256    426    23  40 11.9  14.4    9
c -  548.8     552    12347   3448191   34809    427    23  41 11.9  14.4    9
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c /  550.5     552    12347   3458619   35340    427    23  42 11.9  14.4    9
c -  550.5     552    12347   3458619   29841    427    23  42 11.9  14.4    9
c -  551.1     552    12347   3462372   30362    427    23  42 11.9  14.4    9
c -  551.7     552    12347   3466816   30881    427    23  41 11.9  14.4    9
c -  552.5     552    12347   3471978   31419    427    23  41 11.9  14.4    9
c -  553.3     552    12347   3477919   31933    427    23  40 11.9  14.4    9
c -  554.3     552    12347   3484512   32464    427    23  40 11.9  14.4    9
c -  555.5     552    12347   3491937   33002    428    23  40 11.9  14.4    9
c -  556.6     552    12347   3499887   33529    428    23  41 11.9  14.5    9
c -  557.9     552    12347   3508505   34048    428    23  42 11.9  14.5    9
c -  559.4     552    12347   3517984   34570    428    23  41 11.9  14.5    9
c -  561.0     552    12347   3528182   35107    428    23  40 11.9  14.5    9
c -  562.8     552    12347   3539154   35680    428    23  41 11.9  14.5    9
c -  564.8     552    12347   3550811   36227    428    23  41 11.9  14.5    9
c -  566.9     552    12347   3563005   36799    428    23  41 11.9  14.4    6
c -  569.3     552    12347   3576274   37431    428    23  40 11.9  14.4    8
c -  571.6     552    12347   3589969   37977    428    23  42 11.9  14.4    8
c -  574.1     552    12347   3604119   38552    428    23  40 11.9  14.4    6
c -  576.7     552    12347   3619137   39127    428    23  42 11.9  14.4    6
c -  579.4     552    12347   3634472   39678    428    23  41 11.9  14.4    9
c -  582.4     552    12347   3650830   40276    428    23  41 11.9  14.4    9
c -  585.4     552    12347   3667990   40835    428    23  41 11.9  14.4    9
c -  588.6     552    12347   3685926   41424    428    23  40 11.9  14.4    9
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  591.8     552    12347   3703649   42020    428    23  42 11.9  14.4    7
c -  595.4     552    12347   3723123   42614    429    23  42 11.9  14.4   10
c -  599.2     552    12347   3743138   43247    429    23  40 11.9  14.4   10
c -  603.0     552    12347   3763367   43832    429    23  41 11.9  14.4   10
c -  606.9     552    12347   3783799   44412    429    23  41 11.9  14.4   10
c /  611.0     552    12347   3804978   45053    429    23  41 11.9  14.4   10
c -  611.0     552    12347   3804978   31556    429    23  41 11.9  14.4    9
c -  611.6     552    12347   3808854   32081    429    23  40 11.9  14.4    9
c -  612.2     552    12347   3813476   32601    429    23  42 11.9  14.4    9
c -  613.0     552    12347   3818706   33130    429    23  41 11.9  14.4    9
c -  614.0     552    12347   3824733   33661    429    23  42 11.8  14.4    9
c -  615.0     552    12347   3831456   34191    429    23  41 11.8  14.4    9
c -  616.2     552    12347   3838730   34720    429    23  41 11.8  14.4    9
c -  617.4     552    12347   3846344   35277    429    23  42 11.8  14.4    9
c -  618.9     552    12347   3855287   35821    429    23  41 11.8  14.4    9
c -  620.4     552    12347   3864814   36396    429    23  41 11.8  14.4    9
c -  622.1     552    12347   3874806   36951    429    23  41 11.8  14.4    9
c -  623.9     552    12347   3885722   37521    430    23  41 11.8  14.4    9
c -  625.8     552    12347   3897039   38089    430    23  40 11.8  14.4    9
c 
c [simplification-14] limit of 3906543 conflicts hit after 3906543 conflicts
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 552 free variables schedulable
c [ternres-12] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-4] all 552 free variables schedulable
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 3 hbrs, 0 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 3 transitive binary clauses
c [cce-10] limit of 277833150 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 2 clauses out of 626 (0%) of length 5
c [cce-10-1] eliminated 2 clauses out of 2033 (0%) of length 4
c [cce-10-1] completed large round (ACCE)
c [cce-10-1] eliminated 4 large clauses in 30445807 steps
c [cce-10-1] allowing another 15222903 steps for small clauses
c [cce-10] scheduling 419 clauses = 152 binary + 267 ternary
c [cce-10] tried to eliminate 419 small clauses 100%
c [cce-10-1] completed small round (ACCE)
c [cce-10-1] eliminated 4 covered clauses in round 1
c [cce-10-2] completed large round (ACCE)
c [cce-10-2] allowing another 0 steps for small clauses
c [cce-10] scheduling 419 clauses = 152 binary + 267 ternary
c [cce-10] tried to eliminate 419 small clauses 100%
c [cce-10-2] completed small round (ACCE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 4 covered clauses in TOTAL during 2 rounds
c [cce-10] 4 < 1/1000 * 12347 = 12 considered unsuccessful
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-14] removed 0 variables 0.0% (552 remain 25%)
c [simplification-14] removed 4 irredundant clauses 0.0% (12343 remain 42%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 1000000
c [simplification-14] conflict interval soft limit 1000000 reached
c [simplification-14] new conflict interval 1000000
c [simplification-14] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-14] new conflict limit 4906543
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  628.5     552    12343   3908901   38662    432    23  41 11.8  14.4    6
c -  630.7     552    12343   3921269   39266    432    23  41 11.8  14.4    9
c -  633.1     552    12343   3934264   39872    432    23  41 11.8  14.4    9
c -  635.8     552    12343   3948319   40463    432    23  42 11.8  14.4    9
c -  638.7     552    12343   3963048   41109    433    23  41 11.8  14.4    7
c -  641.6     552    12343   3978496   41724    433    23  42 11.8  14.4    9
c -  644.7     552    12343   3994610   42338    433    23  41 11.8  14.4    9
c -  648.0     552    12343   4011600   42923    433    23  42 11.8  14.4    7
c -  651.6     552    12343   4029371   43602    433    23  41 11.8  14.4   10
c -  655.3     552    12343   4047896   44244    433    23  42 11.8  14.4   10
c -  658.9     552    12343   4066489   44857    433    23  42 11.8  14.4    7
c -  662.9     552    12343   4086010   45470    433    23  41 11.8  14.4   10
c -  667.1     552    12343   4106784   46116    433    23  40 11.8  14.4   10
c -  671.3     552    12343   4127826   46726    433    23  40 11.8  14.4   10
c -  675.9     552    12343   4149244   47362    433    23  41 11.8  14.4   10
c -  680.6     552    12343   4171556   47993    433    23  41 11.8  14.4   10
c -  685.3     552    12343   4194216   48621    433    23  41 11.8  14.4   10
c -  690.4     552    12343   4217989   49251    433    23  41 11.8  14.4    8
c -  696.0     552    12343   4242568   49920    434    23  41 11.8  14.4   12
c -  701.3     552    12343   4267538   50608    434    23  41 11.8  14.4   12
c -  706.6     552    12343   4293226   51244    434    23  41 11.8  14.4   12
c -  712.4     552    12343   4319821   51867    434    23  41 11.8  14.4   12
c -  718.7     552    12343   4347327   52509    434    23  41 11.8  14.4   12
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  725.3     552    12343   4375935   53148    434    23  43 11.8  14.4   12
c -  732.1     552    12343   4405367   53802    435    23  42 11.8  14.4    8
c -  738.8     552    12343   4435075   54474    435    23  40 11.8  14.4   12
c -  745.3     552    12343   4465472   55125    435    23  41 11.8  14.4    9
c -  752.6     552    12343   4497119   55783    435    23  41 11.8  14.4   13
c -  759.9     552    12343   4529324   56464    436    23  41 11.8  14.3   12
c -  767.3     552    12343   4561459   57134    436    23  40 11.8  14.3   12
c -  774.9     552    12343   4594647   57810    436    23  42 11.8  14.3   12
c -  782.6     552    12343   4628578   58538    436    23  41 11.8  14.3   13
c -  791.7     552    12343   4663437   59398    436    23  40 11.8  14.3   13
c -  801.3     552    12343   4699798   60193    436    23  41 11.8  14.3   13
c -  810.4     552    12343   4735072   61052    436    23  40 11.8  14.3   13
c -  820.0     552    12343   4771548   61851    437    23  41 11.8  14.3   14
c -  830.2     552    12343   4809129   62677    437    23  41 11.8  14.3   14
c -  840.6     552    12343   4847089   63509    437    23  41 11.7  14.2   14
c -  851.3     552    12343   4887003   64274    437    23  41 11.7  14.2   14
c 
c [simplification-15] limit of 4906543 conflicts hit after 4906544 conflicts
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 552 free variables schedulable
c [ternres-13] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 12055796 penalty 4 = 4 + 0
c [card-5] no at-most-one constraint found
c [card-5] found 1 at-most-two constraints of average size 4.0
c [card-5] using previous limit 12055796 for elimination
c [card-5] 1 out of 1 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [unhide-5] limit 1250000 with penalty 4 = 4 + 0
c [unhide-5-8] 0 units, 0 failed, 2 tauts, 0 hbrs, 7498 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1 transitive binary clauses
c [rephase-8] after 4906544 conflicts (new increment 2560000, next 7466544)
c [flushphases] 9 phases reset
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-15] removed 0 variables 0.0% (552 remain 25%)
c [simplification-15] removed 0 irredundant clauses 0.0% (12343 remain 42%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 1000000
c [simplification-15] new conflict interval 2000000
c [simplification-15] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-15] new conflict limit 6906544
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  862.5     552    12343   4925947   65053    452    23  41 11.7  14.2   14
c -  873.7     552    12343   4965541   65828    452    23  41 11.7  14.2   14
c -  884.4     552    12343   5006304   66540    452    23  42 11.7  14.2   11
c -  895.7     552    12343   5048245   67291    452    23  42 11.7  14.2   16
c -  908.1     552    12343   5091064   68051    452    23  40 11.7  14.2   16
c -  920.7     552    12343   5134589   68806    452    23  41 11.7  14.2   16
c -  932.3     552    12343   5177307   69500    453    23  40 11.7  14.2   11
c /  944.4     552    12343   5220516   70289    453    23  41 11.7  14.2   16
c -  944.5     552    12343   5220516   40790    453    23  41 11.7  14.2   14
c -  945.1     552    12343   5224525   41311    453    23  41 11.7  14.2   14
c -  945.9     552    12343   5229222   41858    453    23  41 11.7  14.2   14
c -  946.8     552    12343   5234409   42392    453    23  40 11.7  14.2   14
c -  947.9     552    12343   5240337   42926    453    23  41 11.7  14.2   14
c -  949.1     552    12343   5246998   43461    453    23  41 11.7  14.2   14
c -  950.4     552    12343   5254482   43985    453    23  41 11.7  14.2   14
c -  952.1     552    12343   5262832   44555    453    23  41 11.7  14.2   14
c -  953.6     552    12343   5270928   45099    453    23  41 11.7  14.2   14
c -  955.3     552    12343   5280245   45682    453    23  41 11.7  14.2   14
c -  957.2     552    12343   5290567   46232    453    23  41 11.7  14.2   14
c -  959.3     552    12343   5301968   46770    454    23  41 11.7  14.2   14
c -  961.6     552    12343   5313847   47324    454    23  40 11.7  14.2   14
c -  964.0     552    12343   5326373   47888    454    23  42 11.7  14.2   14
c -  966.5     552    12343   5339556   48456    454    23  41 11.7  14.2   14
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  969.3     552    12343   5352958   49026    454    23  40 11.7  14.2   14
c -  972.3     552    12343   5367430   49623    454    23  41 11.7  14.2   14
c -  975.3     552    12343   5382547   50202    454    23  40 11.7  14.2   14
c -  978.6     552    12343   5398514   50815    454    23  41 11.7  14.2   14
c -  982.2     552    12343   5415189   51448    454    23  41 11.7  14.2   14
c -  985.9     552    12343   5432464   52044    455    23  41 11.7  14.2   14
c -  989.9     552    12343   5450705   52653    455    23  42 11.7  14.2   15
c -  993.8     552    12343   5468702   53382    455    23  41 11.7  14.2   15
c -  998.1     552    12343   5487825   54124    456    23  41 11.7  14.2   15
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: 6 count, 5 added (0 skipped), 91145 steps
c bkwd: tried 41652 clauses, 82157 lits, 1.97 lits/clause
c bkwd: checked 11672807 occs, 280.25 occs/clause, 142.08 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 364 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1127 large (0% self)
c blkd: 5 bces, 755 removed, 1752237 resolutions, 2807988 steps
c blkd: 295 blocking literals 7%, 6 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 0 am1, 20637194 steps
c card: 3 rescheduled, 9 eliminated, 74591 resolved, 2921 subsumed
c card: 4 at-most-one constraints found, average size 3.00
c card: 4 at-most-one constraints used 100%, average size 3.00
c card: 2 at-most-two constraints found, average size 4.00
c card: 2 at-most-two constraints used 100%, average size 4.00
c cces: 10 cces, 4090 eliminated, 3844 ate 94%, 246 abce 6%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 1473135 esteps, 26936 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: 352 extracted (52 ands 15%, 293 xors 83%, 7 ites 2%)
c clff: 5 cliffs, 0 lifted, 6 failed
c clff: 254589 decisions, 15475936 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 204132 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 77 gcs, 0 rescored clauses, 2889 rescored vars
c dcps: 27 decompositions, 157 equivalent 7%
c deco: 10 decision-only clauses 0%, 50% reduction
c decs: 5831075 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 396 flipped 0.007% (in 9 phases)
c elms: 10 elims, 1446 eliminated 64%
c elms: 15 rounds, 1.5 rounds/bve
c elms: 1440 small 100%, 0 large 0%
c elms: 6451 tried small, 1440 succeeded 22%, 5011 failed 78%
c elms: 833 subsumed, 1608 strengthened, 14 blocked
c elms: 919041 copies, 3643839 resolutions, 573064 ipos
c elms: 705557 subchks, 908863 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 4406 extracted, 6.3 size, 7 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 21878390 steps, 10939195 extr 50%, 43714 elim 0%
c glue: 11.7 orig avg, 11.7 real avg, 3.3 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 556 = 237 simple + 262 trn 43% + 57 lrg 47%, 29 sub 10%
c hght: 14 average, 1.21 height/glue
c ints: 131134 luby (40505950 steps), 0 inout (0 steps)
c lift: 5 phases, 7950 probed (2650 level1 33%, 5300 level2 67%)
c lift: 5 units, 0 equivalences, 2 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5493527 clauses, 20.0 length
c lrnd: 633685 uips 12%, 4689122 flips 85%
c mega: 0 count, 0 failed, 0 rounds
c mins: 109801507 learned lits, 38% minimized
c mins: 5477866 mins 100%, 2 bin 0%, 15649 size 0%, 10 deco 0%
c move: moved 5493527, 346 bin 0%, 24 trn 0%, 0 lrg 0%
c otfs: str 14226 dyn (14059 red, 167 irr) 2762 drv 19%, 11464 rst 81%
c otfs: sub 453 dyn (437 red, 16 irr)
c phas: 16 computed, 1715 set, 354 pos (21%), 1361 neg (79%)
c prbs: 3 basic, 10835 probed, 20 failed, 0 lifted
c prbs: 4 simple, 5476 probed, 1 failed, 0 eqs
c prbs: 3 treelook, 670 probed, 0 failed, 0 lifted
c prps: 524695996 props, 90 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 83233133 searches, 8196405 hits, 10% 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: 451 count, 63 reset, 131 acts 29%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 451 arith 100%, 3 double 1%
c rmbd: 27 removed, 27 red 100%
c rphs: 8 recomputed phases
c rsts: 122 restarts 0%, 130949 skipped 100%
c rsts: 14 saturating 0%, 130930 agile 100%, 5 reuse 0%
c rsts: 45660.3 avg interval, 45660.3 scaled, 1.0 factor
c rsts: 40 kept 32.8% average 23.1%
c simp: 15 count (15 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 5493527 count (3239909 tried 0.6), 1416564 sub out of 5493317 (25.8%)
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: 1 count
c tops: 100 fixed 4%, 0 its, 0.00 confs/it
c trvs: 80259373839 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 153.2 search traversals per propagation, 14599.3 per conflict
c trvs: 1.8 search traversals per search visit
c trds: 12 transitive reductions, 41 removed, 0 failed
c trds: 16903 nodes, 7935 edges, 51619 steps
c trim: 4600916 words, 17.6 MB
c trnr: 13 count, 0 bin, 311 trn, 7265229 steps
c unhd: 5 count, 8 rounds, 4314441 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: 4988 tauts, 0 bin 0%, 13 trn 0%, 4964 lrg 100%
c unhd: 4988 tauts, 11 stamp 0%, 24 red 0%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 23365 str, 0 bin 0%, 15 trn 0%, 23350 lrg 100%, 14973 red 64%
c vars: 559 remaining 25% and 1703 removed 75% out of 2262
c vars: 100 fixed 4%, 1446 eliminated 64%, 157 equivalent 7%
c vsts: 45464495900 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 86.8 search visits per propagation, 8268.7 per conflict
c wchs: 21801119471 pushed, 5636719 enlarged, 203 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   5493317 100   4006596 100 163536775 100  58631432 100   2956374 100
c 
c  0      42592   1         0   0 141934318  87< 40201168  69   2219731  75 
c  1      62627   1     61236   2   6355134   4   2487947   4<   156439   5<
c  2     517336   9    490290  12   7379835   5   4486182   8    258318   9 
c  3    2568814  47<  2006931  50<  5215422   3   6674403  11    211536   7 
c  4    2262400  41   1424527  36   2608060   2   4701640   8    107702   4 
c  5      39519   1     23606   1     43969   0     80042   0      2647   0 
c  6         26   0         6   0        33   0        44   0         1   0 
c  7          3   0         0   0         4   0         6   0         0   0 
c  8          0   0         0   0         0   0         0   0         0   0 
c  9          0   0         0   0         0   0         0   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   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             3.3           3.2           0.3           0.9           0.6
c std             0.8           0.7           0.8           1.4           1.1
c 
c   34.962   3% analysis
c    9.261   1% mincls
c    6.576   1% cce
c    6.486   1% bump
c    4.766   0% elim
c    4.409   0% decide
c    2.107   0% reduce
c    0.736   0% backward
c    0.729   0% cliff
c    0.487   0% unhide
c    0.479   0% gc
c    0.378   0% probe
c    0.330   0% decomp
c    0.327   0% defrag
c    0.288   0% card
c    0.176   0% block
c    0.169   0% gauss
c    0.156   0% restart
c    0.121   0% phase
c    0.073   0% lift
c    0.070   0% cgrclsr
c    0.051   0% bca
c    0.036   0% ternres
c    0.008   0% transred
c    0.002   0% tabularasa
c    0.001   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 ----------------------------------
c    0.180   0% probe simple     47%
c    0.129   0% probe basic      34%
c    0.070   0% probe tree-look  19%
c ==================================
c    0.588   0% preprocessing     4%
c   13.650   1% inprocessing     96%
c ==================================
c   14.238   1% simplifying
c  985.765  99% search
c ==================================
c 1000.003 100% all
c 
c 5831075 decisions, 5831.1 decisions/sec
c 5496289 conflicts, 5496.3 conflicts/sec
c 524695996 propagations, 0.5 megaprops/sec
c 1000.0 seconds, 28.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
