c launch: /data/cnf/sc2014/app/10pipe_q0_k.cnf.bz2
c host: atom01
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/10pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/10pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 77639 2082017' header
c read 77639 variables, 2082017 clauses, 6164595 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 77638 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   77638  2082016         0       0      0     0   0  0.0   0.0   47
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 896 at-most-one constraints of average size 3.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 896 out of 896 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 12 variables
c [simpleprobe-1] all 77627 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [simpleprobe-1] 69601 variables remain 90% (8026 retained)
c [simpleprobe-1] removed 0 variables, found 4622 hbrs, 0 units
c [unhide-1] limit 1040679 based on 2081358 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 77627 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-1-1] eliminated 34037 variables 44% in round 1 in 162798874 steps
c [elim-1-1] backward subsumption/strengthening limit 237201126
c [elim-1-1] subsumed 0 and strengthened 85 clauses in 237201518 steps
c [elim-1] incomplete 528 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 34037 = 44% variables out of 77627
c [phase-1] phase bias: 5327 positive 12%, 38263 negative 88%
c [simplification-1] removed 34037 variables 43.8% (43590 remain 56%)
c [simplification-1] removed 71905 irredundant clauses 3.5% (2010111 remain 97%)
c [simplification-1] maximum reduction of 44% = max (44%, 3%)
c [simplification-1] large reduction 44% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 2000 = 2 * 1000
c [simplification-1] new conflict limit 2000
c [cut-width] 1403784, max 2971107, min4 778253 at 75%, min10 315803 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   11.5   43590  2010111        69      44      8  4457   1 37.4 123.4   68
c R   11.6   43590  2010111       169     106      8  4460   2 27.1 305.7   68
c R   11.8   43590  2010111       578     508     12  4460   1 58.5 432.4   69
c R   12.0   43590  2010111      1178     996     30  4469   0 53.6 426.4   69
c 
c [simplification-2] limit of 2044 conflicts hit after 2044 conflicts
c [treelook-1] limit 502527 based on 2010111 irredundant clauses
c [treelook-1] scheduled 42105 literals 48%
c [treelook-1] scheduling used 502571 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 502527 based on 2010111 irredundant clauses
c [treelook-1] used 551195 steps
c [treelook-1] 42093 literals remain 48%
c [treelook-1] 39135 variables remain to probed next time 90%
c [treelook-1] removed 0 variables, found 23 hbrs
c [basicprobe-1] limit 4020222 based on 2010111 irredundant clauses
c [basicprobe-1-0] 41112 probes remain 94% after last round
c [basicprobe-1-0] 26 units = 26 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 26 variables, found 1631 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 43564 variables 100%
c [elim-2] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-2] incomplete 33531 not tried 77% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 106 = 0% variables out of 43564
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-2] removed 132 variables 0.3% (43458 remain 56%)
c [simplification-2] removed 4308 irredundant clauses 0.2% (2005803 remain 96%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 40000 = 2 * 20000
c [simplification-2] new conflict limit 42044
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   15.2   43458  2005803      2684    2394     45  6103   2 50.3 526.5   71
c -   15.9   43458  2005803      4871    2172    214  6163   1 46.1 454.5   69
c R   16.0   43458  2005803      5832    2901    224  6163   2 48.5 456.6   70
c -   16.9   43458  2005803      8551    2750    312  6201   1 48.2 450.5   69
c R   18.5   43458  2005803     13098    5742    394  6208   1 59.0 494.7   73
c -   18.9   43458  2005803     13800    3338    410  6214   0 58.8 495.6   69
c i   19.1   43457  2005803     14488    3898    433  6245   0 58.0 487.0   70
c -   20.0   43457  2005803     19112    3986    678  6426   0 53.7 448.5   70
c i   20.1   43456  2005803     19298    4115    678  6455   0 53.4 445.3   70
c -   21.6   43456  2005803     25926    4688    892  6557   1 58.5 439.3   69
c R   22.0   43456  2005803     28102    5187    895  6559   1 65.3 437.9   71
c -   24.2   43456  2005803     34080    5217    956  6639   0 66.5 448.2   70
c 
c [simplification-3] limit of 43122 conflicts hit after 43122 conflicts
c [card-2] limit 545270 penalty 2 = 1 + 1
c [card-2] found 510 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 545270 for elimination
c [card-2] 510 out of 510 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 2 variables
c [simpleprobe-2] 39142 schedulable variables 90%
c [simpleprobe-2] limit 4362165 penalty 2 = 1 + 1
c [simpleprobe-2] 34863 variables remain 80% (8593 retained)
c [simpleprobe-2] removed 0 variables, found 3076 hbrs, 0 units
c [unhide-2] limit 1002574 based on 2005149 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 17 tauts, 0 hbrs, 134985 literals
c [elim-3] 33521 variables 77% will be scheduled this time
c [elim-3] scheduled 33521 variables 77%
c [elim-3] limit of 43621654 steps penalty 1 = 0 + 1
c [elim-3] incomplete 26185 not tried 60% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 429 = 1% variables out of 43456
c [rephase-1] after 43122 conflicts (new increment 20000, next 63122)
c [flushphases] 0 phases reset
c [simplification-3] removed 429 variables 1.0% (43027 remain 55%)
c [simplification-3] removed 5421 irredundant clauses 0.3% (2000382 remain 96%)
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 30000
c [simplification-3] penalized conflict interval 60000 = 2 * 30000
c [simplification-3] new conflict limit 103122
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   32.9   43027  2000382     47746    5840   1114  9590   0 77.1 454.7   70
c -   34.5   43027  2000382     56366    6505   1178  9639   1 77.3 466.3   70
c R   34.9   43027  2000382     60403    8286   1179  9639   1 81.5 464.0   73
c -   36.2   43027  2000382     65995    7072   1323  9759   2 78.2 452.1   70
c -   38.1   43027  2000382     74532    7662   1535  9891   1 74.3 443.3   70
c -   40.1   43027  2000382     83983    8323   1794 10035   1 70.8 440.6   70
c -   42.7   43027  2000382     95199    8861   2052 10212   1 72.8 439.9   70
c 
c [simplification-4] limit of 104692 conflicts hit after 104709 conflicts
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 43027 variables 100%
c [elim-4] limit of 86000315 steps penalty 1 = 0 + 1
c [elim-4] incomplete 18464 not tried 43% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 45 = 0% variables out of 43027
c [rephase-2] after 104709 conflicts (new increment 40000, next 144709)
c [flushphases] 0 phases reset
c [simplification-4] removed 45 variables 0.1% (42982 remain 55%)
c [simplification-4] removed 325 irredundant clauses 0.0% (2000057 remain 96%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 30000
c [simplification-4] new conflict interval 60000
c [simplification-4] penalized conflict interval 120000 = 2 * 60000
c [simplification-4] new conflict limit 224709
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   48.9   42982  2000057    105720    9516   2323 10409   1 70.4 437.9   71
c R   54.0   42982  2000057    131056   15060   2392 10423   1 79.4 424.1   83
c -   55.2   42982  2000057    136139   10253   2545 10525   1 78.3 420.2   71
c -   59.0   42982  2000056    149667   10814   2817 10648   0 76.8 423.7   71
c -   64.5   42982  2000056    171479   11485   3105 10793   1 78.6 417.2   71
c -   70.0   42982  2000056    193458   12136   3276 10875   0 79.3 418.7   71
c -   75.0   42982  2000056    210516   12785   3605 11041   0 78.5 411.4   71
c i   77.1   42981  2000056    221077   20723   3763 11156   0 77.1 410.9   77
c -   78.2   42661  2000056    225928   13458   3817 11210   0 76.4 409.2   71
c 
c [simplification-5] limit of 226227 conflicts hit after 226230 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 45021315 with penalty 1 = 0 + 1
c [ternres-1] all 42661 free variables schedulable
c [ternres-1] 4532 ternary resolvents (1 bin, 4531 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 1800852 penalty 1 = 0 + 1
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 10 variables
c [treelook-2] limit 489519 based on 1958077 irredundant clauses
c [treelook-2] scheduled 39454 literals 46%
c [treelook-2] scheduling used 490122 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 489519 based on 1958077 irredundant clauses
c [treelook-2] used 725998 steps
c [treelook-2] 39448 literals remain 46%
c [treelook-2] 36712 variables remain to probed next time 86%
c [treelook-2] removed 0 variables, found 6 hbrs
c [cgrclsr-1] limit 1800852 penalty 0 = 0 + 0
c [cgrclsr-1] all 42651 free variables schedulable
c [cgrclsr-1] 32308 variables remain 76% (10343 retained)
c [lift-1] limit 10805116 with penalty 0 = 0 + 0
c [lift-1] using 9329 probes 22%
c [lift-1] 62 units, 49 impls, 2 eqs in 1 rounds
c [lift-1] 41691 variables remain 98% (896 retained)
c [lift-1] removed 64 variables
c [cliff-1] limit of 14406821 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 1452
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 41135 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1800852660 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 397804 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 360170530 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 225
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 224
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 223
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 222
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 221
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 220
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 219
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 218
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 217
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 209
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 208
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 206
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 205
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 204
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 203
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 202
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 201
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 200
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 193
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 192
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 189
c [cce-1-1] eliminated 6 clauses out of 10 (60%) of length 188
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 187
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 186
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 185
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 184
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 183
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 178
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 177
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 173
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 172
c [cce-1-1] eliminated 8 clauses out of 14 (57%) of length 171
c [cce-1-1] eliminated 6 clauses out of 7 (86%) of length 170
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 169
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 168
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 167
c [cce-1-1] eliminated 2 clauses out of 10 (20%) of length 164
c [cce-1-1] eliminated 8 clauses out of 12 (67%) of length 163
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 159
c [cce-1-1] eliminated 11 clauses out of 22 (50%) of length 158
c [cce-1-1] eliminated 8 clauses out of 16 (50%) of length 157
c [cce-1-1] eliminated 8 clauses out of 10 (80%) of length 156
c [cce-1-1] eliminated 16 clauses out of 24 (67%) of length 155
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 154
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 153
c [cce-1-1] eliminated 2 clauses out of 8 (25%) of length 152
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 151
c [cce-1-1] eliminated 8 clauses out of 18 (44%) of length 150
c [cce-1-1] eliminated 2 clauses out of 45 (4%) of length 149
c [cce-1-1] eliminated 8 clauses out of 13 (62%) of length 144
c [cce-1-1] eliminated 8 clauses out of 11 (73%) of length 143
c [cce-1-1] eliminated 8 clauses out of 13 (62%) of length 142
c [cce-1-1] eliminated 6 clauses out of 11 (55%) of length 141
c [cce-1-1] eliminated 13 clauses out of 41 (32%) of length 140
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 139
c [cce-1-1] eliminated 8 clauses out of 30 (27%) of length 138
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 137
c [cce-1-1] eliminated 12 clauses out of 24 (50%) of length 136
c [cce-1-1] eliminated 2 clauses out of 10 (20%) of length 135
c [cce-1-1] eliminated 6 clauses out of 47 (13%) of length 131
c [cce-1-1] eliminated 6 clauses out of 12 (50%) of length 130
c [cce-1-1] eliminated 4 clauses out of 27 (15%) of length 129
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 128
c [cce-1-1] eliminated 8 clauses out of 12 (67%) of length 127
c [cce-1-1] eliminated 4 clauses out of 17 (24%) of length 126
c [cce-1-1] eliminated 5 clauses out of 10 (50%) of length 125
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 124
c [cce-1-1] eliminated 10 clauses out of 15 (67%) of length 123
c [cce-1-1] eliminated 2 clauses out of 19 (11%) of length 122
c [cce-1-1] eliminated 7 clauses out of 27 (26%) of length 121
c [cce-1-1] eliminated 6 clauses out of 29 (21%) of length 119
c [cce-1-1] eliminated 4 clauses out of 20 (20%) of length 118
c [cce-1-1] eliminated 12 clauses out of 22 (55%) of length 117
c [cce-1-1] eliminated 4 clauses out of 10 (40%) of length 116
c [cce-1-1] eliminated 4 clauses out of 10 (40%) of length 115
c [cce-1-1] eliminated 4 clauses out of 42 (10%) of length 114
c [cce-1-1] eliminated 4 clauses out of 21 (19%) of length 113
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 112
c [cce-1-1] eliminated 2 clauses out of 27 (7%) of length 111
c [cce-1-1] eliminated 20 clauses out of 27 (74%) of length 110
c [cce-1-1] eliminated 7 clauses out of 28 (25%) of length 109
c [cce-1-1] eliminated 1 clauses out of 10 (10%) of length 108
c [cce-1-1] eliminated 6 clauses out of 12 (50%) of length 107
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 106
c [cce-1-1] eliminated 6 clauses out of 25 (24%) of length 105
c [cce-1-1] eliminated 1 clauses out of 22 (5%) of length 104
c [cce-1-1] eliminated 6 clauses out of 27 (22%) of length 103
c [cce-1-1] eliminated 1 clauses out of 15 (7%) of length 102
c [cce-1-1] eliminated 3 clauses out of 55 (5%) of length 101
c [cce-1-1] eliminated 7 clauses out of 32 (22%) of length 99
c [cce-1-1] eliminated 17 clauses out of 108 (16%) of length 98
c [cce-1-1] eliminated 19 clauses out of 103 (18%) of length 96
c [cce-1-1] eliminated 19 clauses out of 140 (14%) of length 94
c [cce-1-1] eliminated 22 clauses out of 138 (16%) of length 92
c [cce-1-1] eliminated 22 clauses out of 183 (12%) of length 90
c [cce-1-1] eliminated 19 clauses out of 184 (10%) of length 88
c [cce-1-1] eliminated 1 clauses out of 155 (1%) of length 87
c [cce-1-1] eliminated 20 clauses out of 205 (10%) of length 86
c [cce-1-1] eliminated 15 clauses out of 207 (7%) of length 84
c [cce-1-1] eliminated 1 clauses out of 209 (0%) of length 83
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 602 large clauses in 360170531 steps
c [cce-1-1] allowing another 180085265 steps for small clauses
c [cce-1] scheduling 1271817 clauses = 1268288 binary + 3529 ternary
c [cce-1] tried to eliminate 3099 small clauses 0%
c [cce-1] eliminated 215 small clauses 0%
c [cce-1] eliminated 215 binary clauses 0%
c [cce-1-1] eliminated 215 small clauses in 360170531 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 817 covered clauses in round 1
c [cce-1] eliminated 817 covered clauses in TOTAL during 1 rounds
c [cce-1] 817 < 1/1000 * 1359017 = 1359 considered unsuccessful
c [elim-5] 14741 variables 42% will be scheduled this time
c [elim-5] scheduled 14741 variables 42%
c [elim-5] limit of 360170533 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 1035 variables 3% in round 1 in 312139454 steps
c [elim-5-1] backward subsumption/strengthening limit 48031079
c [elim-5-1] subsumed 1 and strengthened 367 clauses in 48032171 steps
c [elim-5] incomplete 1113 not tried 3% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 1035 = 3% variables out of 34967
c [bca-1] limit of 10000000 steps
c [bca-1] 50921 out of 67866 literals actually usable 75%
c [bca-1] added 31835 blocked clauses in 231766 steps
c [rephase-3] after 226230 conflicts (new increment 80000, next 306230)
c [flushphases] 0 phases reset
c [simplification-5] removed 8729 variables 20.5% (33932 remain 44%)
c [simplification-5] removed 643639 irredundant clauses 32.2% (1356417 remain 65%)
c [simplification-5] maximum reduction of 32% = max (20%, 32%)
c [simplification-5] large reduction 32% >= 5% limit
c [simplification-5] new conflict interval 2262 = min (226230/100, 60000)
c [simplification-5] penalized conflict interval 4524 = 2 * 2262
c [simplification-5] new conflict limit 230754
c 
c [simplification-6] limit of 230816 conflicts hit after 230817 conflicts
c [ternres-2] limit 18250278 with penalty 0 = 0 + 0
c [ternres-2] all 33932 free variables schedulable
c [ternres-2] 950 ternary resolvents (15 bin, 935 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 2281284 penalty 2 = 2 + 0
c [card-3] found 1667 at-most-one constraints of average size 3.9
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 2281284 for elimination
c [card-3] 1667 out of 1667 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 77 variables
c [basicprobe-2] limit 18250278 penalty 0 = 0 + 0
c [basicprobe-2-0] 25301 probes remain 75% after last round
c [basicprobe-2-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 7 variables, found 9138 hbrs
c [lift-2] limit 10950166 with penalty 0 = 0 + 0
c [lift-2] using 7457 probes 22%
c [lift-2] 0 units, 13 impls, 4 eqs in 1 rounds
c [lift-2] 31827 variables remain 94% (2017 retained)
c [lift-2] removed 4 variables
c [cliff-2] limit of 14600222 steps penalty 0 = 0 + 0
c [cliff-2] failed 0, lifted 7
c [unhide-3] limit 912513 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 13494 tauts, 0 hbrs, 16974 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 33837 variables 100%
c [block-2] limit of 182502781 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 * 1342347 = 1342 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 33837 variables 100%
c [elim-6] limit of 365005563 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 2163 variables 6% in round 1 in 161870064 steps
c [elim-6-1] backward subsumption/strengthening limit 203135499
c [elim-6-1] subsumed 2 and strengthened 59 clauses in 203136042 steps
c [elim-6] incomplete 512 not tried 2% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 2163 = 6% variables out of 33837
c [bca-2] limit of 10000000 steps
c [bca-2] 45775 out of 63350 literals actually usable 72%
c [bca-2] added 81 blocked clauses in 225404 steps
c [simplification-6] removed 2258 variables 6.7% (31674 remain 41%)
c [simplification-6] removed 17038 irredundant clauses 1.3% (1339379 remain 64%)
c [simplification-6] maximum reduction of 7% = max (7%, 1%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] new conflict interval 2308 = min (230817/100, 60000)
c [simplification-6] penalized conflict interval 4616 = 2 * 2308
c [simplification-6] new conflict limit 235433
c 
c [simplification-7] limit of 235549 conflicts hit after 235558 conflicts
c [ternres-3] limit 18601699 with penalty 0 = 0 + 0
c [ternres-3] all 31674 free variables schedulable
c [ternres-3] 149 ternary resolvents (0 bin, 149 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1860169 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-2] limit 930084 penalty 1 = 1 + 0
c [cgrclsr-2] 23992 schedulable variables 76%
c [cgrclsr-2] 6565 variables remain 21% (25109 retained)
c [lift-3] limit 11161019 with penalty 0 = 0 + 0
c [lift-3] using 5460 probes 17%
c [lift-3] 0 units, 24 impls, 4 eqs in 1 rounds
c [lift-3] 28509 variables remain 90% (3161 retained)
c [lift-3] removed 4 variables
c [cliff-3] limit of 14881359 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 2
c [transred-2] limit 1339358 based on 1339358 irredundant clauses
c [transred-2] removed 5 transitive binary clauses
c [cce-2] limit of 18601699 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 214
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 2 large clauses in 18601700 steps
c [cce-2-1] allowing another 9300850 steps for small clauses
c [cce-2] scheduling 1246036 clauses = 1237469 binary + 8567 ternary
c [cce-2] tried to eliminate 129 small clauses 0%
c [cce-2] eliminated 16 small clauses 0%
c [cce-2] eliminated 16 binary clauses 0%
c [cce-2-1] eliminated 43 small clauses in 18601700 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 45 covered clauses in round 1
c [cce-2] eliminated 45 covered clauses in TOTAL during 1 rounds
c [cce-2] 45 < 1/1000 * 1339358 = 1339 considered unsuccessful
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 31668 variables 100%
c [elim-7] limit of 372033995 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 3 variables 0% in round 1 in 166960380 steps
c [elim-7-1] backward subsumption/strengthening limit 205073615
c [elim-7-1] subsumed 0 and strengthened 52 clauses in 205074369 steps
c [elim-7] incomplete 235 not tried 1% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3 = 0% variables out of 31668
c [elim-7] 3 < 1/1000 * 31668 = 31 considered unsuccessful
c [bca-3] limit of 10000000 steps
c [bca-3] 42645 out of 63332 literals actually usable 67%
c [bca-3] added 3 blocked clauses in 215088 steps
c [simplification-7] removed 9 variables 0.0% (31665 remain 41%)
c [simplification-7] removed 199 irredundant clauses 0.0% (1339167 remain 64%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 60000
c [simplification-7] new conflict interval 120000
c [simplification-7] penalized conflict interval 240000 = 2 * 120000
c [simplification-7] new conflict limit 475558
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  143.8   31665  1339161    243315   14214   7267 59877   3 74.3 405.8   60
c R  147.1   31665  1339161    280404   23513   7294 59902   1 77.2 402.4   76
c -  147.9   31665  1339159    284328   14543   7333 59952   1 76.7 400.0   60
c -  151.6   31665  1339111    303785   15379   7774 60150   1 74.8 400.2   59
c -  155.2   31665  1338987    322977   16063   8274 60410   1 72.8 400.4   59
c -  158.7   31665  1338910    346511   16657   8526 60604   0 71.6 398.1   59
c -  161.8   31665  1338899    367419   17287   8676 60807   0 69.1 395.6   59
c -  166.0   31665  1338855    390147   18157   8976 60908   1 67.3 393.7   59
c i  168.8   31664  1338854    411267   30208   9080 61042   0 66.9 392.7   69
c -  170.0   31664  1338852    416448   18923   9219 61096   1 66.6 393.4   59
c -  174.4   31664  1338796    438787   19814   9706 61309   1 65.5 392.9   60
c i  179.1   31663  1338754    462085   36718  10177 61624   1 63.8 390.6   68
c -  179.1   31663  1338754    462385   21060  10177 61650   1 63.7 390.8   60
c 
c [simplification-8] limit of 479356 conflicts hit after 479359 conflicts
c [ternres-4] limit 29404485 with penalty 0 = 0 + 0
c [ternres-4] all 31663 free variables schedulable
c [ternres-4] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-12] removed 2 variables
c [lift-4] limit 17642691 with penalty 0 = 0 + 0
c [lift-4] using 4101 probes 13%
c [lift-4] 34 units, 76 impls, 6 eqs in 1 rounds
c [lift-4] 26314 variables remain 83% (5299 retained)
c [lift-4] removed 50 variables
c [cliff-4] limit of 23523588 steps penalty 0 = 0 + 0
c [cliff-4] failed 19, lifted 186
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 14 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 31404 variables 100%
c [block-3] limit of 147022425 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 145564 blocked clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 40010 out of 62792 literals actually usable 64%
c [bca-4] added 660 blocked clauses in 193114 steps
c [rephase-4] after 479359 conflicts (new increment 160000, next 639359)
c [flushphases] 0 phases reset
c [simplification-8] removed 268 variables 0.8% (31395 remain 40%)
c [simplification-8] removed 229075 irredundant clauses 17.1% (1109679 remain 53%)
c [simplification-8] maximum reduction of 17% = max (1%, 17%)
c [simplification-8] large reduction 17% >= 5% limit
c [simplification-8] new conflict interval 4793 = min (479359/100, 120000)
c [simplification-8] penalized conflict interval 9586 = 2 * 4793
c [simplification-8] new conflict limit 488945
c 
c [simplification-9] limit of 489133 conflicts hit after 489133 conflicts
c [ternres-5] limit 30043057 with penalty 0 = 0 + 0
c [ternres-5] all 31395 free variables schedulable
c [ternres-5] 58 ternary resolvents (0 bin, 58 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 25176 schedulable variables 80%
c [simpleprobe-3] limit 30043057 penalty 2 = 2 + 0
c [simpleprobe-3] 21936 variables remain 70% (9459 retained)
c [simpleprobe-3] removed 0 variables, found 7469 hbrs, 0 units
c [lift-5] limit 18025834 with penalty 0 = 0 + 0
c [lift-5] using 1939 probes 6%
c [lift-5-1] found 0 units 31 impls in round 1
c [lift-5] 0 units, 37 impls, 4 eqs in 2 rounds
c [lift-5] 24174 variables remain 77% (7217 retained)
c [lift-5] removed 4 variables
c [cliff-5] limit of 24034445 steps penalty 0 = 0 + 0
c [cliff-5] failed 0, lifted 0
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 12 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 31391 variables 100%
c [block-4] limit of 300430573 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 31391 variables 100%
c [elim-8] limit of 300430573 steps penalty 1 = 1 + 0
c [elim-8] incomplete 1583 not tried 5% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 3417 = 11% variables out of 31391
c [bca-5] limit of 10000000 steps
c [bca-5] 32058 out of 55950 literals actually usable 57%
c [bca-5] added 4477 blocked clauses in 205903 steps
c [simplification-9] removed 3421 variables 10.9% (27974 remain 36%)
c [simplification-9] removed 4837 irredundant clauses 0.4% (1104829 remain 53%)
c [simplification-9] maximum reduction of 11% = max (11%, 0%)
c [simplification-9] large reduction 11% >= 5% limit
c [simplification-9] new conflict interval 4891 = min (489133/100, 120000)
c [simplification-9] penalized conflict interval 9782 = 2 * 4891
c [simplification-9] new conflict limit 498915
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  207.5   27974  1104829    494258   19453   8055 69496   1 62.8 387.5   58
c 
c [simplification-10] limit of 499009 conflicts hit after 499009 conflicts
c [ternres-6] limit 30575417 with penalty 0 = 0 + 0
c [ternres-6] all 27974 free variables schedulable
c [ternres-6] 258 ternary resolvents (0 bin, 258 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1910963 penalty 3 = 3 + 0
c [card-4] found 1465 at-most-one constraints of average size 3.8
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1910963 for elimination
c [card-4] 1465 out of 1465 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1528770 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-3] limit 764385 penalty 2 = 2 + 0
c [cgrclsr-3] 5795 schedulable variables 21%
c [cgrclsr-3] fully completed congruence closure
c [lift-6] limit 18345250 with penalty 0 = 0 + 0
c [lift-6] using 9 probes 0%
c [lift-6-1] found 0 units 0 impls in round 1
c [lift-6-2] found 0 units 0 impls in round 2
c [lift-6-3] found 0 units 0 impls in round 3
c [lift-6-4] found 0 units 1 impls in round 4
c [lift-6-5] found 0 units 0 impls in round 5
c [lift-6] 0 units, 1 impls, 0 eqs in 6 rounds
c [lift-6] 21026 variables remain 75% (6948 retained)
c [unhide-4] limit 764385 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 2463 tauts, 0 hbrs, 12356 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 16 transitive binary clauses
c [cce-3] limit of 15287708 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 250
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 249
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 248
c [cce-3-1] eliminated 7 clauses out of 7 (100%) of length 246
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 245
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 244
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 243
c [cce-3-1] eliminated 13 clauses out of 13 (100%) of length 242
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 241
c [cce-3-1] eliminated 12 clauses out of 12 (100%) of length 240
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 239
c [cce-3-1] eliminated 14 clauses out of 14 (100%) of length 238
c [cce-3-1] eliminated 14 clauses out of 14 (100%) of length 236
c [cce-3-1] eliminated 14 clauses out of 14 (100%) of length 234
c [cce-3-1] eliminated 14 clauses out of 14 (100%) of length 232
c [cce-3-1] eliminated 14 clauses out of 14 (100%) of length 230
c [cce-3-1] eliminated 16 clauses out of 16 (100%) of length 228
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 227
c [cce-3-1] eliminated 20 clauses out of 20 (100%) of length 226
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 225
c [cce-3-1] eliminated 22 clauses out of 22 (100%) of length 224
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 223
c [cce-3-1] eliminated 24 clauses out of 24 (100%) of length 222
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 221
c [cce-3-1] eliminated 26 clauses out of 26 (100%) of length 220
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 219
c [cce-3-1] eliminated 26 clauses out of 26 (100%) of length 218
c [cce-3-1] eliminated 28 clauses out of 28 (100%) of length 216
c [cce-3-1] eliminated 28 clauses out of 28 (100%) of length 214
c [cce-3-1] eliminated 28 clauses out of 28 (100%) of length 212
c [cce-3-1] eliminated 28 clauses out of 30 (93%) of length 210
c [cce-3-1] eliminated 27 clauses out of 29 (93%) of length 208
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 207
c [cce-3-1] eliminated 26 clauses out of 28 (93%) of length 206
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 205
c [cce-3-1] eliminated 25 clauses out of 27 (93%) of length 204
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 203
c [cce-3-1] eliminated 27 clauses out of 29 (93%) of length 202
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 201
c [cce-3-1] eliminated 24 clauses out of 24 (100%) of length 200
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 199
c [cce-3-1] eliminated 23 clauses out of 23 (100%) of length 198
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 197
c [cce-3-1] eliminated 22 clauses out of 22 (100%) of length 196
c [cce-3-1] eliminated 9 clauses out of 9 (100%) of length 195
c [cce-3-1] eliminated 23 clauses out of 25 (92%) of length 194
c [cce-3-1] eliminated 7 clauses out of 9 (78%) of length 193
c [cce-3-1] eliminated 23 clauses out of 25 (92%) of length 192
c [cce-3-1] eliminated 7 clauses out of 9 (78%) of length 191
c [cce-3-1] eliminated 23 clauses out of 25 (92%) of length 190
c [cce-3-1] eliminated 6 clauses out of 8 (75%) of length 189
c [cce-3-1] eliminated 22 clauses out of 24 (92%) of length 188
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 700 large clauses in 15287709 steps
c [cce-3-1] allowing another 7643854 steps for small clauses
c [cce-3] scheduling 1019632 clauses = 1012786 binary + 6846 ternary
c [cce-3] tried to eliminate 127 small clauses 0%
c [cce-3] eliminated 2 small clauses 0%
c [cce-3] eliminated 2 binary clauses 0%
c [cce-3-1] eliminated 2 small clauses in 15287709 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 702 covered clauses in round 1
c [cce-3] eliminated 702 covered clauses in TOTAL during 1 rounds
c [cce-3] 702 < 1/1000 * 1104818 = 1104 considered unsuccessful
c [elim-9] 1580 variables 6% will be scheduled this time
c [elim-9] scheduled 1580 variables 6%
c [elim-9] limit of 611508356 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 17 variables 0% in round 1 in 196178696 steps
c [elim-9-1] backward subsumption/strengthening limit 392357392
c [elim-9-1] subsumed 2 and strengthened 165 clauses in 392359464 steps
c [elim-9-1] rescheduled 482 variables 2% by backward subsumption
c [elim-9] incomplete 185 not tried 1% in round 2
c [elim-9] transition to [ all 0 rem 1 ] state
c [elim-9] eliminated 50 = 0% variables out of 27974
c [bca-6] limit of 10000000 steps
c [bca-6] 34467 out of 55850 literals actually usable 62%
c [bca-6] added 1697 blocked clauses in 199136 steps
c [simplification-10] removed 50 variables 0.2% (27924 remain 36%)
c [simplification-10] removed 1644 irredundant clauses 0.1% (1103185 remain 53%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 120000
c [simplification-10] new conflict interval 240000
c [simplification-10] penalized conflict interval 480000 = 2 * 240000
c [simplification-10] new conflict limit 979009
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  232.2   27924  1103185    518291   20366   8480 65958   1 62.2 385.0   56
c -  234.9   27924  1103185    543171   21162   8630 65987   1 62.1 383.3   56
c -  237.9   27924  1103185    569441   21736   8690 66012   1 62.6 382.1   56
c R  241.2   27924  1103185    599208   39365   8715 66022   1 63.3 380.3   73
c -  241.7   27924  1103185    600716   22140   8761 66040   0 63.2 380.1   56
c i  246.1   27923  1103185    627083   40781   8968 66114   1 61.7 376.0   62
c -  246.6   27923  1103185    628657   23032   9022 66140   0 61.6 375.9   56
c i  249.7   27922  1103146    646921   37208   9256 66212   1 60.8 373.7   62
c -  250.8   27902  1103145    655966   23971   9288 66237   2 61.1 373.4   55
c -  255.5   27902  1103134    681665   24670   9658 66515   1 60.4 371.7   55
c -  260.8   27902  1103134    711208   25667  10049 66695   1 59.1 369.1   55
c i  261.5   27901  1103134    717512   30102  10071 66703   1 58.7 368.5   57
c i  263.0   27900  1103133    729535   39841  10082 66790   1 58.7 367.7   64
c i  263.8   27896  1103123    734287   43571  10181 66830   1 58.6 367.1   66
c -  264.7   27896  1103123    738969   26472  10237 66866   1 58.4 366.8   56
c i  266.3   27895  1103118    748919   33852  10403 66914   1 58.1 365.9   60
c -  269.2   27895  1103118    767844   27365  10526 67021   1 57.5 364.4   56
c -  274.1   27895  1103117    798310   28347  10803 67164   3 57.2 361.4   56
c i  279.0   27894  1103112    828622   51705  11266 67283   1 56.3 358.0   68
c -  279.1   27893  1103112    828622   29197  11266 67283   1 56.3 358.0   56
c -  284.3   27893  1103112    869661   30015  11453 67360   1 56.2 354.8   56
c i  288.9   27892  1103112    900681   51186  11653 67450   0 55.4 351.4   68
c -  289.3   27892  1103112    904547   30922  11697 67475   1 55.4 351.4   56
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  289.4   27891  1103112    905069   31360  11699 67492   1 55.4 351.3   57
c -  294.5   27891  1103110    937212   31822  11980 67675   1 55.2 348.5   56
c i  296.0   27890  1103110    944883   37948  12021 67740   1 55.0 347.6   60
c i  296.0   27889  1103110    944884   37948  12021 67740   1 55.0 347.6   60
c i  296.0   27888  1103110    944885   37948  12021 67740   1 55.0 347.6   60
c i  296.0   27887  1103110    944886   37948  12021 67740   1 55.0 347.6   60
c i  297.4   27886  1103110    954118   44898  12084 67768   1 54.7 346.5   62
c i  297.7   27885  1103110    955673   46176  12104 67774   1 54.7 346.3   63
c -  300.0   27885  1103110    969970   32821  12332 67871   1 54.4 344.8   56
c i  300.9   27884  1103110    976580   37866  12367 67898   1 54.2 344.1   59
c 
c [simplification-11] limit of 983421 conflicts hit after 983421 conflicts
c [ternres-7] limit 51609175 with penalty 0 = 0 + 0
c [ternres-7] all 27884 free variables schedulable
c [ternres-7] 118 ternary resolvents (3 bin, 115 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-16] removed 63 variables
c [cliff-6] limit of 20643670 steps penalty 1 = 1 + 0
c [cliff-6] failed 12, lifted 1212
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 8 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 26635 variables 100%
c [block-5] limit of 258045879 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 537585 blocked clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 22453 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] incomplete 659 not tried 3% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 10305 = 46% variables out of 22453
c [bca-7] limit of 10000000 steps
c [bca-7] 12671 out of 24298 literals actually usable 52%
c [bca-7] added 2572 blocked clauses in 60301 steps
c [rephase-5] after 983421 conflicts (new increment 320000, next 1303421)
c [flushphases] 0 phases reset
c [simplification-11] removed 15736 variables 56.4% (12148 remain 16%)
c [simplification-11] removed 777554 irredundant clauses 70.5% (325556 remain 16%)
c [simplification-11] maximum reduction of 70% = max (56%, 70%)
c [simplification-11] large reduction 70% >= 5% limit
c [simplification-11] new conflict interval 9834 = min (983421/100, 240000)
c [simplification-11] penalized conflict interval 9834 = 1 * 9834
c [simplification-11] new conflict limit 993255
c [tabula-rasa-1] number variables 12148 drops below limit 19409
c [tabula-rasa-1] number clauses 325556 drops below limit 1041008
c [flush-cache] 0 binary, 0 ternary, 13781 large
c [flushphases] 12148 phases reset fully
c [phase-3] phase bias: 476 positive 46%, 570 negative 54%
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 3037 and clause limit 162778
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  324.0   12148   325556    988382    2099   3315 15248   5 54.0 342.9   35
c 
c [simplification-12] limit of 993299 conflicts hit after 993299 conflicts
c [ternres-8] limit 51777338 with penalty 0 = 0 + 0
c [ternres-8] all 12148 free variables schedulable
c [ternres-8] 6236 ternary resolvents (2 bin, 6234 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-17] removed 19 variables
c [treelook-3] limit 647216 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 20179 literals 83%
c [treelook-3] scheduling used 647244 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 647216 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 653044 steps
c [treelook-3] 20168 literals remain 83%
c [treelook-3] 10539 variables remain to probed next time 87%
c [treelook-3] removed 0 variables, found 14 hbrs
c [lift-7] limit 10000000 with penalty 1 = 1 + 0
c [lift-7] using 77 probes 1%
c [lift-7-1] found 39 units 8 impls in round 1
c [lift-7-2] found 0 units 1 impls in round 2
c [lift-7-3] found 0 units 4 impls in round 3
c [lift-7-4] found 0 units 0 impls in round 4
c [lift-7-5] found 0 units 1 impls in round 5
c [lift-7] 39 units, 14 impls, 12 eqs in 6 rounds
c [lift-7] 7150 variables remain 59% (4928 retained)
c [lift-7] removed 51 variables
c [cliff-7] limit of 41421871 steps penalty 0 = 0 + 0
c [cliff-7] failed 0, lifted 0
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 100 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 12078 variables 100%
c [block-6] limit of 517773388 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 1593 blocked clauses
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 12078 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] incomplete 483 not tried 4% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 109 = 1% variables out of 12078
c [bca-8] limit of 10000000 steps
c [bca-8] 17690 out of 23940 literals actually usable 74%
c [bca-8] added 14388 blocked clauses in 94777 steps
c [rephase-6] after 993299 conflicts (new increment 20000, next 1013299)
c [flushphases] 45 phases reset
c [phase-4] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-12] removed 179 variables 1.5% (11969 remain 15%)
c [simplification-12] removed 5421 irredundant clauses 1.7% (320135 remain 15%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 26666
c [simplification-12] penalized conflict interval 26666 = 1 * 26666
c [simplification-12] new conflict limit 1019965
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  342.3   11969   320135    993759    2607   9356 39377   4 54.1 342.7   35
c -  342.7   11969   320135   1000264    3196   9368 39378   2 54.3 342.5   35
c -  343.3   11969   320135   1008565    3702   9379 39378   2 54.8 342.1   35
c -  343.9   11969   320135   1014465    4277   9402 39382   2 54.7 341.5   35
c 
c [simplification-13] limit of 1019971 conflicts hit after 1019972 conflicts
c [ternres-9] limit 52228963 with penalty 0 = 0 + 0
c [ternres-9] all 11969 free variables schedulable
c [ternres-9] 281 ternary resolvents (0 bin, 281 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-19] removed 3 variables
c [basicprobe-3] limit 52228963 penalty 0 = 0 + 0
c [basicprobe-3-0] 7829 sched 65%, 1 failed, 0 lifted, 3547 hbrs
c [decomp-20] removed 1 variables
c [basicprobe-3-1] 9477 sched 79%, 1 failed, 0 lifted, 724 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-2] 9473 sched 79%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-3-3] 8599 probes remain 72% after last round
c [basicprobe-3-3] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-3] removed 2 variables, found 4344 hbrs
c [bate-1] eliminated 34 asymmetric tautologies during probing
c [lift-8] limit 20000000 with penalty 0 = 0 + 0
c [lift-8] using 3 probes 0%
c [lift-8-1] found 0 units 0 impls in round 1
c [lift-8-2] found 0 units 0 impls in round 2
c [lift-8-3] found 0 units 0 impls in round 3
c [lift-8-4] found 0 units 0 impls in round 4
c [lift-8-5] found 0 units 0 impls in round 5
c [lift-8] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-8] 7104 variables remain 59% (4860 retained)
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 63 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 11964 variables 100%
c [block-7] limit of 522289639 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 787 blocked clauses
c [elim-12] 452 variables 4% will be scheduled this time
c [elim-12] scheduled 452 variables 4%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] incomplete 464 not tried 4% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 2 = 0% variables out of 11964
c [elim-12] 2 < 1/1000 * 11964 = 11 considered unsuccessful
c [bca-9] limit of 10000000 steps
c [bca-9] 16682 out of 23926 literals actually usable 70%
c [bca-9] added 16178 blocked clauses in 131630 steps
c [rephase-7] after 1019972 conflicts (new increment 40000, next 1059972)
c [flushphases] 39 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-13] removed 7 variables 0.1% (11962 remain 15%)
c [simplification-13] removed 1501 irredundant clauses 0.5% (318634 remain 15%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 26666
c [simplification-13] new conflict interval 53332
c [simplification-13] penalized conflict interval 53332 = 1 * 53332
c [simplification-13] new conflict limit 1073304
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  361.2   11962   318634   1021394    4852   9593 59907   2 54.6 340.8   35
c -  362.0   11962   318634   1028417    5402   9621 59907   2 54.5 340.1   35
c i  362.4   11961   318634   1035359   10429   9667 59915   1 54.3 339.5   37
c -  362.6   11759   318634   1037123    6114   9669 59917   2 54.2 339.3   35
c i  362.8   11758   318634   1039152    7716   9670 59919   3 54.2 339.2   36
c -  363.4   11758   318634   1046233    6794   9686 59940   2 54.1 338.5   35
c i  363.4   11757   318634   1046646    7124   9688 59941   1 54.1 338.4   36
c i  364.0   11756   318634   1053752   12018   9719 59959   2 53.9 337.5   37
c i  364.0   11755   318634   1053822   12057   9722 59959   2 53.9 337.5   37
c i  364.0   11754   318634   1053834   12066   9722 59959   2 53.9 337.5   37
c i  364.0   11753   318634   1053972   12160   9724 59959   2 53.9 337.4   37
c i  364.0   11752   318634   1054261   12321   9736 59965   2 53.9 337.4   37
c i  364.0   11687   318634   1054271   12322   9738 59967   2 53.9 337.4   37
c i  364.0   11686   318634   1054353   12353   9743 59974   2 53.9 337.4   37
c i  364.0   11685   318634   1054402   12369   9747 59979   1 53.9 337.4   37
c i  364.1   11684   318634   1054432   12378   9748 59984   2 53.9 337.4   37
c 0  364.1   10832   318634   1054432   12378   9748 59984   2 53.9 337.4   37
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 34 basic ate = 16 trn 47% + 18 lrg 53% in 1 updates
c bcas: 9 count, 71891 added (8096 skipped), 1557119 steps
c bkwd: tried 396871 clauses, 793431 lits, 2.00 lits/clause
c bkwd: checked 937926267 occs, 2363.30 occs/clause, 1182.11 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 3 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 728 large (0% self)
c blkd: 7 bces, 1083344 removed, 41811581 resolutions, 214482393 steps
c blkd: 33411 blocking literals 22%, 10359 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 11580596 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 826 subsumed
c card: 4538 at-most-one constraints found, average size 3.66
c card: 4538 at-most-one constraints used 100%, average size 3.66
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 3 cces, 1537 eliminated, 1530 ate 100%, 7 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 3 count, 3506383 esteps, 5861283 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: 2537 extracted (2533 ands 100%, 0 xors 0%, 4 ites 0%)
c clff: 7 cliffs, 2859 lifted, 31 failed
c clff: 107961 decisions, 153668861 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 8246612 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 70 gcs, 0 rescored clauses, 512 rescored vars
c dcps: 22 decompositions, 164 equivalent 0%
c deco: 204217 decision-only clauses 21%, 59% reduction
c decs: 20888425 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 264616 flipped 1.267% (in 463 phases)
c elms: 12 elims, 62060 eliminated 80%
c elms: 17 rounds, 1.4 rounds/bve
c elms: 26332 small 42%, 25369 large 41%
c elms: 26390 tried small, 26332 succeeded 100%, 58 failed 0%
c elms: 4590 subsumed, 124424 strengthened, 0 blocked
c elms: 19574726 copies, 38908675 resolutions, 510421 ipos
c elms: 136465332 subchks, 163139308 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10732420 steps, 5366210 extr 50%, 0 elim 0%
c glue: 53.9 orig avg, 49.0 real avg, 6.4 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 55507 = 15167 simple + 40324 trn 27% + 16 lrg 73%, 3434 sub 0%
c hght: 337 average, 6.26 height/glue
c ints: 30647 luby (7823651 steps), 0 inout (0 steps)
c lift: 8 phases, 50073 probed (16774 level1 33%, 33299 level2 67%)
c lift: 135 units, 32 equivalences, 214 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 974215 clauses, 93.7 length
c lrnd: 324294 uips 33%, 511407 flips 52%
c mega: 0 count, 0 failed, 0 rounds
c mins: 91296449 learned lits, 31% minimized
c mins: 752324 mins 77%, 6213 bin 1%, 11461 size 1%, 204217 deco 21%
c move: moved 974215, 999694 bin 103%, 2515 trn 0%, 0 lrg 0%
c otfs: str 467866 dyn (444027 red, 23839 irr) 80217 drv 17%, 387649 rst 83%
c otfs: sub 2559 dyn (2044 red, 515 irr)
c phas: 5 computed, 44637 set, 5803 pos (13%), 38834 neg (87%)
c prbs: 3 basic, 66950 probed, 35 failed, 0 lifted
c prbs: 3 simple, 110768 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 29 probed, 0 failed, 0 lifted
c prps: 1153157521 props, 51 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c psns: 23724749 searches, 2245291 hits, 9% 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: 55 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 55 arith 100%, 0 double 0%
c rmbd: 1403 removed, 1165 red 83%
c rphs: 7 recomputed phases
c rsts: 27707 restarts 90%, 2940 skipped 10%
c rsts: 5 saturating 0%, 0 agile 0%, 2935 reuse 100%
c rsts: 36.4 avg interval, 36.4 scaled, 1.0 factor
c rsts: 25572 kept 92.3% average 27.2%
c simp: 13 count (13 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 974215 count (2162967 tried 2.2), 241719 sub out of 955908 (25.3%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 1 count
c tops: 4583 fixed 6%, 33 its, 31952.48 confs/it
c trvs: 8343263624 traversals, 96% srch, 5% simp, 0% lkhd
c trvs: 7.5 search traversals per propagation, 7627.9 per conflict
c trvs: 1.5 search traversals per search visit
c trds: 8 transitive reductions, 218 removed, 0 failed
c trds: 2493 nodes, 43674 edges, 15341205 steps
c trim: 11343825 words, 43.3 MB
c trnr: 9 count, 21 bin, 12580 trn, 155854797 steps
c unhd: 4 count, 4 rounds, 12012542 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: 15974 tauts, 12 bin 0%, 172 trn 1%, 20 lrg 0%
c unhd: 15974 tauts, 15770 stamp 99%, 2492 red 16%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 164315 str, 0 bin 0%, 100 trn 0%, 164215 lrg 100%, 83653 red 51%
c vars: 10832 remaining 14% and 66807 removed 86% out of 77639
c vars: 4583 fixed 6%, 62060 eliminated 80%, 164 equivalent 0%
c vsts: 5589868998 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 5.0 search visits per propagation, 5016.6 per conflict
c wchs: 621098388 pushed, 53039037 enlarged, 116 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    955908 100    645150 100  23377197 100  10802893 100    948587 100
c 
c  0      12459   1         0   0   7620213  33   1843067  17     32283   3 
c  1      12295   1         0   0   3638249  16   1165117  11     30894   3 
c  2      42873   4     13236   2   6438283  28<  2519874  23    101553  11 
c  3      73132   8     60527   9   2137482   9   1314897  12<    91247  10 
c  4      86543   9     72165  11    948117   4    725969   7     75908   8 
c  5     100550  11     86195  13    684758   3    665534   6    110118  12<
c  6     121446  13    100392  16<   542999   2    686669   6    154924  16 
c  7     130286  14<   106544  17    413356   2    573833   5    129620  14 
c  8     124517  13     95869  15    417435   2    544060   5    105265  11 
c  9     102388  11     57730   9    264860   1    366350   3     65809   7 
c 10     106879  11     40832   6    214588   1    309231   3     44193   5 
c 11      38944   4     10682   2     52292   0     81267   1      6298   1 
c 12       3596   0       978   0      4565   0      7025   0       475   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             6.6           6.4           1.9           3.4           5.4
c std             2.6           2.2           2.2           2.9           2.6
c 
c  105.629  29% elim
c   29.857   8% analysis
c   25.435   7% decide
c   25.245   7% block
c   23.401   6% backward
c   17.564   5% cce
c    8.228   2% probe
c    7.935   2% gc
c    6.725   2% decomp
c    5.751   2% restart
c    4.769   1% bump
c    4.533   1% cliff
c    4.410   1% lift
c    3.571   1% card
c    3.340   1% defrag
c    2.163   1% unhide
c    2.069   1% mincls
c    1.937   1% cgrclsr
c    1.770   0% bca
c    0.838   0% gauss
c    0.811   0% ternres
c    0.685   0% reduce
c    0.467   0% phase
c    0.421   0% transred
c    0.040   0% tabularasa
c    0.038   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    3.332   1% probe simple     40%
c    3.037   1% probe basic      37%
c    1.859   1% probe tree-look  23%
c ==================================
c   11.423   3% preprocessing     6%
c  171.992  47% inprocessing     94%
c ==================================
c  183.415  50% simplifying
c  180.633  50% search
c ==================================
c  364.050 100% all
c 
c 20888425 decisions, 57377.8 decisions/sec
c 1054432 conflicts, 2896.4 conflicts/sec
c 1153157521 propagations, 3.2 megaprops/sec
c 364.1 seconds, 127.5 MB
c launch: done
