c launch: /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c host: atom13
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/atco_enc1_opt2_05_4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c no embedded options
c found 'p cnf 14636 386163' header
c read 14636 variables, 386163 clauses, 1652800 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 14409 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   14409   371044         0       0      0     0   0  0.0   0.0   23
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3123 at-most-one constraints of average size 3.0
c [card-1] found 64 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3187 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1111 variables
c [simpleprobe-1] all 13525 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 259 variables
c [simpleprobe-1] 11182 variables remain 84% (2084 retained)
c [simpleprobe-1] removed 259 variables, found 1956 hbrs, 8 units
c [unhide-1] limit 181231 based on 362463 irredundant clauses
c [unhide-1-1] 58 units, 20 failed, 5673 tauts, 0 hbrs, 62 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13189 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 3581 variables 27% in round 1 in 19328581 steps
c [elim-1-1] backward subsumption/strengthening limit 38657162
c [elim-1-1] subsumed 1393 and strengthened 79 clauses in 38657197 steps
c [elim-1-1] rescheduled 348 variables 3% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 197282 steps
c [elim-1-2] backward subsumption/strengthening limit 394564
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 395520 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 3583 = 27% variables out of 13189
c [phase-1] phase bias: 4703 positive 49%, 4903 negative 51%
c [simplification-1] removed 4558 variables 32.2% (9606 remain 67%)
c [simplification-1] removed 26295 irredundant clauses 7.1% (344749 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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] 191357, max 545453, min4 97022 at 75%, min10 9979 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    2.3    9606   344749         5       5      0   821   1 12.8 377.6   23
c R    2.3    9606   344749        21      17      0   825   3  9.6 328.0   23
c R    2.3    9606   344749        64      51      1   829   4  7.7 294.4   23
c R    2.3    9606   344749       166     137      3   839   5  7.1 239.6   24
c R    2.4    9606   344749       415     325     13   867   6  7.0 177.6   24
c R    2.4    9606   344749       995     815     26   893   7  7.7 137.7   24
c 
c [simplification-2] limit of 1154 conflicts hit after 1154 conflicts
c [decomp-3] removed 13 variables
c [simpleprobe-2] 8136 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 8154 variables remain 85% (1438 retained)
c [simpleprobe-2] removed 1 variables, found 109 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6703 literals 35%
c [treelook-1] scheduling used 302018 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 320857 steps
c [treelook-1] 6683 literals remain 35%
c [treelook-1] 5681 variables remain to probed next time 59%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 70 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1361 probes remain 14% after last round
c [basicprobe-1-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 6 variables, found 1612 hbrs
c [unhide-2] limit 172361 based on 344722 irredundant clauses
c [unhide-2-2] 0 units, 7 failed, 566 tauts, 0 hbrs, 1280 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9579 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 1035 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 298 clauses out of 1032 (29%) of length 12
c [cce-1-1] eliminated 84 clauses out of 130 (65%) of length 11
c [cce-1-1] eliminated 50 clauses out of 446 (11%) of length 10
c [cce-1-1] eliminated 117 clauses out of 1600 (7%) of length 9
c [cce-1-1] eliminated 486 clauses out of 3612 (13%) of length 8
c [cce-1-1] eliminated 10 clauses out of 7477 (0%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1045 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 21290 clauses = 19739 binary + 1551 ternary
c [cce-1] tried to eliminate 9612 small clauses 45%
c [cce-1] eliminated 1016 small clauses 5%
c [cce-1] eliminated 941 binary clauses 5%
c [cce-1] eliminated 75 ternary clauses 5%
c [cce-1-1] eliminated 1016 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2061 covered clauses in round 1
c [cce-1] eliminated 2061 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9579 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 2468 not tried 26% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 164 = 2% variables out of 9579
c [bca-1] limit of 10000000 steps
c [bca-1] 17712 out of 18832 literals actually usable 94%
c [bca-1] added 851 blocked clauses in 43458 steps
c [phase-2] phase bias: 20 positive 28%, 51 negative 72%
c [simplification-2] removed 191 variables 2.0% (9415 remain 65%)
c [simplification-2] removed 4369 irredundant clauses 1.3% (340380 remain 92%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] new conflict limit 7820
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   11.7    9415   340380      2327    1922    971  3491   8  8.6  97.9   23
c -   11.9    9415   340380      4878    2211   1008  3560   9  9.2  72.5   23
c R   11.9    9415   340380      5278    2572   1013  3575   9  9.2  76.6   23
c 
c [simplification-3] limit of 8158 conflicts hit after 8158 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 9415 free variables schedulable
c [ternres-1] 1202 ternary resolvents (1 bin, 1201 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1347 at-most-one constraints of average size 3.1
c [card-2] found 346 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1693 out of 1693 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 154 xors of average arity 2.6
c [gauss-1] connected 407 occurrences of 307 variables (average 1.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 64 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6584 literals 35%
c [treelook-2] scheduling used 302597 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 365230 steps
c [treelook-2] 6541 literals remain 35%
c [treelook-2] 4138 variables remain to probed next time 44%
c [decomp-7] removed 1 variables
c [treelook-2] removed 1 variables, found 140 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 9350 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 8747 probes 94%
c [lift-1] 5 units, 3 impls, 3 eqs in 1 rounds
c [lift-1] 9277 variables remain 99% (65 retained)
c [lift-1] removed 8 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-3] limit 170145 based on 340290 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 519 tauts, 0 hbrs, 3855 literals
c [transred-1] limit 339429 based on 339429 irredundant clauses
c [transred-1] removed 513 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 9339 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 11 blocked clauses
c [block-2] 11 < 1/1000 * 339323 = 339 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 13
c [cce-2-1] eliminated 24 clauses out of 911 (3%) of length 12
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 28 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 20679 clauses = 18037 binary + 2642 ternary
c [cce-2] tried to eliminate 936 small clauses 5%
c [cce-2] eliminated 89 small clauses 0%
c [cce-2] eliminated 71 binary clauses 0%
c [cce-2] eliminated 18 ternary clauses 1%
c [cce-2-1] eliminated 89 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 117 covered clauses in round 1
c [cce-2] eliminated 117 covered clauses in TOTAL during 1 rounds
c [cce-2] 117 < 1/1000 * 339278 = 339 considered unsuccessful
c [elim-3] 2404 variables 26% will be scheduled this time
c [elim-3] scheduled 2404 variables 26%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 1483 not tried 16% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9339
c [bca-2] limit of 10000000 steps
c [bca-2] 16454 out of 18680 literals actually usable 88%
c [bca-2] added 20 blocked clauses in 42927 steps
c [phase-3] phase bias: 12 positive 55%, 10 negative 45%
c [simplification-3] removed 76 variables 0.8% (9339 remain 65%)
c [simplification-3] removed 1500 irredundant clauses 0.4% (338880 remain 91%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] new conflict limit 24824
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.3    9339   338880      8338    2882   2226  3821   7  9.4  62.2   23
c R   15.6    9339   338880     11818    5880   2241  3842   8 11.6  58.8   24
c -   15.7    9339   338880     12502    3509   2244  3847   7 11.4  57.1   23
c -   16.1    9339   338880     16976    4137   2262  3898   7 11.0  52.9   24
c -   16.5    9339   338880     22097    4827   2280  3929   8 10.6  48.7   24
c 
c [simplification-4] limit of 25062 conflicts hit after 25065 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 9339 free variables schedulable
c [ternres-2] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-2] 6053 variables remain 65% (3286 retained)
c [decomp-8] removed 22 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 1009 probes remain 11% after last round
c [basicprobe-2-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1 variables, found 1121 hbrs
c [bate-1] eliminated 14 asymmetric tautologies during probing
c [lift-2] limit 566086 with penalty 0 = 0 + 0
c [lift-2] using 8652 probes 93%
c [lift-2] 5 units, 4 impls, 3 eqs in 1 rounds
c [lift-2] 9197 variables remain 99% (107 retained)
c [lift-2] removed 12 variables
c [unhide-4] limit 188695 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 957 tauts, 0 hbrs, 15943 literals
c [transred-2] limit 943476 with penalty 0 = 0 + 0
c [transred-2] removed 629 transitive binary clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 16362 out of 18610 literals actually usable 88%
c [bca-3] added 84 blocked clauses in 45572 steps
c [rephase-1] after 25065 conflicts (new increment 20000, next 45065)
c [flushphases] 970 phases reset
c [phase-4] phase bias: 2 positive 25%, 6 negative 75%
c [simplification-4] removed 35 variables 0.4% (9304 remain 65%)
c [simplification-4] removed 328 irredundant clauses 0.1% (338552 remain 91%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 36666
c [simplification-4] penalized conflict interval 36666 = 1 * 36666
c [simplification-4] new conflict limit 61731
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   17.7    9304   338552     26201    8632   2281  3879   8 10.8  50.7   24
c -   17.9    9304   338552     27707    5532   2287  3892   7 10.7  49.4   24
c -   18.5    9304   338552     33902    6241   2309  3926   7 10.5  46.7   24
c -   19.2    9304   338552     40522    6901   2331  3954   7 10.5  46.9   24
c -   20.0    9304   338552     47710    7612   2356  3979   7 10.4  45.6   24
c -   20.8    9304   338552     55520    8301   2396  4025   7 10.5  50.5   24
c R   21.0    9304   338552     57630   10247   2406  4030   8 10.5  52.0   24
c 
c [simplification-5] limit of 62067 conflicts hit after 62068 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 6033 schedulable variables 65%
c [ternres-3] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-3] 3385 variables remain 36% (5919 retained)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 95 xors of average arity 2.6
c [gauss-2] connected 250 occurrences of 219 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 81 variables
c [simpleprobe-3] 7849 schedulable variables 85%
c [simpleprobe-3] limit 10424584 penalty 0 = 0 + 0
c [decomp-10] removed 7 variables
c [simpleprobe-3] 7873 variables remain 85% (1343 retained)
c [simpleprobe-3] removed 7 variables, found 769 hbrs, 0 units
c [cgrclsr-2] limit 169232 based on 338464 irredundant clauses
c [cgrclsr-2] all 9216 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 1563687 with penalty 0 = 0 + 0
c [lift-3] using 8511 probes 92%
c [lift-3] 8 units, 6 impls, 1 eqs in 1 rounds
c [lift-3] 8947 variables remain 97% (257 retained)
c [lift-3] removed 12 variables
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 954 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 9204 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 6 blocked clauses
c [block-3] 6 < 1/1000 * 338255 = 338 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 22648 clauses = 17979 binary + 4669 ternary
c [cce-3] tried to eliminate 419 small clauses 2%
c [cce-3] eliminated 77 small clauses 0%
c [cce-3] eliminated 39 binary clauses 0%
c [cce-3] eliminated 38 ternary clauses 1%
c [cce-3-1] eliminated 77 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 77 covered clauses in round 1
c [cce-3] eliminated 77 covered clauses in TOTAL during 1 rounds
c [cce-3] 77 < 1/1000 * 338249 = 338 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9204 variables 100%
c [elim-4] limit of 26061460 steps penalty 1 = 1 + 0
c [elim-4] incomplete 1900 not tried 21% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 67 = 1% variables out of 9204
c [bca-4] limit of 10000000 steps
c [bca-4] 15316 out of 18276 literals actually usable 84%
c [bca-4] added 62 blocked clauses in 45674 steps
c [rephase-2] after 62068 conflicts (new increment 40000, next 102068)
c [flushphases] 92 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 167 variables 1.8% (9137 remain 63%)
c [simplification-5] removed 659 irredundant clauses 0.2% (337893 remain 91%)
c [simplification-5] maximum reduction of 2% = max (2%, 0%)
c [simplification-5] geometric conflict interval increment 12222 = 36666 / 3
c [simplification-5] new conflict interval 48888
c [simplification-5] penalized conflict interval 48888 = 1 * 48888
c [simplification-5] new conflict limit 110956
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   24.5    9137   337893     67757    8989   2445  4519   7 10.3  49.3   24
c -   25.5    9137   337893     76545    9672   2459  4541   6 10.2  48.2   24
c -   26.4    9137   337893     86204   10462   2485  4552   7 10.2  47.2   24
c -   27.6    9137   337893     96315   11266   2520  4587   7 10.2  47.5   24
c -   28.8    9137   337893    107018   12262   2534  4609   8 10.2  46.2   25
c 
c [simplification-6] limit of 111190 conflicts hit after 111190 conflicts
c [ternres-4] limit 4873634 with penalty 0 = 0 + 0
c [ternres-4] 3332 schedulable variables 36%
c [ternres-4] 44 ternary resolvents (1 bin, 43 trn)
c [ternres-4] 450 variables remain 5% (8687 retained)
c [card-3] limit 609204 penalty 2 = 2 + 0
c [card-3] found 1258 at-most-one constraints of average size 3.1
c [card-3] found 168 at-most-two constraints of average size 4.0
c [card-3] using previous limit 609204 for elimination
c [card-3] 1426 out of 1426 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 19 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 6219 literals 34%
c [treelook-3] scheduling used 302832 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 365119 steps
c [treelook-3] 6211 literals remain 34%
c [treelook-3] 3337 variables remain to probed next time 37%
c [treelook-3] removed 0 variables, found 94 hbrs
c [lift-4] limit 2924180 with penalty 0 = 0 + 0
c [lift-4] using 8261 probes 91%
c [lift-4] 6 units, 9 impls, 3 eqs in 1 rounds
c [lift-4] 8491 variables remain 93% (613 retained)
c [lift-4] removed 14 variables
c [unhide-5] limit 487363 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 370 tauts, 0 hbrs, 24485 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 574 transitive binary clauses
c [elim-5] 1371 variables 15% will be scheduled this time
c [elim-5] scheduled 1371 variables 15%
c [elim-5] limit of 97472684 steps penalty 0 = 0 + 0
c [elim-5] incomplete 748 not tried 8% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 7 = 0% variables out of 9104
c [elim-5] 7 < 1/1000 * 9104 = 9 considered unsuccessful
c [bca-5] limit of 10000000 steps
c [bca-5] 14272 out of 18196 literals actually usable 78%
c [bca-5] added 7 blocked clauses in 48002 steps
c [rephase-3] after 111190 conflicts (new increment 80000, next 191190)
c [flushphases] 15 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 40 variables 0.4% (9097 remain 63%)
c [simplification-6] removed 803 irredundant clauses 0.2% (337090 remain 91%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 48888
c [simplification-6] new conflict interval 97776
c [simplification-6] penalized conflict interval 97776 = 1 * 97776
c [simplification-6] new conflict limit 208966
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   32.0    9097   337090    118312   12949   2558  4858   7 10.1  48.3   25
c R   32.9    9097   337090    125602   19528   2609  4894   7 10.4  50.1   27
c -   33.6    9097   337090    130050   13666   2619  4901   6 10.4  49.9   25
c -   35.3    9097   337090    142224   14607   2642  4924   8 10.3  49.7   25
c -   36.8    9097   337090    155200   15507   2662  4942   7 10.3  49.3   25
c -   38.7    9097   337090    168902   16797   2688  4960   8 10.2  48.5   25
c -   40.4    9097   337090    182652   17476   2721  4982   6 10.4  49.8   25
c -   42.7    9097   337090    197326   18510   2771  4997   7 10.3  49.7   25
c 
c [simplification-7] limit of 209282 conflicts hit after 209284 conflicts
c [ternres-5] limit 10482132 with penalty 0 = 0 + 0
c [ternres-5] 448 schedulable variables 5%
c [ternres-5] 202 ternary resolvents (3 bin, 199 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-13] removed 36 variables
c [basicprobe-3] limit 10482132 penalty 0 = 0 + 0
c [basicprobe-3-0] 956 sched 11%, 12 failed, 0 lifted, 2222 hbrs
c [decomp-14] removed 66 variables
c [basicprobe-3-1] 1373 sched 15%, 6 failed, 0 lifted, 375 hbrs
c [decomp-15] removed 8 variables
c [basicprobe-3-2] 1194 probes remain 13% after last round
c [basicprobe-3-2] 18 units = 18 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 74 variables, found 2597 hbrs
c [bate-2] eliminated 21 asymmetric tautologies during probing
c [lift-5] limit 6289279 with penalty 0 = 0 + 0
c [lift-5] using 7778 probes 87%
c [lift-5] 4 units, 15 impls, 3 eqs in 1 rounds
c [lift-5] 7627 variables remain 85% (1352 retained)
c [lift-5] removed 8 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 922 transitive binary clauses
c [bca-6] limit of 10000000 steps
c [bca-6] 13747 out of 17960 literals actually usable 77%
c [bca-6] added 22 blocked clauses in 60625 steps
c [rephase-4] after 209284 conflicts (new increment 160000, next 369284)
c [flushphases] 3 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 118 variables 1.3% (8979 remain 62%)
c [simplification-7] removed 441 irredundant clauses 0.1% (336649 remain 91%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 48888 = 97776 / 2
c [simplification-7] new conflict interval 146664
c [simplification-7] penalized conflict interval 146664 = 1 * 146664
c [simplification-7] new conflict limit 355948
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   46.2    8979   336649    212366   19443   2990  6552   6 10.3  49.2   27
c -   48.9    8979   336649    228483   20797   3021  6554   6 10.2  48.9   26
c -   51.2    8979   336649    244793   21801   3061  6566   8 10.3  50.0   27
c -   53.6    8979   336649    262044   22637   3090  6570   7 10.9  50.8   26
c R   55.2    8979   336649    271622   31491   3107  6575   6 11.1  50.9   30
c -   56.8    8979   336649    279245   23504   3139  6579   7 11.0  50.9   26
c -   60.3    8979   336649    297658   24944   3176  6589   7 10.9  51.5   26
c -   64.9    8979   336649    316447   26291   3248  6596   5 10.8  51.5   27
c -   69.1    8979   336649    335881   27425   3303  6605   6 11.0  52.3   44
c 
c [simplification-8] limit of 356088 conflicts hit after 356088 conflicts
c [ternres-6] limit 24274504 with penalty 0 = 0 + 0
c [ternres-6] all 8979 free variables schedulable
c [ternres-6] 526 ternary resolvents (9 bin, 517 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1213725 penalty 2 = 2 + 0
c [gauss-3] extracted 68 xors of average arity 2.9
c [gauss-3] connected 195 occurrences of 156 variables (average 1.2)
c [gauss-3] limit 1213725 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 17 variables
c [simpleprobe-4] 7661 schedulable variables 85%
c [simpleprobe-4] limit 97098017 penalty 0 = 0 + 0
c [decomp-17] removed 25 variables
c [simpleprobe-4] 4908 variables remain 55% (4029 retained)
c [simpleprobe-4] removed 25 variables, found 2451 hbrs, 9 units
c [cgrclsr-3] limit 606862 penalty 2 = 2 + 0
c [cgrclsr-3] all 8937 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-6] limit 14564702 with penalty 0 = 0 + 0
c [lift-6] using 6995 probes 78%
c [lift-6] 7 units, 34 impls, 4 eqs in 1 rounds
c [lift-6] 5870 variables remain 66% (3056 retained)
c [lift-6] removed 11 variables
c [cliff-3] limit of 4854900 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2035 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8926 variables 100%
c [block-4] limit of 60686260 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 69 blocked clauses
c [block-4] 69 < 1/1000 * 335728 = 335 considered unsuccessful
c [cce-4] limit of 12137252 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 6068626 steps for small clauses
c [cce-4] scheduling 102849 clauses = 17790 binary + 85059 ternary
c [cce-4] tried to eliminate 455 small clauses 0%
c [cce-4] eliminated 49 small clauses 0%
c [cce-4] eliminated 4 binary clauses 0%
c [cce-4] eliminated 45 ternary clauses 0%
c [cce-4-1] eliminated 49 small clauses in 12137253 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 49 covered clauses in round 1
c [cce-4] eliminated 49 covered clauses in TOTAL during 1 rounds
c [cce-4] 49 < 1/1000 * 335659 = 335 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 8925 variables 100%
c [elim-6] limit of 242745043 steps penalty 1 = 1 + 0
c [elim-6] incomplete 619 not tried 7% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 60 = 1% variables out of 8925
c [bca-7] limit of 10000000 steps
c [bca-7] 12919 out of 17732 literals actually usable 73%
c [bca-7] added 4 blocked clauses in 68393 steps
c [simplification-8] removed 114 variables 1.3% (8865 remain 62%)
c [simplification-8] removed 1461 irredundant clauses 0.4% (335188 remain 90%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 73332 = 146664 / 2
c [simplification-8] new conflict interval 219996
c [simplification-8] penalized conflict interval 219996 = 1 * 219996
c [simplification-8] new conflict limit 576084
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   81.6    8865   335188    362379   28261   3458  7611   5 11.0  52.5   27
c -   87.6    8865   335188    383078   29681   3556  7630   6 11.1  52.8   27
c -   93.3    8865   335188    404541   31011   3624  7643   6 11.2  52.9   27
c -  100.3    8865   335188    426216   32391   3712  7654   6 11.2  52.7   27
c -  107.9    8865   335188    448350   33913   3783  7668   6 11.2  52.3   27
c -  115.7    8865   335188    470840   35163   3857  7681   5 11.2  51.8   27
c -  124.0    8865   335188    493609   36336   3912  7695   6 11.2  51.2   45
c -  132.3    8865   335188    517417   37598   3936  7701   5 11.3  50.8   45
c -  139.1    8865   335188    541709   38848   3952  7702   5 11.5  50.4   46
c -  148.5    8865   335188    566105   40012   3979  7707   4 11.6  50.0   46
c 
c [simplification-9] limit of 576256 conflicts hit after 576256 conflicts
c [ternres-7] limit 58233672 with penalty 0 = 0 + 0
c [ternres-7] all 8865 free variables schedulable
c [ternres-7] 4002 ternary resolvents (84 bin, 3918 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-18] removed 22 variables
c [lift-7] limit 20000000 with penalty 0 = 0 + 0
c [lift-7] using 5217 probes 59%
c [lift-7] 109 units, 82 impls, 4 eqs in 1 rounds
c [lift-7] 3533 variables remain 41% (5190 retained)
c [lift-7] removed 120 variables
c [unhide-6] limit 2911683 with penalty 2 = 2 + 0
c [unhide-6-7] 0 units, 0 failed, 7415 tauts, 0 hbrs, 85790 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 726 transitive binary clauses
c [transred-7] found 2 units
c [elim-7] 515 variables 6% will be scheduled this time
c [elim-7] scheduled 515 variables 6%
c [elim-7] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-7] incomplete 63 not tried 1% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 48 = 1% variables out of 8721
c [bca-8] limit of 10000000 steps
c [bca-8] 12619 out of 17348 literals actually usable 73%
c [bca-8] added 42 blocked clauses in 75422 steps
c [rephase-5] after 576256 conflicts (new increment 320000, next 896256)
c [flushphases] 0 phases reset
c [simplification-9] removed 192 variables 2.2% (8673 remain 60%)
c [simplification-9] removed 14093 irredundant clauses 4.2% (321095 remain 87%)
c [simplification-9] maximum reduction of 4% = max (2%, 4%)
c [simplification-9] geometric conflict interval increment 43999 = 219996 / 5
c [simplification-9] new conflict interval 263995
c [simplification-9] penalized conflict interval 263995 = 1 * 263995
c [simplification-9] new conflict limit 840251
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  163.2    8673   321095    583796   54238   4769  5880   3 11.7  49.7   31
c -  167.1    8673   321095    592181   40088   4787  5881   5 11.6  49.4   28
c -  177.8    8673   321095    617582   41458   4842  5886   5 11.6  48.7   28
c -  188.2    8673   321095    643514   42666   4880  5887   5 11.6  48.1   28
c -  199.6    8673   321095    670038   44032   4901  5890   4 11.6  47.3   28
c -  211.5    8673   321095    696811   45256   4925  5892   5 11.6  46.6   28
c -  222.1    8673   321095    724489   46484   4942  5896   5 11.5  46.0   46
c -  234.6    8673   321095    752687   47644   4971  5899   4 11.5  45.3   45
c -  247.1    8673   321095    781804   49026   4981  5899   5 11.5  44.6   45
c -  260.0    8673   321095    810692   50067   4989  5899   4 11.5  43.9   45
c 
c [simplification-10] limit of 840275 conflicts hit after 840276 conflicts
c [ternres-8] limit 106972262 with penalty 0 = 0 + 0
c [ternres-8] all 8673 free variables schedulable
c [ternres-8] 11945 ternary resolvents (299 bin, 11646 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6685766 penalty 3 = 3 + 0
c [card-4] found 1236 at-most-one constraints of average size 3.1
c [card-4] found 223 at-most-two constraints of average size 4.1
c [card-4] using previous limit 6685766 for elimination
c [card-4] 1457 out of 1459 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-19] removed 11 variables
c [treelook-4] limit 2674306 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 13875 literals 80%
c [treelook-4] scheduling used 867415 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2674306 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 2758166 steps
c [treelook-4] 13788 literals remain 80%
c [treelook-4] 3008 variables remain to probed next time 35%
c [treelook-4] removed 3 variables, found 518 hbrs
c [lift-8] limit 20000000 with penalty 0 = 0 + 0
c [lift-8] using 2931 probes 34%
c [lift-8] 48 units, 91 impls, 4 eqs in 1 rounds
c [lift-8] 1598 variables remain 19% (7000 retained)
c [lift-8] removed 61 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1391 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8598 variables 100%
c [elim-8] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-8] incomplete 146 not tried 2% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 41 = 0% variables out of 8598
c [bca-9] limit of 10000000 steps
c [bca-9] 12381 out of 17116 literals actually usable 72%
c [bca-9] added 27 blocked clauses in 103031 steps
c [simplification-10] removed 116 variables 1.3% (8557 remain 59%)
c [simplification-10] removed 3512 irredundant clauses 1.1% (317583 remain 86%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 131997 = 263995 / 2
c [simplification-10] new conflict interval 395992
c [simplification-10] penalized conflict interval 395992 = 1 * 395992
c [simplification-10] new conflict limit 1236268
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  279.0    8557   317583    841951   50383  13335  7616   3 11.5  43.5   31
c -  292.3    8557   317583    873149   51389  13337  7618   4 11.5  42.9   31
c -  305.9    8557   317583    903894   52416  13346  7618   4 11.5  42.3   30
c -  319.5    8557   317583    935905   53487  13354  7622   6 11.5  41.8   30
c -  332.9    8557   317583    968210   54393  13366  7623   4 11.5  41.2   30
c -  347.5    8557   317583   1002443   55355  13376  7623   3 11.4  40.7   30
c -  360.9    8557   317583   1036324   56343  13381  7624   4 11.4  40.2   30
c -  375.7    8557   317583   1070281   57296  13389  7625   3 11.4  39.6   30
c -  389.2    8557   317583   1106001   58108  13396  7626   3 11.4  39.2   30
c -  400.2    8557   317583   1145438   59090  13396  7626   4 11.4  38.8   30
c -  414.6    8557   317583   1185205   60106  13398  7626   4 11.4  38.4   30
c -  426.5    8557   317583   1225764   61002  13399  7627   3 11.3  38.1   30
c 
c [simplification-11] limit of 1236280 conflicts hit after 1236280 conflicts
c [ternres-9] limit 181575127 with penalty 0 = 0 + 0
c [ternres-9] all 8557 free variables schedulable
c [ternres-9] 9261 ternary resolvents (168 bin, 9093 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-21] removed 6 variables
c [basicprobe-4] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 1194 sched 14%, 14 failed, 0 lifted, 1990 hbrs
c [decomp-22] removed 17 variables
c [basicprobe-4-1] 1349 sched 16%, 7 failed, 0 lifted, 381 hbrs
c [decomp-23] removed 7 variables
c [basicprobe-4-2] 1346 sched 16%, 3 failed, 0 lifted, 77 hbrs
c [decomp-24] removed 9 variables
c [basicprobe-4-3] 1345 sched 16%, 1 failed, 0 lifted, 26 hbrs
c [decomp-25] removed 1 variables
c [basicprobe-4-4] 1345 sched 16%, 1 failed, 0 lifted, 9 hbrs
c [decomp-26] removed 1 variables
c [basicprobe-4-5] 1345 sched 16%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-4-6] 1345 sched 16%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-7] 1345 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-7] fully completed probing
c [basicprobe-4-7] 26 units = 26 failed (100%) + 0 lifted (0%)
c [basicprobe-4-7] removed 35 variables, found 2513 hbrs
c [bate-3] eliminated 370 asymmetric tautologies during probing
c [lift-9] limit 20000000 with penalty 0 = 0 + 0
c [lift-9] using 1009 probes 12%
c [lift-9-1] found 0 units 31 impls in round 1
c [lift-9] 2 units, 47 impls, 3 eqs in 2 rounds
c [lift-9] 568 variables remain 7% (7943 retained)
c [lift-9] removed 5 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1363 transitive binary clauses
c [elim-9] 49 variables 1% will be scheduled this time
c [elim-9] scheduled 49 variables 1%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 8 variables 0% in round 1 in 437881139 steps
c [elim-9-1] backward subsumption/strengthening limit 362118861
c [elim-9-1] subsumed 698 and strengthened 1138 clauses in 362119946 steps
c [elim-9] incomplete 285 not tried 3% in round 1
c [elim-9] transition to [ all 0 rem 1 ] state
c [elim-9] eliminated 8 = 0% variables out of 8511
c [bca-10] limit of 10000000 steps
c [bca-10] 12311 out of 17008 literals actually usable 72%
c [bca-10] added 28 blocked clauses in 96899 steps
c [rephase-6] after 1236280 conflicts (new increment 640000, next 1876280)
c [flushphases] 0 phases reset
c [simplification-11] removed 54 variables 0.6% (8503 remain 59%)
c [simplification-11] removed 4308 irredundant clauses 1.4% (313275 remain 84%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 197996 = 395992 / 2
c [simplification-11] new conflict interval 593988
c [simplification-11] penalized conflict interval 593988 = 1 * 593988
c [simplification-11] new conflict limit 1830268
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  454.3    8503   313275   1250235   81065  19508  9236   3 11.3  37.8   35
c -  462.0    8503   313275   1264754   61683  19511  9236   3 11.3  37.6   30
c -  479.8    8503   313275   1302720   62596  19526  9237   3 11.3  37.2   30
c -  497.6    8503   313275   1341522   63428  19532  9238   4 11.3  36.7   30
c -  514.4    8503   313275   1381627   64303  19536  9238   4 11.3  36.3   30
c -  533.2    8503   313275   1421639   65110  19537  9239   3 11.3  35.9   30
c -  550.6    8503   313275   1462195   66037  19538  9240   4 11.4  35.5   30
c -  568.5    8503   313275   1505261   66922  19539  9240   4 11.4  35.1   30
c -  587.4    8503   313275   1548582   67793  19540  9240   3 11.4  34.8   30
c -  606.8    8503   313275   1590597   68584  19540  9241   3 11.4  34.4   30
c -  627.5    8503   313275   1633955   69386  19547  9242   4 11.4  34.0   50
c -  648.3    8503   313275   1678750   70248  19548  9242   4 11.4  33.7   50
c -  669.3    8503   313275   1723975   71030  19553  9242   4 11.4  33.3   50
c -  690.5    8503   313275   1770610   71833  19559  9242   4 11.4  33.0   50
c -  711.0    8503   313275   1823762   72714  19574  9243   4 11.4  32.7   50
c 
c [simplification-12] limit of 1830278 conflicts hit after 1830278 conflicts
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 8503 free variables schedulable
c [ternres-10] 8405 ternary resolvents (120 bin, 8285 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 182 xors of average arity 3.0
c [gauss-4] connected 542 occurrences of 377 variables (average 1.4)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 3 variables
c [simpleprobe-5] 4629 schedulable variables 54%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-30] removed 2 variables
c [simpleprobe-5] 3688 variables remain 43% (4810 retained)
c [simpleprobe-5] removed 2 variables, found 3794 hbrs, 0 units
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 8498 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 2 probes 0%
c [lift-10-1] found 0 units 0 impls in round 1
c [lift-10-2] found 0 units 0 impls in round 2
c [lift-10-3] found 0 units 0 impls in round 3
c [lift-10-4] found 0 units 0 impls in round 4
c [lift-10-5] found 0 units 0 impls in round 5
c [lift-10] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-10] 563 variables remain 7% (7935 retained)
c [cliff-4] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-4] failed 1, lifted 0
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2368 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 8497 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 33 blocked clauses
c [block-5] 33 < 1/1000 * 312925 = 312 considered unsuccessful
c [cce-5] limit of 77426091 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 605 clauses out of 1088 (56%) of length 12
c [cce-5-1] eliminated 276 clauses out of 361 (76%) of length 11
c [cce-5-1] eliminated 63 clauses out of 430 (15%) of length 10
c [cce-5-1] eliminated 19 clauses out of 1039 (2%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 963 large clauses in 77426092 steps
c [cce-5-1] allowing another 38713046 steps for small clauses
c [cce-5] scheduling 94827 clauses = 17077 binary + 77750 ternary
c [cce-5] tried to eliminate 2552 small clauses 3%
c [cce-5] eliminated 345 small clauses 0%
c [cce-5] eliminated 47 binary clauses 0%
c [cce-5] eliminated 298 ternary clauses 0%
c [cce-5-1] eliminated 345 small clauses in 77426092 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1308 covered clauses in round 1
c [cce-5] eliminated 1308 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8496 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] incomplete 111 not tried 1% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 43 = 1% variables out of 8496
c [bca-11] limit of 10000000 steps
c [bca-11] 12293 out of 16908 literals actually usable 73%
c [bca-11] added 19 blocked clauses in 103729 steps
c [simplification-12] removed 50 variables 0.6% (8453 remain 59%)
c [simplification-12] removed 3277 irredundant clauses 1.0% (309998 remain 84%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 296994 = 593988 / 2
c [simplification-12] new conflict interval 890982
c [simplification-12] penalized conflict interval 890982 = 1 * 890982
c [simplification-12] new conflict limit 2721260
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  747.4    8453   309998   1871421   72649  25950 10845   3 11.4  32.4   33
c -  769.5    8453   309998   1919309   73370  25952 10845   4 11.4  32.1   33
c -  791.1    8453   309998   1967946   74085  25953 10845   4 11.4  31.8   33
c -  813.8    8453   309998   2016632   74866  25961 10845   4 11.4  31.5   33
c -  838.6    8453   309998   2066017   75589  25963 10845   4 11.5  31.2   33
c -  861.7    8453   309998   2120175   76469  25965 10845   3 11.4  30.9   52
c -  886.6    8453   309998   2170957   77234  25968 10846   3 11.5  30.6   52
c -  911.2    8453   309998   2222432   78088  25970 10846   5 11.5  30.4   52
c -  937.5    8453   309998   2275442   78876  25973 10846   4 11.5  30.1   52
c -  963.8    8453   309998   2328974   79610  25978 10846   4 11.5  29.8   52
c -  987.3    8453   309998   2385777   80362  25981 10847   3 11.5  29.6   52
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 405 basic ate = 109 trn 27% + 296 lrg 73% in 3 updates
c bcas: 11 count, 1166 added (183 skipped), 733732 steps
c bkwd: tried 320368 clauses, 637495 lits, 1.99 lits/clause
c bkwd: checked 207675460 occs, 648.24 occs/clause, 325.77 occs/lit
c bkwd: subsumed 6 binary, 248 ternary, 1837 large
c bkwd: strengthened 0 binary, 77 ternary (100% self), 1140 large (65% self)
c blkd: 5 bces, 1154 removed, 7432982 resolutions, 24607912 steps
c blkd: 1273 blocking literals 4%, 2 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 11898766 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 19566 subsumed
c card: 6964 at-most-one constraints found, average size 3.07
c card: 6964 at-most-one constraints used 100%, average size 3.07
c card: 801 at-most-two constraints found, average size 4.02
c card: 798 at-most-two constraints used 100%, average size 4.02
c cces: 5 cces, 3612 eliminated, 3189 ate 88%, 423 abce 12%
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, 1977285 esteps, 6950 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: 332 extracted (301 ands 91%, 15 xors 5%, 16 ites 5%)
c clff: 4 cliffs, 0 lifted, 1 failed
c clff: 98055 decisions, 32361131 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2038963 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 80 gcs, 0 rescored clauses, 1265 rescored vars
c dcps: 30 decompositions, 1279 equivalent 9%
c deco: 12642 decision-only clauses 1%, 57% reduction
c decs: 5338956 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 135355 flipped 2.535% (in 3597 phases)
c elms: 10 elims, 4023 eliminated 27%
c elms: 13 rounds, 1.3 rounds/bve
c elms: 2270 small 56%, 1751 large 44%
c elms: 3259 tried small, 2270 succeeded 70%, 989 failed 30%
c elms: 12205 subsumed, 1787 strengthened, 1896 blocked
c elms: 5977721 copies, 6924615 resolutions, 65152 ipos
c elms: 17879445 subchks, 4858104 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 499 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 20973836 steps, 10486918 extr 50%, 7124 elim 0%
c glue: 11.5 orig avg, 11.5 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 27420 = 9079 simple + 17985 trn 33% + 356 lrg 66%, 1153 sub 1%
c hght: 29 average, 2.56 height/glue
c ints: 65533 luby (18677713 steps), 0 inout (0 steps)
c lift: 10 phases, 53546 probed (17883 level1 33%, 35663 level2 67%)
c lift: 194 units, 28 equivalences, 291 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2404637 clauses, 23.1 length
c lrnd: 702085 uips 29%, 1485919 flips 62%
c mega: 0 count, 0 failed, 0 rounds
c mins: 55641001 learned lits, 33% minimized
c mins: 2371870 mins 99%, 927 bin 0%, 19198 size 1%, 12642 deco 1%
c move: moved 2404637, 1246 bin 0%, 2882 trn 0%, 0 lrg 0%
c otfs: str 39767 dyn (39606 red, 161 irr) 12949 drv 33%, 26818 rst 67%
c otfs: sub 391 dyn (391 red, 0 irr)
c phas: 7 computed, 9707 set, 4737 pos (49%), 4970 neg (51%)
c prbs: 4 basic, 27289 probed, 51 failed, 0 lifted
c prbs: 5 simple, 39194 probed, 17 failed, 255 eqs
c prbs: 4 treelook, 156 probed, 3 failed, 0 lifted
c prps: 1095137196 props, 204 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c psns: 64965636 searches, 10553956 hits, 16% 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: 86 count, 0 reset, 13 acts 15%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 86 arith 100%, 0 double 0%
c rmbd: 808 removed, 155 red 19%
c rphs: 6 recomputed phases
c rsts: 64129 restarts 98%, 1404 skipped 2%
c rsts: 0 saturating 0%, 0 agile 0%, 1404 reuse 100%
c rsts: 37.0 avg interval, 37.0 scaled, 1.0 factor
c rsts: 25976 kept 40.5% average 25.4%
c simp: 12 count (12 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2404637 count (1124353 tried 0.5), 282797 sub out of 2401770 (11.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: 0 count
c tops: 881 fixed 6%, 0 its, 0.00 confs/it
c trvs: 74986488908 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 68.7 search traversals per propagation, 30936.6 per conflict
c trvs: 1.7 search traversals per search visit
c trds: 10 transitive reductions, 11475 removed, 2 failed
c trds: 167613 nodes, 215737 edges, 7289835 steps
c trim: 1529965 words, 5.8 MB
c trnr: 10 count, 685 bin, 34948 trn, 595366949 steps
c unhd: 6 count, 7 rounds, 21199603 steps
c unhd: 224 non-trivial sccs of average size 2.0
c unhd: 58 units, 58 bin, 0 trn, 0 lrg
c unhd: 28 failed, 27 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 15500 tauts, 476 bin 3%, 3064 trn 20%, 4041 lrg 26%
c unhd: 15500 tauts, 7919 stamp 51%, 6737 red 43%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 131415 str, 58 bin 0%, 303 trn 0%, 131054 lrg 100%, 127897 red 97%
c vars: 8453 remaining 58% and 6183 removed 42% out of 14636
c vars: 881 fixed 6%, 4023 eliminated 27%, 1279 equivalent 9%
c vsts: 44750935193 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 40.9 search visits per propagation, 18430.1 per conflict
c wchs: 13361070384 pushed, 23835521 enlarged, 136 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2401770 100   1998958 100  50569240 100  20526343 100   1635238 100
c 
c  0      40793   2         0   0  22918239  45   5762789  28    406810  25 
c  1      73807   3     25420   1  18881414  37<  6975278  34<   596295  36<
c  2     485613  20    460571  23   4345566   9   2863898  14    271337  17 
c  3     934950  39<   824569  41<  3032708   6   3007439  15    245828  15 
c  4     702944  29    556652  28   1145530   2   1570879   8     92701   6 
c  5     137114   6    115010   6    203717   0    288115   1     17928   1 
c  6      17371   1     12365   1     28586   0     38475   0      2936   0 
c  7       4387   0      2310   0      6623   0      9468   0       772   0 
c  8       2374   0      1066   0      3631   0      5104   0       346   0 
c  9       1740   0       677   0      2321   0      3553   0       200   0 
c 10        630   0       302   0       845   0      1251   0        80   0 
c 11         47   0        16   0        60   0        94   0         5   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.1           3.2           0.8           1.5           1.4
c std             1.1           0.9           1.0           1.3           1.3
c 
c   38.985   4% elim
c   27.747   3% analysis
c   11.200   1% cce
c   10.808   1% backward
c    7.440   1% probe
c    6.626   1% ternres
c    6.474   1% mincls
c    5.439   1% gc
c    4.460   0% lift
c    4.338   0% decide
c    4.064   0% decomp
c    3.871   0% bump
c    2.743   0% restart
c    2.319   0% defrag
c    1.701   0% block
c    1.514   0% unhide
c    1.254   0% bca
c    0.993   0% reduce
c    0.934   0% transred
c    0.654   0% cliff
c    0.594   0% cgrclsr
c    0.547   0% gauss
c    0.528   0% card
c    0.315   0% phase
c    0.008   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c    0.000   0% tabularasa
c ----------------------------------
c    2.174   0% probe simple     29%
c    4.348   0% probe basic      58%
c    0.918   0% probe tree-look  12%
c ==================================
c    2.309   0% preprocessing     3%
c   76.658   8% inprocessing     97%
c ==================================
c   78.967   8% simplifying
c  920.806  92% search
c ==================================
c  999.773 100% all
c 
c 5338956 decisions, 5340.2 decisions/sec
c 2417586 conflicts, 2418.1 conflicts/sec
c 1095137196 propagations, 1.1 megaprops/sec
c 999.8 seconds, 77.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
