c launch: /data/cnf/sc2014/app/12pipe_q0_k.cnf.bz2
c host: atom04
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/12pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/12pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 136800 4216460' header
c read 136800 variables, 4216460 clauses, 12513320 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 136799 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  136799  4216459         0       0      0     0   0  0.0   0.0   93
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 1054114 based on 4216459 irredundant clauses
c [card-1] found 654 at-most-one constraints of average size 3.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1054114 for elimination
c [card-1] 654 out of 654 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 14 variables
c [simpleprobe-1] all 136786 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 5000000 penalty 2 = 0 + 2
c [simpleprobe-1] 127380 variables remain 93% (9406 retained)
c [simpleprobe-1] removed 0 variables, found 1397 hbrs, 0 units
c [unhide-1] limit 2107665 based on 4215330 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 136786 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-1] incomplete 69786 not tried 51% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 58551 = 43% variables out of 136786
c [phase-1] phase bias: 7872 positive 10%, 70363 negative 90%
c [simplification-1] removed 58551 variables 42.8% (78235 remain 57%)
c [simplification-1] removed 120353 irredundant clauses 2.9% (4096106 remain 97%)
c [simplification-1] maximum reduction of 43% = max (43%, 3%)
c [simplification-1] large reduction 43% >= 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] 2687488, max 5833285, min4 1457044 at 75%, min10 553556 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   12.9   78235  4096106        10       3      2  1397   6 28.6  80.1  130
c R   13.0   78235  4096106        30      11      6  1398  18 10.6 104.2  131
c R   13.3   78235  4096106        70      49      8  1398   0 10.2 1070.3  132
c R   13.4   78235  4096106       215     172     11  1398   1 28.5 1015.8  132
c R   14.0   78235  4096106       582     527     22  1398   1 52.3 924.7  133
c R   14.4   78235  4096106      1211    1025     43  1409   0 56.0 870.7  133
c 
c [simplification-2] limit of 2254 conflicts hit after 2254 conflicts
c [treelook-1] limit 1024026 based on 4096106 irredundant clauses
c [treelook-1] scheduled 75202 literals 48%
c [treelook-1] scheduling used 1026420 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1024026 based on 4096106 irredundant clauses
c [treelook-1] used 5127246 steps
c [treelook-1] 75194 literals remain 48%
c [treelook-1] 68805 variables remain to probed next time 88%
c [treelook-1] removed 0 variables, found 209 hbrs
c [basicprobe-1] limit 8192212 based on 4096106 irredundant clauses
c [basicprobe-1-0] 70632 probes remain 90% after last round
c [basicprobe-1-0] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 33 variables, found 2765 hbrs
c [elim-2] 69664 variables 89% will be scheduled this time
c [elim-2] scheduled 69664 variables 89%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] incomplete 69123 not tried 88% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 218 = 0% variables out of 78202
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-2] removed 251 variables 0.3% (77984 remain 57%)
c [simplification-2] removed 6881 irredundant clauses 0.2% (4089225 remain 97%)
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 42254
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   21.0   77984  4089225      2613    2028    165  4482   0 48.5 715.8  133
c -   21.8   77984  4089225      5302    2224    261  4598   1 47.3 582.3  133
c R   21.9   77984  4089225      5706    2554    261  4599   1 49.1 579.7  133
c -   23.3   77984  4089225      8923    2742    454  4730   0 48.7 524.6  133
c R   24.2   77984  4089225     12770    5942    544  4790   2 51.5 517.9  136
c -   24.6   77984  4089225     13174    3254    601  4798   0 51.1 519.0  133
c i   25.7   77983  4089225     15581    5232    697  4907   0 50.9 513.8  135
c -   27.0   77571  4089225     18227    3954    843  4980   0 50.1 518.4  133
c i   27.3   77570  4089225     18840    4519    854  4980   0 50.3 525.6  134
c i   27.3   77569  4089225     18841    4519    854  4980   0 50.3 525.6  134
c i   28.8   77568  4089225     22454    7525    983  5080   0 49.6 527.2  136
c -   29.3   77265  4089225     23674    4489   1080  5108   2 49.3 521.5  133
c R   29.9   77265  4089225     28157    7739   1109  5119   1 54.9 517.1  137
c -   30.8   77265  4089225     30626    5040   1335  5258   1 53.9 499.5  133
c -   33.8   77265  4089225     36954    5612   1530  5357   0 54.0 535.4  133
c -   36.6   77265  4089225     44177    6162   1711  5482   0 54.2 522.1  133
c 
c [simplification-3] limit of 44322 conflicts hit after 44331 conflicts
c [card-2] limit 1022306 based on 4089225 irredundant clauses
c [card-2] found 739 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1022306 for elimination
c [card-2] 739 out of 739 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 852 variables
c [simpleprobe-2] 71866 schedulable variables 93%
c [simpleprobe-2] limit 2497355 penalty 3 = 1 + 2
c [simpleprobe-2] 71911 variables remain 93% (5221 retained)
c [simpleprobe-2] removed 0 variables, found 523 hbrs, 0 units
c [unhide-2] limit 1982571 based on 3965143 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 15 tauts, 0 hbrs, 33865 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 77132 variables 100%
c [elim-3] limit of 24973555 steps penalty 2 = 0 + 2
c [elim-3] incomplete 66274 not tried 86% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1871 = 2% variables out of 77132
c [rephase-1] after 44331 conflicts (new increment 20000, next 64331)
c [flushphases] 0 phases reset
c [simplification-3] removed 2004 variables 2.6% (75261 remain 55%)
c [simplification-3] removed 128304 irredundant clauses 3.1% (3960921 remain 94%)
c [simplification-3] maximum reduction of 3% = max (3%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 25000
c [simplification-3] penalized conflict interval 50000 = 2 * 25000
c [simplification-3] new conflict limit 94331
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   45.3   75260  3960921     50422   11178   1878  6053   0 52.5 505.7  132
c -   46.1   75113  3960921     52432    6859   1937  6056   1 52.8 516.7  129
c R   47.3   75113  3960921     61397   13887   1942  6084   1 58.6 521.4  136
c -   47.5   75113  3960921     61640    7588   1944  6103   0 58.5 520.4  129
c i   48.1   75112  3960921     63022    8768   1981  6143   0 58.0 516.3  130
c -   51.0   74874  3960921     71238    8158   2185  6370   0 56.7 498.3  129
c -   55.1   74874  3960921     81089    8765   2490  6556   1 56.1 501.1  129
c -   59.3   74874  3960921     91267    9486   2653  6607   0 58.2 512.7  130
c 
c [simplification-4] limit of 96029 conflicts hit after 96052 conflicts
c [decomp-7] removed 438 variables
c [elim-4] 65671 variables 88% will be scheduled this time
c [elim-4] scheduled 65671 variables 88%
c [elim-4] limit of 52733057 steps penalty 2 = 0 + 2
c [elim-4] incomplete 60312 not tried 81% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 1822 = 2% variables out of 74823
c [rephase-2] after 96052 conflicts (new increment 40000, next 136052)
c [flushphases] 0 phases reset
c [simplification-4] removed 1873 variables 2.5% (73001 remain 53%)
c [simplification-4] removed 69345 irredundant clauses 1.8% (3891576 remain 92%)
c [simplification-4] maximum reduction of 3% = max (3%, 2%)
c [simplification-4] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-4] new conflict interval 31250
c [simplification-4] penalized conflict interval 62500 = 2 * 31250
c [simplification-4] new conflict limit 158552
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   67.2   73001  3891576    102956   10090   2979  6713   0 57.3 511.7  129
c -   72.6   73001  3891576    114821   11105   3277  6908   1 57.9 511.9  129
c R   75.9   73001  3891576    133168   16886   3310  6920   1 68.0 506.9  143
c -   78.9   73001  3891576    138105   11619   3479  6997   0 67.4 513.1  129
c -   84.0   73001  3891576    150518   12324   3672  7113   1 66.2 526.4  129
c i   86.9   73000  3891576    156197   17258   3741  7141   0 66.0 536.4  133
c 
c [simplification-5] limit of 159610 conflicts hit after 159611 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 23508166 with penalty 2 = 0 + 2
c [ternres-1] all 72604 free variables schedulable
c [ternres-1] 1886 ternary resolvents (0 bin, 1886 trn)
c [ternres-1] 6 variables remain 0% (72598 retained)
c [gauss-1] limit 1945788 based on 3891576 irredundant clauses
c [gauss-1] extracted 2 xors of average arity 2.0
c [gauss-1] connected 4 occurrences of 4 variables (average 1.0)
c [gauss-1] limit 1909174 based on 3818349 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 108 variables
c [treelook-2] limit 954533 based on 3818133 irredundant clauses
c [treelook-2] scheduled 69144 literals 48%
c [treelook-2] scheduling used 954603 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 954533 based on 3818133 irredundant clauses
c [treelook-2] used 1118802 steps
c [treelook-2] 69139 literals remain 48%
c [treelook-2] 62854 variables remain to probed next time 87%
c [treelook-2] removed 0 variables, found 8 hbrs
c [cgrclsr-1] limit 1909066 based on 3818133 irredundant clauses
c [cgrclsr-1] all 72496 free variables schedulable
c [cgrclsr-1] 57507 variables remain 79% (14989 retained)
c [lift-1] limit 2820979 with penalty 2 = 0 + 2
c [lift-1] using 15399 probes 21%
c [lift-1] 6 units, 18 impls, 0 eqs in 1 rounds
c [lift-1] 72280 variables remain 100% (210 retained)
c [lift-1] removed 6 variables
c [cliff-1] limit of 7631496 steps based on 3815748 irredundant clauses
c [cliff-1] failed 0, lifted 700
c [transred-1] limit 3815748 based on 3815748 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 71790 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 470163327 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 726126 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 188065330 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 339
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 337
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 335
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 334
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 333
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 331
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 330
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 329
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 328
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 327
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 326
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 316
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 314
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 312
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 311
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 310
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 308
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 307
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 306
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 305
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 304
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 303
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 302
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 301
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 300
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 299
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 298
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 297
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 296
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 295
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 293
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 291
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 289
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 288
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 287
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 286
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 285
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 284
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 283
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 282
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 281
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 280
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 279
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 278
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 277
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 276
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 275
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 274
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 271
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 269
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 267
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 266
c [cce-1-1] eliminated 8 clauses out of 10 (80%) of length 265
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 264
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 263
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 262
c [cce-1-1] eliminated 8 clauses out of 11 (73%) of length 261
c [cce-1-1] eliminated 7 clauses out of 8 (88%) of length 260
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 259
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 258
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 257
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 256
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 255
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 254
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 253
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 250
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 248
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 247
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 246
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 245
c [cce-1-1] eliminated 7 clauses out of 9 (78%) of length 244
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 242
c [cce-1-1] eliminated 12 clauses out of 12 (100%) of length 241
c [cce-1-1] eliminated 9 clauses out of 14 (64%) of length 240
c [cce-1-1] eliminated 8 clauses out of 9 (89%) of length 239
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 238
c [cce-1-1] eliminated 7 clauses out of 8 (88%) of length 237
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 236
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 235
c [cce-1-1] eliminated 2 clauses out of 7 (29%) of length 234
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 233
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 232
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 231
c [cce-1-1] eliminated 7 clauses out of 13 (54%) of length 230
c [cce-1-1] eliminated 3 clauses out of 10 (30%) of length 229
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 228
c [cce-1-1] eliminated 8 clauses out of 11 (73%) of length 227
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 226
c [cce-1-1] eliminated 1 clauses out of 13 (8%) of length 224
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 356 large clauses in 188065331 steps
c [cce-1-1] allowing another 94032665 steps for small clauses
c [cce-1] scheduling 2793266 clauses = 2790757 binary + 2509 ternary
c [cce-1] tried to eliminate 686 small clauses 0%
c [cce-1] eliminated 121 small clauses 0%
c [cce-1] eliminated 121 binary clauses 0%
c [cce-1-1] eliminated 121 small clauses in 188065331 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 477 covered clauses in round 1
c [cce-1] eliminated 477 covered clauses in TOTAL during 1 rounds
c [cce-1] 477 < 1/1000 * 2931654 = 2931 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 63195 variables 100%
c [elim-5] limit of 188065331 steps penalty 1 = 0 + 1
c [elim-5] incomplete 30295 not tried 48% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 6852 = 11% variables out of 63195
c [bca-1] limit of 10000000 steps
c [bca-1] 90648 out of 112688 literals actually usable 80%
c [bca-1] added 1815 blocked clauses in 296031 steps
c [rephase-3] after 159611 conflicts (new increment 80000, next 239611)
c [flushphases] 0 phases reset
c [simplification-5] removed 16261 variables 22.4% (56343 remain 41%)
c [simplification-5] removed 1054627 irredundant clauses 27.1% (2836949 remain 67%)
c [simplification-5] maximum reduction of 27% = max (22%, 27%)
c [simplification-5] large reduction 27% >= 5% limit
c [simplification-5] new conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 4000 = 2 * 2000
c [simplification-5] new conflict limit 163611
c 
c [simplification-6] limit of 163621 conflicts hit after 163622 conflicts
c [ternres-2] limit 11347788 based on 2836947 irredundant clauses
c [ternres-2] 5 schedulable variables 0%
c [ternres-2] 112 ternary resolvents (0 bin, 112 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 1193527 penalty 3 = 2 + 1
c [card-3] found 676 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1193527 for elimination
c [card-3] 676 out of 676 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 1 variables
c [basicprobe-2] limit 9548216 penalty 1 = 0 + 1
c [basicprobe-2-0] 49061 probes remain 87% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 75 variables, found 5494 hbrs
c [bate-1] eliminated 5 asymmetric tautologies during probing
c [lift-2] limit 5728929 with penalty 1 = 0 + 1
c [lift-2] using 12296 probes 22%
c [lift-2] 8 units, 26 impls, 3 eqs in 1 rounds
c [lift-2] 55467 variables remain 99% (747 retained)
c [lift-2] removed 53 variables
c [cliff-2] limit of 7638573 steps penalty 1 = 0 + 1
c [cliff-2] failed 0, lifted 156
c [unhide-3] limit 1409703 based on 2819406 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 8594 tauts, 0 hbrs, 79181 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 56058 variables 100%
c [block-2] limit of 95482166 steps penalty 1 = 0 + 1
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 101863 blocked clauses
c [elim-6] 29012 variables 53% will be scheduled this time
c [elim-6] scheduled 29012 variables 53%
c [elim-6] limit of 190964332 steps penalty 1 = 0 + 1
c [elim-6] incomplete 14320 not tried 26% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 711 = 1% variables out of 54448
c [bca-2] limit of 10000000 steps
c [bca-2] 85419 out of 107476 literals actually usable 79%
c [bca-2] added 59 blocked clauses in 282763 steps
c [simplification-6] removed 2606 variables 4.6% (53737 remain 39%)
c [simplification-6] removed 190382 irredundant clauses 6.7% (2646565 remain 63%)
c [simplification-6] maximum reduction of 7% = max (5%, 7%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] new conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 4000 = 2 * 2000
c [simplification-6] new conflict limit 167622
c 
c [simplification-7] limit of 167682 conflicts hit after 167684 conflicts
c [ternres-3] limit 10586172 based on 2646543 irredundant clauses
c [ternres-3] all 53737 free variables schedulable
c [ternres-3] 1212 ternary resolvents (0 bin, 1212 trn)
c [ternres-3] 25530 variables remain 48% (28207 retained)
c [gauss-2] limit 1323271 based on 2646543 irredundant clauses
c [gauss-2] extracted 1 xors of average arity 2.0
c [gauss-2] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-2] limit 1323271 based on 2646543 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 59 variables
c [cgrclsr-2] limit 1323212 based on 2646425 irredundant clauses
c [cgrclsr-2] 42550 schedulable variables 79%
c [cgrclsr-2] 25121 variables remain 47% (28557 retained)
c [lift-3] limit 5820479 with penalty 1 = 0 + 1
c [lift-3] using 11536 probes 21%
c [lift-3] 2 units, 9 impls, 0 eqs in 1 rounds
c [lift-3] 52421 variables remain 98% (1255 retained)
c [lift-3] removed 2 variables
c [cliff-3] limit of 7760638 steps penalty 1 = 0 + 1
c [cliff-3] failed 0, lifted 118
c [transred-2] limit 2645685 based on 2645685 irredundant clauses
c [transred-2] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 53558 variables 100%
c [block-3] limit of 97007983 steps penalty 1 = 0 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 93708 blocked clauses
c [cce-2] limit of 9700798 steps penalty 2 = 1 + 1
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] allowing another 4850399 steps for small clauses
c [cce-2] scheduling 2414696 clauses = 2399279 binary + 15417 ternary
c [cce-2] tried to eliminate 69 small clauses 0%
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 0 covered clauses in round 1
c [cce-2] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 51894 variables 100%
c [elim-7] limit of 194015967 steps penalty 1 = 0 + 1
c [elim-7] incomplete 12411 not tried 24% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 1194 = 2% variables out of 51894
c [bca-3] limit of 10000000 steps
c [bca-3] 77920 out of 101402 literals actually usable 77%
c [bca-3] added 3722 blocked clauses in 277656 steps
c [simplification-7] removed 3037 variables 5.7% (50700 remain 37%)
c [simplification-7] removed 109207 irredundant clauses 4.1% (2537336 remain 60%)
c [simplification-7] maximum reduction of 6% = max (6%, 4%)
c [simplification-7] large reduction 6% >= 5% limit
c [simplification-7] new conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 4000 = 2 * 2000
c [simplification-7] new conflict limit 171684
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  172.7   50700  2537336    170384   12847   5957 31465   1 69.7 534.9  106
c 
c [simplification-8] limit of 171752 conflicts hit after 171764 conflicts
c [ternres-4] limit 10149324 based on 2537331 irredundant clauses
c [ternres-4] 24082 schedulable variables 47%
c [ternres-4] 1214 ternary resolvents (0 bin, 1214 trn)
c [ternres-4] 22 variables remain 0% (50678 retained)
c [lift-4] limit 5899307 with penalty 1 = 0 + 1
c [lift-4] using 9616 probes 19%
c [lift-4] 0 units, 11 impls, 3 eqs in 1 rounds
c [lift-4] 48982 variables remain 97% (1715 retained)
c [lift-4] removed 3 variables
c [cliff-4] limit of 7865743 steps penalty 1 = 0 + 1
c [cliff-4] failed 0, lifted 0
c [transred-3] limit 2537325 based on 2537325 irredundant clauses
c [transred-3] removed 0 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 50697 variables 100%
c [block-4] limit of 98321795 steps penalty 1 = 0 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 150 blocked clauses
c [block-4] 150 < 1/1000 * 2537325 = 2537 considered unsuccessful
c [elim-8] 12332 variables 24% will be scheduled this time
c [elim-8] scheduled 12332 variables 24%
c [elim-8] limit of 196643590 steps penalty 1 = 0 + 1
c [elim-8] incomplete 4985 not tried 10% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 99 = 0% variables out of 50697
c [bca-4] limit of 10000000 steps
c [bca-4] 82896 out of 101198 literals actually usable 82%
c [bca-4] added 2108 blocked clauses in 300200 steps
c [simplification-8] removed 102 variables 0.2% (50598 remain 37%)
c [simplification-8] removed 453 irredundant clauses 0.0% (2536878 remain 60%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 31250
c [simplification-8] new conflict interval 62500
c [simplification-8] penalized conflict interval 125000 = 2 * 62500
c [simplification-8] new conflict limit 296764
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  194.1   50598  2536806    185363   13572   7414 34168   1 69.8 556.2  106
c -  199.2   50598  2536712    205892   14203   8005 34399   2 71.8 561.9  106
c -  203.1   50598  2536658    221809   14944   8454 34577   1 71.0 559.0  106
c -  209.0   50598  2536635    238914   15868   8860 34703   0 70.4 560.7  106
c -  214.1   50598  2536635    267590   16689   9335 34861   1 69.7 557.7  106
c R  216.8   50598  2536635    285223   23042   9383 35064   1 70.0 552.4  116
c -  219.8   50598  2536635    298411   17413   9485 35085   0 68.9 551.7  108
c 
c [simplification-9] limit of 298668 conflicts hit after 298669 conflicts
c [ternres-5] limit 13872542 with penalty 1 = 0 + 1
c [ternres-5] 22 schedulable variables 0%
c [ternres-5] 298 ternary resolvents (0 bin, 298 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 47196 schedulable variables 93%
c [simpleprobe-3] limit 13872542 penalty 3 = 2 + 1
c [simpleprobe-3] 43231 variables remain 85% (7367 retained)
c [simpleprobe-3] removed 0 variables, found 4597 hbrs, 0 units
c [lift-5] limit 8323525 with penalty 1 = 0 + 1
c [lift-5] using 9349 probes 18%
c [lift-5] 0 units, 14 impls, 3 eqs in 1 rounds
c [lift-5] 48231 variables remain 95% (2364 retained)
c [lift-5] removed 3 variables
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 50595 variables 100%
c [elim-9] limit of 277450857 steps penalty 1 = 0 + 1
c [elim-9] incomplete 4230 not tried 8% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 139 = 0% variables out of 50595
c [bca-5] limit of 10000000 steps
c [bca-5] 78983 out of 100914 literals actually usable 78%
c [bca-5] added 3 blocked clauses in 277600 steps
c [rephase-4] after 298669 conflicts (new increment 160000, next 458669)
c [flushphases] 0 phases reset
c [simplification-9] removed 142 variables 0.3% (50456 remain 37%)
c [simplification-9] removed 567 irredundant clauses 0.0% (2536068 remain 60%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 62500
c [simplification-9] new conflict interval 125000
c [simplification-9] penalized conflict interval 250000 = 2 * 125000
c [simplification-9] new conflict limit 548669
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  232.6   50455  2536068    318333   30677   9954 40111   0 66.3 547.7  114
c -  233.6   50455  2536064    320439   18337  10113 40206   0 66.2 550.0  109
c -  239.7   50455  2536047    343106   19104  10523 40258   1 67.2 546.6  109
c -  246.5   50455  2536020    363672   19770  11009 40389   0 66.9 547.4  109
c -  252.2   50455  2536020    387307   20822  11487 40434   0 65.5 543.0  109
c i  252.4   50454  2536020    388183   21314  11487 40512   1 65.4 543.7  110
c -  257.2   50454  2536020    411599   21682  11675 40729   1 63.2 539.5  109
c i  259.0   50453  2536020    419852   26621  11725 40749   1 62.3 538.7  110
c -  264.8   50453  2536018    437642   22634  12078 40913   0 62.3 540.3  109
c -  271.8   50453  2535952    461598   23468  12878 41239   0 61.7 539.3  110
c -  278.1   50453  2535845    486153   24184  13499 41539   0 62.1 537.9  110
c -  284.3   50453  2535818    509646   25050  13962 41861   0 61.4 535.7  110
c -  291.7   50453  2535796    545167   25903  14300 42041   1 63.1 531.7  110
c 
c [simplification-10] limit of 552715 conflicts hit after 552716 conflicts
c [ternres-6] limit 22337162 with penalty 1 = 0 + 1
c [ternres-6] all 50453 free variables schedulable
c [ternres-6] 301 ternary resolvents (0 bin, 301 trn)
c [ternres-6] 7 variables remain 0% (50446 retained)
c [card-4] limit 1396072 penalty 4 = 3 + 1
c [card-4] found 607 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1396072 for elimination
c [card-4] 607 out of 607 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1267898 based on 2535796 irredundant clauses
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 1264071 based on 2528143 irredundant clauses
c [cgrclsr-3] 23639 schedulable variables 47%
c [cgrclsr-3] 9738 variables remain 19% (40715 retained)
c [lift-6] limit 10000000 with penalty 1 = 0 + 1
c [lift-6] using 8636 probes 17%
c [lift-6] 18 units, 56 impls, 0 eqs in 1 rounds
c [lift-6] 47221 variables remain 94% (3212 retained)
c [lift-6] removed 20 variables
c [cliff-5] limit of 8934865 steps penalty 2 = 1 + 1
c [cliff-5] failed 5, lifted 230
c [unhide-4] limit 1259253 based on 2518507 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 1475 tauts, 0 hbrs, 11667 literals
c [transred-4] limit 2422814 based on 2422814 irredundant clauses
c [transred-4] removed 1 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 50197 variables 100%
c [block-5] limit of 111685814 steps penalty 2 = 1 + 1
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 254713 blocked clauses
c [cce-3] limit of 11168581 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 335
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 334
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 333
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 331
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 330
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 329
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 328
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 327
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 326
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 324
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 323
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 322
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 320
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 312
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 309
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 307
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 306
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 305
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 304
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 303
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 302
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 300
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 299
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 298
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 290
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 288
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 54 large clauses in 11168582 steps
c [cce-3-1] allowing another 5584291 steps for small clauses
c [cce-3] scheduling 2030980 clauses = 2015379 binary + 15601 ternary
c [cce-3] tried to eliminate 38 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 11168582 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 56 covered clauses in round 1
c [cce-3] eliminated 56 covered clauses in TOTAL during 1 rounds
c [cce-3] 56 < 1/1000 * 2168100 = 2168 considered unsuccessful
c [elim-10] 3924 variables 8% will be scheduled this time
c [elim-10] scheduled 3924 variables 8%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10-1] eliminated 199 variables 0% in round 1 in 335023588 steps
c [elim-10-1] backward subsumption/strengthening limit 64976412
c [elim-10-1] subsumed 0 and strengthened 136 clauses in 64978948 steps
c [elim-10] incomplete 483 not tried 1% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 199 = 0% variables out of 50191
c [bca-6] limit of 10000000 steps
c [bca-6] 79071 out of 99986 literals actually usable 79%
c [bca-6] added 1137 blocked clauses in 260816 steps
c [rephase-5] after 552716 conflicts (new increment 320000, next 872716)
c [flushphases] 0 phases reset
c [simplification-10] removed 461 variables 0.9% (49992 remain 37%)
c [simplification-10] removed 368505 irredundant clauses 14.5% (2167291 remain 51%)
c [simplification-10] maximum reduction of 15% = max (1%, 15%)
c [simplification-10] large reduction 15% >= 5% limit
c [simplification-10] new conflict interval 5527 = min (552716/100, 125000)
c [simplification-10] penalized conflict interval 11054 = 2 * 5527
c [simplification-10] new conflict limit 563770
c 
c [simplification-11] limit of 563822 conflicts hit after 563824 conflicts
c [ternres-7] limit 22525257 with penalty 1 = 0 + 1
c [ternres-7] 7 schedulable variables 0%
c [ternres-7] 339 ternary resolvents (0 bin, 339 trn)
c [ternres-7] fully completed ternary resolution
c [lift-7] limit 10000000 with penalty 1 = 0 + 1
c [lift-7] using 7618 probes 15%
c [lift-7] 0 units, 22 impls, 6 eqs in 1 rounds
c [lift-7] 45877 variables remain 92% (4109 retained)
c [lift-7] removed 6 variables
c [cliff-6] limit of 18020206 steps penalty 1 = 0 + 1
c [cliff-6] failed 0, lifted 22
c [transred-5] limit 2167278 based on 2167278 irredundant clauses
c [transred-5] removed 14 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 49964 variables 100%
c [block-6] limit of 225252575 steps penalty 1 = 0 + 1
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 937 blocked clauses
c [block-6] 937 < 1/1000 * 2167270 = 2167 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 49601 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-11] incomplete 3087 not tried 6% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 4497 = 9% variables out of 49601
c [bca-7] limit of 10000000 steps
c [bca-7] 68994 out of 90210 literals actually usable 76%
c [bca-7] added 2852 blocked clauses in 268021 steps
c [simplification-11] removed 4888 variables 9.8% (45104 remain 33%)
c [simplification-11] removed 21255 irredundant clauses 1.0% (2146035 remain 51%)
c [simplification-11] maximum reduction of 10% = max (10%, 1%)
c [simplification-11] large reduction 10% >= 5% limit
c [simplification-11] new conflict interval 5638 = min (563824/100, 125000)
c [simplification-11] penalized conflict interval 11276 = 2 * 5638
c [simplification-11] new conflict limit 575100
c 
c [simplification-12] limit of 575106 conflicts hit after 575110 conflicts
c [ternres-8] limit 22759020 with penalty 1 = 0 + 1
c [ternres-8] all 45104 free variables schedulable
c [ternres-8] 289 ternary resolvents (4 bin, 285 trn)
c [ternres-8] 26 variables remain 0% (45078 retained)
c [decomp-17] removed 1 variables
c [treelook-3] limit 536508 based on 2146032 irredundant clauses
c [treelook-3] scheduled 42896 literals 48%
c [treelook-3] scheduling used 537748 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 536508 based on 2146032 irredundant clauses
c [treelook-3] used 711411 steps
c [treelook-3] 42891 literals remain 48%
c [treelook-3] 39704 variables remain to probed next time 88%
c [treelook-3] removed 0 variables, found 3 hbrs
c [lift-8] limit 10000000 with penalty 1 = 0 + 1
c [lift-8] using 6453 probes 14%
c [lift-8] 0 units, 18 impls, 3 eqs in 1 rounds
c [lift-8] 40183 variables remain 89% (4917 retained)
c [lift-8] removed 3 variables
c [cliff-7] limit of 18207216 steps penalty 1 = 0 + 1
c [cliff-7] failed 0, lifted 9
c [transred-6] limit 2146026 based on 2146026 irredundant clauses
c [transred-6] removed 6 transitive binary clauses
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 45091 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-12] incomplete 2404 not tried 5% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 4 = 0% variables out of 45091
c [elim-12] 4 < 1/1000 * 45091 = 45 considered unsuccessful
c [bca-8] limit of 10000000 steps
c [bca-8] 67979 out of 90176 literals actually usable 75%
c [bca-8] added 197 blocked clauses in 268227 steps
c [simplification-12] removed 17 variables 0.0% (45087 remain 33%)
c [simplification-12] removed 1332 irredundant clauses 0.1% (2144702 remain 51%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 125000
c [simplification-12] new conflict interval 250000
c [simplification-12] penalized conflict interval 500000 = 2 * 250000
c [simplification-12] new conflict limit 1075110
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  360.3   45087  2144701    598094   25505  11692 37424   0 65.9 527.5  106
c R  361.4   45087  2144701    605289   31633  11693 37447   0 66.0 527.0  112
c -  365.9   45087  2144690    627024   26140  11829 37506   1 64.5 522.9  106
c i  366.7   45086  2144689    631917   29470  11863 37518   1 64.1 522.3  107
c i  366.7   45085  2144689    631918   29470  11863 37518   1 64.1 522.3  107
c i  367.5   45084  2144687    633595   30904  11961 37571   0 64.0 522.6  108
c -  373.8   45084  2144635    654800   27148  12491 38040   1 63.7 521.2  105
c -  381.0   45084  2144595    687900   27905  12962 38307   1 63.5 518.1  105
c -  389.3   45084  2144582    718964   28706  13565 38552   1 63.4 517.3  105
c -  397.7   45084  2144580    757636   29431  13853 38836   1 63.5 515.7  105
c i  400.9   45083  2144577    770364   37696  13955 38898   0 63.3 515.7  110
c -  405.1   45081  2144572    789135   30466  14302 39159   1 63.1 514.2  105
c -  411.5   45081  2144568    819086   31226  14636 39422   2 63.0 510.7  105
c -  419.1   45081  2144564    850234   32012  14987 39796   1 62.7 508.5  105
c i  425.8   45080  2144563    890174   49225  15076 39894   1 63.9 506.5  126
c -  428.6   45080  2144562    899305   32777  15188 39954   0 63.9 506.2  105
c i  435.1   45079  2144550    929166   56044  15553 40238   0 63.2 501.8  121
c -  435.5   45079  2144550    930995   33521  15567 40240   0 63.2 501.6  105
c -  443.3   45079  2144492    963469   34697  16100 40688   2 62.8 499.3  106
c -  451.7   45079  2144475    997018   35247  16455 41048   1 62.2 496.6  106
c -  462.0   45079  2144474   1038091   36385  16813 41187   2 62.6 494.5  106
c i  469.5   45078  2144471   1070630   61055  17178 41549   0 62.0 492.5  121
c i  469.5   45069  2144471   1070631   61055  17178 41549   0 62.0 492.5  121
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  469.8   45066  2144471   1073588   37433  17186 41588   1 61.9 492.6  106
c i  470.2   45065  2144471   1075281   38756  17189 41617   0 61.8 492.6  109
c 
c [simplification-13] limit of 1083868 conflicts hit after 1083868 conflicts
c [ternres-9] limit 38281307 with penalty 1 = 0 + 1
c [ternres-9] 25 schedulable variables 0%
c [ternres-9] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-19] removed 22 variables
c [basicprobe-3] limit 38281307 penalty 1 = 0 + 1
c [basicprobe-3-0] 30801 probes remain 68% after last round
c [basicprobe-3-0] 85 units = 85 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 97 variables, found 14929 hbrs
c [bate-2] eliminated 10 asymmetric tautologies during probing
c [lift-9] limit 10000000 with penalty 1 = 0 + 1
c [lift-9] using 5553 probes 12%
c [lift-9] 30 units, 43 impls, 3 eqs in 1 rounds
c [lift-9] 39068 variables remain 87% (5859 retained)
c [lift-9] removed 41 variables
c [cliff-8] limit of 30625046 steps penalty 1 = 0 + 1
c [cliff-8] failed 4, lifted 312
c [transred-7] limit 2077046 based on 2077046 irredundant clauses
c [transred-7] removed 11 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 44610 variables 100%
c [block-7] limit of 382813077 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 398060 blocked clauses
c [bca-9] limit of 10000000 steps
c [bca-9] 60350 out of 87782 literals actually usable 69%
c [bca-9] added 1621 blocked clauses in 181603 steps
c [rephase-6] after 1083868 conflicts (new increment 640000, next 1723868)
c [flushphases] 0 phases reset
c [simplification-13] removed 1175 variables 2.6% (43890 remain 32%)
c [simplification-13] removed 565907 irredundant clauses 26.4% (1578564 remain 37%)
c [simplification-13] maximum reduction of 26% = max (3%, 26%)
c [simplification-13] large reduction 26% >= 5% limit
c [simplification-13] new conflict interval 10838 = min (1083868/100, 250000)
c [simplification-13] penalized conflict interval 21676 = 2 * 10838
c [simplification-13] new conflict limit 1105544
c [tabula-rasa-1] number clauses 1578564 drops below limit 2108229
c [flush-cache] 0 binary, 0 ternary, 27519 large
c [flushphases] 43890 phases reset fully
c [phase-3] phase bias: 670 positive 36%, 1189 negative 64%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] new conflict limit 1103868
c [tabula-rasa-1] new variable limit 10972 and clause limit 789282
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  490.2   43890  1578564   1088927    2076  12413 429406   0 61.7 491.2  100
c -  491.0   43890  1578562   1092991    2615  12486 429430   1 61.6 490.8   99
c -  491.8   43890  1578562   1097810    3180  12558 429458   1 61.5 490.0  100
c -  492.6   43890  1578562   1102874    3696  12585 429493   0 61.6 489.8  100
c 
c [simplification-14] limit of 1104106 conflicts hit after 1104107 conflicts
c [gauss-4] limit 1941203 penalty 3 = 3 + 0
c [gauss-4] extracted 3 xors of average arity 2.0
c [gauss-4] connected 6 occurrences of 6 variables (average 1.0)
c [gauss-4] limit 1941203 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 23 variables
c [cgrclsr-4] limit 970601 penalty 3 = 3 + 0
c [cgrclsr-4] 8475 schedulable variables 19%
c [cgrclsr-4] fully completed congruence closure
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 4343 probes 10%
c [lift-10] 0 units, 44 impls, 2 eqs in 1 rounds
c [lift-10] 36167 variables remain 82% (7698 retained)
c [lift-10] removed 2 variables
c [cliff-9] limit of 62118515 steps penalty 0 = 0 + 0
c [cliff-9] failed 0, lifted 10
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 43855 variables 100%
c [block-8] limit of 776481438 steps penalty 0 = 0 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 867 blocked clauses
c [block-8] 867 < 1/1000 * 1578510 = 1578 considered unsuccessful
c [cce-4] limit of 19412035 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 325
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 323
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 321
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 319
c [cce-4-1] eliminated 10 clauses out of 10 (100%) of length 317
c [cce-4-1] eliminated 12 clauses out of 12 (100%) of length 315
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 313
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 311
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 309
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 307
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 305
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 303
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 302
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 301
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 300
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 299
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 298
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 297
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 296
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 295
c [cce-4-1] eliminated 10 clauses out of 10 (100%) of length 294
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 293
c [cce-4-1] eliminated 12 clauses out of 12 (100%) of length 292
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 291
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 290
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 289
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 288
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 287
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 286
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 285
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 284
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 283
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 282
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 281
c [cce-4-1] eliminated 15 clauses out of 15 (100%) of length 280
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 279
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 278
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 277
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 276
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 275
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 274
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 273
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 272
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 271
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 270
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 269
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 268
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 267
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 266
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 265
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 264
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 263
c [cce-4-1] eliminated 15 clauses out of 15 (100%) of length 262
c [cce-4-1] eliminated 19 clauses out of 19 (100%) of length 261
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 260
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 259
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 258
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 257
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 256
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 255
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 254
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 253
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 252
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 251
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 250
c [cce-4-1] eliminated 12 clauses out of 12 (100%) of length 249
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 248
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 247
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 246
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 245
c [cce-4-1] eliminated 22 clauses out of 22 (100%) of length 244
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 243
c [cce-4-1] eliminated 24 clauses out of 24 (100%) of length 242
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 241
c [cce-4-1] eliminated 28 clauses out of 28 (100%) of length 240
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 239
c [cce-4-1] eliminated 28 clauses out of 28 (100%) of length 238
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 237
c [cce-4-1] eliminated 30 clauses out of 30 (100%) of length 236
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 235
c [cce-4-1] eliminated 32 clauses out of 32 (100%) of length 234
c [cce-4-1] eliminated 16 clauses out of 16 (100%) of length 233
c [cce-4-1] eliminated 35 clauses out of 35 (100%) of length 232
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 231
c [cce-4-1] eliminated 40 clauses out of 40 (100%) of length 230
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 229
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 228
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 226
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 225
c [cce-4-1] eliminated 18 clauses out of 18 (100%) of length 224
c [cce-4-1] eliminated 14 clauses out of 14 (100%) of length 223
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 222
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 221
c [cce-4-1] eliminated 8 clauses out of 8 (100%) of length 220
c [cce-4-1] eliminated 19 clauses out of 21 (90%) of length 219
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 218
c [cce-4-1] eliminated 20 clauses out of 22 (91%) of length 217
c [cce-4-1] eliminated 7 clauses out of 7 (100%) of length 216
c [cce-4-1] eliminated 20 clauses out of 22 (91%) of length 215
c [cce-4-1] eliminated 11 clauses out of 13 (85%) of length 214
c [cce-4-1] eliminated 28 clauses out of 30 (93%) of length 213
c [cce-4-1] eliminated 3 clauses out of 22 (14%) of length 212
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 1544 large clauses in 19412036 steps
c [cce-4-1] allowing another 9706018 steps for small clauses
c [cce-4] scheduling 1457426 clauses = 1446241 binary + 11185 ternary
c [cce-4] tried to eliminate 59 small clauses 0%
c [cce-4] eliminated 54 small clauses 0%
c [cce-4] eliminated 54 binary clauses 0%
c [cce-4-1] eliminated 54 small clauses in 19412036 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 1598 covered clauses in round 1
c [cce-4] eliminated 1598 covered clauses in TOTAL during 1 rounds
c [elim-13] 2240 variables 5% will be scheduled this time
c [elim-13] scheduled 2240 variables 5%
c [elim-13] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-13] incomplete 1600 not tried 4% in round 1
c [elim-13] transition to [ all 0 rem 1 ] state
c [elim-13] eliminated 718 = 2% variables out of 43060
c [bca-10] limit of 10000000 steps
c [bca-10] 75445 out of 84686 literals actually usable 89%
c [bca-10] added 9587 blocked clauses in 246856 steps
c [rephase-7] after 1104107 conflicts (new increment 20000, next 1124107)
c [flushphases] 62 phases reset
c [phase-4] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-14] removed 1548 variables 3.5% (42342 remain 31%)
c [simplification-14] removed 5551 irredundant clauses 0.4% (1573009 remain 37%)
c [simplification-14] maximum reduction of 4% = max (4%, 0%)
c [simplification-14] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-14] new conflict interval 24000
c [simplification-14] penalized conflict interval 48000 = 2 * 24000
c [simplification-14] new conflict limit 1152107
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  519.2   42342  1573009   1108904    4311  12387 375628   1 61.5 489.5   96
c -  520.5   42342  1573009   1114911    4880  12441 375656   1 61.4 489.0   96
c -  522.0   42342  1573004   1121465    5492  12505 375676   1 61.3 488.6   96
c -  523.3   42342  1573004   1128848    6193  12543 375715   2 61.3 488.1   96
c -  524.6   42342  1573004   1139847    6817  12548 375730   1 62.1 488.0   96
c 
c [simplification-15] limit of 1152383 conflicts hit after 1152383 conflicts
c [ternres-10] limit 40020471 with penalty 1 = 1 + 0
c [ternres-10] all 42342 free variables schedulable
c [ternres-10] 308 ternary resolvents (1 bin, 307 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 2501279 penalty 4 = 4 + 0
c [card-5] found 1114 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2501279 for elimination
c [card-5] 1114 out of 1114 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 2146 probes 5%
c [lift-11] 1 units, 37 impls, 7 eqs in 1 rounds
c [lift-11] 32867 variables remain 78% (9467 retained)
c [lift-11] removed 8 variables
c [cliff-10] limit of 64032753 steps penalty 0 = 0 + 0
c [cliff-10] failed 0, lifted 46
c [unhide-5] limit 1000511 with penalty 4 = 4 + 0
c [unhide-5-5] 0 units, 0 failed, 16383 tauts, 0 hbrs, 142366 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 14 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 42288 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] incomplete 1648 not tried 4% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 6413 = 15% variables out of 42288
c [bca-11] limit of 10000000 steps
c [bca-11] 57666 out of 71752 literals actually usable 80%
c [bca-11] added 464 blocked clauses in 220597 steps
c [rephase-8] after 1152383 conflicts (new increment 40000, next 1192383)
c [flushphases] 10 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-15] removed 6467 variables 15.3% (35875 remain 26%)
c [simplification-15] removed 27157 irredundant clauses 1.7% (1545847 remain 37%)
c [simplification-15] maximum reduction of 15% = max (15%, 2%)
c [simplification-15] large reduction 15% >= 5% limit
c [simplification-15] new conflict interval 11523 = min (1152383/100, 24000)
c [simplification-15] penalized conflict interval 23046 = 2 * 11523
c [simplification-15] new conflict limit 1175429
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  548.9   35875  1545847   1158131    7503  12542 48769   1 63.3 487.5   87
c 
c [simplification-16] limit of 1175455 conflicts hit after 1175457 conflicts
c [ternres-11] limit 80725500 with penalty 0 = 0 + 0
c [ternres-11] all 35875 free variables schedulable
c [ternres-11] 164 ternary resolvents (0 bin, 164 trn)
c [ternres-11] fully completed ternary resolution
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 137 probes 0%
c [lift-12-1] found 0 units 5 impls in round 1
c [lift-12-2] found 0 units 3 impls in round 2
c [lift-12-3] found 0 units 1 impls in round 3
c [lift-12-4] found 0 units 0 impls in round 4
c [lift-12-5] found 0 units 1 impls in round 5
c [lift-12] 0 units, 10 impls, 1 eqs in 6 rounds
c [lift-12] 26588 variables remain 74% (9286 retained)
c [lift-12] removed 1 variables
c [cliff-11] limit of 64580400 steps penalty 0 = 0 + 0
c [cliff-11] failed 0, lifted 0
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 3 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 35874 variables 100%
c [block-9] limit of 400000000 steps penalty 1 = 1 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 1236 blocked clauses
c [block-9] 1236 < 1/1000 * 1545847 = 1545 considered unsuccessful
c [cce-5] limit of 40362750 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 279
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 277
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 275
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 273
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 271
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 269
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 267
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 265
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 263
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 261
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 259
c [cce-5-1] eliminated 8 clauses out of 8 (100%) of length 257
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 255
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 254
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 253
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 252
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 251
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 250
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 249
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 248
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 247
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 246
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 245
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 244
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 243
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 242
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 241
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 240
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 239
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 238
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 237
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 236
c [cce-5-1] eliminated 12 clauses out of 12 (100%) of length 235
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 234
c [cce-5-1] eliminated 14 clauses out of 14 (100%) of length 233
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 232
c [cce-5-1] eliminated 13 clauses out of 13 (100%) of length 231
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 230
c [cce-5-1] eliminated 12 clauses out of 12 (100%) of length 229
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 228
c [cce-5-1] eliminated 12 clauses out of 12 (100%) of length 227
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 226
c [cce-5-1] eliminated 13 clauses out of 13 (100%) of length 225
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 224
c [cce-5-1] eliminated 14 clauses out of 14 (100%) of length 223
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 222
c [cce-5-1] eliminated 14 clauses out of 14 (100%) of length 221
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 220
c [cce-5-1] eliminated 13 clauses out of 15 (87%) of length 219
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 218
c [cce-5-1] eliminated 13 clauses out of 15 (87%) of length 217
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 216
c [cce-5-1] eliminated 17 clauses out of 19 (89%) of length 215
c [cce-5-1] eliminated 8 clauses out of 10 (80%) of length 214
c [cce-5-1] eliminated 20 clauses out of 22 (91%) of length 213
c [cce-5-1] eliminated 14 clauses out of 16 (88%) of length 212
c [cce-5-1] eliminated 25 clauses out of 27 (93%) of length 211
c [cce-5-1] eliminated 10 clauses out of 10 (100%) of length 210
c [cce-5-1] eliminated 15 clauses out of 15 (100%) of length 209
c [cce-5-1] eliminated 8 clauses out of 8 (100%) of length 208
c [cce-5-1] eliminated 13 clauses out of 13 (100%) of length 207
c [cce-5-1] eliminated 8 clauses out of 10 (80%) of length 206
c [cce-5-1] eliminated 14 clauses out of 14 (100%) of length 205
c [cce-5-1] eliminated 9 clauses out of 11 (82%) of length 204
c [cce-5-1] eliminated 13 clauses out of 13 (100%) of length 203
c [cce-5-1] eliminated 10 clauses out of 12 (83%) of length 202
c [cce-5-1] eliminated 15 clauses out of 17 (88%) of length 201
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 200
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 199
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 198
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 197
c [cce-5-1] eliminated 14 clauses out of 16 (88%) of length 196
c [cce-5-1] eliminated 12 clauses out of 16 (75%) of length 195
c [cce-5-1] eliminated 16 clauses out of 20 (80%) of length 194
c [cce-5-1] eliminated 14 clauses out of 16 (88%) of length 193
c [cce-5-1] eliminated 13 clauses out of 15 (87%) of length 192
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 191
c [cce-5-1] eliminated 13 clauses out of 13 (100%) of length 190
c [cce-5-1] eliminated 13 clauses out of 15 (87%) of length 189
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 188
c [cce-5-1] eliminated 14 clauses out of 14 (100%) of length 187
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 186
c [cce-5-1] eliminated 11 clauses out of 11 (100%) of length 185
c [cce-5-1] eliminated 12 clauses out of 14 (86%) of length 184
c [cce-5-1] eliminated 8 clauses out of 10 (80%) of length 183
c [cce-5-1] eliminated 9 clauses out of 11 (82%) of length 182
c [cce-5-1] eliminated 9 clauses out of 11 (82%) of length 181
c [cce-5-1] eliminated 11 clauses out of 13 (85%) of length 180
c [cce-5-1] eliminated 8 clauses out of 10 (80%) of length 179
c [cce-5-1] eliminated 13 clauses out of 19 (68%) of length 178
c [cce-5-1] eliminated 10 clauses out of 14 (71%) of length 177
c [cce-5-1] eliminated 14 clauses out of 16 (88%) of length 176
c [cce-5-1] eliminated 14 clauses out of 16 (88%) of length 175
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 855 large clauses in 40362751 steps
c [cce-5-1] allowing another 20181375 steps for small clauses
c [cce-5] scheduling 1433775 clauses = 1423063 binary + 10712 ternary
c [cce-5] tried to eliminate 221 small clauses 0%
c [cce-5] eliminated 39 small clauses 0%
c [cce-5] eliminated 37 binary clauses 0%
c [cce-5] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 39 small clauses in 40362751 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 894 covered clauses in round 1
c [cce-5] eliminated 894 covered clauses in TOTAL during 1 rounds
c [cce-5] 894 < 1/1000 * 1544611 = 1544 considered unsuccessful
c [elim-15] 1544 variables 4% will be scheduled this time
c [elim-15] scheduled 1544 variables 4%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] incomplete 1154 not tried 3% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 0 = 0% variables out of 35874
c [bca-12] limit of 10000000 steps
c [bca-12] 57816 out of 71750 literals actually usable 81%
c [bca-12] added 0 blocked clauses in 220513 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-16] removed 1 variables 0.0% (35874 remain 26%)
c [simplification-16] removed 2251 irredundant clauses 0.1% (1543596 remain 37%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 24000
c [simplification-16] new conflict interval 48000
c [simplification-16] penalized conflict interval 96000 = 2 * 48000
c [simplification-16] new conflict limit 1271457
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  573.5   35874  1543596   1175869    7923  12596 49930   1 64.5 487.1   87
c -  576.8   35874  1543596   1203867    8521  12597 49945   1 69.6 487.2   87
c -  581.3   35874  1543596   1248602    9003  12599 49960   1 72.5 485.7   87
c 
c [simplification-17] limit of 1271529 conflicts hit after 1271529 conflicts
c [ternres-12] limit 83614880 with penalty 0 = 0 + 0
c [ternres-12] all 35874 free variables schedulable
c [ternres-12] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-12] fully completed ternary resolution
c [simpleprobe-4] 30658 schedulable variables 85%
c [simpleprobe-4] limit 25000000 penalty 3 = 3 + 0
c [simpleprobe-4] 30141 variables remain 84% (5733 retained)
c [simpleprobe-4] removed 0 variables, found 4321 hbrs, 0 units
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 9181 probes 26%
c [lift-13] 0 units, 40 impls, 2 eqs in 1 rounds
c [lift-13] 33642 variables remain 94% (2230 retained)
c [lift-13] removed 2 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 4 transitive binary clauses
c [rephase-9] after 1271529 conflicts (new increment 80000, next 1351529)
c [flushphases] 10 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-17] removed 2 variables 0.0% (35872 remain 26%)
c [simplification-17] removed 6 irredundant clauses 0.0% (1543590 remain 37%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 48000
c [simplification-17] new conflict interval 96000
c [simplification-17] penalized conflict interval 192000 = 2 * 96000
c [simplification-17] new conflict limit 1463529
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  587.7   35872  1543590   1289039   14861  12558 54555   1 74.5 484.1  103
c -  588.7   35872  1543590   1293487    9527  12577 54593   1 74.4 483.7   87
c -  591.2   35872  1543589   1305535   10225  12692 54667   0 74.2 483.4   87
c -  593.4   35872  1543589   1319312   10872  12768 54741   2 73.9 482.6   87
c -  596.1   35872  1543585   1332397   11543  12926 54850   1 73.8 481.8   87
c -  598.4   35872  1543585   1345390   12249  12982 54906   1 73.6 481.8   87
c -  601.8   35872  1543575   1362163   12905  13104 54952   1 73.5 481.0   87
c -  604.4   35872  1543569   1377447   13520  13245 54987   1 73.2 480.3   87
c -  607.4   35872  1543567   1393381   14078  13355 55074   2 72.9 478.9   87
c -  609.7   35872  1543564   1409767   14813  13430 55125   2 72.9 478.8   87
c -  612.8   35872  1543560   1427739   15249  13539 55177   1 73.4 478.4   87
c -  615.9   35872  1543556   1445158   15913  13695 55220   1 73.0 477.1   87
c -  618.8   35872  1543553   1464770   16601  13803 55341   1 72.8 475.5   87
c 
c [simplification-18] limit of 1465167 conflicts hit after 1465168 conflicts
c [ternres-13] limit 93333312 with penalty 0 = 0 + 0
c [ternres-13] all 35872 free variables schedulable
c [ternres-13] 31 ternary resolvents (0 bin, 31 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-25] removed 2 variables
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 6996 probes 20%
c [lift-14] 0 units, 23 impls, 6 eqs in 1 rounds
c [lift-14] 31523 variables remain 88% (4341 retained)
c [lift-14] removed 6 variables
c [cliff-12] limit of 37333325 steps penalty 1 = 1 + 0
c [cliff-12] failed 0, lifted 0
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 3 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 35864 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] incomplete 1942 not tried 5% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 233 = 1% variables out of 35864
c [bca-13] limit of 10000000 steps
c [bca-13] 51154 out of 71264 literals actually usable 72%
c [bca-13] added 222 blocked clauses in 195717 steps
c [rephase-10] after 1465168 conflicts (new increment 160000, next 1625168)
c [flushphases] 10 phases reset
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-18] removed 241 variables 0.7% (35631 remain 26%)
c [simplification-18] removed 5883 irredundant clauses 0.4% (1537670 remain 36%)
c [simplification-18] maximum reduction of 1% = max (1%, 0%)
c [simplification-18] geometric conflict interval increment 48000 = 96000 / 2
c [simplification-18] new conflict interval 144000
c [simplification-18] penalized conflict interval 288000 = 2 * 144000
c [simplification-18] new conflict limit 1753168
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  634.5   35631  1537670   1484015   17235  13771 52271   1 72.5 474.7   88
c -  639.7   35631  1537669   1507831   18120  13884 52357   1 72.4 473.6   88
c -  644.4   35631  1537664   1529763   18818  14067 52452   1 72.1 472.4   88
c -  647.2   35631  1537661   1554306   19726  14173 52493   1 72.2 471.9   88
c -  651.5   35631  1537657   1581955   20351  14284 52595   1 73.0 471.3   88
c -  655.5   35631  1537656   1604791   21027  14456 52648   1 72.7 469.8   87
c -  660.3   35631  1537653   1632079   21771  14620 52712   1 72.4 468.5   87
c i  665.0   35630  1537653   1657008   37775  14761 52863   1 71.9 466.6   96
c -  665.6   35625  1537653   1661116   22731  14792 52907   0 71.9 466.7   88
c -  670.2   35625  1537653   1686331   23604  15034 53082   1 71.6 464.9   88
c -  675.8   35625  1537643   1720519   24213  15181 53208   1 71.5 463.4   88
c -  680.9   35625  1537639   1747823   25049  15424 53249   1 71.2 461.8   88
c 
c [simplification-19] limit of 1755346 conflicts hit after 1755346 conflicts
c [ternres-14] limit 107668734 with penalty 0 = 0 + 0
c [ternres-14] all 35625 free variables schedulable
c [ternres-14] 190 ternary resolvents (5 bin, 185 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1345859 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-5] limit 766389 based on 1532779 irredundant clauses
c [cgrclsr-5] all 35625 free variables schedulable
c [cgrclsr-5] 10463 variables remain 29% (25162 retained)
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 4814 probes 14%
c [lift-15] 24 units, 59 impls, 2 eqs in 1 rounds
c [lift-15] 29320 variables remain 82% (6273 retained)
c [lift-15] removed 32 variables
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 7 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 35593 variables 100%
c [block-10] limit of 200000000 steps penalty 2 = 2 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 1205 blocked clauses
c [block-10] 1205 < 1/1000 * 1526222 = 1526 considered unsuccessful
c [cce-6] limit of 26917183 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 216
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 215
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 214
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 213
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 212
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 211
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 206
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 205
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 204
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 202
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 201
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 200
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 199
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 198
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 195
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 194
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 193
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 192
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 191
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 171
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 170
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 169
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 157
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 44 large clauses in 26917184 steps
c [cce-6-1] allowing another 13458592 steps for small clauses
c [cce-6] scheduling 1420842 clauses = 1410760 binary + 10082 ternary
c [cce-6] tried to eliminate 194 small clauses 0%
c [cce-6] eliminated 3 small clauses 0%
c [cce-6] eliminated 3 binary clauses 0%
c [cce-6-1] eliminated 3 small clauses in 26917184 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 47 covered clauses in round 1
c [cce-6] eliminated 47 covered clauses in TOTAL during 1 rounds
c [cce-6] 47 < 1/1000 * 1525017 = 1525 considered unsuccessful
c [elim-17] 1142 variables 3% will be scheduled this time
c [elim-17] scheduled 1142 variables 3%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] incomplete 960 not tried 3% in round 1
c [elim-17] transition to [ all 0 rem 1 ] state
c [elim-17] eliminated 0 = 0% variables out of 35475
c [bca-14] limit of 10000000 steps
c [bca-14] 43772 out of 70952 literals actually usable 62%
c [bca-14] added 2283 blocked clauses in 177225 steps
c [rephase-11] after 1755346 conflicts (new increment 320000, next 2075346)
c [flushphases] 10 phases reset
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-19] removed 150 variables 0.4% (35475 remain 26%)
c [simplification-19] removed 12679 irredundant clauses 0.8% (1524960 remain 36%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 72000 = 144000 / 2
c [simplification-19] new conflict interval 216000
c [simplification-19] penalized conflict interval 432000 = 2 * 216000
c [simplification-19] new conflict limit 2187346
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  705.7   35475  1524958   1778673   24660  14028 56214   2 71.0 461.2   89
c i  711.6   35474  1524958   1809798   45998  14207 56330   0 70.4 458.9   99
c -  711.6   35470  1524958   1809882   25540  14214 56355   1 70.4 458.9   89
c -  717.0   35470  1524956   1848779   26186  14305 56415   1 70.8 458.1   89
c -  723.6   35470  1524954   1902883   26925  14344 56480   2 71.3 456.3   89
c -  729.5   35470  1524954   1932633   27665  14508 56629   1 70.9 454.8   88
c -  734.9   35470  1524954   1961201   28331  14674 56720   0 70.7 453.8   88
c i  736.7   35469  1524950   1970756   36151  14728 56785   1 70.6 453.3   94
c i  738.9   35468  1524950   1982357   44890  14777 56842   1 70.3 452.6   99
c i  738.9   35437  1524950   1982358   44890  14777 56842   1 70.3 452.6   99
c -  741.3   35437  1524950   1992067   29148  14846 56909   0 70.2 452.0   88
c -  746.5   35437  1524949   2026313   29936  14938 57028   1 70.1 450.9   88
c i  750.5   35436  1524949   2050516   47905  15100 57096   0 69.7 449.2   97
c i  750.5   35429  1524949   2050846   48092  15100 57114   1 69.7 449.1   97
c i  750.5   35428  1524949   2050852   48095  15100 57114   1 69.7 449.1   97
c i  751.4   35427  1524949   2054498   51092  15122 57141   1 69.6 449.0   98
c -  752.6   35426  1524949   2059176   30884  15144 57194   1 69.6 448.7   88
c i  759.0   35425  1524949   2092556   55843  15361 57382   1 69.3 447.1  108
c -  759.1   35423  1524949   2093185   31849  15371 57407   1 69.3 447.1   88
c i  761.0   35422  1524949   2103131   39624  15401 57435   2 69.2 446.5   94
c -  765.3   35422  1524949   2127598   32686  15548 57549   0 68.9 445.1   88
c i  765.8   35421  1524949   2130115   34663  15575 57567   1 68.9 444.9   91
c i  765.8   35420  1524949   2130116   34663  15575 57567   1 68.9 444.9   91
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  769.5   35419  1524949   2159295   56061  15757 57598   1 68.3 443.5  100
c -  770.0   35415  1524949   2163853   33954  15878 57624   2 68.3 443.4   88
c i  771.7   35414  1524949   2177619   44541  15912 57651   1 68.2 443.1   97
c i  773.3   35413  1524949   2188880   52239  15961 57662   1 68.0 442.3  101
c i  773.3   34307  1524948   2188884   52242  15961 57662   1 68.0 442.3  101
c 
c [simplification-20] limit of 2190716 conflicts hit after 2190716 conflicts
c [ternres-15] limit 127974436 with penalty 0 = 0 + 0
c [ternres-15] all 34304 free variables schedulable
c [ternres-15] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-27] removed 3176 variables
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 2074 probes 6%
c [lift-16-1] found 113 units 159 impls in round 1
c [lift-16] 123 units, 193 impls, 136 eqs in 2 rounds
c [lift-16] 25640 variables remain 80% (6317 retained)
c [lift-16] removed 342 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 19 transitive binary clauses
c [bca-15] limit of 10000000 steps
c [bca-15] 46498 out of 63916 literals actually usable 73%
c [bca-15] added 1696 blocked clauses in 195599 steps
c [rephase-12] after 2190716 conflicts (new increment 640000, next 2830716)
c [flushphases] 10 phases reset
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-20] removed 2347 variables 6.8% (31957 remain 23%)
c [simplification-20] removed 201190 irredundant clauses 13.2% (1323758 remain 31%)
c [simplification-20] maximum reduction of 13% = max (7%, 13%)
c [simplification-20] large reduction 13% >= 5% limit
c [simplification-20] new conflict interval 21907 = min (2190716/100, 216000)
c [simplification-20] penalized conflict interval 43814 = 2 * 21907
c [simplification-20] new conflict limit 2234530
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  775.8   31956  1323758   2191103   17122    610 49972   1 68.0 442.1   82
c i  776.1   31955  1323758   2193129   18565    623 49978   0 68.0 442.0   82
c i  776.2   31954  1323758   2193395   18790    627 49978   0 68.0 441.9   82
c i  776.2   31953  1323758   2193396   18790    627 49978   0 68.0 441.9   82
c i  776.3   31952  1323758   2193664   19020    626 49980   0 68.0 441.9   82
c i  776.6   31951  1323758   2196115   20751    651 49988   0 67.9 441.7   82
c i  776.7   31950  1323758   2196929   21295    658 49995   0 67.9 441.6   82
c i  776.8   31949  1323758   2197159   21429    667 50001   0 67.9 441.6   82
c i  776.8   31948  1323758   2197160   21429    667 50001   0 67.9 441.6   82
c i  777.6   31947  1323754   2203583   26208    703 50038   0 67.8 441.3   82
c i  777.6   31946  1323754   2203584   26208    703 50038   0 67.8 441.3   82
c i  777.8   31945  1323754   2204872   27155    705 50048   0 67.8 441.2   83
c i  777.8   31944  1323754   2204873   27155    705 50048   0 67.8 441.2   83
c i  778.4   31943  1323752   2208065   29175    746 50076   0 67.8 440.9   87
c i  778.4   31526  1323752   2208376   29329    749 50082   0 67.7 440.9   87
c i  778.5   31525  1323752   2208527   29395    756 50085   0 67.7 440.9   87
c i  778.5   29686  1323752   2208529   29395    756 50085   0 67.7 440.9   87
c 0  778.5   29519  1323752   2208529   29395    756 50085   0 67.7 440.9   87
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 15 basic ate = 10 trn 67% + 5 lrg 33% in 2 updates
c bcas: 15 count, 27766 added (35290 skipped), 3669424 steps
c bkwd: tried 18342 clauses, 36555 lits, 1.99 lits/clause
c bkwd: checked 51114338 occs, 2786.74 occs/clause, 1398.29 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 136 large (0% self)
c blkd: 10 bces, 1578865 removed, 140377006 resolutions, 621552440 steps
c blkd: 43541 blocking literals 16%, 13871 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 0 am1, 14438556 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1462 subsumed
c card: 3790 at-most-one constraints found, average size 3.17
c card: 3790 at-most-one constraints used 100%, average size 3.17
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: 6 cces, 3072 eliminated, 3035 ate 99%, 37 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 5 count, 6235751 esteps, 11993442 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: 4543 extracted (4521 ands 100%, 0 xors 0%, 22 ites 0%)
c clff: 12 cliffs, 1603 lifted, 9 failed
c clff: 154812 decisions, 337416166 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 16729780 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 108 gcs, 0 rescored clauses, 1066 rescored vars
c dcps: 27 decompositions, 2560 equivalent 2%
c deco: 442093 decision-only clauses 22%, 59% reduction
c decs: 49899022 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 837752 flipped 1.679% (in 1105 phases)
c elms: 17 elims, 97392 eliminated 71%
c elms: 18 rounds, 1.1 rounds/bve
c elms: 48332 small 50%, 35189 large 36%
c elms: 48424 tried small, 48332 succeeded 100%, 92 failed 0%
c elms: 5264 subsumed, 205162 strengthened, 0 blocked
c elms: 28661370 copies, 66807056 resolutions, 982230 ipos
c elms: 235526455 subchks, 192419716 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 6 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16561048 steps, 8280524 extr 50%, 18 elim 0%
c glue: 67.7 orig avg, 60.8 real avg, 7.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 63284 = 10838 simple + 52247 trn 17% + 199 lrg 83%, 3905 sub 0%
c hght: 441 average, 6.51 height/glue
c ints: 58681 luby (16166738 steps), 0 inout (0 steps)
c lift: 16 phases, 119936 probed (40202 level1 34%, 79734 level2 66%)
c lift: 212 units, 177 equivalences, 623 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2027058 clauses, 121.3 length
c lrnd: 690776 uips 34%, 1084685 flips 54%
c mega: 0 count, 0 failed, 0 rounds
c mins: 245827250 learned lits, 30% minimized
c mins: 1548991 mins 76%, 13490 bin 1%, 22484 size 1%, 442093 deco 22%
c move: moved 2027058, 1548087 bin 76%, 3107 trn 0%, 0 lrg 0%
c otfs: str 1126898 dyn (1106559 red, 20339 irr) 181471 drv 16%, 945427 rst 84%
c otfs: sub 5330 dyn (4458 red, 872 irr)
c phas: 10 computed, 80095 set, 8543 pos (11%), 71552 neg (89%)
c prbs: 3 basic, 22545 probed, 127 failed, 0 lifted
c prbs: 4 simple, 146978 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 18 probed, 0 failed, 0 lifted
c prps: 2848507605 props, 53 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c psns: 55586460 searches, 4169683 hits, 8% 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: 97 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 97 arith 100%, 0 double 0%
c rmbd: 2960 removed, 2473 red 84%
c rphs: 12 recomputed phases
c rsts: 53525 restarts 91%, 5156 skipped 9%
c rsts: 0 saturating 0%, 0 agile 0%, 5156 reuse 100%
c rsts: 39.2 avg interval, 39.2 scaled, 1.0 factor
c rsts: 46570 kept 87.0% average 23.0%
c simp: 20 count (20 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2027058 count (4867253 tried 2.4), 511321 sub out of 1991748 (25.7%)
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: 7329 fixed 5%, 53 its, 41670.36 confs/it
c trvs: 20066736652 traversals, 97% srch, 4% simp, 0% lkhd
c trvs: 7.3 search traversals per propagation, 8818.8 per conflict
c trvs: 1.5 search traversals per search visit
c trds: 14 transitive reductions, 87 removed, 0 failed
c trds: 2124 nodes, 49104 edges, 31818781 steps
c trim: 29723439 words, 113.4 MB
c trnr: 15 count, 10 bin, 6335 trn, 232338617 steps
c unhd: 5 count, 5 rounds, 23335679 steps
c unhd: 106 non-trivial sccs of average size 2.1
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: 26467 tauts, 1546 bin 6%, 58 trn 0%, 249 lrg 1%
c unhd: 26467 tauts, 24614 stamp 93%, 3072 red 12%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 267079 str, 0 bin 0%, 523 trn 0%, 266556 lrg 100%, 216978 red 81%
c vars: 29519 remaining 22% and 107281 removed 78% out of 136800
c vars: 7329 fixed 5%, 97392 eliminated 71%, 2560 equivalent 2%
c vsts: 13460442226 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 4.8 search visits per propagation, 5827.5 per conflict
c wchs: 1374371120 pushed, 111439449 enlarged, 176 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   1991748 100   1345277 100  48376268 100  22756155 100   2163274 100
c 
c  0      25846   1         0   0  15009808  31   3654300  16     64852   3 
c  1      20513   1         0   0   8104147  17   2290903  10     54757   3 
c  2      78118   4     25628   2  12481077  26<  4939335  22    198696   9 
c  3     131259   7    115573   9   4021409   8   2360528  10    172435   8 
c  4     157382   8    134431  10   2293402   5   1669474   7<   152491   7 
c  5     159714   8    137564  10   1485846   3   1272832   6    168639   8 
c  6     184854   9    152842  11   1140585   2   1368470   6    329268  15<
c  7     223050  11<   179969  13<   834483   2   1179006   5    288743  13 
c  8     238393  12    201946  15    709791   1   1007095   4    230925  11 
c  9     243159  12    175861  13   1107918   2   1276463   6    221277  10 
c 10     382629  19    178811  13    967466   2   1390311   6    243495  11 
c 11     117556   6     36615   3    185413   0    290945   1     34813   2 
c 12      29006   1      5912   0     34524   0     55965   0      2854   0 
c 13        269   0       125   0       399   0       528   0        29   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             7.1           6.9           2.1           3.8           6.1
c std             2.8           2.4           2.5           3.2           2.8
c 
c  119.848  15% elim
c   98.765  13% block
c   74.106  10% analysis
c   64.110   8% decide
c   21.947   3% gc
c   20.268   3% cce
c   18.152   2% restart
c   16.033   2% decomp
c   14.191   2% lift
c   13.913   2% probe
c   11.537   1% bump
c    9.542   1% cliff
c    9.271   1% defrag
c    6.027   1% card
c    5.636   1% bca
c    5.054   1% unhide
c    4.807   1% cgrclsr
c    4.253   1% mincls
c    2.361   0% gauss
c    1.884   0% reduce
c    1.877   0% phase
c    1.365   0% backward
c    0.888   0% ternres
c    0.822   0% transred
c    0.192   0% tabularasa
c    0.068   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    5.511   1% probe simple     40%
c    2.825   0% probe basic      20%
c    5.577   1% probe tree-look  40%
c ==================================
c   12.897   2% preprocessing     4%
c  306.755  39% inprocessing     96%
c ==================================
c  319.652  41% simplifying
c  458.810  59% search
c ==================================
c  778.466 100% all
c 
c 49899022 decisions, 64099.2 decisions/sec
c 2208529 conflicts, 2837.0 conflicts/sec
c 2848507605 propagations, 3.7 megaprops/sec
c 778.5 seconds, 233.2 MB
c launch: done
