c launch: /data/cnf/sc2014/app/aaai10-planning-ipc5-pathways-17-step21.cnf.bz2
c host: atom27
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/aaai10-planning-ipc5-pathways-17-step21.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/aaai10-planning-ipc5-pathways-17-step21.cnf.bz2
c no embedded options
c found 'p cnf 53919 308235' header
c read 53919 variables, 308235 clauses, 690466 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 53505 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   53505   307816         0       0      0     0   0  0.0   0.0   13
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 10817 at-most-one constraints of average size 3.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 10817 out of 10817 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 3318 variables
c [simpleprobe-1] all 50601 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 1210 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1210 variables, found 90200 hbrs, 21 units
c [unhide-1] limit 147776 based on 295552 irredundant clauses
c [unhide-1-1] 0 units, 26 failed, 32947 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 48694 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] eliminated 13460 variables 28% in round 1 in 28833002 steps
c [elim-1-1] backward subsumption/strengthening limit 57666004
c [elim-1-1] subsumed 114 and strengthened 661 clauses in 8931122 steps
c [elim-1-1] rescheduled 367 variables 1% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 93637 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 13460 = 28% variables out of 48694
c [phase-1] phase bias: 2510 positive 7%, 32724 negative 93%
c [simplification-1] removed 16863 variables 32.4% (35234 remain 66%)
c [simplification-1] removed 56496 irredundant clauses 18.4% (251320 remain 82%)
c [simplification-1] maximum reduction of 32% = max (32%, 18%)
c [simplification-1] large reduction 32% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] new conflict limit 1000
c [cut-width] 101379, max 173470, min4 66167 at 25%, min10 24701 at 10%
c [cut-width] cut-width based bias -1
c [decision-order] bias -1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.4   35234   251320         5       5      0 10624  20  7.8  57.0   11
c R    2.4   35234   251320        25      12      1 10625   8  6.9  40.9   11
c R    2.4   35234   251320        67      49      3 10626   4  5.8  46.7   11
c i    2.4   35233   251320       140     103     11 10633   3  6.8  60.6   11
c R    2.4   35232   251320       172     133     12 10633   2  7.5  69.3   11
c i    2.4   35231   251320       183     141     14 10633   2  7.3  70.4   11
c i    2.4   35228   251320       184     141     14 10633   2  7.3  69.9   11
c i    2.5   35220   251320       394     319     22 10643   1  7.2  69.9   11
c R    2.5   35219   251320       419     341     24 10643   2  7.2  71.2   11
c R    2.6   35219   251320      1002     860     40 10652   2 10.0  73.5   11
c 
c [simplification-2] limit of 1134 conflicts hit after 1134 conflicts
c [decomp-3] removed 31 variables
c [simpleprobe-2] all 35203 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 9 variables
c [simpleprobe-2] 2867 variables remain 8% (32327 retained)
c [simpleprobe-2] removed 9 variables, found 961 hbrs, 3 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 45253 literals 64%
c [treelook-1] scheduling used 300005 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 337427 steps
c [treelook-1] 45247 literals remain 64%
c [treelook-1] 34044 variables remain to probed next time 97%
c [treelook-1] removed 0 variables, found 1074 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 23079 probes remain 66% after last round
c [basicprobe-1-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 365 variables, found 3319 hbrs
c [unhide-2] limit 125531 based on 251063 irredundant clauses
c [unhide-2-2] 0 units, 17 failed, 465 tauts, 0 hbrs, 633 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 34813 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 17986 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 89 (4%) of length 61
c [cce-1-1] eliminated 2 clauses out of 16 (12%) of length 60
c [cce-1-1] eliminated 5 clauses out of 106 (5%) of length 59
c [cce-1-1] eliminated 1 clauses out of 18 (6%) of length 58
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 41
c [cce-1-1] eliminated 7 clauses out of 26 (27%) of length 20
c [cce-1-1] eliminated 9 clauses out of 37 (24%) of length 19
c [cce-1-1] eliminated 15 clauses out of 68 (22%) of length 18
c [cce-1-1] eliminated 16 clauses out of 78 (21%) of length 17
c [cce-1-1] eliminated 23 clauses out of 73 (32%) of length 16
c [cce-1-1] eliminated 23 clauses out of 179 (13%) of length 15
c [cce-1-1] eliminated 23 clauses out of 77 (30%) of length 14
c [cce-1-1] eliminated 20 clauses out of 88 (23%) of length 13
c [cce-1-1] eliminated 19 clauses out of 102 (19%) of length 12
c [cce-1-1] eliminated 23 clauses out of 104 (22%) of length 11
c [cce-1-1] eliminated 22 clauses out of 117 (19%) of length 10
c [cce-1-1] eliminated 21 clauses out of 103 (20%) of length 9
c [cce-1-1] eliminated 23 clauses out of 126 (18%) of length 8
c [cce-1-1] eliminated 29 clauses out of 185 (16%) of length 7
c [cce-1-1] eliminated 55 clauses out of 328 (17%) of length 6
c [cce-1-1] eliminated 154 clauses out of 2235 (7%) of length 5
c [cce-1-1] eliminated 864 clauses out of 5944 (15%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1359 large clauses in 11136181 steps
c [cce-1-1] allowing another 5568090 steps for small clauses
c [cce-1] scheduling 215820 clauses = 210576 binary + 5244 ternary
c [cce-1] tried to eliminate 22424 small clauses 10%
c [cce-1] eliminated 2838 small clauses 1%
c [cce-1] eliminated 2654 binary clauses 1%
c [cce-1] eliminated 184 ternary clauses 4%
c [cce-1-1] eliminated 2838 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4197 covered clauses in round 1
c [cce-1] eliminated 4197 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 33328 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 13726 not tried 41% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 4260 = 13% variables out of 33328
c [bca-1] limit of 10000000 steps
c [bca-1] 56418 out of 58138 literals actually usable 97%
c [bca-1] added 153715 blocked clauses in 558582 steps
c [phase-2] phase bias: 571 positive 94%, 38 negative 6%
c [simplification-2] removed 6151 variables 17.5% (29068 remain 54%)
c [simplification-2] removed 44961 irredundant clauses 17.9% (206359 remain 67%)
c [simplification-2] maximum reduction of 18% = max (17%, 18%)
c [simplification-2] large reduction 18% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 3134
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   13.2   29067   206359      1559     896    508 169820   2  9.5  67.9   15
c R   13.3   29066   206359      2323    1572    528 169826   3 13.2  75.4   16
c i   13.4   29065   206359      2867    2062    549 169829   1 12.3  79.0   16
c 
c [simplification-3] limit of 3230 conflicts hit after 3232 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 29034 free variables schedulable
c [ternres-1] 985 ternary resolvents (0 bin, 985 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 8971 at-most-one constraints of average size 7.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 8971 out of 8971 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 33 xors of average arity 2.9
c [gauss-1] connected 97 occurrences of 80 variables (average 1.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 5 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 29029 free variables schedulable
c [cgrclsr-1] 28042 variables remain 97% (987 retained)
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 14502 probes 50%
c [lift-1] 1 units, 1 impls, 0 eqs in 1 rounds
c [lift-1] 28867 variables remain 100% (136 retained)
c [lift-1] removed 26 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 93, lifted 0
c [unhide-3] limit 102897 based on 205795 irredundant clauses
c [unhide-3-3] 0 units, 5 failed, 2543 tauts, 0 hbrs, 4573 literals
c [transred-1] limit 202795 based on 202795 irredundant clauses
c [transred-1] removed 32 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 28868 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 3430 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 5 clauses out of 5 (100%) of length 120
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 66
c [cce-2-1] eliminated 119 clauses out of 239 (50%) of length 61
c [cce-2-1] eliminated 46 clauses out of 180 (26%) of length 60
c [cce-2-1] eliminated 58 clauses out of 546 (11%) of length 59
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 229 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 183028 clauses = 180999 binary + 2029 ternary
c [cce-2] tried to eliminate 729 small clauses 0%
c [cce-2] eliminated 260 small clauses 0%
c [cce-2] eliminated 260 binary clauses 0%
c [cce-2-1] eliminated 260 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 489 covered clauses in round 1
c [cce-2] eliminated 489 covered clauses in TOTAL during 1 rounds
c [elim-3] 13515 variables 47% will be scheduled this time
c [elim-3] scheduled 13515 variables 47%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 2296 not tried 8% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 176 = 1% variables out of 28812
c [bca-2] limit of 10000000 steps
c [bca-2] 52299 out of 57274 literals actually usable 91%
c [bca-2] added 23347 blocked clauses in 470028 steps
c [phase-3] phase bias: 101 positive 78%, 29 negative 22%
c [simplification-3] removed 398 variables 1.4% (28636 remain 54%)
c [simplification-3] removed 7889 irredundant clauses 3.8% (198470 remain 64%)
c [simplification-3] maximum reduction of 4% = max (1%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] new conflict limit 7232
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   18.7   28635   198470      3391    2416   1603 194382   1 13.3  79.8   16
c i   18.7   28634   198470      3412    2433   1604 194382   1 13.3  79.6   16
c i   18.8   28633   198470      4164    3117   1624 194395   1 13.3  80.4   17
c R   19.0   28633   198470      5285    4081   1631 194402   2 15.9  83.0   17
c -   19.1   28633   198470      5876    2605   1647 194408   1 16.7  83.7   16
c i   19.1   28632   198470      5978    2701   1648 194408   1 16.6  83.2   16
c i   19.3   28631   198470      7010    3628   1668 194416   1 17.4  82.3   17
c 
c [simplification-4] limit of 7412 conflicts hit after 7414 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 28631 free variables schedulable
c [ternres-2] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-7] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 23915 literals 42%
c [treelook-2] scheduling used 150083 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 409827 steps
c [treelook-2] 23913 literals remain 42%
c [treelook-2] 21231 variables remain to probed next time 74%
c [treelook-2] removed 0 variables, found 592 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 14107 probes 49%
c [lift-2] 0 units, 2 impls, 0 eqs in 1 rounds
c [lift-2] 28402 variables remain 99% (228 retained)
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 12, lifted 0
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 7 failed, 18302 tauts, 0 hbrs, 6599 literals
c [transred-2] limit 276550 with penalty 0 = 0 + 0
c [transred-2] removed 39 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 28580 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 142 blocked clauses
c [block-3] 142 < 1/1000 * 197908 = 197 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 98
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 84
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 70
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 64
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 63
c [cce-3-1] eliminated 7 clauses out of 7 (100%) of length 62
c [cce-3-1] eliminated 56 clauses out of 161 (35%) of length 61
c [cce-3-1] eliminated 43 clauses out of 134 (32%) of length 60
c [cce-3-1] eliminated 119 clauses out of 534 (22%) of length 59
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 243 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 183896 clauses = 179812 binary + 4084 ternary
c [cce-3] tried to eliminate 549 small clauses 0%
c [cce-3] eliminated 267 small clauses 0%
c [cce-3] eliminated 264 binary clauses 0%
c [cce-3] eliminated 3 ternary clauses 0%
c [cce-3-1] eliminated 267 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 510 covered clauses in round 1
c [cce-3] eliminated 510 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 28568 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 4108 not tried 14% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 424 = 1% variables out of 28568
c [bca-3] limit of 10000000 steps
c [bca-3] 50764 out of 56290 literals actually usable 90%
c [bca-3] added 19540 blocked clauses in 452186 steps
c [phase-4] phase bias: 7 positive 41%, 10 negative 59%
c [simplification-4] removed 487 variables 1.7% (28144 remain 53%)
c [simplification-4] removed 3561 irredundant clauses 1.8% (194909 remain 63%)
c [simplification-4] maximum reduction of 2% = max (2%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 10666
c [simplification-4] penalized conflict interval 10666 = 1 * 10666
c [simplification-4] new conflict limit 18080
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   23.6   28143   194909      8034    4144   1583 194052   2 17.7  82.6   17
c i   23.7   28142   194909      8466    4530   1591 194068   2 17.7  81.9   17
c i   23.9   28121   194909      9034    5023   1597 194068   1 18.8  81.9   18
c i   23.9   28115   194909      9198    5175   1599 194070   2 18.8  82.0   18
c -   24.0   28115   194909      9926    3350   1614 194076   3 18.2  82.2   17
c R   24.2   28115   194909     11848    4957   1621 194077   4 21.8  85.1   18
c i   24.5   28114   194909     13445    6425   1644 194087   1 21.0  85.4   19
c -   24.6   28106   194909     14201    4080   1647 194091   1 21.1  85.2   17
c i   24.6   28105   194909     14297    4168   1650 194093   1 21.0  85.0   17
c i   24.7   28101   194909     14484    4334   1658 194096   2 20.9  84.7   17
c i   24.7   28100   194909     14612    4445   1663 194098   1 20.8  84.6   17
c i   24.7   28095   194909     14843    4645   1672 194103   1 20.6  84.3   17
c i   24.9   28089   194909     15669    5403   1680 194106   1 20.4  84.2   17
c 
c [simplification-5] limit of 18448 conflicts hit after 18449 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 28085 free variables schedulable
c [ternres-3] 23 ternary resolvents (1 bin, 22 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 29 xors of average arity 2.9
c [gauss-2] connected 84 occurrences of 70 variables (average 1.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 5 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 17682 probes remain 64% after last round
c [basicprobe-2-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 433 variables, found 2591 hbrs
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] 26703 schedulable variables 97%
c [cgrclsr-2] fully completed congruence closure
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 0
c [unhide-5] limit 143433 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 3 failed, 1641 tauts, 0 hbrs, 13862 literals
c [transred-3] limit 717168 with penalty 0 = 0 + 0
c [transred-3] removed 79 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-4-1] eliminated 32 clauses out of 124 (26%) of length 61
c [cce-4-1] eliminated 5 clauses out of 24 (21%) of length 59
c [cce-4-1] eliminated 5 clauses out of 95 (5%) of length 58
c [cce-4-1] eliminated 6 clauses out of 49 (12%) of length 57
c [cce-4-1] eliminated 84 clauses out of 381 (22%) of length 56
c [cce-4-1] eliminated 36 clauses out of 93 (39%) of length 55
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 51
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 50
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 49
c [cce-4-1] eliminated 1 clauses out of 8 (12%) of length 48
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 45
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 44
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 185 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 176395 clauses = 172444 binary + 3951 ternary
c [cce-4] tried to eliminate 501 small clauses 0%
c [cce-4] eliminated 253 small clauses 0%
c [cce-4] eliminated 248 binary clauses 0%
c [cce-4] eliminated 5 ternary clauses 0%
c [cce-4-1] eliminated 259 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 444 covered clauses in round 1
c [cce-4] eliminated 444 covered clauses in TOTAL during 1 rounds
c [elim-5] 1850 variables 7% will be scheduled this time
c [elim-5] scheduled 1850 variables 7%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 45 variables 0% in round 1 in 15559213 steps
c [elim-5-1] backward subsumption/strengthening limit 4440787
c [elim-5-1] subsumed 2 and strengthened 7 clauses in 4440794 steps
c [elim-5] incomplete 29 not tried 0% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 45 = 0% variables out of 27646
c [bca-4] limit of 10000000 steps
c [bca-4] 47402 out of 55204 literals actually usable 86%
c [bca-4] added 2502 blocked clauses in 383035 steps
c [rephase-1] after 18449 conflicts (new increment 20000, next 38449)
c [flushphases] 3804 phases reset
c [phase-5] phase bias: 37 positive 43%, 49 negative 57%
c [simplification-5] removed 484 variables 1.7% (27601 remain 52%)
c [simplification-5] removed 6943 irredundant clauses 3.6% (187966 remain 61%)
c [simplification-5] maximum reduction of 4% = max (2%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 14666
c [simplification-5] penalized conflict interval 14666 = 1 * 14666
c [simplification-5] new conflict limit 33115
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   28.9   27601   187966     19618    4920   1753 177815   2 20.8  82.7   16
c R   29.7   27601   187966     26264    9665   1786 177832   4 27.1  82.7   19
c -   29.7   27601   187966     26285    5678   1786 177833   2 27.2  82.7   16
c i   29.8   27600   187966     26522    5887   1791 177845   1 27.1  82.4   17
c i   30.4   27599   187966     29742    8794   1823 177867   1 26.3  80.5   18
c -   30.9   27543   187966     32570    6616   1856 177880   2 26.6  80.0   16
c 
c [simplification-6] limit of 33307 conflicts hit after 33307 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 27543 free variables schedulable
c [ternres-4] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 4951 at-most-one constraints of average size 7.7
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 4951 out of 4951 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 59 variables
c [simpleprobe-3] 2338 schedulable variables 8%
c [simpleprobe-3] limit 5299755 penalty 0 = 0 + 0
c [decomp-11] removed 2 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 2 variables, found 10368 hbrs, 2 units
c [lift-3] limit 397481 with penalty 1 = 1 + 0
c [lift-3] using 13466 probes 49%
c [lift-3] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-3] 27218 variables remain 99% (322 retained)
c [unhide-6] limit 264987 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 0 failed, 18698 tauts, 0 hbrs, 6746 literals
c [transred-4] limit 1324938 with penalty 0 = 0 + 0
c [transred-4] removed 104 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 27540 variables 100%
c [block-4] limit of 25000000 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 112 blocked clauses
c [block-4] 112 < 1/1000 * 187243 = 187 considered unsuccessful
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 134
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 133
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 121
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 118
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 107
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 106
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 105
c [cce-5-1] eliminated 14 clauses out of 110 (13%) of length 61
c [cce-5-1] eliminated 2 clauses out of 87 (2%) of length 58
c [cce-5-1] eliminated 1 clauses out of 293 (0%) of length 56
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 41
c [cce-5-1] eliminated 2 clauses out of 14 (14%) of length 40
c [cce-5-1] eliminated 4 clauses out of 13 (31%) of length 39
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 29
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 28
c [cce-5-1] eliminated 4 clauses out of 12 (33%) of length 27
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 26
c [cce-5-1] eliminated 4 clauses out of 14 (29%) of length 25
c [cce-5-1] eliminated 21 clauses out of 24 (88%) of length 24
c [cce-5-1] eliminated 23 clauses out of 44 (52%) of length 22
c [cce-5-1] eliminated 4 clauses out of 13 (31%) of length 21
c [cce-5-1] eliminated 89 clauses out of 103 (86%) of length 20
c [cce-5-1] eliminated 91 clauses out of 111 (82%) of length 19
c [cce-5-1] eliminated 27 clauses out of 198 (14%) of length 18
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 317 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 173250 clauses = 171327 binary + 1923 ternary
c [cce-5] tried to eliminate 709 small clauses 0%
c [cce-5] eliminated 286 small clauses 0%
c [cce-5] eliminated 285 binary clauses 0%
c [cce-5] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 286 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 603 covered clauses in round 1
c [cce-5] eliminated 603 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 27403 variables 100%
c [elim-6] limit of 26498779 steps penalty 0 = 0 + 0
c [elim-6] incomplete 401 not tried 1% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 226 = 1% variables out of 27403
c [bca-5] limit of 10000000 steps
c [bca-5] 47251 out of 54356 literals actually usable 87%
c [bca-5] added 21861 blocked clauses in 412600 steps
c [phase-6] phase bias: 4 positive 20%, 16 negative 80%
c [simplification-6] removed 366 variables 1.3% (27177 remain 51%)
c [simplification-6] removed 3093 irredundant clauses 1.6% (184873 remain 60%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 21332
c [simplification-6] penalized conflict interval 21332 = 1 * 21332
c [simplification-6] new conflict limit 54639
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   35.4   27176   184873     34692    8305   1867 190130   2 26.3  79.5   18
c -   36.3   27176   184873     39833    7214   1897 190148   1 27.0  78.6   17
c i   36.8   27175   184873     41927    9108   1909 190153   2 26.8  78.3   18
c -   37.7   27175   184873     46933    8007   1949 190162   1 26.5  77.8   17
c i   37.8   27174   184873     47499    8527   1959 190164   1 26.4  77.7   17
c 
c [simplification-7] limit of 54809 conflicts hit after 54809 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 27174 free variables schedulable
c [ternres-5] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-12] removed 3 variables
c [cliff-4] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-4] failed 12, lifted 0
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 221 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 117
c [cce-6-1] eliminated 20 clauses out of 107 (19%) of length 61
c [cce-6-1] eliminated 2 clauses out of 23 (9%) of length 59
c [cce-6-1] eliminated 2 clauses out of 87 (2%) of length 58
c [cce-6-1] eliminated 7 clauses out of 309 (2%) of length 56
c [cce-6-1] eliminated 4 clauses out of 65 (6%) of length 55
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-6-1] eliminated 1 clauses out of 10 (10%) of length 40
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 38
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-6-1] eliminated 7 clauses out of 7 (100%) of length 34
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 31
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 28
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-6-1] eliminated 1 clauses out of 11 (9%) of length 21
c [cce-6-1] eliminated 1 clauses out of 20 (5%) of length 19
c [cce-6-1] eliminated 135 clauses out of 171 (79%) of length 18
c [cce-6-1] eliminated 5 clauses out of 22 (23%) of length 17
c [cce-6-1] eliminated 5 clauses out of 47 (11%) of length 16
c [cce-6-1] eliminated 7 clauses out of 85 (8%) of length 15
c [cce-6-1] eliminated 5 clauses out of 19 (26%) of length 14
c [cce-6-1] eliminated 3 clauses out of 128 (2%) of length 13
c [cce-6-1] eliminated 6 clauses out of 83 (7%) of length 12
c [cce-6-1] eliminated 7 clauses out of 93 (8%) of length 11
c [cce-6-1] eliminated 15 clauses out of 130 (12%) of length 10
c [cce-6-1] eliminated 6 clauses out of 86 (7%) of length 9
c [cce-6-1] eliminated 14 clauses out of 106 (13%) of length 8
c [cce-6-1] eliminated 40 clauses out of 266 (15%) of length 7
c [cce-6-1] eliminated 47 clauses out of 364 (13%) of length 6
c [cce-6-1] eliminated 496 clauses out of 1971 (25%) of length 5
c [cce-6-1] eliminated 777 clauses out of 4396 (18%) of length 4
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 1636 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 173980 clauses = 170076 binary + 3904 ternary
c [cce-6] tried to eliminate 941 small clauses 1%
c [cce-6] eliminated 410 small clauses 0%
c [cce-6] eliminated 399 binary clauses 0%
c [cce-6] eliminated 11 ternary clauses 0%
c [cce-6-1] eliminated 539 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 2175 covered clauses in round 1
c [cce-6] eliminated 2175 covered clauses in TOTAL during 1 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 27162 variables 100%
c [elim-7] limit of 44567536 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 1106 variables 4% in round 1 in 28454132 steps
c [elim-7-1] backward subsumption/strengthening limit 16113404
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 5807707 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1106 = 4% variables out of 27162
c [bca-6] limit of 10000000 steps
c [bca-6] 45278 out of 52114 literals actually usable 87%
c [bca-6] added 20294 blocked clauses in 434339 steps
c [rephase-2] after 54809 conflicts (new increment 40000, next 94809)
c [flushphases] 3302 phases reset
c [phase-7] phase bias: 8 positive 62%, 5 negative 38%
c [simplification-7] removed 1118 variables 4.1% (26056 remain 49%)
c [simplification-7] removed 7213 irredundant clauses 3.9% (177660 remain 58%)
c [simplification-7] maximum reduction of 4% = max (4%, 4%)
c [simplification-7] geometric conflict interval increment 4266 = 21332 / 5
c [simplification-7] new conflict interval 25598
c [simplification-7] penalized conflict interval 25598 = 1 * 25598
c [simplification-7] new conflict limit 80407
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   42.9   26056   177660     57737   11467   1677 207955   4 30.6  79.6   20
c i   43.2   26055   177660     58984   12545   1684 207956   1 30.7  79.2   21
c -   43.6   26055   177660     61240    8580   1716 207967   1 30.4  79.1   18
c i   43.6   26054   177660     61415    8738   1716 207968   1 30.4  79.0   18
c i   43.7   26053   177660     61609    8920   1717 207969   1 30.3  78.9   18
c i   43.8   25997   177660     63116   10289   1726 207973   1 29.9  79.2   19
c i   44.4   25884   177660     66006   12770   1754 207989   1 29.8  78.9   20
c -   45.1   25881   177660     70288    9393   1770 207998   1 30.0  78.7   18
c -   46.8   25881   177660     79270   10165   1832 208022   1 29.7  77.3   18
c 
c [simplification-8] limit of 80643 conflicts hit after 80643 conflicts
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 25881 free variables schedulable
c [ternres-6] 59 ternary resolvents (0 bin, 59 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 20 xors of average arity 2.9
c [gauss-3] connected 57 occurrences of 51 variables (average 1.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 5 variables
c [cgrclsr-3] limit 87823 based on 175646 irredundant clauses
c [cgrclsr-3] all 25876 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 1, lifted 0
c [unhide-7] limit 332654 with penalty 1 = 1 + 0
c [unhide-7-7] 0 units, 0 failed, 1661 tauts, 0 hbrs, 8257 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 188 transitive binary clauses
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 129
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 127
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 118
c [cce-7-1] eliminated 7 clauses out of 7 (100%) of length 117
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 116
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 113
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 85
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 73
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 72
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 71
c [cce-7-1] eliminated 15 clauses out of 99 (15%) of length 61
c [cce-7-1] eliminated 2 clauses out of 85 (2%) of length 58
c [cce-7-1] eliminated 1 clauses out of 44 (2%) of length 57
c [cce-7-1] eliminated 14 clauses out of 303 (5%) of length 56
c [cce-7-1] eliminated 3 clauses out of 61 (5%) of length 55
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 43
c [cce-7-1] eliminated 4 clauses out of 12 (33%) of length 42
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 41
c [cce-7-1] eliminated 7 clauses out of 17 (41%) of length 40
c [cce-7-1] eliminated 2 clauses out of 8 (25%) of length 39
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 29
c [cce-7-1] eliminated 1 clauses out of 9 (11%) of length 28
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 25
c [cce-7-1] eliminated 3 clauses out of 13 (23%) of length 24
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-7-1] eliminated 1 clauses out of 23 (4%) of length 22
c [cce-7-1] eliminated 4 clauses out of 19 (21%) of length 21
c [cce-7-1] eliminated 8 clauses out of 18 (44%) of length 20
c [cce-7-1] eliminated 2 clauses out of 16 (12%) of length 19
c [cce-7-1] eliminated 4 clauses out of 14 (29%) of length 18
c [cce-7-1] eliminated 8 clauses out of 41 (20%) of length 17
c [cce-7-1] eliminated 7 clauses out of 28 (25%) of length 16
c [cce-7-1] eliminated 13 clauses out of 112 (12%) of length 15
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 14
c [cce-7-1] eliminated 3 clauses out of 63 (5%) of length 13
c [cce-7-1] eliminated 5 clauses out of 126 (4%) of length 12
c [cce-7-1] eliminated 11 clauses out of 111 (10%) of length 11
c [cce-7-1] eliminated 17 clauses out of 144 (12%) of length 10
c [cce-7-1] eliminated 8 clauses out of 78 (10%) of length 9
c [cce-7-1] eliminated 14 clauses out of 112 (12%) of length 8
c [cce-7-1] eliminated 37 clauses out of 240 (15%) of length 7
c [cce-7-1] eliminated 83 clauses out of 465 (18%) of length 6
c [cce-7-1] eliminated 308 clauses out of 1416 (22%) of length 5
c [cce-7-1] eliminated 806 clauses out of 3489 (23%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1437 large clauses in 20313510 steps
c [cce-7-1] allowing another 10156755 steps for small clauses
c [cce-7] scheduling 165713 clauses = 162282 binary + 3431 ternary
c [cce-7] tried to eliminate 1314 small clauses 1%
c [cce-7] eliminated 679 small clauses 0%
c [cce-7] eliminated 666 binary clauses 0%
c [cce-7] eliminated 13 ternary clauses 0%
c [cce-7-1] eliminated 679 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 2116 covered clauses in round 1
c [cce-7] eliminated 2116 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 25837 variables 100%
c [elim-8] limit of 66530904 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 1783 variables 7% in round 1 in 29073142 steps
c [elim-8-1] backward subsumption/strengthening limit 37457762
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 5334981 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1783 = 7% variables out of 25837
c [bca-7] limit of 10000000 steps
c [bca-7] 41435 out of 48110 literals actually usable 86%
c [bca-7] added 38988 blocked clauses in 458102 steps
c [phase-8] phase bias: 118 positive 53%, 103 negative 47%
c [simplification-8] removed 1827 variables 7.1% (24054 remain 45%)
c [simplification-8] removed 14891 irredundant clauses 8.4% (162769 remain 53%)
c [simplification-8] maximum reduction of 8% = max (7%, 8%)
c [simplification-8] large reduction 8% >= 5% limit
c [simplification-8] new conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] new conflict limit 82643
c 
c [simplification-9] limit of 82647 conflicts hit after 82648 conflicts
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 24054 free variables schedulable
c [ternres-7] 53 ternary resolvents (0 bin, 53 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-3] limit 75000 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 16691 literals 35%
c [treelook-3] scheduling used 75205 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 75000 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 115428 steps
c [treelook-3] 16689 literals remain 35%
c [treelook-3] 15515 variables remain to probed next time 65%
c [treelook-3] removed 0 variables, found 26 hbrs
c [lift-4] limit 506866 with penalty 2 = 2 + 0
c [lift-4] using 11124 probes 46%
c [lift-4] 4 units, 6 impls, 0 eqs in 1 rounds
c [lift-4] 23645 variables remain 98% (405 retained)
c [lift-4] removed 4 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 3, lifted 0
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 208 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 24040 variables 100%
c [block-5] limit of 12500000 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 155
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 118
c [cce-8-1] eliminated 12 clauses out of 12 (100%) of length 116
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 114
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-8-1] eliminated 1 clauses out of 6 (17%) of length 70
c [cce-8-1] eliminated 16 clauses out of 85 (19%) of length 61
c [cce-8-1] eliminated 3 clauses out of 81 (4%) of length 58
c [cce-8-1] eliminated 2 clauses out of 47 (4%) of length 57
c [cce-8-1] eliminated 9 clauses out of 289 (3%) of length 56
c [cce-8-1] eliminated 3 clauses out of 58 (5%) of length 55
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 39
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 38
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-8-1] eliminated 1 clauses out of 7 (14%) of length 28
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-8-1] eliminated 7 clauses out of 17 (41%) of length 24
c [cce-8-1] eliminated 3 clauses out of 17 (18%) of length 22
c [cce-8-1] eliminated 7 clauses out of 20 (35%) of length 21
c [cce-8-1] eliminated 17 clauses out of 30 (57%) of length 20
c [cce-8-1] eliminated 69 clauses out of 82 (84%) of length 19
c [cce-8-1] eliminated 4 clauses out of 21 (19%) of length 18
c [cce-8-1] eliminated 4 clauses out of 36 (11%) of length 17
c [cce-8-1] eliminated 3 clauses out of 29 (10%) of length 16
c [cce-8-1] eliminated 3 clauses out of 79 (4%) of length 15
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 14
c [cce-8-1] eliminated 2 clauses out of 50 (4%) of length 13
c [cce-8-1] eliminated 5 clauses out of 103 (5%) of length 12
c [cce-8-1] eliminated 14 clauses out of 99 (14%) of length 11
c [cce-8-1] eliminated 17 clauses out of 125 (14%) of length 10
c [cce-8-1] eliminated 5 clauses out of 72 (7%) of length 9
c [cce-8-1] eliminated 14 clauses out of 120 (12%) of length 8
c [cce-8-1] eliminated 38 clauses out of 228 (17%) of length 7
c [cce-8-1] eliminated 92 clauses out of 415 (22%) of length 6
c [cce-8-1] eliminated 232 clauses out of 1111 (21%) of length 5
c [cce-8-1] eliminated 447 clauses out of 2651 (17%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 1053 large clauses in 20023556 steps
c [cce-8-1] allowing another 10011778 steps for small clauses
c [cce-8] scheduling 153695 clauses = 152199 binary + 1496 ternary
c [cce-8] tried to eliminate 1331 small clauses 1%
c [cce-8] eliminated 740 small clauses 0%
c [cce-8] eliminated 734 binary clauses 0%
c [cce-8] eliminated 6 ternary clauses 0%
c [cce-8-1] eliminated 740 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 1793 covered clauses in round 1
c [cce-8] eliminated 1793 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 24037 variables 100%
c [elim-9] limit of 67582226 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 975 variables 4% in round 1 in 30155401 steps
c [elim-9-1] backward subsumption/strengthening limit 37426825
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 5053309 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 975 = 4% variables out of 24037
c [bca-8] limit of 10000000 steps
c [bca-8] 39517 out of 46126 literals actually usable 86%
c [bca-8] added 29195 blocked clauses in 489849 steps
c [phase-9] phase bias: 10 positive 67%, 5 negative 33%
c [simplification-9] removed 992 variables 4.1% (23062 remain 43%)
c [simplification-9] removed 7226 irredundant clauses 4.4% (155543 remain 51%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 5119 = 25598 / 5
c [simplification-9] new conflict interval 30717
c [simplification-9] penalized conflict interval 30717 = 1 * 30717
c [simplification-9] new conflict limit 113365
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   56.2   23061   155543     84283   11611   1478 256421   1 30.3  78.6   20
c i   56.4   23002   155543     85409   12634   1483 256426   1 30.2  78.3   21
c i   56.4   22947   155543     85465   12688   1483 256426   1 30.2  78.3   21
c i   57.3   22946   155543     90854   17140   1515 256436   2 30.1  78.0   24
c -   57.6   22946   155543     92189   10758   1520 256439   1 30.2  77.8   19
c i   59.0   22945   155543    101875   19330   1564 256465   2 30.1  77.9   25
c -   59.0   22832   155543    102216   11655   1570 256467   2 30.1  78.1   19
c i   59.3   22831   155543    103838   13122   1586 256474   2 29.9  77.8   20
c -   60.5   22830   155543    112879   12496   1603 256481   2 29.7  77.7   19
c 
c [simplification-10] limit of 113603 conflicts hit after 113605 conflicts
c [ternres-8] limit 4499357 with penalty 0 = 0 + 0
c [ternres-8] all 22830 free variables schedulable
c [ternres-8] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 281209 penalty 3 = 3 + 0
c [card-4] found 1729 at-most-one constraints of average size 11.7
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 281209 for elimination
c [card-4] 1729 out of 1729 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-16] removed 233 variables
c [basicprobe-3] limit 4499357 penalty 0 = 0 + 0
c [basicprobe-3-0] 13310 probes remain 60% after last round
c [basicprobe-3-0] 17 units = 17 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 682 variables, found 3719 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 5, lifted 0
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 306 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 118
c [cce-9-1] eliminated 6 clauses out of 6 (100%) of length 115
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 83
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-9-1] eliminated 16 clauses out of 41 (39%) of length 61
c [cce-9-1] eliminated 11 clauses out of 66 (17%) of length 60
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 57
c [cce-9-1] eliminated 7 clauses out of 61 (11%) of length 55
c [cce-9-1] eliminated 1 clauses out of 43 (2%) of length 52
c [cce-9-1] eliminated 4 clauses out of 113 (4%) of length 51
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 40
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 24
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 23
c [cce-9-1] eliminated 2 clauses out of 12 (17%) of length 22
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-9-1] eliminated 4 clauses out of 12 (33%) of length 20
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-9-1] eliminated 4 clauses out of 28 (14%) of length 18
c [cce-9-1] eliminated 6 clauses out of 32 (19%) of length 17
c [cce-9-1] eliminated 7 clauses out of 24 (29%) of length 16
c [cce-9-1] eliminated 2 clauses out of 47 (4%) of length 15
c [cce-9-1] eliminated 7 clauses out of 33 (21%) of length 14
c [cce-9-1] eliminated 13 clauses out of 50 (26%) of length 13
c [cce-9-1] eliminated 18 clauses out of 63 (29%) of length 12
c [cce-9-1] eliminated 3 clauses out of 76 (4%) of length 11
c [cce-9-1] eliminated 11 clauses out of 97 (11%) of length 10
c [cce-9-1] eliminated 10 clauses out of 109 (9%) of length 9
c [cce-9-1] eliminated 16 clauses out of 84 (19%) of length 8
c [cce-9-1] eliminated 32 clauses out of 188 (17%) of length 7
c [cce-9-1] eliminated 73 clauses out of 365 (20%) of length 6
c [cce-9-1] eliminated 155 clauses out of 896 (17%) of length 5
c [cce-9-1] eliminated 331 clauses out of 2240 (15%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 754 large clauses in 14248890 steps
c [cce-9-1] allowing another 7124445 steps for small clauses
c [cce-9] scheduling 138922 clauses = 136353 binary + 2569 ternary
c [cce-9] tried to eliminate 1832 small clauses 1%
c [cce-9] eliminated 1004 small clauses 1%
c [cce-9] eliminated 989 binary clauses 1%
c [cce-9] eliminated 15 ternary clauses 1%
c [cce-9-1] eliminated 8500 small clauses in 30000001 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 9254 covered clauses in round 1
c [cce-9] eliminated 9254 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 22137 variables 100%
c [elim-10] limit of 89987145 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 923 variables 4% in round 1 in 22010075 steps
c [elim-10-1] backward subsumption/strengthening limit 44020150
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 4400580 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 923 = 4% variables out of 22137
c [bca-9] limit of 10000000 steps
c [bca-9] 36006 out of 42430 literals actually usable 85%
c [bca-9] added 6225 blocked clauses in 426690 steps
c [rephase-3] after 113605 conflicts (new increment 80000, next 193605)
c [flushphases] 2788 phases reset
c [phase-10] phase bias: 104 positive 75%, 35 negative 25%
c [simplification-10] removed 1616 variables 7.1% (21214 remain 40%)
c [simplification-10] removed 14984 irredundant clauses 9.6% (140559 remain 46%)
c [simplification-10] maximum reduction of 10% = max (7%, 10%)
c [simplification-10] large reduction 10% >= 5% limit
c [simplification-10] new conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] new conflict limit 115605
c [tabula-rasa-1] number clauses 140559 drops below limit 153908
c [flush-cache] 0 binary, 0 ternary, 11606 large
c [flushphases] 21214 phases reset fully
c [phase-11] phase bias: 494 positive 47%, 557 negative 53%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] conflict limit 20000 does not change
c [tabula-rasa-1] new variable limit 5303 and clause limit 70279
c 
c [simplification-11] limit of 115617 conflicts hit after 115619 conflicts
c [ternres-9] limit 4530542 with penalty 0 = 0 + 0
c [ternres-9] all 21214 free variables schedulable
c [ternres-9] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-9] fully completed ternary resolution
c [simpleprobe-4] all 21214 free variables schedulable
c [simpleprobe-4] limit 18122171 penalty 0 = 0 + 0
c [decomp-18] removed 5 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 5 variables, found 15297 hbrs, 5 units
c [lift-5] limit 1359162 with penalty 1 = 1 + 0
c [lift-5] using 9579 probes 45%
c [lift-5] 7 units, 12 impls, 0 eqs in 1 rounds
c [lift-5] 20440 variables remain 96% (746 retained)
c [lift-5] removed 23 variables
c [cliff-8] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-8] failed 0, lifted 0
c [unhide-8] limit 226527 with penalty 2 = 2 + 0
c [unhide-8-8] 0 units, 0 failed, 25778 tauts, 0 hbrs, 5264 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 266 transitive binary clauses
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 4 clauses out of 4 (100%) of length 114
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 112
c [cce-10-1] eliminated 17 clauses out of 44 (39%) of length 61
c [cce-10-1] eliminated 15 clauses out of 72 (21%) of length 60
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 57
c [cce-10-1] eliminated 3 clauses out of 234 (1%) of length 50
c [cce-10-1] eliminated 4 clauses out of 4 (100%) of length 30
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-10-1] eliminated 2 clauses out of 10 (20%) of length 23
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-10-1] eliminated 2 clauses out of 30 (7%) of length 18
c [cce-10-1] eliminated 1 clauses out of 41 (2%) of length 15
c [cce-10-1] eliminated 2 clauses out of 29 (7%) of length 14
c [cce-10-1] eliminated 3 clauses out of 36 (8%) of length 13
c [cce-10-1] eliminated 1 clauses out of 44 (2%) of length 12
c [cce-10-1] eliminated 9 clauses out of 81 (11%) of length 11
c [cce-10-1] eliminated 6 clauses out of 83 (7%) of length 10
c [cce-10-1] eliminated 12 clauses out of 111 (11%) of length 9
c [cce-10-1] eliminated 12 clauses out of 80 (15%) of length 8
c [cce-10-1] eliminated 25 clauses out of 185 (14%) of length 7
c [cce-10-1] eliminated 31 clauses out of 287 (11%) of length 6
c [cce-10-1] eliminated 116 clauses out of 762 (15%) of length 5
c [cce-10-1] eliminated 225 clauses out of 1874 (12%) of length 4
c [cce-10-1] completed large round (ACCE)
c [cce-10-1] eliminated 495 large clauses in 13369967 steps
c [cce-10-1] allowing another 6684983 steps for small clauses
c [cce-10] scheduling 133538 clauses = 132260 binary + 1278 ternary
c [cce-10] tried to eliminate 1975 small clauses 1%
c [cce-10] eliminated 969 small clauses 1%
c [cce-10] eliminated 961 binary clauses 1%
c [cce-10] eliminated 8 ternary clauses 1%
c [cce-10-1] eliminated 969 small clauses in 30000001 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 1464 covered clauses in round 1
c [cce-10] eliminated 1464 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 21186 variables 100%
c [elim-11] limit of 90610859 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 366 variables 2% in round 1 in 16910089 steps
c [elim-11-1] backward subsumption/strengthening limit 33820178
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 4232393 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 366 = 2% variables out of 21186
c [bca-10] limit of 10000000 steps
c [bca-10] 40706 out of 41642 literals actually usable 98%
c [bca-10] added 29890 blocked clauses in 443084 steps
c [rephase-4] after 115619 conflicts (new increment 20000, next 135619)
c [flushphases] 7272 phases reset
c [phase-12] phase bias: 27 positive 41%, 39 negative 59%
c [simplification-11] removed 394 variables 1.9% (20820 remain 39%)
c [simplification-11] removed 3146 irredundant clauses 2.2% (137413 remain 45%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-11] new conflict interval 26666
c [simplification-11] penalized conflict interval 26666 = 1 * 26666
c [simplification-11] new conflict limit 142285
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   68.1   20820   137413    119149    2287   1409 244905   3 29.4  78.0   15
c -   68.5   20820   137413    123083    2926   1417 244905   6 29.4  78.0   15
c R   68.7   20820   137413    125751    5074   1419 244905   2 29.4  77.9   17
c i   68.7   20819   137413    126119    5395   1427 244908   1 29.3  77.8   17
c -   68.9   20819   137413    127350    3515   1447 244925   1 29.2  77.6   15
c i   69.4   20818   137413    131552    7349   1487 244934   2 28.8  77.7   17
c -   69.6   20817   137413    132204    4393   1492 244940   2 28.8  77.6   15
c -   70.4   20817   137413    138024    5237   1538 244956   1 28.4  77.0   16
c 
c [simplification-12] limit of 142457 conflicts hit after 142457 conflicts
c [ternres-10] limit 5277563 with penalty 0 = 0 + 0
c [ternres-10] all 20817 free variables schedulable
c [ternres-10] 26 ternary resolvents (0 bin, 26 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] extracted 4 xors of average arity 2.8
c [gauss-4] connected 11 occurrences of 8 variables (average 1.4)
c [gauss-4] limit 250000 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 2 variables
c [cgrclsr-4] limit 68691 based on 137383 irredundant clauses
c [cgrclsr-4] all 20815 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-6] limit 3166538 with penalty 0 = 0 + 0
c [lift-6] using 8950 probes 43%
c [lift-6] 12 units, 14 impls, 0 eqs in 1 rounds
c [lift-6] 19310 variables remain 93% (1493 retained)
c [lift-6] removed 12 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 277 transitive binary clauses
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 3 clauses out of 3 (100%) of length 113
c [cce-11-1] eliminated 10 clauses out of 38 (26%) of length 61
c [cce-11-1] eliminated 5 clauses out of 66 (8%) of length 60
c [cce-11-1] eliminated 1 clauses out of 231 (0%) of length 50
c [cce-11-1] eliminated 2 clauses out of 6 (33%) of length 20
c [cce-11-1] eliminated 2 clauses out of 30 (7%) of length 18
c [cce-11-1] eliminated 2 clauses out of 17 (12%) of length 16
c [cce-11-1] eliminated 1 clauses out of 39 (3%) of length 15
c [cce-11-1] eliminated 1 clauses out of 27 (4%) of length 14
c [cce-11-1] eliminated 1 clauses out of 35 (3%) of length 13
c [cce-11-1] eliminated 5 clauses out of 40 (12%) of length 12
c [cce-11-1] eliminated 9 clauses out of 71 (13%) of length 11
c [cce-11-1] eliminated 3 clauses out of 70 (4%) of length 10
c [cce-11-1] eliminated 1 clauses out of 102 (1%) of length 9
c [cce-11-1] eliminated 6 clauses out of 68 (9%) of length 8
c [cce-11-1] eliminated 23 clauses out of 152 (15%) of length 7
c [cce-11-1] eliminated 36 clauses out of 283 (13%) of length 6
c [cce-11-1] eliminated 55 clauses out of 632 (9%) of length 5
c [cce-11-1] eliminated 125 clauses out of 1657 (8%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 291 large clauses in 12695202 steps
c [cce-11-1] allowing another 6347601 steps for small clauses
c [cce-11] scheduling 132128 clauses = 129927 binary + 2201 ternary
c [cce-11] tried to eliminate 1881 small clauses 1%
c [cce-11] eliminated 1034 small clauses 1%
c [cce-11] eliminated 1014 binary clauses 1%
c [cce-11] eliminated 20 ternary clauses 1%
c [cce-11-1] eliminated 1034 small clauses in 30000001 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 1325 covered clauses in round 1
c [cce-11] eliminated 1325 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 20803 variables 100%
c [elim-12] limit of 105551268 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 362 variables 2% in round 1 in 15896914 steps
c [elim-12-1] backward subsumption/strengthening limit 31793828
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 4137966 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 362 = 2% variables out of 20803
c [bca-11] limit of 10000000 steps
c [bca-11] 34883 out of 40884 literals actually usable 85%
c [bca-11] added 1315 blocked clauses in 423925 steps
c [rephase-5] after 142457 conflicts (new increment 40000, next 182457)
c [flushphases] 3593 phases reset
c [phase-13] phase bias: 4 positive 40%, 6 negative 60%
c [simplification-12] removed 376 variables 1.8% (20441 remain 38%)
c [simplification-12] removed 2640 irredundant clauses 1.9% (134773 remain 44%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-12] new conflict interval 35554
c [simplification-12] penalized conflict interval 35554 = 1 * 35554
c [simplification-12] new conflict limit 178011
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   74.2   20441   134773    144732    6047   1498 244979   2 28.1  76.4   16
c -   74.9   20441   134773    151272    6815   1523 244997   9 27.9  76.4   16
c i   74.9   20440   134773    152087    7579   1526 244998   4 27.9  76.5   16
c -   75.9   20384   134773    158318    7565   1566 245014   2 27.9  76.3   16
c i   76.3   20383   134773    161077    9939   1582 245017   2 27.9  76.2   17
c i   76.7   20382   134773    164774   13333   1598 245018   2 27.7  76.1   19
c -   76.9   20374   134773    165930    8325   1603 245020   2 27.7  76.0   16
c i   76.9   20373   134773    165977    8366   1603 245022   2 27.7  76.0   16
c i   77.6   20372   134773    170545   12425   1625 245035   1 27.5  75.7   19
c -   78.1   20372   134773    174187    9255   1643 245041   4 27.4  75.5   16
c 
c [simplification-13] limit of 178259 conflicts hit after 178260 conflicts
c [ternres-11] limit 6414123 with penalty 0 = 0 + 0
c [ternres-11] all 20372 free variables schedulable
c [ternres-11] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-20] removed 70 variables
c [lift-7] limit 3848473 with penalty 0 = 0 + 0
c [lift-7] using 7950 probes 39%
c [lift-7] 15 units, 18 impls, 0 eqs in 1 rounds
c [lift-7] 17971 variables remain 88% (2385 retained)
c [lift-7] removed 15 variables
c [cliff-9] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-9] failed 39, lifted 0
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 292 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 20281 variables 100%
c [block-6] limit of 8017653 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 1 blocked clauses
c [block-6] 1 < 1/1000 * 133856 = 133 considered unsuccessful
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 5 clauses out of 5 (100%) of length 112
c [cce-12-1] eliminated 16 clauses out of 39 (41%) of length 61
c [cce-12-1] eliminated 6 clauses out of 41 (15%) of length 60
c [cce-12-1] eliminated 1 clauses out of 60 (2%) of length 55
c [cce-12-1] eliminated 1 clauses out of 230 (0%) of length 50
c [cce-12-1] eliminated 3 clauses out of 4 (75%) of length 48
c [cce-12-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-12-1] eliminated 1 clauses out of 29 (3%) of length 18
c [cce-12-1] eliminated 2 clauses out of 23 (9%) of length 17
c [cce-12-1] eliminated 3 clauses out of 40 (8%) of length 15
c [cce-12-1] eliminated 3 clauses out of 40 (8%) of length 13
c [cce-12-1] eliminated 2 clauses out of 34 (6%) of length 12
c [cce-12-1] eliminated 10 clauses out of 79 (13%) of length 11
c [cce-12-1] eliminated 3 clauses out of 59 (5%) of length 10
c [cce-12-1] eliminated 1 clauses out of 107 (1%) of length 9
c [cce-12-1] eliminated 7 clauses out of 52 (13%) of length 8
c [cce-12-1] eliminated 9 clauses out of 115 (8%) of length 7
c [cce-12-1] eliminated 26 clauses out of 300 (9%) of length 6
c [cce-12-1] eliminated 83 clauses out of 640 (13%) of length 5
c [cce-12-1] eliminated 87 clauses out of 1552 (6%) of length 4
c [cce-12-1] completed large round (ACCE)
c [cce-12-1] eliminated 271 large clauses in 12973201 steps
c [cce-12-1] allowing another 6486600 steps for small clauses
c [cce-12] scheduling 128088 clauses = 126054 binary + 2034 ternary
c [cce-12] tried to eliminate 1981 small clauses 2%
c [cce-12] eliminated 1084 small clauses 1%
c [cce-12] eliminated 1077 binary clauses 1%
c [cce-12] eliminated 7 ternary clauses 0%
c [cce-12-1] eliminated 1084 small clauses in 30000001 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 1355 covered clauses in round 1
c [cce-12] eliminated 1355 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 20261 variables 100%
c [elim-13] limit of 128282463 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 252 variables 1% in round 1 in 16890648 steps
c [elim-13-1] backward subsumption/strengthening limit 33781296
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 4010791 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 252 = 1% variables out of 20261
c [bca-12] limit of 10000000 steps
c [bca-12] 34138 out of 40020 literals actually usable 85%
c [bca-12] added 1661 blocked clauses in 422764 steps
c [phase-14] phase bias: 27 positive 56%, 21 negative 44%
c [simplification-13] removed 363 variables 1.8% (20009 remain 37%)
c [simplification-13] removed 3776 irredundant clauses 2.8% (130997 remain 43%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 8888 = 35554 / 4
c [simplification-13] new conflict interval 44442
c [simplification-13] penalized conflict interval 44442 = 1 * 44442
c [simplification-13] new conflict limit 222702
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   82.4   20009   130997    185832    9745   1631 244857   2 27.4  75.7   16
c i   82.4   20008   130997    185843    9755   1631 244857   2 27.4  75.7   17
c i   82.5   19955   130997    186328   10204   1634 244857   2 27.4  75.6   17
c i   82.6   19902   130997    187285   11069   1644 244862   1 27.4  75.5   17
c -   83.9   19902   130997    195574   10577   1686 244881   1 27.4  75.1   16
c i   84.3   19901   130997    198465   13227   1702 244892   1 27.2  74.8   18
c -   85.5   19901   130997    205804   11445   1737 244896   3 27.2  74.4   16
c i   86.9   19900   130997    216713   20234   1764 244914   1 27.6  74.0   22
c -   87.0   19900   130997    217184   12193   1764 244914   2 27.6  74.0   16
c i   87.1   19899   130997    218026   13007   1767 244919   2 27.5  74.0   17
c i   87.3   19847   130997    219056   13925   1774 244927   1 27.5  73.9   18
c 
c [simplification-14] limit of 223012 conflicts hit after 223012 conflicts
c [ternres-12] limit 8015758 with penalty 0 = 0 + 0
c [ternres-12] all 19796 free variables schedulable
c [ternres-12] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-21] removed 215 variables
c [lift-8] limit 4809455 with penalty 0 = 0 + 0
c [lift-8] using 6835 probes 35%
c [lift-8] 63 units, 15 impls, 0 eqs in 1 rounds
c [lift-8] 16364 variables remain 83% (3367 retained)
c [lift-8] removed 63 variables
c [cliff-10] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-10] failed 22, lifted 0
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 367 transitive binary clauses
c [cce-13] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 1 (100%) of length 115
c [cce-13-1] eliminated 5 clauses out of 5 (100%) of length 111
c [cce-13-1] eliminated 10 clauses out of 35 (29%) of length 61
c [cce-13-1] eliminated 7 clauses out of 41 (17%) of length 60
c [cce-13-1] eliminated 4 clauses out of 50 (8%) of length 58
c [cce-13-1] eliminated 4 clauses out of 52 (8%) of length 55
c [cce-13-1] eliminated 4 clauses out of 35 (11%) of length 54
c [cce-13-1] eliminated 2 clauses out of 36 (6%) of length 53
c [cce-13-1] eliminated 3 clauses out of 42 (7%) of length 52
c [cce-13-1] eliminated 3 clauses out of 48 (6%) of length 51
c [cce-13-1] eliminated 10 clauses out of 229 (4%) of length 50
c [cce-13-1] eliminated 1 clauses out of 4 (25%) of length 42
c [cce-13-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-13-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-13-1] eliminated 1 clauses out of 8 (12%) of length 23
c [cce-13-1] eliminated 1 clauses out of 3 (33%) of length 19
c [cce-13-1] eliminated 1 clauses out of 30 (3%) of length 18
c [cce-13-1] eliminated 9 clauses out of 43 (21%) of length 13
c [cce-13-1] eliminated 4 clauses out of 36 (11%) of length 12
c [cce-13-1] eliminated 3 clauses out of 63 (5%) of length 11
c [cce-13-1] eliminated 1 clauses out of 87 (1%) of length 10
c [cce-13-1] eliminated 6 clauses out of 65 (9%) of length 9
c [cce-13-1] eliminated 7 clauses out of 84 (8%) of length 8
c [cce-13-1] eliminated 4 clauses out of 120 (3%) of length 7
c [cce-13-1] eliminated 15 clauses out of 271 (6%) of length 6
c [cce-13-1] eliminated 18 clauses out of 537 (3%) of length 5
c [cce-13-1] eliminated 48 clauses out of 1460 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 175 large clauses in 11980967 steps
c [cce-13-1] allowing another 5990483 steps for small clauses
c [cce-13] scheduling 122998 clauses = 121061 binary + 1937 ternary
c [cce-13] tried to eliminate 2016 small clauses 2%
c [cce-13] eliminated 1122 small clauses 1%
c [cce-13] eliminated 1113 binary clauses 1%
c [cce-13] eliminated 9 ternary clauses 0%
c [cce-13-1] eliminated 1330 small clauses in 30000001 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 1505 covered clauses in round 1
c [cce-13] eliminated 1505 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 19709 variables 100%
c [elim-14] limit of 160315171 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 457 variables 2% in round 1 in 16229258 steps
c [elim-14-1] backward subsumption/strengthening limit 32458516
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 3743506 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 457 = 2% variables out of 19709
c [bca-13] limit of 10000000 steps
c [bca-13] 32412 out of 38506 literals actually usable 84%
c [bca-13] added 833 blocked clauses in 406497 steps
c [rephase-6] after 223012 conflicts (new increment 80000, next 303012)
c [flushphases] 3202 phases reset
c [phase-15] phase bias: 156 positive 66%, 82 negative 34%
c [simplification-14] removed 544 variables 2.7% (19252 remain 36%)
c [simplification-14] removed 7559 irredundant clauses 5.8% (123438 remain 40%)
c [simplification-14] maximum reduction of 6% = max (3%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] new conflict interval 2230 = min (223012/100, 44442)
c [simplification-14] penalized conflict interval 2230 = 1 * 2230
c [simplification-14] new conflict limit 225242
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   91.2   19251   123438    224385   17903   1687 232971   1 27.3  73.6   22
c 
c [simplification-15] limit of 225264 conflicts hit after 225267 conflicts
c [ternres-13] limit 8106997 with penalty 0 = 0 + 0
c [ternres-13] all 19251 free variables schedulable
c [ternres-13] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 253343 penalty 4 = 4 + 0
c [card-5] found 1579 at-most-one constraints of average size 11.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 253343 for elimination
c [card-5] 1579 out of 1579 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-22] removed 3 variables
c [treelook-4] limit 50668 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 12508 literals 32%
c [treelook-4] scheduling used 51216 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 50668 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 140720 steps
c [treelook-4] 12474 literals remain 32%
c [treelook-4] 11514 variables remain to probed next time 60%
c [treelook-4] removed 0 variables, found 31 hbrs
c [lift-9] limit 4864198 with penalty 0 = 0 + 0
c [lift-9] using 5678 probes 29%
c [lift-9] 149 units, 32 impls, 1 eqs in 1 rounds
c [lift-9] 14556 variables remain 76% (4543 retained)
c [lift-9] removed 150 variables
c [cliff-11] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-11] failed 4, lifted 0
c [unhide-9] limit 202674 with penalty 3 = 3 + 0
c [unhide-9-9] 0 units, 0 failed, 1267 tauts, 0 hbrs, 116251 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 370 transitive binary clauses
c [cce-14] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-14-1] eliminated 1 clauses out of 1 (100%) of length 110
c [cce-14-1] eliminated 7 clauses out of 35 (20%) of length 61
c [cce-14-1] eliminated 4 clauses out of 27 (15%) of length 60
c [cce-14-1] eliminated 2 clauses out of 13 (15%) of length 59
c [cce-14-1] eliminated 7 clauses out of 9 (78%) of length 58
c [cce-14-1] eliminated 2 clauses out of 40 (5%) of length 57
c [cce-14-1] eliminated 2 clauses out of 45 (4%) of length 51
c [cce-14-1] eliminated 6 clauses out of 219 (3%) of length 50
c [cce-14-1] eliminated 2 clauses out of 4 (50%) of length 32
c [cce-14-1] eliminated 36 clauses out of 64 (56%) of length 18
c [cce-14-1] eliminated 66 clauses out of 94 (70%) of length 17
c [cce-14-1] eliminated 99 clauses out of 118 (84%) of length 15
c [cce-14-1] eliminated 3 clauses out of 25 (12%) of length 14
c [cce-14-1] eliminated 2 clauses out of 35 (6%) of length 13
c [cce-14-1] eliminated 3 clauses out of 32 (9%) of length 12
c [cce-14-1] eliminated 2 clauses out of 55 (4%) of length 11
c [cce-14-1] eliminated 1 clauses out of 43 (2%) of length 10
c [cce-14-1] eliminated 3 clauses out of 115 (3%) of length 8
c [cce-14-1] eliminated 3 clauses out of 121 (2%) of length 7
c [cce-14-1] eliminated 7 clauses out of 252 (3%) of length 6
c [cce-14-1] eliminated 14 clauses out of 534 (3%) of length 5
c [cce-14-1] eliminated 56 clauses out of 1411 (4%) of length 4
c [cce-14-1] completed large round (ACCE)
c [cce-14-1] eliminated 330 large clauses in 15059210 steps
c [cce-14-1] allowing another 7529605 steps for small clauses
c [cce-14] scheduling 115822 clauses = 114728 binary + 1094 ternary
c [cce-14] tried to eliminate 2243 small clauses 2%
c [cce-14] eliminated 1159 small clauses 1%
c [cce-14] eliminated 1155 binary clauses 1%
c [cce-14] eliminated 4 ternary clauses 0%
c [cce-14-1] eliminated 1159 small clauses in 30000001 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 1489 covered clauses in round 1
c [cce-14] eliminated 1489 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 19095 variables 100%
c [elim-15] limit of 162139943 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 245 variables 1% in round 1 in 14945625 steps
c [elim-15-1] backward subsumption/strengthening limit 29891250
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 3571135 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 245 = 1% variables out of 19095
c [bca-14] limit of 10000000 steps
c [bca-14] 31659 out of 37702 literals actually usable 84%
c [bca-14] added 1349 blocked clauses in 400278 steps
c [phase-16] phase bias: 19 positive 54%, 16 negative 46%
c [simplification-15] removed 401 variables 2.1% (18850 remain 35%)
c [simplification-15] removed 4096 irredundant clauses 3.3% (119342 remain 39%)
c [simplification-15] maximum reduction of 3% = max (2%, 3%)
c [simplification-15] geometric conflict interval increment 11110 = 44442 / 4
c [simplification-15] new conflict interval 55552
c [simplification-15] penalized conflict interval 55552 = 1 * 55552
c [simplification-15] new conflict limit 280819
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   95.7   18850   119342    230155   12781   1679 227750   1 27.3  73.3   16
c -   97.1   18850   119342    243182   13668   1729 227761   3 27.3  73.0   16
c -   98.9   18850   119342    261109   14270   1740 227762   1 27.7  72.5   16
c R  100.1   18850   119342    272074   20933   1746 227764   4 28.2  72.4   22
c -  100.9   18850   119342    277293   15055   1767 227771   3 28.1  72.1   17
c 
c [simplification-16] limit of 280879 conflicts hit after 280881 conflicts
c [ternres-14] limit 9921104 with penalty 0 = 0 + 0
c [ternres-14] all 18850 free variables schedulable
c [ternres-14] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-24] removed 1 variables
c [basicprobe-4] limit 9921104 penalty 0 = 0 + 0
c [basicprobe-4-0] 10506 probes remain 56% after last round
c [basicprobe-4-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 24 variables, found 424 hbrs
c [bate-2] eliminated 2 asymmetric tautologies during probing
c [lift-10] limit 5952662 with penalty 0 = 0 + 0
c [lift-10] using 4315 probes 23%
c [lift-10] 9 units, 31 impls, 0 eqs in 1 rounds
c [lift-10] 12971 variables remain 69% (5845 retained)
c [lift-10] removed 9 variables
c [cliff-12] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-12] failed 28, lifted 0
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 319 transitive binary clauses
c [cce-15] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 3 clauses out of 6 (50%) of length 109
c [cce-15-1] eliminated 5 clauses out of 32 (16%) of length 61
c [cce-15-1] eliminated 6 clauses out of 34 (18%) of length 60
c [cce-15-1] eliminated 1 clauses out of 43 (2%) of length 57
c [cce-15-1] eliminated 1 clauses out of 256 (0%) of length 50
c [cce-15-1] eliminated 2 clauses out of 22 (9%) of length 15
c [cce-15-1] eliminated 1 clauses out of 24 (4%) of length 14
c [cce-15-1] eliminated 2 clauses out of 33 (6%) of length 13
c [cce-15-1] eliminated 2 clauses out of 30 (7%) of length 12
c [cce-15-1] eliminated 2 clauses out of 52 (4%) of length 11
c [cce-15-1] eliminated 1 clauses out of 46 (2%) of length 10
c [cce-15-1] eliminated 4 clauses out of 69 (6%) of length 9
c [cce-15-1] eliminated 7 clauses out of 118 (6%) of length 8
c [cce-15-1] eliminated 4 clauses out of 126 (3%) of length 7
c [cce-15-1] eliminated 13 clauses out of 245 (5%) of length 6
c [cce-15-1] eliminated 20 clauses out of 558 (4%) of length 5
c [cce-15-1] eliminated 35 clauses out of 1357 (3%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 109 large clauses in 11168398 steps
c [cce-15-1] allowing another 5584199 steps for small clauses
c [cce-15] scheduling 113488 clauses = 112432 binary + 1056 ternary
c [cce-15] tried to eliminate 2212 small clauses 2%
c [cce-15] eliminated 1190 small clauses 1%
c [cce-15] eliminated 1187 binary clauses 1%
c [cce-15] eliminated 3 ternary clauses 0%
c [cce-15-1] eliminated 1480 small clauses in 30000001 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 1589 covered clauses in round 1
c [cce-15] eliminated 1589 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 18788 variables 100%
c [elim-16] limit of 198422091 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 151 variables 1% in round 1 in 11176686 steps
c [elim-16-1] backward subsumption/strengthening limit 22353372
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 3439472 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 151 = 1% variables out of 18788
c [bca-15] limit of 10000000 steps
c [bca-15] 30750 out of 37276 literals actually usable 82%
c [bca-15] added 565 blocked clauses in 392723 steps
c [phase-17] phase bias: 1 positive 11%, 8 negative 89%
c [simplification-16] removed 213 variables 1.1% (18637 remain 35%)
c [simplification-16] removed 2275 irredundant clauses 1.9% (117067 remain 38%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 18517 = 55552 / 3
c [simplification-16] new conflict interval 74069
c [simplification-16] penalized conflict interval 74069 = 1 * 74069
c [simplification-16] new conflict limit 354950
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  105.9   18637   117067    291616   15892   1800 226516   3 28.0  71.4   17
c i  107.1   18636   117067    301557   24064   1842 226524   2 28.0  71.1   22
c -  107.8   18636   117067    306442   16761   1863 226530   2 27.9  70.8   17
c -  110.0   18636   117067    321546   17646   1906 226536   4 27.7  70.0   17
c -  112.1   18636   117067    338067   18382   1941 226547   2 27.7  69.7   17
c i  113.0   18635   117067    344430   23926   1953 226549   2 27.6  69.4   21
c i  113.1   18634   117067    344933   24388   1954 226549   2 27.6  69.4   21
c i  113.8   18633   117067    349785   28696   1970 226551   1 27.5  69.2   24
c i  113.9   18581   117067    350004   28886   1970 226551   2 27.5  69.2   24
c -  114.4   18581   117067    353889   19244   1978 226553   2 27.4  69.0   17
c 
c [simplification-17] limit of 355140 conflicts hit after 355142 conflicts
c [ternres-15] limit 12605829 with penalty 0 = 0 + 0
c [ternres-15] all 18581 free variables schedulable
c [ternres-15] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 157572 penalty 4 = 4 + 0
c [gauss-5] extracted 1 xors of average arity 3.0
c [gauss-5] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-5] limit 157572 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 18581 free variables schedulable
c [simpleprobe-5] limit 50423318 penalty 0 = 0 + 0
c [decomp-26] removed 12 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 12 variables, found 8701 hbrs, 3 units
c [cgrclsr-5] limit 78786 penalty 4 = 4 + 0
c [cgrclsr-5] all 18569 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-11] limit 7563497 with penalty 0 = 0 + 0
c [lift-11] using 2877 probes 15%
c [lift-11] 112 units, 38 impls, 1 eqs in 1 rounds
c [lift-11] 10874 variables remain 59% (7529 retained)
c [lift-11] removed 166 variables
c [cliff-13] limit of 10084663 steps penalty 0 = 0 + 0
c [cliff-13] failed 1, lifted 0
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 430 transitive binary clauses
c [cce-16] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 2 clauses out of 2 (100%) of length 108
c [cce-16-1] eliminated 2 clauses out of 33 (6%) of length 61
c [cce-16-1] eliminated 8 clauses out of 34 (24%) of length 60
c [cce-16-1] eliminated 2 clauses out of 75 (3%) of length 54
c [cce-16-1] eliminated 3 clauses out of 30 (10%) of length 53
c [cce-16-1] eliminated 3 clauses out of 41 (7%) of length 52
c [cce-16-1] eliminated 15 clauses out of 255 (6%) of length 50
c [cce-16-1] eliminated 1 clauses out of 22 (5%) of length 15
c [cce-16-1] eliminated 2 clauses out of 25 (8%) of length 14
c [cce-16-1] eliminated 2 clauses out of 48 (4%) of length 11
c [cce-16-1] eliminated 1 clauses out of 44 (2%) of length 10
c [cce-16-1] eliminated 4 clauses out of 101 (4%) of length 9
c [cce-16-1] eliminated 9 clauses out of 114 (8%) of length 8
c [cce-16-1] eliminated 21 clauses out of 131 (16%) of length 7
c [cce-16-1] eliminated 31 clauses out of 235 (13%) of length 6
c [cce-16-1] eliminated 42 clauses out of 550 (8%) of length 5
c [cce-16-1] eliminated 40 clauses out of 1311 (3%) of length 4
c [cce-16-1] completed large round (ACCE)
c [cce-16-1] eliminated 188 large clauses in 10646640 steps
c [cce-16-1] allowing another 5323320 steps for small clauses
c [cce-16] scheduling 109468 clauses = 108466 binary + 1002 ternary
c [cce-16] tried to eliminate 2468 small clauses 2%
c [cce-16] eliminated 1288 small clauses 1%
c [cce-16] eliminated 1283 binary clauses 1%
c [cce-16] eliminated 5 ternary clauses 0%
c [cce-16-1] eliminated 1298 small clauses in 30000001 steps
c [cce-16-1] incomplete small round (ACCE)
c [cce-16-1] eliminated 1486 covered clauses in round 1
c [cce-16] eliminated 1486 covered clauses in TOTAL during 1 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 18402 variables 100%
c [elim-17] limit of 252116594 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 509 variables 3% in round 1 in 8759042 steps
c [elim-17-1] backward subsumption/strengthening limit 17518084
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 3157378 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 509 = 3% variables out of 18402
c [bca-16] limit of 10000000 steps
c [bca-16] 29734 out of 35788 literals actually usable 83%
c [bca-16] added 744 blocked clauses in 372862 steps
c [rephase-7] after 355142 conflicts (new increment 160000, next 515142)
c [flushphases] 2934 phases reset
c [phase-18] phase bias: 106 positive 47%, 121 negative 53%
c [simplification-17] removed 688 variables 3.7% (17893 remain 33%)
c [simplification-17] removed 7293 irredundant clauses 6.2% (109774 remain 36%)
c [simplification-17] maximum reduction of 6% = max (4%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] new conflict interval 3551 = min (355142/100, 74069)
c [simplification-17] penalized conflict interval 3551 = 1 * 3551
c [simplification-17] new conflict limit 358693
c 
c [simplification-18] limit of 358707 conflicts hit after 358707 conflicts
c [ternres-16] limit 12723042 with penalty 0 = 0 + 0
c [ternres-16] all 17893 free variables schedulable
c [ternres-16] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [lift-12] limit 7633825 with penalty 0 = 0 + 0
c [lift-12] using 1083 probes 6%
c [lift-12-1] found 3 units 10 impls in round 1
c [lift-12] 7 units, 23 impls, 0 eqs in 2 rounds
c [lift-12] 9433 variables remain 53% (8450 retained)
c [lift-12] removed 9 variables
c [cliff-14] limit of 10178434 steps penalty 0 = 0 + 0
c [cliff-14] failed 1, lifted 0
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 317 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 17882 variables 100%
c [block-7] limit of 7951901 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 24 blocked clauses
c [block-7] 24 < 1/1000 * 109643 = 109 considered unsuccessful
c [cce-17] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 6 clauses out of 6 (100%) of length 118
c [cce-17-1] eliminated 2 clauses out of 5 (40%) of length 117
c [cce-17-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-17-1] eliminated 5 clauses out of 5 (100%) of length 108
c [cce-17-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-17-1] eliminated 3 clauses out of 3 (100%) of length 103
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 102
c [cce-17-1] eliminated 3 clauses out of 3 (100%) of length 101
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 100
c [cce-17-1] eliminated 3 clauses out of 3 (100%) of length 72
c [cce-17-1] eliminated 2 clauses out of 3 (67%) of length 71
c [cce-17-1] eliminated 2 clauses out of 33 (6%) of length 61
c [cce-17-1] eliminated 3 clauses out of 32 (9%) of length 60
c [cce-17-1] eliminated 10 clauses out of 237 (4%) of length 50
c [cce-17-1] eliminated 1 clauses out of 22 (5%) of length 18
c [cce-17-1] eliminated 35 clauses out of 58 (60%) of length 17
c [cce-17-1] eliminated 1 clauses out of 20 (5%) of length 16
c [cce-17-1] eliminated 62 clauses out of 94 (66%) of length 15
c [cce-17-1] eliminated 105 clauses out of 128 (82%) of length 14
c [cce-17-1] eliminated 2 clauses out of 43 (5%) of length 10
c [cce-17-1] eliminated 1 clauses out of 97 (1%) of length 9
c [cce-17-1] eliminated 2 clauses out of 108 (2%) of length 8
c [cce-17-1] eliminated 16 clauses out of 213 (8%) of length 6
c [cce-17-1] eliminated 40 clauses out of 561 (7%) of length 5
c [cce-17-1] eliminated 59 clauses out of 1257 (5%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 369 large clauses in 15254494 steps
c [cce-17-1] allowing another 7627247 steps for small clauses
c [cce-17] scheduling 104512 clauses = 103543 binary + 969 ternary
c [cce-17] tried to eliminate 2143 small clauses 2%
c [cce-17] eliminated 1102 small clauses 1%
c [cce-17] eliminated 1095 binary clauses 1%
c [cce-17] eliminated 7 ternary clauses 1%
c [cce-17-1] eliminated 1102 small clauses in 30000001 steps
c [cce-17-1] incomplete small round (ACCE)
c [cce-17-1] eliminated 1471 covered clauses in round 1
c [cce-17] eliminated 1471 covered clauses in TOTAL during 1 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 17882 variables 100%
c [elim-18] limit of 254460858 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 424 variables 2% in round 1 in 8636522 steps
c [elim-18-1] backward subsumption/strengthening limit 17273044
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 3047280 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 424 = 2% variables out of 17882
c [bca-17] limit of 10000000 steps
c [bca-17] 28880 out of 34918 literals actually usable 83%
c [bca-17] added 5730 blocked clauses in 374314 steps
c [phase-19] phase bias: 4 positive 80%, 1 negative 20%
c [simplification-18] removed 435 variables 2.4% (17458 remain 33%)
c [simplification-18] removed 3280 irredundant clauses 3.0% (106494 remain 35%)
c [simplification-18] maximum reduction of 3% = max (2%, 3%)
c [simplification-18] geometric conflict interval increment 18517 = 74069 / 4
c [simplification-18] new conflict interval 92586
c [simplification-18] penalized conflict interval 92586 = 1 * 92586
c [simplification-18] new conflict limit 451293
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  122.7   17458   106494    372782   19927   1867 218864   3 27.1  68.3   17
c i  123.5   17457   106494    379327   25871   1879 218868   2 27.0  68.0   21
c -  124.7   17457   106494    391461   20603   1889 218872   7 27.3  68.2   17
c i  126.2   17456   106494    404916   31611   1912 218880   1 27.3  67.9   25
c -  126.9   17456   106494    409914   21484   1915 218881   5 27.2  67.7   18
c i  127.1   17455   106494    411098   22514   1917 218881   2 27.2  67.7   19
c -  129.6   17455   106494    428685   22239   1936 218891   2 27.1  67.1   18
c -  132.2   17455   106494    447388   23185   1965 218915   2 26.8  66.5   18
c 
c [simplification-19] limit of 451487 conflicts hit after 451489 conflicts
c [ternres-17] limit 16006571 with penalty 0 = 0 + 0
c [ternres-17] all 17455 free variables schedulable
c [ternres-17] 24 ternary resolvents (1 bin, 23 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-28] removed 3 variables
c [lift-13] limit 9603942 with penalty 0 = 0 + 0
c [lift-13] using 19 probes 0%
c [lift-13-1] found 4 units 2 impls in round 1
c [lift-13-2] found 0 units 1 impls in round 2
c [lift-13-3] found 0 units 1 impls in round 3
c [lift-13-4] found 0 units 1 impls in round 4
c [lift-13-5] found 0 units 2 impls in round 5
c [lift-13] 4 units, 7 impls, 0 eqs in 6 rounds
c [lift-13] 9331 variables remain 53% (8116 retained)
c [lift-13] removed 8 variables
c [cliff-15] limit of 12805257 steps penalty 0 = 0 + 0
c [cliff-15] failed 53, lifted 0
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 441 transitive binary clauses
c [cce-18] limit of 32013142 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 66
c [cce-18-1] eliminated 2 clauses out of 2 (100%) of length 64
c [cce-18-1] eliminated 2 clauses out of 3 (67%) of length 63
c [cce-18-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-18-1] eliminated 3 clauses out of 29 (10%) of length 61
c [cce-18-1] eliminated 2 clauses out of 30 (7%) of length 60
c [cce-18-1] eliminated 1 clauses out of 31 (3%) of length 53
c [cce-18-1] eliminated 1 clauses out of 36 (3%) of length 52
c [cce-18-1] eliminated 1 clauses out of 7 (14%) of length 51
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 48
c [cce-18-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-18-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-18-1] eliminated 1 clauses out of 3 (33%) of length 33
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-18-1] eliminated 1 clauses out of 15 (7%) of length 21
c [cce-18-1] eliminated 1 clauses out of 19 (5%) of length 17
c [cce-18-1] eliminated 1 clauses out of 23 (4%) of length 16
c [cce-18-1] eliminated 2 clauses out of 25 (8%) of length 14
c [cce-18-1] eliminated 2 clauses out of 25 (8%) of length 12
c [cce-18-1] eliminated 1 clauses out of 48 (2%) of length 11
c [cce-18-1] eliminated 2 clauses out of 108 (2%) of length 8
c [cce-18-1] eliminated 8 clauses out of 86 (9%) of length 7
c [cce-18-1] eliminated 18 clauses out of 242 (7%) of length 6
c [cce-18-1] eliminated 21 clauses out of 516 (4%) of length 5
c [cce-18-1] eliminated 42 clauses out of 1147 (4%) of length 4
c [cce-18-1] completed large round (ACCE)
c [cce-18-1] eliminated 119 large clauses in 8437631 steps
c [cce-18-1] allowing another 4218815 steps for small clauses
c [cce-18] scheduling 101202 clauses = 100337 binary + 865 ternary
c [cce-18] tried to eliminate 2800 small clauses 3%
c [cce-18] eliminated 1454 small clauses 1%
c [cce-18] eliminated 1450 binary clauses 1%
c [cce-18] eliminated 4 ternary clauses 0%
c [cce-18-1] eliminated 2000 small clauses in 32013143 steps
c [cce-18-1] incomplete small round (ACCE)
c [cce-18-1] eliminated 2119 covered clauses in round 1
c [cce-18] eliminated 2119 covered clauses in TOTAL during 1 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 17394 variables 100%
c [elim-19] limit of 320131426 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 182 variables 1% in round 1 in 7252773 steps
c [elim-19-1] backward subsumption/strengthening limit 14505546
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 2922967 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 182 = 1% variables out of 17394
c [bca-18] limit of 10000000 steps
c [bca-18] 27979 out of 34426 literals actually usable 81%
c [bca-18] added 2284 blocked clauses in 377023 steps
c [phase-20] phase bias: 9 positive 64%, 5 negative 36%
c [simplification-19] removed 243 variables 1.4% (17212 remain 32%)
c [simplification-19] removed 2787 irredundant clauses 2.6% (103707 remain 34%)
c [simplification-19] maximum reduction of 3% = max (1%, 3%)
c [simplification-19] geometric conflict interval increment 23146 = 92586 / 4
c [simplification-19] new conflict interval 115732
c [simplification-19] penalized conflict interval 115732 = 1 * 115732
c [simplification-19] new conflict limit 567221
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  135.3   17211   103707    456829   30405   1952 220291   1 26.9  66.6   23
c -  137.1   17211   103707    468752   24026   1970 220306   3 26.9  66.2   18
c -  139.9   17211   103707    488722   24905   1990 220318   2 26.7  65.5   19
c i  140.8   17210   103707    495569   30481   2005 220323   1 26.7  65.4   23
c -  142.9   17210   103707    512588   25852   2030 220327   2 27.0  65.2   19
c -  145.2   17210   103707    535723   26855   2044 220330   4 26.9  65.3   19
c -  147.4   17210   103707    557259   27647   2066 220334   5 27.8  67.2   19
c 
c [simplification-20] limit of 567347 conflicts hit after 567348 conflicts
c [ternres-18] limit 19956281 with penalty 0 = 0 + 0
c [ternres-18] all 17210 free variables schedulable
c [ternres-18] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-29] removed 2 variables
c [lift-14] limit 11973768 with penalty 0 = 0 + 0
c [lift-14] using 20 probes 0%
c [lift-14-1] found 0 units 0 impls in round 1
c [lift-14-2] found 0 units 2 impls in round 2
c [lift-14-3] found 0 units 3 impls in round 3
c [lift-14-4] found 0 units 4 impls in round 4
c [lift-14-5] found 0 units 2 impls in round 5
c [lift-14] 0 units, 11 impls, 0 eqs in 6 rounds
c [lift-14] 9233 variables remain 54% (7977 retained)
c [cliff-16] limit of 15965024 steps penalty 0 = 0 + 0
c [cliff-16] failed 5, lifted 0
c [unhide-10] limit 249453 with penalty 4 = 4 + 0
c [unhide-10-10] 0 units, 0 failed, 24443 tauts, 0 hbrs, 215322 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 397 transitive binary clauses
c [cce-19] limit of 39912562 steps penalty 0 = 0 + 0
c [cce-19-1] eliminated 1 clauses out of 26 (4%) of length 61
c [cce-19-1] eliminated 4 clauses out of 33 (12%) of length 60
c [cce-19-1] eliminated 2 clauses out of 29 (7%) of length 59
c [cce-19-1] eliminated 1 clauses out of 45 (2%) of length 57
c [cce-19-1] eliminated 1 clauses out of 1 (100%) of length 55
c [cce-19-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-19-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-19-1] eliminated 1 clauses out of 9 (11%) of length 19
c [cce-19-1] eliminated 1 clauses out of 16 (6%) of length 17
c [cce-19-1] eliminated 3 clauses out of 34 (9%) of length 15
c [cce-19-1] eliminated 4 clauses out of 27 (15%) of length 14
c [cce-19-1] eliminated 1 clauses out of 25 (4%) of length 12
c [cce-19-1] eliminated 2 clauses out of 75 (3%) of length 8
c [cce-19-1] eliminated 1 clauses out of 111 (1%) of length 7
c [cce-19-1] eliminated 5 clauses out of 226 (2%) of length 6
c [cce-19-1] eliminated 19 clauses out of 519 (4%) of length 5
c [cce-19-1] eliminated 27 clauses out of 1098 (2%) of length 4
c [cce-19-1] completed large round (ACCE)
c [cce-19-1] eliminated 75 large clauses in 8183485 steps
c [cce-19-1] allowing another 4091742 steps for small clauses
c [cce-19] scheduling 98693 clauses = 97864 binary + 829 ternary
c [cce-19] tried to eliminate 3750 small clauses 4%
c [cce-19] eliminated 1894 small clauses 2%
c [cce-19] eliminated 1889 binary clauses 2%
c [cce-19] eliminated 5 ternary clauses 1%
c [cce-19-1] eliminated 1894 small clauses in 39912563 steps
c [cce-19-1] incomplete small round (ACCE)
c [cce-19-1] eliminated 1969 covered clauses in round 1
c [cce-19] eliminated 1969 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 17163 variables 100%
c [elim-20] limit of 399125624 steps penalty 0 = 0 + 0
c [elim-20-1] eliminated 189 variables 1% in round 1 in 6454649 steps
c [elim-20-1] backward subsumption/strengthening limit 12909298
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 2808496 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 189 = 1% variables out of 17163
c [bca-19] limit of 10000000 steps
c [bca-19] 27379 out of 33950 literals actually usable 81%
c [bca-19] added 19712 blocked clauses in 374470 steps
c [rephase-8] after 567348 conflicts (new increment 320000, next 887348)
c [flushphases] 2751 phases reset
c [phase-21] phase bias: 5 positive 31%, 11 negative 69%
c [simplification-20] removed 236 variables 1.4% (16974 remain 32%)
c [simplification-20] removed 2848 irredundant clauses 2.7% (100859 remain 33%)
c [simplification-20] maximum reduction of 3% = max (1%, 3%)
c [simplification-20] geometric conflict interval increment 28933 = 115732 / 4
c [simplification-20] new conflict interval 144665
c [simplification-20] penalized conflict interval 144665 = 1 * 144665
c [simplification-20] new conflict limit 712013
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  153.7   16974   100859    585521   39652   1997 214902   2 28.1  68.5   39
c -  155.2   16974   100859    593162   27627   2007 214914   2 28.1  68.2   20
c i  155.5   16973   100859    594875   29218   2010 214916   1 28.1  68.1   21
c -  158.8   16972   100859    616857   28452   2043 214916   2 27.9  67.5   19
c -  162.1   16972   100859    640602   29359   2074 214926   2 27.7  66.9   19
c -  165.9   16972   100859    665195   30139   2100 214936   2 27.6  66.2   26
c -  169.6   16972   100859    690372   31151   2159 214949   3 27.4  65.6   26
c 
c [simplification-21] limit of 712131 conflicts hit after 712131 conflicts
c [ternres-19] limit 25677944 with penalty 0 = 0 + 0
c [ternres-19] all 16972 free variables schedulable
c [ternres-19] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 802435 penalty 4 = 4 + 0
c [card-6] found 4196 at-most-one constraints of average size 12.6
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 802435 for elimination
c [card-6] 4196 out of 4196 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-30] removed 2 variables
c [cliff-17] limit of 20542355 steps penalty 0 = 0 + 0
c [cliff-17] failed 29, lifted 1
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 420 transitive binary clauses
c [cce-20] limit of 51355888 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 2 clauses out of 26 (8%) of length 61
c [cce-20-1] eliminated 1 clauses out of 30 (3%) of length 60
c [cce-20-1] eliminated 6 clauses out of 95 (6%) of length 54
c [cce-20-1] eliminated 3 clauses out of 35 (9%) of length 52
c [cce-20-1] eliminated 2 clauses out of 231 (1%) of length 50
c [cce-20-1] eliminated 1 clauses out of 7 (14%) of length 22
c [cce-20-1] eliminated 1 clauses out of 9 (11%) of length 21
c [cce-20-1] eliminated 1 clauses out of 24 (4%) of length 18
c [cce-20-1] eliminated 1 clauses out of 19 (5%) of length 17
c [cce-20-1] eliminated 1 clauses out of 33 (3%) of length 15
c [cce-20-1] eliminated 1 clauses out of 22 (5%) of length 14
c [cce-20-1] eliminated 1 clauses out of 65 (2%) of length 9
c [cce-20-1] eliminated 3 clauses out of 77 (4%) of length 8
c [cce-20-1] eliminated 3 clauses out of 108 (3%) of length 7
c [cce-20-1] eliminated 5 clauses out of 223 (2%) of length 6
c [cce-20-1] eliminated 17 clauses out of 501 (3%) of length 5
c [cce-20-1] eliminated 26 clauses out of 1040 (2%) of length 4
c [cce-20-1] completed large round (ACCE)
c [cce-20-1] eliminated 75 large clauses in 8358035 steps
c [cce-20-1] allowing another 4179017 steps for small clauses
c [cce-20] scheduling 96830 clauses = 95331 binary + 1499 ternary
c [cce-20] tried to eliminate 4990 small clauses 5%
c [cce-20] eliminated 2477 small clauses 3%
c [cce-20] eliminated 2456 binary clauses 3%
c [cce-20] eliminated 21 ternary clauses 1%
c [cce-20-1] eliminated 2734 small clauses in 51355889 steps
c [cce-20-1] incomplete small round (ACCE)
c [cce-20-1] eliminated 2809 covered clauses in round 1
c [cce-20] eliminated 2809 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 16942 variables 100%
c [elim-21] limit of 513558882 steps penalty 0 = 0 + 0
c [elim-21-1] eliminated 200 variables 1% in round 1 in 6291601 steps
c [elim-21-1] backward subsumption/strengthening limit 12583202
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 2675614 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 200 = 1% variables out of 16942
c [bca-20] limit of 10000000 steps
c [bca-20] 26199 out of 33486 literals actually usable 78%
c [bca-20] added 1716 blocked clauses in 392311 steps
c [phase-22] phase bias: 1 positive 20%, 4 negative 80%
c [simplification-21] removed 230 variables 1.4% (16742 remain 31%)
c [simplification-21] removed 3291 irredundant clauses 3.3% (97568 remain 32%)
c [simplification-21] maximum reduction of 3% = max (1%, 3%)
c [simplification-21] geometric conflict interval increment 36166 = 144665 / 4
c [simplification-21] new conflict interval 180831
c [simplification-21] penalized conflict interval 180831 = 1 * 180831
c [simplification-21] new conflict limit 892962
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  176.0   16742    97568    719845   31931   2162 217768   2 27.7  65.6   21
c -  180.0   16742    97568    746567   32826   2189 217769   2 27.6  65.0   21
c -  183.9   16742    97568    774856   33691   2235 217783   2 27.5  64.6   21
c i  184.2   16741    97568    776192   34897   2239 217786   1 27.5  64.6   23
c -  188.2   16741    97568    803431   34568   2269 217794   3 27.4  64.1   21
c -  192.3   16741    97568    835612   35513   2295 217799   2 27.7  64.1   21
c -  195.9   16741    97568    865205   36380   2329 217806   1 27.6  63.7   29
c 
c [simplification-22] limit of 893074 conflicts hit after 893075 conflicts
c [ternres-20] limit 32938278 with penalty 0 = 0 + 0
c [ternres-20] all 16741 free variables schedulable
c [ternres-20] 31 ternary resolvents (0 bin, 31 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-31] removed 1 variables
c [treelook-5] limit 102932 penalty 4 = 4 + 0 boost 1
c [treelook-5] scheduled 13095 literals 39%
c [treelook-5] scheduling used 104532 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 102932 penalty 4 = 4 + 0 boost 1
c [treelook-5] used 144774 steps
c [treelook-5] 13092 literals remain 39%
c [treelook-5] 10350 variables remain to probed next time 62%
c [treelook-5] removed 0 variables, found 72 hbrs
c [lift-15] limit 9881483 with penalty 1 = 1 + 0
c [lift-15] using 73 probes 0%
c [lift-15-1] found 3 units 5 impls in round 1
c [lift-15-2] found 0 units 7 impls in round 2
c [lift-15-3] found 1 units 11 impls in round 3
c [lift-15-4] found 12 units 8 impls in round 4
c [lift-15-5] found 2 units 7 impls in round 5
c [lift-15] 18 units, 38 impls, 0 eqs in 6 rounds
c [lift-15] 9001 variables remain 54% (7722 retained)
c [lift-15] removed 18 variables
c [cliff-18] limit of 26350622 steps penalty 0 = 0 + 0
c [cliff-18] failed 1, lifted 0
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 399 transitive binary clauses
c [cce-21] limit of 65876556 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 3 clauses out of 24 (12%) of length 61
c [cce-21-1] eliminated 3 clauses out of 33 (9%) of length 60
c [cce-21-1] eliminated 12 clauses out of 238 (5%) of length 50
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-21-1] eliminated 1 clauses out of 13 (8%) of length 20
c [cce-21-1] eliminated 1 clauses out of 19 (5%) of length 17
c [cce-21-1] eliminated 2 clauses out of 32 (6%) of length 15
c [cce-21-1] eliminated 2 clauses out of 21 (10%) of length 14
c [cce-21-1] eliminated 1 clauses out of 27 (4%) of length 12
c [cce-21-1] eliminated 3 clauses out of 37 (8%) of length 10
c [cce-21-1] eliminated 1 clauses out of 57 (2%) of length 9
c [cce-21-1] eliminated 1 clauses out of 107 (1%) of length 7
c [cce-21-1] eliminated 7 clauses out of 215 (3%) of length 6
c [cce-21-1] eliminated 10 clauses out of 493 (2%) of length 5
c [cce-21-1] eliminated 9 clauses out of 1004 (1%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 57 large clauses in 8256300 steps
c [cce-21-1] allowing another 4128150 steps for small clauses
c [cce-21] scheduling 93060 clauses = 92251 binary + 809 ternary
c [cce-21] tried to eliminate 6541 small clauses 7%
c [cce-21] eliminated 3184 small clauses 3%
c [cce-21] eliminated 3161 binary clauses 3%
c [cce-21] eliminated 23 ternary clauses 3%
c [cce-21-1] eliminated 3195 small clauses in 65876557 steps
c [cce-21-1] incomplete small round (ACCE)
c [cce-21-1] eliminated 3252 covered clauses in round 1
c [cce-21] eliminated 3252 covered clauses in TOTAL during 1 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 16722 variables 100%
c [elim-22] limit of 658765565 steps penalty 0 = 0 + 0
c [elim-22-1] eliminated 231 variables 1% in round 1 in 7767649 steps
c [elim-22-1] backward subsumption/strengthening limit 15535298
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 2541109 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 231 = 1% variables out of 16722
c [bca-21] limit of 10000000 steps
c [bca-21] 25438 out of 32984 literals actually usable 77%
c [bca-21] added 986 blocked clauses in 394879 steps
c [rephase-9] after 893075 conflicts (new increment 640000, next 1533075)
c [flushphases] 2578 phases reset
c [phase-23] phase bias: 6 positive 43%, 8 negative 57%
c [simplification-22] removed 250 variables 1.5% (16491 remain 31%)
c [simplification-22] removed 3935 irredundant clauses 4.0% (93633 remain 30%)
c [simplification-22] maximum reduction of 4% = max (1%, 4%)
c [simplification-22] geometric conflict interval increment 36166 = 180831 / 5
c [simplification-22] new conflict interval 216997
c [simplification-22] penalized conflict interval 216997 = 1 * 216997
c [simplification-22] new conflict limit 1110072
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  205.9   16491    93633    902943   36964   2311 219725   2 27.3  63.1   22
c -  210.7   16491    93633    933659   37826   2338 219740   2 27.2  62.7   22
c i  212.7   16490    93633    948897   50546   2359 219744   1 27.1  62.4   29
c -  215.3   16443    93633    963722   38668   2375 219749   2 27.0  62.2   22
c -  219.3   16443    93633    994376   39435   2391 219756   2 26.9  62.0   22
c -  224.5   16443    93633   1026560   40328   2436 219783   2 26.8  61.5   30
c -  229.2   16443    93633   1059407   41178   2475 219804   2 26.8  61.2   30
c i  230.5   16442    93633   1070024   50574   2482 219806   2 26.7  61.0   35
c -  234.2   16442    93633   1091678   42257   2514 219820   5 26.6  60.7   30
c 
c [simplification-23] limit of 1110310 conflicts hit after 1110311 conflicts
c [ternres-21] limit 42376683 with penalty 0 = 0 + 0
c [ternres-21] all 16442 free variables schedulable
c [ternres-21] 45 ternary resolvents (0 bin, 45 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 529708 penalty 4 = 4 + 0
c [gauss-6] extracted 2 xors of average arity 3.0
c [gauss-6] connected 6 occurrences of 6 variables (average 1.0)
c [gauss-6] limit 529708 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 1 variables
c [basicprobe-5] limit 42376683 penalty 0 = 0 + 0
c [basicprobe-5-0] 5618 probes remain 34% after last round
c [basicprobe-5-0] 52 units = 52 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 63 variables, found 1086 hbrs
c [bate-3] eliminated 11 asymmetric tautologies during probing
c [cgrclsr-6] limit 264854 penalty 4 = 4 + 0
c [cgrclsr-6] all 16378 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 27 probes 0%
c [lift-16-1] found 1 units 1 impls in round 1
c [lift-16-2] found 0 units 0 impls in round 2
c [lift-16-3] found 0 units 1 impls in round 3
c [lift-16-4] found 0 units 1 impls in round 4
c [lift-16-5] found 0 units 0 impls in round 5
c [lift-16] 1 units, 3 impls, 0 eqs in 6 rounds
c [lift-16] 8835 variables remain 54% (7542 retained)
c [lift-16] removed 1 variables
c [cliff-19] limit of 33901347 steps penalty 0 = 0 + 0
c [cliff-19] failed 6, lifted 0
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 312 transitive binary clauses
c [cce-22] limit of 84753367 steps penalty 0 = 0 + 0
c [cce-22-1] eliminated 1 clauses out of 1 (100%) of length 112
c [cce-22-1] eliminated 5 clauses out of 23 (22%) of length 61
c [cce-22-1] eliminated 12 clauses out of 33 (36%) of length 60
c [cce-22-1] eliminated 4 clauses out of 28 (14%) of length 59
c [cce-22-1] eliminated 4 clauses out of 50 (8%) of length 57
c [cce-22-1] eliminated 2 clauses out of 224 (1%) of length 50
c [cce-22-1] eliminated 1 clauses out of 3 (33%) of length 33
c [cce-22-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-22-1] eliminated 3 clauses out of 10 (30%) of length 21
c [cce-22-1] eliminated 1 clauses out of 10 (10%) of length 19
c [cce-22-1] eliminated 3 clauses out of 21 (14%) of length 15
c [cce-22-1] eliminated 1 clauses out of 78 (1%) of length 8
c [cce-22-1] eliminated 1 clauses out of 116 (1%) of length 7
c [cce-22-1] eliminated 1 clauses out of 172 (1%) of length 6
c [cce-22-1] eliminated 4 clauses out of 532 (1%) of length 5
c [cce-22-1] eliminated 20 clauses out of 999 (2%) of length 4
c [cce-22-1] completed large round (ACCE)
c [cce-22-1] eliminated 65 large clauses in 8026314 steps
c [cce-22-1] allowing another 4013157 steps for small clauses
c [cce-22] scheduling 88925 clauses = 87533 binary + 1392 ternary
c [cce-22] tried to eliminate 8735 small clauses 10%
c [cce-22] eliminated 4055 small clauses 5%
c [cce-22] eliminated 4010 binary clauses 5%
c [cce-22] eliminated 45 ternary clauses 3%
c [cce-22-1] eliminated 4117 small clauses in 84753368 steps
c [cce-22-1] incomplete small round (ACCE)
c [cce-22-1] eliminated 4182 covered clauses in round 1
c [cce-22] eliminated 4182 covered clauses in TOTAL during 1 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 16371 variables 100%
c [elim-23] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-23-1] eliminated 369 variables 2% in round 1 in 8983290 steps
c [elim-23-1] backward subsumption/strengthening limit 17966580
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 2351608 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 369 = 2% variables out of 16371
c [bca-22] limit of 10000000 steps
c [bca-22] 24638 out of 32006 literals actually usable 77%
c [bca-22] added 3990 blocked clauses in 383165 steps
c [phase-24] phase bias: 11 positive 41%, 16 negative 59%
c [simplification-23] removed 440 variables 2.7% (16002 remain 30%)
c [simplification-23] removed 6108 irredundant clauses 6.5% (87525 remain 28%)
c [simplification-23] maximum reduction of 7% = max (3%, 7%)
c [simplification-23] large reduction 7% >= 5% limit
c [simplification-23] new conflict interval 11103 = min (1110311/100, 216997)
c [simplification-23] penalized conflict interval 11103 = 1 * 11103
c [simplification-23] new conflict limit 1121414
c 
c [simplification-24] limit of 1121414 conflicts hit after 1121414 conflicts
c [ternres-22] limit 42735620 with penalty 0 = 0 + 0
c [ternres-22] all 16002 free variables schedulable
c [ternres-22] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-22] fully completed ternary resolution
c [simpleprobe-6] all 16002 free variables schedulable
c [simpleprobe-6] limit 170942483 penalty 0 = 0 + 0
c [decomp-35] removed 2 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 2 variables, found 5333 hbrs, 2 units
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 2 probes 0%
c [lift-17-1] found 0 units 0 impls in round 1
c [lift-17-2] found 0 units 0 impls in round 2
c [lift-17-3] found 0 units 0 impls in round 3
c [lift-17-4] found 0 units 0 impls in round 4
c [lift-17-5] found 0 units 0 impls in round 5
c [lift-17] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-17] 8766 variables remain 55% (7234 retained)
c [cliff-20] limit of 34188496 steps penalty 0 = 0 + 0
c [cliff-20] failed 0, lifted 0
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 348 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 16000 variables 100%
c [block-8] limit of 26709763 steps penalty 4 = 4 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 1 blocked clauses
c [block-8] 1 < 1/1000 * 87456 = 87 considered unsuccessful
c [cce-23] limit of 85471241 steps penalty 0 = 0 + 0
c [cce-23-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-23-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-23-1] eliminated 5 clauses out of 22 (23%) of length 61
c [cce-23-1] eliminated 7 clauses out of 29 (24%) of length 60
c [cce-23-1] eliminated 6 clauses out of 50 (12%) of length 57
c [cce-23-1] eliminated 6 clauses out of 104 (6%) of length 54
c [cce-23-1] eliminated 2 clauses out of 37 (5%) of length 52
c [cce-23-1] eliminated 9 clauses out of 222 (4%) of length 50
c [cce-23-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-23-1] eliminated 2 clauses out of 12 (17%) of length 19
c [cce-23-1] eliminated 2 clauses out of 21 (10%) of length 18
c [cce-23-1] eliminated 1 clauses out of 21 (5%) of length 16
c [cce-23-1] eliminated 2 clauses out of 20 (10%) of length 15
c [cce-23-1] eliminated 2 clauses out of 113 (2%) of length 7
c [cce-23-1] eliminated 9 clauses out of 172 (5%) of length 6
c [cce-23-1] eliminated 6 clauses out of 531 (1%) of length 5
c [cce-23-1] eliminated 31 clauses out of 983 (3%) of length 4
c [cce-23-1] completed large round (ACCE)
c [cce-23-1] eliminated 95 large clauses in 7946476 steps
c [cce-23-1] allowing another 3973238 steps for small clauses
c [cce-23] scheduling 83380 clauses = 82613 binary + 767 ternary
c [cce-23] tried to eliminate 8693 small clauses 10%
c [cce-23] eliminated 3945 small clauses 5%
c [cce-23] eliminated 3931 binary clauses 5%
c [cce-23] eliminated 14 ternary clauses 2%
c [cce-23-1] eliminated 3945 small clauses in 85471242 steps
c [cce-23-1] incomplete small round (ACCE)
c [cce-23-1] eliminated 4040 covered clauses in round 1
c [cce-23] eliminated 4040 covered clauses in TOTAL during 1 rounds
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 16000 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24-1] eliminated 213 variables 1% in round 1 in 9041949 steps
c [elim-24-1] backward subsumption/strengthening limit 18083898
c [elim-24-1] subsumed 0 and strengthened 0 clauses in 2171950 steps
c [elim-24] fully completed in 1 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 213 = 1% variables out of 16000
c [bca-23] limit of 10000000 steps
c [bca-23] 24198 out of 31576 literals actually usable 77%
c [bca-23] added 673 blocked clauses in 384885 steps
c [phase-25] phase bias: 7 positive 88%, 1 negative 12%
c [simplification-24] removed 215 variables 1.3% (15787 remain 30%)
c [simplification-24] removed 4395 irredundant clauses 5.0% (83130 remain 27%)
c [simplification-24] maximum reduction of 5% = max (1%, 5%)
c [simplification-24] large reduction 5% >= 5% limit
c [simplification-24] new conflict interval 11214 = min (1121414/100, 216997)
c [simplification-24] penalized conflict interval 11214 = 1 * 11214
c [simplification-24] new conflict limit 1132628
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  247.9   15786    83130   1128262   52299   2503 228661  10 27.0  61.0   32
c 
c [simplification-25] limit of 1132652 conflicts hit after 1132655 conflicts
c [ternres-23] limit 43004614 with penalty 0 = 0 + 0
c [ternres-23] all 15785 free variables schedulable
c [ternres-23] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-36] removed 3 variables
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 376 transitive binary clauses
c [cce-24] limit of 86009229 steps penalty 0 = 0 + 0
c [cce-24-1] eliminated 6 clauses out of 24 (25%) of length 61
c [cce-24-1] eliminated 8 clauses out of 29 (28%) of length 60
c [cce-24-1] eliminated 2 clauses out of 50 (4%) of length 57
c [cce-24-1] eliminated 1 clauses out of 106 (1%) of length 54
c [cce-24-1] eliminated 2 clauses out of 39 (5%) of length 52
c [cce-24-1] eliminated 2 clauses out of 222 (1%) of length 50
c [cce-24-1] eliminated 3 clauses out of 13 (23%) of length 19
c [cce-24-1] eliminated 1 clauses out of 20 (5%) of length 17
c [cce-24-1] eliminated 2 clauses out of 21 (10%) of length 16
c [cce-24-1] eliminated 9 clauses out of 530 (2%) of length 5
c [cce-24-1] eliminated 14 clauses out of 962 (1%) of length 4
c [cce-24-1] completed large round (ACCE)
c [cce-24-1] eliminated 50 large clauses in 8036298 steps
c [cce-24-1] allowing another 4018149 steps for small clauses
c [cce-24] scheduling 79593 clauses = 78298 binary + 1295 ternary
c [cce-24] tried to eliminate 9421 small clauses 12%
c [cce-24] eliminated 3876 small clauses 5%
c [cce-24] eliminated 3838 binary clauses 5%
c [cce-24] eliminated 38 ternary clauses 3%
c [cce-24-1] eliminated 3876 small clauses in 86009230 steps
c [cce-24-1] incomplete small round (ACCE)
c [cce-24-1] eliminated 3926 covered clauses in round 1
c [cce-24] eliminated 3926 covered clauses in TOTAL during 1 rounds
c [elim-25] scheduling all variables this time
c [elim-25] scheduled 15784 variables 100%
c [elim-25] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-25-1] eliminated 305 variables 2% in round 1 in 10487289 steps
c [elim-25-1] backward subsumption/strengthening limit 20974578
c [elim-25-1] subsumed 0 and strengthened 0 clauses in 2030096 steps
c [elim-25] fully completed in 1 rounds
c [elim-25] transition to [ all 0 rem 0 ] state
c [elim-25] eliminated 305 = 2% variables out of 15784
c [bca-24] limit of 10000000 steps
c [bca-24] 23529 out of 30960 literals actually usable 76%
c [bca-24] added 970 blocked clauses in 382685 steps
c [phase-26] phase bias: 3 positive 23%, 10 negative 77%
c [simplification-25] removed 306 variables 1.9% (15479 remain 29%)
c [simplification-25] removed 4652 irredundant clauses 5.6% (78478 remain 25%)
c [simplification-25] maximum reduction of 6% = max (2%, 6%)
c [simplification-25] large reduction 6% >= 5% limit
c [simplification-25] new conflict interval 11326 = min (1132655/100, 216997)
c [simplification-25] penalized conflict interval 11326 = 1 * 11326
c [simplification-25] new conflict limit 1143981
c 
c [simplification-26] limit of 1143987 conflicts hit after 1143987 conflicts
c [lift-18] limit 10000000 with penalty 1 = 1 + 0
c [lift-18] using 3 probes 0%
c [lift-18-1] found 1 units 0 impls in round 1
c [lift-18-2] found 0 units 0 impls in round 2
c [lift-18-3] found 0 units 0 impls in round 3
c [lift-18-4] found 0 units 0 impls in round 4
c [lift-18-5] found 0 units 0 impls in round 5
c [lift-18] 1 units, 0 impls, 0 eqs in 6 rounds
c [lift-18] 8658 variables remain 56% (6820 retained)
c [lift-18] removed 1 variables
c [cliff-21] limit of 17396820 steps penalty 1 = 1 + 0
c [cliff-21] failed 0, lifted 0
c [unhide-11] limit 543650 with penalty 4 = 4 + 0
c [unhide-11-11] 0 units, 0 failed, 1164 tauts, 0 hbrs, 156379 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 391 transitive binary clauses
c [cce-25] limit of 86984100 steps penalty 0 = 0 + 0
c [cce-25-1] eliminated 1 clauses out of 1 (100%) of length 108
c [cce-25-1] eliminated 1 clauses out of 1 (100%) of length 104
c [cce-25-1] eliminated 4 clauses out of 24 (17%) of length 61
c [cce-25-1] eliminated 15 clauses out of 32 (47%) of length 60
c [cce-25-1] eliminated 7 clauses out of 25 (28%) of length 59
c [cce-25-1] eliminated 2 clauses out of 50 (4%) of length 57
c [cce-25-1] eliminated 4 clauses out of 107 (4%) of length 54
c [cce-25-1] eliminated 6 clauses out of 41 (15%) of length 53
c [cce-25-1] eliminated 3 clauses out of 220 (1%) of length 50
c [cce-25-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-25-1] eliminated 1 clauses out of 1 (100%) of length 29
c [cce-25-1] eliminated 3 clauses out of 16 (19%) of length 19
c [cce-25-1] eliminated 2 clauses out of 120 (2%) of length 7
c [cce-25-1] eliminated 4 clauses out of 165 (2%) of length 6
c [cce-25-1] eliminated 8 clauses out of 515 (2%) of length 5
c [cce-25-1] eliminated 24 clauses out of 972 (2%) of length 4
c [cce-25-1] completed large round (ACCE)
c [cce-25-1] eliminated 87 large clauses in 7968651 steps
c [cce-25-1] allowing another 3984325 steps for small clauses
c [cce-25] scheduling 74421 clauses = 73202 binary + 1219 ternary
c [cce-25] tried to eliminate 9960 small clauses 13%
c [cce-25] eliminated 3721 small clauses 5%
c [cce-25] eliminated 3687 binary clauses 5%
c [cce-25] eliminated 34 ternary clauses 3%
c [cce-25-1] eliminated 3721 small clauses in 86984101 steps
c [cce-25-1] incomplete small round (ACCE)
c [cce-25-1] eliminated 3808 covered clauses in round 1
c [cce-25] eliminated 3808 covered clauses in TOTAL during 1 rounds
c [elim-26] scheduling all variables this time
c [elim-26] scheduled 15478 variables 100%
c [elim-26] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-26-1] eliminated 329 variables 2% in round 1 in 7962366 steps
c [elim-26-1] backward subsumption/strengthening limit 15924732
c [elim-26-1] subsumed 0 and strengthened 0 clauses in 1821384 steps
c [elim-26] fully completed in 1 rounds
c [elim-26] transition to [ all 0 rem 0 ] state
c [elim-26] eliminated 329 = 2% variables out of 15478
c [bca-25] limit of 10000000 steps
c [bca-25] 22756 out of 30300 literals actually usable 75%
c [bca-25] added 2067 blocked clauses in 383070 steps
c [phase-27] phase bias: 26 positive 62%, 16 negative 38%
c [simplification-26] removed 330 variables 2.1% (15149 remain 28%)
c [simplification-26] removed 5228 irredundant clauses 6.7% (73250 remain 24%)
c [simplification-26] maximum reduction of 7% = max (2%, 7%)
c [simplification-26] large reduction 7% >= 5% limit
c [simplification-26] new conflict interval 11439 = min (1143987/100, 216997)
c [simplification-26] penalized conflict interval 11439 = 1 * 11439
c [simplification-26] new conflict limit 1155426
c 
c [simplification-27] limit of 1155432 conflicts hit after 1155432 conflicts
c [ternres-24] limit 22018881 with penalty 1 = 1 + 0
c [ternres-24] all 15149 free variables schedulable
c [ternres-24] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-24] fully completed ternary resolution
c [lift-19] limit 20000000 with penalty 0 = 0 + 0
c [lift-19] using 12 probes 0%
c [lift-19-1] found 0 units 0 impls in round 1
c [lift-19-2] found 0 units 0 impls in round 2
c [lift-19-3] found 0 units 3 impls in round 3
c [lift-19-4] found 0 units 1 impls in round 4
c [lift-19-5] found 0 units 0 impls in round 5
c [lift-19] 0 units, 4 impls, 0 eqs in 6 rounds
c [lift-19] 8537 variables remain 56% (6612 retained)
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 411 transitive binary clauses
c [cce-26] limit of 88075524 steps penalty 0 = 0 + 0
c [cce-26-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-26-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-26-1] eliminated 5 clauses out of 25 (20%) of length 61
c [cce-26-1] eliminated 8 clauses out of 27 (30%) of length 60
c [cce-26-1] eliminated 4 clauses out of 25 (16%) of length 59
c [cce-26-1] eliminated 2 clauses out of 50 (4%) of length 57
c [cce-26-1] eliminated 14 clauses out of 110 (13%) of length 54
c [cce-26-1] eliminated 1 clauses out of 38 (3%) of length 52
c [cce-26-1] eliminated 1 clauses out of 3 (33%) of length 51
c [cce-26-1] eliminated 3 clauses out of 218 (1%) of length 50
c [cce-26-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-26-1] eliminated 1 clauses out of 11 (9%) of length 21
c [cce-26-1] eliminated 1 clauses out of 38 (3%) of length 11
c [cce-26-1] eliminated 3 clauses out of 113 (3%) of length 7
c [cce-26-1] eliminated 11 clauses out of 519 (2%) of length 5
c [cce-26-1] eliminated 11 clauses out of 936 (1%) of length 4
c [cce-26-1] completed large round (ACCE)
c [cce-26-1] eliminated 70 large clauses in 7845530 steps
c [cce-26-1] allowing another 3922765 steps for small clauses
c [cce-26] scheduling 69816 clauses = 68645 binary + 1171 ternary
c [cce-26] tried to eliminate 10403 small clauses 15%
c [cce-26] eliminated 3412 small clauses 5%
c [cce-26] eliminated 3371 binary clauses 5%
c [cce-26] eliminated 41 ternary clauses 4%
c [cce-26-1] eliminated 3412 small clauses in 88075525 steps
c [cce-26-1] incomplete small round (ACCE)
c [cce-26-1] eliminated 3482 covered clauses in round 1
c [cce-26] eliminated 3482 covered clauses in TOTAL during 1 rounds
c [elim-27] scheduling all variables this time
c [elim-27] scheduled 15149 variables 100%
c [elim-27] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-27-1] eliminated 306 variables 2% in round 1 in 14209293 steps
c [elim-27-1] backward subsumption/strengthening limit 28418586
c [elim-27-1] subsumed 0 and strengthened 0 clauses in 1740531 steps
c [elim-27] fully completed in 1 rounds
c [elim-27] transition to [ all 0 rem 0 ] state
c [elim-27] eliminated 306 = 2% variables out of 15149
c [bca-26] limit of 10000000 steps
c [bca-26] 22166 out of 29688 literals actually usable 75%
c [bca-26] added 1762 blocked clauses in 385805 steps
c [phase-28] phase bias: 10 positive 59%, 7 negative 41%
c [simplification-27] removed 306 variables 2.0% (14843 remain 28%)
c [simplification-27] removed 4182 irredundant clauses 5.7% (69068 remain 22%)
c [simplification-27] maximum reduction of 6% = max (2%, 6%)
c [simplification-27] large reduction 6% >= 5% limit
c [simplification-27] new conflict interval 11554 = min (1155432/100, 216997)
c [simplification-27] penalized conflict interval 11554 = 1 * 11554
c [simplification-27] new conflict limit 1166986
c [tabula-rasa-2] number clauses 69068 drops below limit 70279
c [flush-cache] 0 binary, 0 ternary, 62094 large
c [flushphases] 14843 phases reset fully
c [phase-29] phase bias: 214 positive 38%, 355 negative 62%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] conflict limit 20000 does not change
c [tabula-rasa-2] new variable limit 3710 and clause limit 34534
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  263.8   14843    69068   1160312    2187   2605 226685   2 26.9  61.0   20
c -  264.2   14843    69068   1163930    2822   2611 226685   2 26.9  60.9   20
c 
c [simplification-28] limit of 1166992 conflicts hit after 1166993 conflicts
c [ternres-25] limit 44324214 with penalty 0 = 0 + 0
c [ternres-25] all 14843 free variables schedulable
c [ternres-25] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-25] fully completed ternary resolution
c [card-7] limit 1385131 penalty 4 = 4 + 0
c [card-7] found 6760 at-most-one constraints of average size 12.7
c [card-7] no at-most-two constraint found
c [card-7] using previous limit 1385131 for elimination
c [card-7] 6760 out of 6760 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] no at-most-one constraints generated
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 312 transitive binary clauses
c [cce-27] limit of 88648429 steps penalty 0 = 0 + 0
c [cce-27-1] eliminated 1 clauses out of 1 (100%) of length 106
c [cce-27-1] eliminated 4 clauses out of 4 (100%) of length 104
c [cce-27-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-27-1] eliminated 2 clauses out of 23 (9%) of length 60
c [cce-27-1] eliminated 4 clauses out of 25 (16%) of length 59
c [cce-27-1] eliminated 1 clauses out of 1 (100%) of length 58
c [cce-27-1] eliminated 7 clauses out of 50 (14%) of length 57
c [cce-27-1] eliminated 16 clauses out of 110 (15%) of length 54
c [cce-27-1] eliminated 2 clauses out of 39 (5%) of length 52
c [cce-27-1] eliminated 10 clauses out of 222 (5%) of length 50
c [cce-27-1] eliminated 1 clauses out of 33 (3%) of length 10
c [cce-27-1] eliminated 1 clauses out of 39 (3%) of length 9
c [cce-27-1] eliminated 1 clauses out of 114 (1%) of length 7
c [cce-27-1] eliminated 6 clauses out of 164 (4%) of length 6
c [cce-27-1] eliminated 5 clauses out of 507 (1%) of length 5
c [cce-27-1] eliminated 19 clauses out of 932 (2%) of length 4
c [cce-27-1] completed large round (ACCE)
c [cce-27-1] eliminated 81 large clauses in 7793194 steps
c [cce-27-1] allowing another 3896597 steps for small clauses
c [cce-27] scheduling 65243 clauses = 64559 binary + 684 ternary
c [cce-27] tried to eliminate 10978 small clauses 17%
c [cce-27] eliminated 3464 small clauses 5%
c [cce-27] eliminated 3450 binary clauses 5%
c [cce-27] eliminated 14 ternary clauses 2%
c [cce-27-1] eliminated 3464 small clauses in 88648430 steps
c [cce-27-1] incomplete small round (ACCE)
c [cce-27-1] eliminated 3545 covered clauses in round 1
c [cce-27] eliminated 3545 covered clauses in TOTAL during 1 rounds
c [elim-28] scheduling all variables this time
c [elim-28] scheduled 14843 variables 100%
c [elim-28] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-28-1] eliminated 321 variables 2% in round 1 in 16285984 steps
c [elim-28-1] backward subsumption/strengthening limit 32571968
c [elim-28-1] subsumed 0 and strengthened 0 clauses in 1606077 steps
c [elim-28] fully completed in 1 rounds
c [elim-28] transition to [ all 0 rem 0 ] state
c [elim-28] eliminated 321 = 2% variables out of 14843
c [bca-27] limit of 10000000 steps
c [bca-27] 24945 out of 29046 literals actually usable 86%
c [bca-27] added 4091 blocked clauses in 334028 steps
c [rephase-10] after 1166993 conflicts (new increment 20000, next 1186993)
c [flushphases] 2507 phases reset
c [phase-30] phase bias: 16 positive 33%, 32 negative 67%
c [simplification-28] removed 321 variables 2.2% (14522 remain 27%)
c [simplification-28] removed 4499 irredundant clauses 6.5% (64569 remain 21%)
c [simplification-28] maximum reduction of 7% = max (2%, 7%)
c [simplification-28] large reduction 7% >= 5% limit
c [simplification-28] new conflict interval 11669 = min (1166993/100, 20000)
c [simplification-28] penalized conflict interval 11669 = 1 * 11669
c [simplification-28] new conflict limit 1178662
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  268.9   14522    64569   1169352    3492   2610 226592   6 27.0  61.0   18
c -  269.3   14522    64569   1174863    4126   2614 226593   4 27.1  61.2   18
c 
c [simplification-29] limit of 1178662 conflicts hit after 1178663 conflicts
c [ternres-26] limit 44531287 with penalty 0 = 0 + 0
c [ternres-26] all 14522 free variables schedulable
c [ternres-26] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-26] fully completed ternary resolution
c [lift-20] limit 10000000 with penalty 1 = 1 + 0
c [lift-20] using 1 probes 0%
c [lift-20-1] found 0 units 1 impls in round 1
c [lift-20-2] found 0 units 0 impls in round 2
c [lift-20-3] found 0 units 0 impls in round 3
c [lift-20-4] found 0 units 0 impls in round 4
c [lift-20-5] found 0 units 0 impls in round 5
c [lift-20] 0 units, 1 impls, 0 eqs in 6 rounds
c [lift-20] 8298 variables remain 57% (6224 retained)
c [cliff-22] limit of 8906257 steps penalty 2 = 2 + 0
c [cliff-22] failed 0, lifted 0
c [transred-27] limit 2000000 with penalty 0 = 0 + 0
c [transred-27] removed 363 transitive binary clauses
c [cce-28] limit of 89062575 steps penalty 0 = 0 + 0
c [cce-28-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-28-1] eliminated 1 clauses out of 1 (100%) of length 102
c [cce-28-1] eliminated 3 clauses out of 3 (100%) of length 101
c [cce-28-1] eliminated 5 clauses out of 24 (21%) of length 61
c [cce-28-1] eliminated 6 clauses out of 23 (26%) of length 60
c [cce-28-1] eliminated 3 clauses out of 26 (12%) of length 59
c [cce-28-1] eliminated 8 clauses out of 51 (16%) of length 57
c [cce-28-1] eliminated 4 clauses out of 111 (4%) of length 54
c [cce-28-1] eliminated 2 clauses out of 42 (5%) of length 53
c [cce-28-1] eliminated 7 clauses out of 220 (3%) of length 50
c [cce-28-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-28-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-28-1] eliminated 1 clauses out of 9 (11%) of length 21
c [cce-28-1] eliminated 1 clauses out of 11 (9%) of length 19
c [cce-28-1] eliminated 1 clauses out of 19 (5%) of length 18
c [cce-28-1] eliminated 1 clauses out of 19 (5%) of length 17
c [cce-28-1] eliminated 1 clauses out of 20 (5%) of length 16
c [cce-28-1] eliminated 1 clauses out of 20 (5%) of length 13
c [cce-28-1] eliminated 1 clauses out of 76 (1%) of length 8
c [cce-28-1] eliminated 1 clauses out of 112 (1%) of length 7
c [cce-28-1] eliminated 2 clauses out of 156 (1%) of length 6
c [cce-28-1] eliminated 14 clauses out of 496 (3%) of length 5
c [cce-28-1] eliminated 12 clauses out of 913 (1%) of length 4
c [cce-28-1] completed large round (ACCE)
c [cce-28-1] eliminated 81 large clauses in 7928648 steps
c [cce-28-1] allowing another 3964324 steps for small clauses
c [cce-28] scheduling 60828 clauses = 60163 binary + 665 ternary
c [cce-28] tried to eliminate 10999 small clauses 18%
c [cce-28] eliminated 2936 small clauses 5%
c [cce-28] eliminated 2916 binary clauses 5%
c [cce-28] eliminated 20 ternary clauses 3%
c [cce-28-1] eliminated 2936 small clauses in 89062576 steps
c [cce-28-1] incomplete small round (ACCE)
c [cce-28-1] eliminated 3017 covered clauses in round 1
c [cce-28] eliminated 3017 covered clauses in TOTAL during 1 rounds
c [elim-29] scheduling all variables this time
c [elim-29] scheduled 14522 variables 100%
c [elim-29] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-29-1] eliminated 322 variables 2% in round 1 in 9667890 steps
c [elim-29-1] backward subsumption/strengthening limit 19335780
c [elim-29-1] subsumed 0 and strengthened 0 clauses in 1453236 steps
c [elim-29] fully completed in 1 rounds
c [elim-29] transition to [ all 0 rem 0 ] state
c [elim-29] eliminated 322 = 2% variables out of 14522
c [bca-28] limit of 10000000 steps
c [bca-28] 23818 out of 28402 literals actually usable 84%
c [bca-28] added 1336 blocked clauses in 328324 steps
c [phase-31] phase bias: 14 positive 67%, 7 negative 33%
c [simplification-29] removed 322 variables 2.2% (14200 remain 27%)
c [simplification-29] removed 3736 irredundant clauses 5.8% (60833 remain 20%)
c [simplification-29] maximum reduction of 6% = max (2%, 6%)
c [simplification-29] large reduction 6% >= 5% limit
c [simplification-29] new conflict interval 11786 = min (1178663/100, 20000)
c [simplification-29] penalized conflict interval 11786 = 1 * 11786
c [simplification-29] new conflict limit 1190449
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  273.3   14200    60833   1181010    4740   2606 223842   5 27.1  61.2   19
c -  273.7   14200    60833   1186624    5490   2610 223842   4 27.1  61.2   19
c 
c [simplification-30] limit of 1190451 conflicts hit after 1190451 conflicts
c [ternres-27] limit 44721922 with penalty 0 = 0 + 0
c [ternres-27] all 14200 free variables schedulable
c [ternres-27] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-27] fully completed ternary resolution
c [gauss-7] limit 559024 penalty 4 = 4 + 0
c [gauss-7] extracted 1 xors of average arity 3.0
c [gauss-7] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-7] limit 559024 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 139756 penalty 4 = 4 + 0 boost 1
c [treelook-6] scheduled 14501 literals 51%
c [treelook-6] scheduling used 139834 steps
c [treelook-6] not fully scheduled
c [treelook-6] limit 139756 penalty 4 = 4 + 0 boost 1
c [treelook-6] used 214789 steps
c [treelook-6] 14497 literals remain 51%
c [treelook-6] 9571 variables remain to probed next time 67%
c [treelook-6] removed 0 variables, found 8 hbrs
c [cgrclsr-7] limit 279512 penalty 4 = 4 + 0
c [cgrclsr-7] all 14200 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [transred-28] limit 2000000 with penalty 0 = 0 + 0
c [transred-28] removed 273 transitive binary clauses
c [cce-29] limit of 89443844 steps penalty 0 = 0 + 0
c [cce-29-1] eliminated 1 clauses out of 1 (100%) of length 102
c [cce-29-1] eliminated 2 clauses out of 2 (100%) of length 101
c [cce-29-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-29-1] eliminated 3 clauses out of 26 (12%) of length 61
c [cce-29-1] eliminated 6 clauses out of 21 (29%) of length 60
c [cce-29-1] eliminated 6 clauses out of 51 (12%) of length 57
c [cce-29-1] eliminated 14 clauses out of 113 (12%) of length 54
c [cce-29-1] eliminated 6 clauses out of 46 (13%) of length 53
c [cce-29-1] eliminated 7 clauses out of 217 (3%) of length 50
c [cce-29-1] eliminated 2 clauses out of 4 (50%) of length 35
c [cce-29-1] eliminated 1 clauses out of 34 (3%) of length 11
c [cce-29-1] eliminated 2 clauses out of 27 (7%) of length 10
c [cce-29-1] eliminated 1 clauses out of 40 (2%) of length 9
c [cce-29-1] eliminated 4 clauses out of 79 (5%) of length 8
c [cce-29-1] eliminated 8 clauses out of 118 (7%) of length 7
c [cce-29-1] eliminated 19 clauses out of 155 (12%) of length 6
c [cce-29-1] eliminated 9 clauses out of 474 (2%) of length 5
c [cce-29-1] eliminated 15 clauses out of 882 (2%) of length 4
c [cce-29-1] completed large round (ACCE)
c [cce-29-1] eliminated 108 large clauses in 7863985 steps
c [cce-29-1] allowing another 3931992 steps for small clauses
c [cce-29] scheduling 57589 clauses = 56527 binary + 1062 ternary
c [cce-29] tried to eliminate 11459 small clauses 20%
c [cce-29] eliminated 2522 small clauses 4%
c [cce-29] eliminated 2484 binary clauses 4%
c [cce-29] eliminated 38 ternary clauses 4%
c [cce-29-1] eliminated 2522 small clauses in 89443845 steps
c [cce-29-1] incomplete small round (ACCE)
c [cce-29-1] eliminated 2630 covered clauses in round 1
c [cce-29] eliminated 2630 covered clauses in TOTAL during 1 rounds
c [elim-30] scheduling all variables this time
c [elim-30] scheduled 14200 variables 100%
c [elim-30] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-30-1] eliminated 238 variables 2% in round 1 in 4221003 steps
c [elim-30-1] backward subsumption/strengthening limit 8442006
c [elim-30-1] subsumed 0 and strengthened 0 clauses in 1279038 steps
c [elim-30] fully completed in 1 rounds
c [elim-30] transition to [ all 0 rem 0 ] state
c [elim-30] eliminated 238 = 2% variables out of 14200
c [bca-29] limit of 10000000 steps
c [bca-29] 23642 out of 27926 literals actually usable 85%
c [bca-29] added 1166 blocked clauses in 327276 steps
c [rephase-11] after 1190451 conflicts (new increment 40000, next 1230451)
c [flushphases] 2254 phases reset
c [phase-32] phase bias: 16 positive 53%, 14 negative 47%
c [simplification-30] removed 238 variables 1.7% (13962 remain 26%)
c [simplification-30] removed 3021 irredundant clauses 5.0% (57812 remain 19%)
c [simplification-30] maximum reduction of 5% = max (2%, 5%)
c [simplification-30] large reduction 5% >= 5% limit
c [simplification-30] new conflict interval 11904 = min (1190451/100, 20000)
c [simplification-30] penalized conflict interval 11904 = 1 * 11904
c [simplification-30] new conflict limit 1202355
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  277.2   13962    57812   1193258    6165   2615 221525   2 27.1  61.1   19
c -  278.0   13962    57812   1202035    6810   2617 221526   2 27.1  61.1   19
c 
c [simplification-31] limit of 1202357 conflicts hit after 1202357 conflicts
c [decomp-43] removed 1 variables
c [basicprobe-6] limit 45049226 penalty 0 = 0 + 0
c [basicprobe-6-0] 1010 probes remain 7% after last round
c [basicprobe-6-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-6-0] removed 10 variables, found 1005 hbrs
c [bate-4] eliminated 4 asymmetric tautologies during probing
c [transred-29] limit 2000000 with penalty 0 = 0 + 0
c [transred-29] removed 246 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 13951 variables 100%
c [block-9] limit of 28155766 steps penalty 4 = 4 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 23 blocked clauses
c [block-9] 23 < 1/1000 * 57778 = 57 considered unsuccessful
c [cce-30] limit of 90098453 steps penalty 0 = 0 + 0
c [cce-30-1] eliminated 1 clauses out of 1 (100%) of length 101
c [cce-30-1] eliminated 3 clauses out of 26 (12%) of length 61
c [cce-30-1] eliminated 4 clauses out of 21 (19%) of length 60
c [cce-30-1] eliminated 12 clauses out of 25 (48%) of length 59
c [cce-30-1] eliminated 14 clauses out of 53 (26%) of length 57
c [cce-30-1] eliminated 14 clauses out of 113 (12%) of length 54
c [cce-30-1] eliminated 6 clauses out of 44 (14%) of length 53
c [cce-30-1] eliminated 8 clauses out of 45 (18%) of length 52
c [cce-30-1] eliminated 1 clauses out of 12 (8%) of length 20
c [cce-30-1] eliminated 1 clauses out of 12 (8%) of length 19
c [cce-30-1] eliminated 1 clauses out of 33 (3%) of length 11
c [cce-30-1] eliminated 1 clauses out of 40 (2%) of length 9
c [cce-30-1] eliminated 1 clauses out of 73 (1%) of length 8
c [cce-30-1] eliminated 5 clauses out of 115 (4%) of length 7
c [cce-30-1] eliminated 3 clauses out of 135 (2%) of length 6
c [cce-30-1] eliminated 2 clauses out of 457 (0%) of length 5
c [cce-30-1] eliminated 15 clauses out of 886 (2%) of length 4
c [cce-30-1] completed large round (ACCE)
c [cce-30-1] eliminated 92 large clauses in 7578628 steps
c [cce-30-1] allowing another 3789314 steps for small clauses
c [cce-30] scheduling 54175 clauses = 53553 binary + 622 ternary
c [cce-30] tried to eliminate 11777 small clauses 22%
c [cce-30] eliminated 2276 small clauses 4%
c [cce-30] eliminated 2260 binary clauses 4%
c [cce-30] eliminated 16 ternary clauses 3%
c [cce-30-1] eliminated 2276 small clauses in 90098454 steps
c [cce-30-1] incomplete small round (ACCE)
c [cce-30-1] eliminated 2368 covered clauses in round 1
c [cce-30] eliminated 2368 covered clauses in TOTAL during 1 rounds
c [elim-31] scheduling all variables this time
c [elim-31] scheduled 13949 variables 100%
c [elim-31] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-31-1] eliminated 250 variables 2% in round 1 in 5965190 steps
c [elim-31-1] backward subsumption/strengthening limit 11930380
c [elim-31-1] subsumed 0 and strengthened 0 clauses in 1210184 steps
c [elim-31] fully completed in 1 rounds
c [elim-31] transition to [ all 0 rem 0 ] state
c [elim-31] eliminated 250 = 2% variables out of 13949
c [bca-30] limit of 10000000 steps
c [bca-30] 23470 out of 27400 literals actually usable 86%
c [bca-30] added 2232 blocked clauses in 323535 steps
c [phase-33] phase bias: 7 positive 32%, 15 negative 68%
c [simplification-31] removed 263 variables 1.9% (13699 remain 26%)
c [simplification-31] removed 2925 irredundant clauses 5.1% (54887 remain 18%)
c [simplification-31] maximum reduction of 5% = max (2%, 5%)
c [simplification-31] large reduction 5% >= 5% limit
c [simplification-31] new conflict interval 12023 = min (1202357/100, 20000)
c [simplification-31] penalized conflict interval 12023 = 1 * 12023
c [simplification-31] new conflict limit 1214380
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  282.8   13699    54887   1209095    7514   2578 217816   6 27.0  61.1   19
c 
c [simplification-32] limit of 1214380 conflicts hit after 1214382 conflicts
c [ternres-28] limit 22618246 with penalty 1 = 1 + 0
c [ternres-28] all 13699 free variables schedulable
c [ternres-28] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-28] fully completed ternary resolution
c [simpleprobe-7] all 13699 free variables schedulable
c [simpleprobe-7] limit 180945970 penalty 0 = 0 + 0
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 0 variables, found 1254 hbrs, 0 units
c [lift-21] limit 5000000 with penalty 2 = 2 + 0
c [lift-21] using 1 probes 0%
c [lift-21-1] found 0 units 0 impls in round 1
c [lift-21-2] found 0 units 0 impls in round 2
c [lift-21-3] found 0 units 0 impls in round 3
c [lift-21-4] found 0 units 0 impls in round 4
c [lift-21-5] found 0 units 0 impls in round 5
c [lift-21] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-21] 8017 variables remain 59% (5682 retained)
c [transred-30] limit 2000000 with penalty 0 = 0 + 0
c [transred-30] removed 255 transitive binary clauses
c [cce-31] limit of 90472985 steps penalty 0 = 0 + 0
c [cce-31-1] eliminated 2 clauses out of 23 (9%) of length 61
c [cce-31-1] eliminated 8 clauses out of 21 (38%) of length 60
c [cce-31-1] eliminated 13 clauses out of 28 (46%) of length 59
c [cce-31-1] eliminated 10 clauses out of 50 (20%) of length 57
c [cce-31-1] eliminated 20 clauses out of 111 (18%) of length 54
c [cce-31-1] eliminated 6 clauses out of 44 (14%) of length 53
c [cce-31-1] eliminated 8 clauses out of 46 (17%) of length 52
c [cce-31-1] eliminated 5 clauses out of 229 (2%) of length 50
c [cce-31-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-31-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-31-1] eliminated 1 clauses out of 11 (9%) of length 20
c [cce-31-1] eliminated 2 clauses out of 11 (18%) of length 19
c [cce-31-1] eliminated 1 clauses out of 74 (1%) of length 8
c [cce-31-1] eliminated 1 clauses out of 128 (1%) of length 6
c [cce-31-1] eliminated 6 clauses out of 460 (1%) of length 5
c [cce-31-1] eliminated 9 clauses out of 875 (1%) of length 4
c [cce-31-1] completed large round (ACCE)
c [cce-31-1] eliminated 94 large clauses in 7673135 steps
c [cce-31-1] allowing another 3836567 steps for small clauses
c [cce-31] scheduling 51743 clauses = 50739 binary + 1004 ternary
c [cce-31] tried to eliminate 12213 small clauses 24%
c [cce-31] eliminated 1806 small clauses 3%
c [cce-31] eliminated 1777 binary clauses 4%
c [cce-31] eliminated 29 ternary clauses 3%
c [cce-31-1] eliminated 1806 small clauses in 90472986 steps
c [cce-31-1] incomplete small round (ACCE)
c [cce-31-1] eliminated 1900 covered clauses in round 1
c [cce-31] eliminated 1900 covered clauses in TOTAL during 1 rounds
c [elim-32] scheduling all variables this time
c [elim-32] scheduled 13699 variables 100%
c [elim-32] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-32-1] eliminated 222 variables 2% in round 1 in 4243338 steps
c [elim-32-1] backward subsumption/strengthening limit 8486676
c [elim-32-1] subsumed 0 and strengthened 0 clauses in 1138462 steps
c [elim-32] fully completed in 1 rounds
c [elim-32] transition to [ all 0 rem 0 ] state
c [elim-32] eliminated 222 = 2% variables out of 13699
c [bca-31] limit of 10000000 steps
c [bca-31] 23440 out of 26956 literals actually usable 87%
c [bca-31] added 3109 blocked clauses in 327791 steps
c [phase-34] phase bias: 21 positive 64%, 12 negative 36%
c [simplification-32] removed 222 variables 1.6% (13477 remain 25%)
c [simplification-32] removed 2433 irredundant clauses 4.4% (52454 remain 17%)
c [simplification-32] maximum reduction of 4% = max (2%, 4%)
c [simplification-32] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-32] new conflict interval 24000
c [simplification-32] penalized conflict interval 24000 = 1 * 24000
c [simplification-32] new conflict limit 1238382
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  286.4   13477    52454   1216969    8156   2601 215337   2 26.9  61.1   20
c -  287.6   13477    52454   1226315    9046   2623 215344   1 26.9  61.0   20
c -  288.6   13477    52454   1236296    9936   2649 215347   4 26.8  60.9   20
c 
c [simplification-33] limit of 1238408 conflicts hit after 1238409 conflicts
c [ternres-29] limit 45962171 with penalty 0 = 0 + 0
c [ternres-29] all 13477 free variables schedulable
c [ternres-29] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-29] fully completed ternary resolution
c [cliff-23] limit of 4596217 steps penalty 3 = 3 + 0
c [cliff-23] failed 0, lifted 0
c [unhide-12] limit 574527 with penalty 4 = 4 + 0
c [unhide-12-12] 0 units, 0 failed, 19992 tauts, 0 hbrs, 19280 literals
c [transred-31] limit 2000000 with penalty 0 = 0 + 0
c [transred-31] removed 62 transitive binary clauses
c [cce-32] limit of 91924342 steps penalty 0 = 0 + 0
c [cce-32-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-32-1] eliminated 2 clauses out of 19 (11%) of length 60
c [cce-32-1] eliminated 12 clauses out of 29 (41%) of length 59
c [cce-32-1] eliminated 6 clauses out of 52 (12%) of length 57
c [cce-32-1] eliminated 2 clauses out of 111 (2%) of length 54
c [cce-32-1] eliminated 1 clauses out of 230 (0%) of length 50
c [cce-32-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-32-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-32-1] eliminated 1 clauses out of 22 (5%) of length 15
c [cce-32-1] eliminated 1 clauses out of 71 (1%) of length 8
c [cce-32-1] eliminated 2 clauses out of 113 (2%) of length 7
c [cce-32-1] eliminated 2 clauses out of 441 (0%) of length 5
c [cce-32-1] eliminated 2 clauses out of 843 (0%) of length 4
c [cce-32-1] completed large round (ACCE)
c [cce-32-1] eliminated 37 large clauses in 7735072 steps
c [cce-32-1] allowing another 3867536 steps for small clauses
c [cce-32] scheduling 49008 clauses = 48418 binary + 590 ternary
c [cce-32] tried to eliminate 12042 small clauses 25%
c [cce-32] eliminated 1448 small clauses 3%
c [cce-32] eliminated 1432 binary clauses 3%
c [cce-32] eliminated 16 ternary clauses 3%
c [cce-32-1] eliminated 1448 small clauses in 91924343 steps
c [cce-32-1] incomplete small round (ACCE)
c [cce-32-1] eliminated 1485 covered clauses in round 1
c [cce-32] eliminated 1485 covered clauses in TOTAL during 1 rounds
c [elim-33] scheduling all variables this time
c [elim-33] scheduled 13477 variables 100%
c [elim-33] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-33-1] eliminated 220 variables 2% in round 1 in 3078833 steps
c [elim-33-1] backward subsumption/strengthening limit 6157666
c [elim-33-1] subsumed 0 and strengthened 0 clauses in 1061649 steps
c [elim-33] fully completed in 1 rounds
c [elim-33] transition to [ all 0 rem 0 ] state
c [elim-33] eliminated 220 = 2% variables out of 13477
c [bca-32] limit of 10000000 steps
c [bca-32] 22494 out of 26516 literals actually usable 85%
c [bca-32] added 15325 blocked clauses in 320669 steps
c [rephase-12] after 1238409 conflicts (new increment 80000, next 1318409)
c [flushphases] 1807 phases reset
c [phase-35] phase bias: 7 positive 47%, 8 negative 53%
c [simplification-33] removed 220 variables 1.6% (13257 remain 25%)
c [simplification-33] removed 1932 irredundant clauses 3.7% (50522 remain 16%)
c [simplification-33] maximum reduction of 4% = max (2%, 4%)
c [simplification-33] geometric conflict interval increment 4800 = 24000 / 5
c [simplification-33] new conflict interval 28800
c [simplification-33] penalized conflict interval 28800 = 1 * 28800
c [simplification-33] new conflict limit 1267209
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  292.8   13257    50522   1247821   10645   2624 203858   3 26.9  61.0   20
c R  293.3   13257    50522   1253491   14505   2624 203858   2 27.0  61.1   25
c -  294.1   13257    50522   1259289   11303   2645 203873   1 26.9  61.1   20
c 
c [simplification-34] limit of 1267247 conflicts hit after 1267247 conflicts
c [ternres-30] limit 46762129 with penalty 0 = 0 + 0
c [ternres-30] all 13257 free variables schedulable
c [ternres-30] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-30] fully completed ternary resolution
c [transred-32] limit 2000000 with penalty 0 = 0 + 0
c [transred-32] removed 59 transitive binary clauses
c [cce-33] limit of 93524258 steps penalty 0 = 0 + 0
c [cce-33-1] eliminated 9 clauses out of 20 (45%) of length 60
c [cce-33-1] eliminated 12 clauses out of 26 (46%) of length 59
c [cce-33-1] eliminated 8 clauses out of 52 (15%) of length 57
c [cce-33-1] eliminated 6 clauses out of 109 (6%) of length 54
c [cce-33-1] eliminated 5 clauses out of 42 (12%) of length 53
c [cce-33-1] eliminated 8 clauses out of 229 (3%) of length 50
c [cce-33-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-33-1] eliminated 2 clauses out of 445 (0%) of length 5
c [cce-33-1] eliminated 4 clauses out of 844 (0%) of length 4
c [cce-33-1] completed large round (ACCE)
c [cce-33-1] eliminated 56 large clauses in 7488608 steps
c [cce-33-1] allowing another 3744304 steps for small clauses
c [cce-33] scheduling 47510 clauses = 46523 binary + 987 ternary
c [cce-33] tried to eliminate 13008 small clauses 27%
c [cce-33] eliminated 1134 small clauses 2%
c [cce-33] eliminated 1092 binary clauses 2%
c [cce-33] eliminated 42 ternary clauses 4%
c [cce-33-1] eliminated 1134 small clauses in 93524259 steps
c [cce-33-1] incomplete small round (ACCE)
c [cce-33-1] eliminated 1190 covered clauses in round 1
c [cce-33] eliminated 1190 covered clauses in TOTAL during 1 rounds
c [elim-34] scheduling all variables this time
c [elim-34] scheduled 13257 variables 100%
c [elim-34] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-34-1] eliminated 176 variables 1% in round 1 in 3131810 steps
c [elim-34-1] backward subsumption/strengthening limit 6263620
c [elim-34-1] subsumed 0 and strengthened 0 clauses in 1021826 steps
c [elim-34] fully completed in 1 rounds
c [elim-34] transition to [ all 0 rem 0 ] state
c [elim-34] eliminated 176 = 1% variables out of 13257
c [bca-33] limit of 10000000 steps
c [bca-33] 20820 out of 26164 literals actually usable 80%
c [bca-33] added 1379 blocked clauses in 318453 steps
c [phase-36] phase bias: 5 positive 50%, 5 negative 50%
c [simplification-34] removed 176 variables 1.3% (13081 remain 24%)
c [simplification-34] removed 1514 irredundant clauses 3.0% (49008 remain 16%)
c [simplification-34] maximum reduction of 3% = max (1%, 3%)
c [simplification-34] geometric conflict interval increment 7200 = 28800 / 4
c [simplification-34] new conflict interval 36000
c [simplification-34] penalized conflict interval 36000 = 1 * 36000
c [simplification-34] new conflict limit 1303247
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  298.3   13081    49008   1270649   12331   2714 198932   3 26.9  61.0   20
c -  299.7   13081    49008   1283200   13162   2762 198942   2 26.8  60.9   21
c -  301.2   13081    49008   1295469   14007   2784 198945   2 26.8  60.8   21
c 
c [simplification-35] limit of 1303285 conflicts hit after 1303285 conflicts
c [ternres-31] limit 47921165 with penalty 0 = 0 + 0
c [ternres-31] all 13081 free variables schedulable
c [ternres-31] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-31] fully completed ternary resolution
c [transred-33] limit 2000000 with penalty 0 = 0 + 0
c [transred-33] removed 27 transitive binary clauses
c [cce-34] limit of 95842330 steps penalty 0 = 0 + 0
c [cce-34-1] eliminated 1 clauses out of 1 (100%) of length 97
c [cce-34-1] eliminated 6 clauses out of 17 (35%) of length 60
c [cce-34-1] eliminated 12 clauses out of 20 (60%) of length 59
c [cce-34-1] eliminated 8 clauses out of 52 (15%) of length 57
c [cce-34-1] eliminated 4 clauses out of 109 (4%) of length 54
c [cce-34-1] eliminated 1 clauses out of 54 (2%) of length 52
c [cce-34-1] eliminated 1 clauses out of 219 (0%) of length 50
c [cce-34-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-34-1] eliminated 2 clauses out of 123 (2%) of length 6
c [cce-34-1] eliminated 1 clauses out of 441 (0%) of length 5
c [cce-34-1] eliminated 3 clauses out of 843 (0%) of length 4
c [cce-34-1] completed large round (ACCE)
c [cce-34-1] eliminated 41 large clauses in 7611253 steps
c [cce-34-1] allowing another 3805626 steps for small clauses
c [cce-34] scheduling 45631 clauses = 45071 binary + 560 ternary
c [cce-34] tried to eliminate 13749 small clauses 30%
c [cce-34] eliminated 760 small clauses 2%
c [cce-34] eliminated 745 binary clauses 2%
c [cce-34] eliminated 15 ternary clauses 3%
c [cce-34-1] eliminated 760 small clauses in 95842331 steps
c [cce-34-1] incomplete small round (ACCE)
c [cce-34-1] eliminated 801 covered clauses in round 1
c [cce-34] eliminated 801 covered clauses in TOTAL during 1 rounds
c [elim-35] scheduling all variables this time
c [elim-35] scheduled 13081 variables 100%
c [elim-35] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-35-1] eliminated 213 variables 2% in round 1 in 24937434 steps
c [elim-35-1] backward subsumption/strengthening limit 49874868
c [elim-35-1] subsumed 0 and strengthened 0 clauses in 1146393 steps
c [elim-35] fully completed in 1 rounds
c [elim-35] transition to [ all 0 rem 0 ] state
c [elim-35] eliminated 213 = 2% variables out of 13081
c [bca-34] limit of 10000000 steps
c [bca-34] 20713 out of 25738 literals actually usable 80%
c [bca-34] added 6412 blocked clauses in 325272 steps
c [phase-37] phase bias: 3 positive 30%, 7 negative 70%
c [simplification-35] removed 213 variables 1.6% (12868 remain 24%)
c [simplification-35] removed 1895 irredundant clauses 3.9% (47113 remain 15%)
c [simplification-35] maximum reduction of 4% = max (2%, 4%)
c [simplification-35] geometric conflict interval increment 7200 = 36000 / 5
c [simplification-35] new conflict interval 43200
c [simplification-35] penalized conflict interval 43200 = 1 * 43200
c [simplification-35] new conflict limit 1346485
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  308.4   12868    47113   1310948   14852   2820 201006   2 26.7  60.6   21
c i  309.0   12867    47113   1315587   19080   2827 201010   2 26.7  60.5   24
c -  310.1   12867    47113   1324608   15845   2860 201020   2 26.7  60.5   21
c i  311.0   12866    47113   1331732   22286   2879 201025   2 26.6  60.4   25
c -  311.8   12866    47113   1338297   16659   2888 201026   1 26.6  60.3   21
c 
c [simplification-36] limit of 1346597 conflicts hit after 1346597 conflicts
c [ternres-32] limit 49300583 with penalty 0 = 0 + 0
c [ternres-32] all 12866 free variables schedulable
c [ternres-32] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-32] fully completed ternary resolution
c [card-8] limit 1540643 penalty 4 = 4 + 0
c [card-8] found 6635 at-most-one constraints of average size 10.8
c [card-8] found 72 at-most-two constraints of average size 4.3
c [card-8] using previous limit 1540643 for elimination
c [card-8] 6706 out of 6707 constraints (100%) meet size limits
c [card-8] no units found
c [card-8] no at-most-one constraints generated
c [decomp-49] removed 2 variables
c [lift-22] limit 2500000 with penalty 3 = 3 + 0
c [lift-22] using 29 probes 0%
c [lift-22-1] found 0 units 3 impls in round 1
c [lift-22-2] found 0 units 2 impls in round 2
c [lift-22-3] found 0 units 1 impls in round 3
c [lift-22-4] found 0 units 3 impls in round 4
c [lift-22-5] found 0 units 1 impls in round 5
c [lift-22] 0 units, 10 impls, 0 eqs in 6 rounds
c [lift-22] 7604 variables remain 59% (5262 retained)
c [transred-34] limit 2000000 with penalty 0 = 0 + 0
c [transred-34] removed 60 transitive binary clauses
c [cce-35] limit of 98601167 steps penalty 0 = 0 + 0
c [cce-35-1] eliminated 2 clauses out of 2 (100%) of length 95
c [cce-35-1] eliminated 7 clauses out of 16 (44%) of length 59
c [cce-35-1] eliminated 15 clauses out of 52 (29%) of length 57
c [cce-35-1] eliminated 15 clauses out of 111 (14%) of length 54
c [cce-35-1] eliminated 6 clauses out of 49 (12%) of length 52
c [cce-35-1] eliminated 2 clauses out of 6 (33%) of length 33
c [cce-35-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-35-1] eliminated 1 clauses out of 104 (1%) of length 7
c [cce-35-1] eliminated 5 clauses out of 419 (1%) of length 5
c [cce-35-1] eliminated 4 clauses out of 822 (0%) of length 4
c [cce-35-1] completed large round (ACCE)
c [cce-35-1] eliminated 59 large clauses in 7256357 steps
c [cce-35-1] allowing another 3628178 steps for small clauses
c [cce-35] scheduling 43801 clauses = 43265 binary + 536 ternary
c [cce-35] tried to eliminate 14608 small clauses 33%
c [cce-35] eliminated 907 small clauses 2%
c [cce-35] eliminated 896 binary clauses 2%
c [cce-35] eliminated 11 ternary clauses 2%
c [cce-35-1] eliminated 907 small clauses in 98601168 steps
c [cce-35-1] incomplete small round (ACCE)
c [cce-35-1] eliminated 966 covered clauses in round 1
c [cce-35] eliminated 966 covered clauses in TOTAL during 1 rounds
c [elim-36] scheduling all variables this time
c [elim-36] scheduled 12866 variables 100%
c [elim-36] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-36-1] eliminated 160 variables 1% in round 1 in 7467781 steps
c [elim-36-1] backward subsumption/strengthening limit 14935562
c [elim-36-1] subsumed 0 and strengthened 0 clauses in 967325 steps
c [elim-36] fully completed in 1 rounds
c [elim-36] transition to [ all 0 rem 0 ] state
c [elim-36] eliminated 160 = 1% variables out of 12866
c [bca-35] limit of 10000000 steps
c [bca-35] 19403 out of 25414 literals actually usable 76%
c [bca-35] added 1417 blocked clauses in 318886 steps
c [rephase-13] after 1346597 conflicts (new increment 160000, next 1506597)
c [flushphases] 1549 phases reset
c [phase-38] phase bias: 3 positive 38%, 5 negative 62%
c [simplification-36] removed 160 variables 1.2% (12706 remain 24%)
c [simplification-36] removed 1313 irredundant clauses 2.8% (45800 remain 15%)
c [simplification-36] maximum reduction of 3% = max (1%, 3%)
c [simplification-36] geometric conflict interval increment 10800 = 43200 / 4
c [simplification-36] new conflict interval 54000
c [simplification-36] penalized conflict interval 54000 = 1 * 54000
c [simplification-36] new conflict limit 1400597
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  317.4   12706    45800   1353395   17527   2899 195122   2 26.5  60.3   22
c -  319.1   12706    45800   1370810   18413   2921 195125   7 26.5  60.2   22
c -  320.5   12706    45800   1386189   19101   2935 195132   2 26.4  60.2   22
c 
c [simplification-37] limit of 1400693 conflicts hit after 1400693 conflicts
c [ternres-33] limit 50877142 with penalty 0 = 0 + 0
c [ternres-33] all 12706 free variables schedulable
c [ternres-33] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-33] fully completed ternary resolution
c [transred-35] limit 2000000 with penalty 0 = 0 + 0
c [transred-35] removed 38 transitive binary clauses
c [cce-36] limit of 101754284 steps penalty 0 = 0 + 0
c [cce-36-1] eliminated 21 clauses out of 52 (40%) of length 57
c [cce-36-1] eliminated 2 clauses out of 108 (2%) of length 54
c [cce-36-1] eliminated 4 clauses out of 43 (9%) of length 53
c [cce-36-1] eliminated 2 clauses out of 220 (1%) of length 50
c [cce-36-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-36-1] eliminated 1 clauses out of 61 (2%) of length 8
c [cce-36-1] eliminated 3 clauses out of 117 (3%) of length 6
c [cce-36-1] eliminated 14 clauses out of 419 (3%) of length 5
c [cce-36-1] eliminated 10 clauses out of 823 (1%) of length 4
c [cce-36-1] completed large round (ACCE)
c [cce-36-1] eliminated 59 large clauses in 7211296 steps
c [cce-36-1] allowing another 3605648 steps for small clauses
c [cce-36] scheduling 42911 clauses = 41988 binary + 923 ternary
c [cce-36] tried to eliminate 14944 small clauses 35%
c [cce-36] eliminated 556 small clauses 1%
c [cce-36] eliminated 532 binary clauses 1%
c [cce-36] eliminated 24 ternary clauses 3%
c [cce-36-1] eliminated 556 small clauses in 101754285 steps
c [cce-36-1] incomplete small round (ACCE)
c [cce-36-1] eliminated 615 covered clauses in round 1
c [cce-36] eliminated 615 covered clauses in TOTAL during 1 rounds
c [elim-37] scheduling all variables this time
c [elim-37] scheduled 12706 variables 100%
c [elim-37] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-37-1] eliminated 98 variables 1% in round 1 in 4505170 steps
c [elim-37-1] backward subsumption/strengthening limit 9010340
c [elim-37-1] subsumed 0 and strengthened 0 clauses in 897223 steps
c [elim-37] fully completed in 1 rounds
c [elim-37] transition to [ all 0 rem 0 ] state
c [elim-37] eliminated 98 = 1% variables out of 12706
c [bca-36] limit of 10000000 steps
c [bca-36] 18779 out of 25218 literals actually usable 74%
c [bca-36] added 929 blocked clauses in 322195 steps
c [phase-39] phase bias: 7 positive 64%, 4 negative 36%
c [simplification-37] removed 98 variables 0.8% (12608 remain 24%)
c [simplification-37] removed 732 irredundant clauses 1.6% (45068 remain 15%)
c [simplification-37] maximum reduction of 2% = max (1%, 2%)
c [simplification-37] geometric conflict interval increment 18000 = 54000 / 3
c [simplification-37] new conflict interval 72000
c [simplification-37] penalized conflict interval 72000 = 1 * 72000
c [simplification-37] new conflict limit 1472693
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  325.9   12608    45068   1403935   20136   2981 192692   7 26.4  60.2   23
c -  327.8   12608    45068   1420782   20972   3004 192697   2 26.3  60.0   23
c -  330.0   12608    45068   1438329   21772   3015 192700   2 26.2  59.9   23
c i  330.9   12607    45068   1445748   28518   3028 192705   2 26.2  59.8   27
c -  332.3   12607    45068   1456667   22657   3038 192708   2 26.2  59.7   23
c i  332.4   12606    45068   1457054   23019   3038 192709   2 26.2  59.7   24
c 
c [simplification-38] limit of 1472783 conflicts hit after 1472783 conflicts
c [ternres-34] limit 53306242 with penalty 0 = 0 + 0
c [ternres-34] all 12606 free variables schedulable
c [ternres-34] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-34] fully completed ternary resolution
c [gauss-8] limit 666328 penalty 4 = 4 + 0
c [gauss-8] extracted 1 xors of average arity 3.0
c [gauss-8] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-8] limit 666328 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-8] limit 333164 penalty 4 = 4 + 0
c [cgrclsr-8] all 12606 free variables schedulable
c [cgrclsr-8] fully completed congruence closure
c [cliff-24] limit of 2665312 steps penalty 4 = 4 + 0
c [cliff-24] failed 0, lifted 0
c [transred-36] limit 2000000 with penalty 0 = 0 + 0
c [transred-36] removed 47 transitive binary clauses
c [cce-37] limit of 106612485 steps penalty 0 = 0 + 0
c [cce-37-1] eliminated 8 clauses out of 49 (16%) of length 57
c [cce-37-1] eliminated 6 clauses out of 100 (6%) of length 54
c [cce-37-1] eliminated 2 clauses out of 6 (33%) of length 33
c [cce-37-1] eliminated 1 clauses out of 100 (1%) of length 7
c [cce-37-1] eliminated 4 clauses out of 408 (1%) of length 5
c [cce-37-1] eliminated 4 clauses out of 820 (0%) of length 4
c [cce-37-1] completed large round (ACCE)
c [cce-37-1] eliminated 25 large clauses in 7225972 steps
c [cce-37-1] allowing another 3612986 steps for small clauses
c [cce-37] scheduling 42179 clauses = 41293 binary + 886 ternary
c [cce-37] tried to eliminate 16124 small clauses 38%
c [cce-37] eliminated 404 small clauses 1%
c [cce-37] eliminated 386 binary clauses 1%
c [cce-37] eliminated 18 ternary clauses 2%
c [cce-37-1] eliminated 404 small clauses in 106612486 steps
c [cce-37-1] incomplete small round (ACCE)
c [cce-37-1] eliminated 429 covered clauses in round 1
c [cce-37] eliminated 429 covered clauses in TOTAL during 1 rounds
c [elim-38] scheduling all variables this time
c [elim-38] scheduled 12606 variables 100%
c [elim-38] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-38-1] eliminated 73 variables 1% in round 1 in 2647112 steps
c [elim-38-1] backward subsumption/strengthening limit 5294224
c [elim-38-1] subsumed 0 and strengthened 0 clauses in 877569 steps
c [elim-38] fully completed in 1 rounds
c [elim-38] transition to [ all 0 rem 0 ] state
c [elim-38] eliminated 73 = 1% variables out of 12606
c [bca-37] limit of 10000000 steps
c [bca-37] 18608 out of 25068 literals actually usable 74%
c [bca-37] added 843 blocked clauses in 324982 steps
c [phase-40] phase bias: 0 positive 0%, 6 negative 100%
c [simplification-38] removed 73 variables 0.6% (12533 remain 23%)
c [simplification-38] removed 517 irredundant clauses 1.1% (44551 remain 14%)
c [simplification-38] maximum reduction of 1% = max (1%, 1%)
c [simplification-38] geometric conflict interval increment 36000 = 72000 / 2
c [simplification-38] new conflict interval 108000
c [simplification-38] penalized conflict interval 108000 = 1 * 108000
c [simplification-38] new conflict limit 1580783
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  338.0   12533    44551   1476111   23499   3078 190519   1 26.1  59.6   24
c -  340.1   12533    44551   1497056   24518   3100 190524   3 26.1  59.5   24
c -  342.3   12533    44551   1522668   25437   3111 190525   2 26.3  59.7   24
c -  344.7   12533    44551   1542978   26216   3135 190530   2 26.3  59.6   24
c -  347.0   12533    44551   1563587   27195   3159 190531   4 26.2  59.5   24
c 
c [simplification-39] limit of 1580811 conflicts hit after 1580812 conflicts
c [ternres-35] limit 56621087 with penalty 0 = 0 + 0
c [ternres-35] all 12533 free variables schedulable
c [ternres-35] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-35] fully completed ternary resolution
c [treelook-7] limit 176940 penalty 4 = 4 + 0 boost 1
c [treelook-7] scheduled 13675 literals 55%
c [treelook-7] scheduling used 176996 steps
c [treelook-7] not fully scheduled
c [treelook-7] limit 176940 penalty 4 = 4 + 0 boost 1
c [treelook-7] used 234080 steps
c [treelook-7] 13670 literals remain 55%
c [treelook-7] 8762 variables remain to probed next time 70%
c [transred-37] limit 2000000 with penalty 0 = 0 + 0
c [transred-37] removed 40 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 12533 variables 100%
c [block-10] limit of 35388179 steps penalty 4 = 4 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 0 blocked clauses
c [cce-38] limit of 113242175 steps penalty 0 = 0 + 0
c [cce-38-1] eliminated 10 clauses out of 49 (20%) of length 57
c [cce-38-1] eliminated 2 clauses out of 6 (33%) of length 33
c [cce-38-1] eliminated 7 clauses out of 808 (1%) of length 4
c [cce-38-1] completed large round (ACCE)
c [cce-38-1] eliminated 19 large clauses in 7309949 steps
c [cce-38-1] allowing another 3654974 steps for small clauses
c [cce-38] scheduling 41352 clauses = 40820 binary + 532 ternary
c [cce-38] tried to eliminate 16619 small clauses 40%
c [cce-38] eliminated 308 small clauses 1%
c [cce-38] eliminated 298 binary clauses 1%
c [cce-38] eliminated 10 ternary clauses 2%
c [cce-38-1] eliminated 308 small clauses in 113242176 steps
c [cce-38-1] incomplete small round (ACCE)
c [cce-38-1] eliminated 327 covered clauses in round 1
c [cce-38] eliminated 327 covered clauses in TOTAL during 1 rounds
c [elim-39] scheduling all variables this time
c [elim-39] scheduled 12533 variables 100%
c [elim-39] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-39-1] eliminated 33 variables 0% in round 1 in 2538851 steps
c [elim-39-1] backward subsumption/strengthening limit 5077702
c [elim-39-1] subsumed 0 and strengthened 0 clauses in 861283 steps
c [elim-39] fully completed in 1 rounds
c [elim-39] transition to [ all 0 rem 0 ] state
c [elim-39] eliminated 33 = 0% variables out of 12533
c [bca-38] limit of 10000000 steps
c [bca-38] 18438 out of 25002 literals actually usable 74%
c [bca-38] added 414 blocked clauses in 328866 steps
c [rephase-14] after 1580812 conflicts (new increment 320000, next 1900812)
c [flushphases] 1459 phases reset
c [phase-41] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-39] removed 33 variables 0.3% (12500 remain 23%)
c [simplification-39] removed 356 irredundant clauses 0.8% (44195 remain 14%)
c [simplification-39] maximum reduction of 1% = max (0%, 1%)
c [simplification-39] geometric conflict interval increment 54000 = 108000 / 2
c [simplification-39] new conflict interval 162000
c [simplification-39] penalized conflict interval 162000 = 1 * 162000
c [simplification-39] new conflict limit 1742812
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  352.8   12500    44195   1585899   28011   3201 189612   3 26.1  59.3   24
c -  355.6   12500    44195   1608032   29068   3237 189620   2 26.0  59.2   24
c i  357.4   12499    44195   1622504   41121   3251 189631   2 26.0  59.0   32
c -  358.9   12499    44195   1631794   29960   3258 189635   3 26.0  58.9   24
c -  361.2   12499    44195   1654985   30718   3273 189638   2 25.9  58.9   24
c i  361.6   12498    44195   1658050   33537   3279 189651   2 25.8  58.9   27
c -  364.4   12498    44195   1679771   31528   3304 189660   1 25.8  58.7   31
c i  364.5   12497    44195   1680906   32613   3305 189660   2 25.8  58.7   33
c -  367.6   12497    44195   1703697   32447   3312 189661   2 25.7  58.5   31
c i  368.5   12496    44195   1713230   40991   3319 189663   2 25.7  58.4   35
c -  370.6   12496    44195   1728233   33224   3334 189667   2 25.6  58.3   31
c 
c [simplification-40] limit of 1743008 conflicts hit after 1743008 conflicts
c [ternres-36] limit 62683371 with penalty 0 = 0 + 0
c [ternres-36] all 12496 free variables schedulable
c [ternres-36] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-36] fully completed ternary resolution
c [decomp-53] removed 4 variables
c [basicprobe-7] limit 62683371 penalty 0 = 0 + 0
c [basicprobe-7-0] 1066 sched 9%, 10 failed, 0 lifted, 470 hbrs
c [decomp-54] removed 10 variables
c [basicprobe-7-1] 3541 probes remain 28% after last round
c [basicprobe-7-1] 41 units = 41 failed (100%) + 0 lifted (0%)
c [basicprobe-7-1] removed 41 variables, found 1066 hbrs
c [transred-38] limit 2000000 with penalty 0 = 0 + 0
c [transred-38] removed 31 transitive binary clauses
c [cce-39] limit of 125366743 steps penalty 0 = 0 + 0
c [cce-39-1] eliminated 5 clauses out of 42 (12%) of length 57
c [cce-39-1] eliminated 4 clauses out of 96 (4%) of length 54
c [cce-39-1] eliminated 4 clauses out of 47 (9%) of length 53
c [cce-39-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-39-1] eliminated 1 clauses out of 116 (1%) of length 6
c [cce-39-1] eliminated 2 clauses out of 404 (0%) of length 5
c [cce-39-1] eliminated 5 clauses out of 791 (1%) of length 4
c [cce-39-1] completed large round (ACCE)
c [cce-39-1] eliminated 22 large clauses in 6975977 steps
c [cce-39-1] allowing another 3487988 steps for small clauses
c [cce-39] scheduling 40818 clauses = 40296 binary + 522 ternary
c [cce-39] tried to eliminate 19063 small clauses 47%
c [cce-39] eliminated 179 small clauses 0%
c [cce-39] eliminated 175 binary clauses 0%
c [cce-39] eliminated 4 ternary clauses 1%
c [cce-39-1] eliminated 319 small clauses in 125366744 steps
c [cce-39-1] incomplete small round (ACCE)
c [cce-39-1] eliminated 341 covered clauses in round 1
c [cce-39] eliminated 341 covered clauses in TOTAL during 1 rounds
c [elim-40] scheduling all variables this time
c [elim-40] scheduled 12455 variables 100%
c [elim-40] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-40-1] eliminated 77 variables 1% in round 1 in 5326274 steps
c [elim-40-1] backward subsumption/strengthening limit 10652548
c [elim-40-1] subsumed 0 and strengthened 0 clauses in 905317 steps
c [elim-40] fully completed in 1 rounds
c [elim-40] transition to [ all 0 rem 0 ] state
c [elim-40] eliminated 77 = 1% variables out of 12455
c [bca-39] limit of 10000000 steps
c [bca-39] 18059 out of 24758 literals actually usable 73%
c [bca-39] added 738 blocked clauses in 327274 steps
c [phase-42] phase bias: 4 positive 67%, 2 negative 33%
c [simplification-40] removed 118 variables 0.9% (12378 remain 23%)
c [simplification-40] removed 595 irredundant clauses 1.3% (43600 remain 14%)
c [simplification-40] maximum reduction of 1% = max (1%, 1%)
c [simplification-40] geometric conflict interval increment 81000 = 162000 / 2
c [simplification-40] new conflict interval 243000
c [simplification-40] penalized conflict interval 243000 = 1 * 243000
c [simplification-40] new conflict limit 1986008
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  380.0   12378    43600   1755755   34206   3287 187468   2 25.5  58.1   25
c -  383.4   12378    43600   1786776   35211   3310 187470   4 25.6  58.1   25
c -  386.2   12378    43600   1821890   35909   3317 187470   2 26.0  58.3   25
c -  390.1   12378    43600   1854909   36543   3340 187474   2 26.1  58.3   32
c -  394.0   12378    43600   1883433   37405   3365 187481   2 26.1  58.0   32
c i  394.7   12377    43600   1889100   42490   3368 187483   2 26.0  58.0   36
c -  397.6   12377    43600   1911830   38291   3378 187486   2 26.0  57.9   32
c -  401.6   12377    43600   1940684   39219   3412 187491   3 25.9  57.7   32
c i  404.2   12376    43600   1965807   59297   3419 187491   2 25.8  57.6   43
c -  405.4   12376    43600   1972345   39933   3425 187492   2 25.8  57.5   32
c 
c [simplification-41] limit of 1986110 conflicts hit after 1986111 conflicts
c [ternres-37] limit 71711773 with penalty 0 = 0 + 0
c [ternres-37] all 12376 free variables schedulable
c [ternres-37] 52 ternary resolvents (1 bin, 51 trn)
c [ternres-37] fully completed ternary resolution
c [decomp-55] removed 2 variables
c [lift-23] limit 1250000 with penalty 4 = 4 + 0
c [lift-23] using 42 probes 0%
c [lift-23-1] found 2 units 3 impls in round 1
c [lift-23] 2 units, 5 impls, 0 eqs in 2 rounds
c [lift-23] 7219 variables remain 58% (5155 retained)
c [lift-23] removed 2 variables
c [unhide-13] limit 896397 with penalty 4 = 4 + 0
c [unhide-13-13] 0 units, 0 failed, 211 tauts, 0 hbrs, 239148 literals
c [transred-39] limit 2000000 with penalty 0 = 0 + 0
c [transred-39] removed 10 transitive binary clauses
c [cce-40] limit of 143423546 steps penalty 0 = 0 + 0
c [cce-40-1] eliminated 2 clauses out of 96 (2%) of length 54
c [cce-40-1] eliminated 15 clauses out of 49 (31%) of length 52
c [cce-40-1] eliminated 1 clauses out of 789 (0%) of length 4
c [cce-40-1] completed large round (ACCE)
c [cce-40-1] eliminated 18 large clauses in 6883077 steps
c [cce-40-1] allowing another 3441538 steps for small clauses
c [cce-40] scheduling 40411 clauses = 39896 binary + 515 ternary
c [cce-40] tried to eliminate 21868 small clauses 54%
c [cce-40] eliminated 161 small clauses 0%
c [cce-40] eliminated 156 binary clauses 0%
c [cce-40] eliminated 5 ternary clauses 1%
c [cce-40-1] eliminated 161 small clauses in 143423547 steps
c [cce-40-1] incomplete small round (ACCE)
c [cce-40-1] eliminated 179 covered clauses in round 1
c [cce-40] eliminated 179 covered clauses in TOTAL during 1 rounds
c [elim-41] scheduling all variables this time
c [elim-41] scheduled 12374 variables 100%
c [elim-41] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-41-1] eliminated 33 variables 0% in round 1 in 2484478 steps
c [elim-41-1] backward subsumption/strengthening limit 4968956
c [elim-41-1] subsumed 0 and strengthened 0 clauses in 837961 steps
c [elim-41] fully completed in 1 rounds
c [elim-41] transition to [ all 0 rem 0 ] state
c [elim-41] eliminated 33 = 0% variables out of 12374
c [bca-40] limit of 10000000 steps
c [bca-40] 17830 out of 24684 literals actually usable 72%
c [bca-40] added 556 blocked clauses in 333057 steps
c [rephase-15] after 1986111 conflicts (new increment 640000, next 2626111)
c [flushphases] 1439 phases reset
c [phase-43] phase bias: 3 positive 75%, 1 negative 25%
c [simplification-41] removed 35 variables 0.3% (12341 remain 23%)
c [simplification-41] removed 246 irredundant clauses 0.6% (43354 remain 14%)
c [simplification-41] maximum reduction of 1% = max (0%, 1%)
c [simplification-41] geometric conflict interval increment 121500 = 243000 / 2
c [simplification-41] new conflict interval 364500
c [simplification-41] penalized conflict interval 364500 = 1 * 364500
c [simplification-41] new conflict limit 2350611
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  413.7   12340    43354   2000361   64199   3512 186419   1 25.7  57.3   38
c -  414.1   12340    43354   2002802   40783   3513 186419   3 25.7  57.3   26
c -  418.2   12340    43354   2033523   41674   3528 186425   4 25.7  57.2   33
c -  422.7   12340    43354   2064957   42521   3558 186435   2 25.6  57.0   33
c 1  423.6   12340    43354   2071908   48912   3560 186437   6 25.5  57.2   36
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s SATISFIABLE
c
c bate: 18 basic ate = 18 trn 100% + 0 lrg 0% in 4 updates
c bcas: 40 count, 431861 added (1107 skipped), 15340759 steps
c bkwd: tried 3501879 clauses, 7003607 lits, 2.00 lits/clause
c bkwd: checked 81321146 occs, 23.22 occs/clause, 11.61 occs/lit
c bkwd: subsumed 60 binary, 47 ternary, 9 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 668 large (0% self)
c blkd: 10 bces, 21719 removed, 7221391 resolutions, 24728459 steps
c blkd: 33372 blocking literals 31%, 1715 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 8 count, 0 units, 0 am1, 14391108 steps
c card: 18 rescheduled, 10 eliminated, 10 resolved, 67431 subsumed
c card: 45638 at-most-one constraints found, average size 8.47
c card: 45638 at-most-one constraints used 100%, average size 8.47
c card: 72 at-most-two constraints found, average size 4.32
c card: 71 at-most-two constraints used 99%, average size 4.32
c cces: 40 cces, 73490 eliminated, 13577 ate 18%, 59913 abce 82%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 8 count, 1412831 esteps, 466448 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: 980 extracted (968 ands 99%, 12 xors 1%, 0 ites 0%)
c clff: 24 cliffs, 1 lifted, 315 failed
c clff: 65922 decisions, 308913211 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 998701 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 262 gcs, 0 rescored clauses, 1084 rescored vars
c dcps: 55 decompositions, 2733 equivalent 5%
c deco: 336106 decision-only clauses 16%, 74% reduction
c decs: 7243176 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 250346 flipped 3.456% (in 3942 phases)
c elms: 41 elims, 32619 eliminated 60%
c elms: 78 rounds, 1.9 rounds/bve
c elms: 19450 small 60%, 11454 large 35%
c elms: 128115 tried small, 19450 succeeded 15%, 108665 failed 85%
c elms: 22016 subsumed, 90594 strengthened, 42808 blocked
c elms: 24969288 copies, 27134499 resolutions, 2823639 ipos
c elms: 20669298 subchks, 32952085 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 8 extractions, 91 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11342196 steps, 5671098 extr 50%, 482 elim 0%
c glue: 25.5 orig avg, 23.5 real avg, 4.3 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 168833 = 132114 simple + 35836 trn 78% + 883 lrg 21%, 880 sub 1%
c hght: 57 average, 2.24 height/glue
c ints: 57336 luby (15776795 steps), 0 inout (0 steps)
c lift: 23 phases, 65390 probed (21895 level1 33%, 43495 level2 67%)
c lift: 405 units, 2 equivalences, 271 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2060709 clauses, 92.0 length
c lrnd: 646480 uips 31%, 1239667 flips 60%
c mega: 0 count, 0 failed, 0 rounds
c mins: 189670748 learned lits, 37% minimized
c mins: 1708615 mins 83%, 1096 bin 0%, 14892 size 1%, 336106 deco 16%
c move: moved 2060709, 71505 bin 3%, 1729 trn 0%, 0 lrg 0%
c otfs: str 33467 dyn (33409 red, 58 irr) 11199 drv 33%, 22268 rst 67%
c otfs: sub 302 dyn (302 red, 0 irr)
c phas: 43 computed, 39122 set, 4706 pos (12%), 34416 neg (88%)
c prbs: 7 basic, 30346 probed, 138 failed, 0 lifted
c prbs: 7 simple, 421823 probed, 36 failed, 2687 eqs
c prbs: 7 treelook, 56 probed, 0 failed, 0 lifted
c prps: 1637990843 props, 199 props/dec
c prps: 88% srch, 12% simp, 0% lkhd
c psns: 253816791 searches, 90970131 hits, 36% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 115 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 115 arith 100%, 0 double 0%
c rmbd: 7531 removed, 5692 red 76%
c rphs: 15 recomputed phases
c rsts: 56767 restarts 99%, 569 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 569 reuse 100%
c rsts: 35.7 avg interval, 35.7 scaled, 1.0 factor
c rsts: 14046 kept 24.7% average 20.9%
c simp: 41 count (41 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2060709 count (2114571 tried 1.0), 338081 sub out of 2055628 (16.4%)
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: 2 count
c tops: 6227 fixed 12%, 78 its, 26562.92 confs/it
c trvs: 13385159037 traversals, 96% srch, 5% simp, 0% lkhd
c trvs: 8.9 search traversals per propagation, 6202.0 per conflict
c trvs: 1.7 search traversals per search visit
c trds: 39 transitive reductions, 9133 removed, 0 failed
c trds: 25368 nodes, 120885 edges, 72572969 steps
c trim: 11772072 words, 44.9 MB
c trnr: 37 count, 3 bin, 1589 trn, 47230359 steps
c unhd: 13 count, 13 rounds, 13856909 steps
c unhd: 6 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 58 failed, 57 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 149112 tauts, 34692 bin 23%, 391 trn 0%, 118 lrg 0%
c unhd: 149112 tauts, 113911 stamp 76%, 142519 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 792314 str, 0 bin 0%, 365 trn 0%, 791949 lrg 100%, 789036 red 100%
c vars: 12340 remaining 23% and 41579 removed 77% out of 53919
c vars: 6227 fixed 12%, 32619 eliminated 60%, 2733 equivalent 5%
c vsts: 8079996066 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 5.2 search visits per propagation, 3641.5 per conflict
c wchs: 1619465308 pushed, 92678009 enlarged, 389 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2055628 100   1524544 100  67410221 100  18582276 100   1275037 100
c 
c  0      40005   2         0   0  30520267  45   4840295  26    215641  17 
c  1      49085   2         0   0  22976964  34<  5116094  28    282424  22 
c  2     266536  13    224937  15   5874222   9   2439357  13<   181572  14 
c  3     469674  23    437017  29   3729178   6   2254807  12    201132  16<
c  4     445682  22<   403175  26<  2211503   3   1714111   9    178482  14 
c  5     318273  15    287580  19   1149957   2   1070766   6    119241   9 
c  6     156812   8     77471   5    404340   1    432819   2     40464   3 
c  7      98669   5     30540   2    196621   0    238053   1     19245   2 
c  8      79467   4     24509   2    141148   0    185430   1     15074   1 
c  9      56802   3     16814   1     91616   0    126485   1      9525   1 
c 10      56010   3     16207   1     84907   0    121974   1      9114   1 
c 11      16312   1      5647   0     25182   0     36439   0      2731   0 
c 12       2301   0       647   0      4316   0      5646   0       392   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             4.3           4.0           1.0           2.0           2.6
c std             2.2           1.6           1.4           2.1           2.1
c 
c   72.765  17% cce
c   53.698  13% analysis
c   42.245  10% elim
c   16.466   4% mincls
c    9.485   2% cliff
c    9.348   2% bump
c    8.980   2% decide
c    8.912   2% probe
c    8.698   2% gc
c    6.122   1% restart
c    5.164   1% decomp
c    4.447   1% lift
c    3.588   1% bca
c    3.255   1% block
c    2.617   1% unhide
c    2.475   1% defrag
c    2.328   1% backward
c    2.257   1% transred
c    1.500   0% phase
c    0.926   0% reduce
c    0.811   0% cgrclsr
c    0.705   0% gauss
c    0.648   0% card
c    0.256   0% ternres
c    0.053   0% tabularasa
c    0.006   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    2.671   1% probe simple     30%
c    5.211   1% probe basic      58%
c    1.030   0% probe tree-look  12%
c ==================================
c    2.384   1% preprocessing     2%
c  156.374  37% inprocessing     98%
c ==================================
c  158.758  37% simplifying
c  264.814  63% search
c ==================================
c  423.592 100% all
c 
c 7243176 decisions, 17099.4 decisions/sec
c 2071908 conflicts, 4891.3 conflicts/sec
c 1637990843 propagations, 3.9 megaprops/sec
c 423.6 seconds, 52.7 MB
c launch: done
