c launch: /data/cnf/sc2014/app/partial-10-11-s.cnf.bz2
c host: atom06
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/partial-10-11-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-10-11-s.cnf.bz2
c no embedded options
c found 'p cnf 189456 850574' header
c read 189456 variables, 850574 clauses, 1937804 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 182257 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  182257   835269         0       0      0     0   7  0.0   0.0   35
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 31740 at-most-one constraints of average size 4.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 31740 out of 31740 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 91571 variables
c [simpleprobe-1] all 97885 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 882 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 882 variables, found 10605 hbrs, 7 units
c [unhide-1] limit 265447 based on 530894 irredundant clauses
c [unhide-1-1] 0 units, 153 failed, 4385 tauts, 0 hbrs, 4446 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 96765 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 37392 variables 39% in round 1 in 55778671 steps
c [elim-1-1] backward subsumption/strengthening limit 111557342
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 13907211 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 37392 = 39% variables out of 96765
c [phase-1] phase bias: 13082 positive 22%, 46291 negative 78%
c [simplification-1] removed 85933 variables 59.1% (59373 remain 33%)
c [simplification-1] removed 445684 irredundant clauses 53.4% (389585 remain 47%)
c [simplification-1] maximum reduction of 59% = max (59%, 53%)
c [simplification-1] large reduction 59% >= 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] 133959, max 258760, min4 44141 at 75%, min10 44141 at 75%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number clauses 389585 drops below limit 417634
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 59373 phases reset fully
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
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 14843 and clause limit 194792
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    4.4   59372   389585        35      25      2  6854  11 25.5  69.2   27
c i    4.4   59243   389585        37      26      2  6854  11 24.1  67.5   27
c R    4.4   59233   389585        67      52      5  6855   7 17.9  78.2   27
c R    4.5   59233   389585       169     142     10  6857   3 27.0 119.9   28
c i    4.5   59232   389585       173     145     10  6857   3 27.4 124.5   28
c i    4.5   58801   389585       181     149     10  6860   3 26.5 134.8   28
c i    4.6   58442   389585       242     189     18  6870   2 24.6 142.2   28
c i    4.6   58430   389585       243     189     18  6870   2 24.5 142.2   28
c i    4.6   58408   389585       244     189     18  6870   2 24.4 142.2   28
c i    4.6   58397   389585       245     189     18  6870   1 24.3 140.8   28
c i    4.6   58386   389585       246     189     18  6870   1 24.2 139.6   28
c i    4.6   58375   389585       247     189     18  6870   1 24.1 138.3   28
c i    4.6   58366   389585       248     189     18  6870   1 24.0 137.1   28
c i    4.6   58356   389585       249     189     18  6870   0 23.9 136.0   28
c i    4.6   58347   389585       250     189     18  6870   0 23.8 134.9   28
c i    4.6   58336   389585       251     189     18  6870   0 23.7 133.8   28
c i    4.6   58325   389585       252     189     18  6870   0 23.6 132.7   28
c i    4.6   58313   389585       253     189     18  6870   0 23.5 131.7   28
c i    4.6   58301   389585       254     189     18  6870   0 23.4 130.8   28
c i    4.7   58290   389585       356     276     22  6876   2 22.2 134.1   28
c R    4.7   58281   389585       424     319     29  6886   3 19.5 135.3   28
c i    4.7   58280   389585       430     323     30  6886   3 19.3 134.5   28
c i    4.9   58275   389585       592     454     43  6901   2 18.3 185.6   28
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    4.9   58011   389585       609     468     43  6902   3 18.4 190.5   28
c i    4.9   57915   389585       611     467     44  6902   3 18.4 190.5   28
c i    5.0   57624   389585       635     483     47  6903   2 19.1 196.4   28
c R    5.2   57369   389585       994     773     60  6916   4 48.7 204.4   28
c i    5.2   57368   389585      1005     782     60  6916   2 48.5 222.5   28
c i    5.3   57322   389585      1114     873     66  6920   1 52.8 225.5   28
c i    5.3   57310   389585      1144     901     67  6920   2 52.2 223.9   28
c i    5.3   56966   389585      1150     902     70  6921   2 52.0 223.3   28
c i    5.4   56813   389585      1311    1022     82  6926   3 52.2 219.5   28
c i    5.5   56666   389585      1472    1149     92  6933   2 57.7 222.5   29
c i    5.5   56616   389585      1473    1149     92  6933   2 57.7 222.4   29
c i    5.5   56475   389585      1485    1150     99  6935   2 57.2 222.1   29
c i    5.5   56426   389585      1488    1152     99  6935   2 57.2 221.7   29
c i    5.5   56408   389585      1489    1152     99  6935   2 57.1 221.1   29
c i    5.6   56268   389585      1520    1179    101  6936   3 56.8 218.9   29
c i    5.6   56211   389585      1547    1199    103  6939   2 56.5 221.0   29
c i    5.6   56071   389585      1575    1224    104  6939   2 56.9 221.9   29
c i    5.8   55817   389585      1695    1324    116  6945   2 55.4 219.3   29
c i    5.8   55329   389585      1737    1357    119  6950   1 54.5 223.7   29
c 
c [simplification-2] limit of 1791 conflicts hit after 1791 conflicts
c [decomp-3] removed 4500 variables
c [simpleprobe-2] all 54873 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 138 variables
c [simpleprobe-2] 45941 variables remain 84% (8794 retained)
c [simpleprobe-2] removed 138 variables, found 5893 hbrs, 54 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 48755 literals 45%
c [treelook-1] scheduling used 300020 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 311902 steps
c [treelook-1] 48751 literals remain 45%
c [treelook-1] 46274 variables remain to probed next time 85%
c [treelook-1] removed 0 variables, found 1935 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 17880 probes remain 33% after last round
c [basicprobe-1-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1140 variables, found 6394 hbrs
c [unhide-2] limit 179613 based on 359226 irredundant clauses
c [unhide-2-2] 1 units, 240 failed, 3832 tauts, 0 hbrs, 15336 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 53264 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 8151 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 3 clauses out of 77 (4%) of length 10
c [cce-1-1] eliminated 1050 clauses out of 1887 (56%) of length 9
c [cce-1-1] eliminated 583 clauses out of 1043 (56%) of length 8
c [cce-1-1] eliminated 2437 clauses out of 2990 (82%) of length 7
c [cce-1-1] eliminated 4094 clauses out of 5496 (74%) of length 6
c [cce-1-1] eliminated 19918 clauses out of 29162 (68%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 28085 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 233075 clauses = 181905 binary + 51170 ternary
c [cce-1] tried to eliminate 5748 small clauses 2%
c [cce-1] eliminated 2098 small clauses 1%
c [cce-1] eliminated 1819 binary clauses 1%
c [cce-1] eliminated 279 ternary clauses 1%
c [cce-1-1] eliminated 2098 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 30183 covered clauses in round 1
c [cce-1] eliminated 30183 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 53264 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 3373 not tried 6% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 11965 = 22% variables out of 53264
c [bca-1] limit of 10000000 steps
c [bca-1] 80369 out of 82600 literals actually usable 97%
c [bca-1] added 418 blocked clauses in 197718 steps
c [phase-3] phase bias: 10 positive 5%, 188 negative 95%
c [simplification-2] removed 14015 variables 25.3% (41299 remain 23%)
c [simplification-2] removed 108766 irredundant clauses 27.9% (280819 remain 34%)
c [simplification-2] maximum reduction of 28% = max (25%, 28%)
c [simplification-2] large reduction 28% >= 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 3791
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   20.2   41298   280819      1864     392    353 18814   3 54.0 229.1   23
c R   20.3   41295   280819      2329     713    360 18819   6 63.3 228.7   24
c i   20.4   41294   280819      2369     743    364 18822   3 62.4 227.5   24
c i   20.5   41288   280819      2644     956    388 18842   3 57.5 219.2   24
c i   20.6   41189   280819      2781    1068    394 18854   3 55.5 216.7   24
c i   20.6   41185   280819      2835    1112    401 18856   2 54.5 214.8   24
c i   20.6   41181   280819      2844    1117    402 18858   2 54.4 214.6   24
c i   20.7   41106   280819      2919    1173    408 18866   1 53.2 211.7   24
c i   20.8   41007   280819      3043    1280    417 18869   2 51.8 208.4   24
c i   20.8   40927   280819      3069    1297    421 18873   3 51.4 207.8   24
c i   20.8   40820   280819      3076    1301    421 18875   3 51.3 207.7   24
c i   20.9   40817   280819      3227    1431    426 18881   3 51.6 208.0   24
c i   21.0   40758   280819      3483    1656    436 18889   3 50.5 207.8   24
c i   21.1   40749   280819      3735    1875    442 18895   2 49.0 209.7   24
c i   21.2   40748   280819      3858    1976    449 18904   3 48.2 207.4   24
c i   21.3   40745   280819      4074    2147    464 18914   5 47.3 204.1   24
c 
c [simplification-3] limit of 4315 conflicts hit after 4315 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 40742 free variables schedulable
c [ternres-1] 50 ternary resolvents (0 bin, 50 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 8610 at-most-one constraints of average size 4.6
c [card-2] found 319 at-most-two constraints of average size 5.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 8925 out of 8929 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 126 xors of average arity 2.3
c [gauss-1] connected 284 occurrences of 145 variables (average 2.0)
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 40 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 40702 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 35215 probes 87%
c [lift-1] 17 units, 5 impls, 0 eqs in 1 rounds
c [lift-1] 40681 variables remain 100% (4 retained)
c [lift-1] removed 17 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 27, lifted 440
c [unhide-3] limit 160134 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 396 failed, 6093 tauts, 0 hbrs, 11293 literals
c [transred-1] limit 800671 with penalty 0 = 0 + 0
c [transred-1] removed 97 transitive binary clauses
c [transred-1] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 39754 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 71 blocked clauses
c [block-2] 71 < 1/1000 * 265051 = 265 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 349 (1%) of length 7
c [cce-2-1] eliminated 6 clauses out of 2305 (0%) of length 6
c [cce-2-1] eliminated 2 clauses out of 9296 (0%) of length 5
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 12 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 179985 clauses = 137301 binary + 42684 ternary
c [cce-2] tried to eliminate 657 small clauses 0%
c [cce-2] eliminated 271 small clauses 0%
c [cce-2] eliminated 216 binary clauses 0%
c [cce-2] eliminated 55 ternary clauses 0%
c [cce-2-1] eliminated 271 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 283 covered clauses in round 1
c [cce-2] eliminated 283 covered clauses in TOTAL during 1 rounds
c [elim-3] 3322 variables 8% will be scheduled this time
c [elim-3] scheduled 3322 variables 8%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 51 variables 0% in round 1 in 6121402 steps
c [elim-3-1] backward subsumption/strengthening limit 12242804
c [elim-3-1] subsumed 17 and strengthened 5 clauses in 8054402 steps
c [elim-3-1] rescheduled 61 variables 0% by backward subsumption
c [elim-3-2] eliminated 7 variables 0% in round 2 in 74365 steps
c [elim-3-2] backward subsumption/strengthening limit 148730
c [elim-3-2] subsumed 0 and strengthened 0 clauses in 148752 steps
c [elim-3-2] fully rescheduled 39694 variables 100%
c [elim-3] incomplete 15153 not tried 38% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 867 = 2% variables out of 39752
c [bca-2] limit of 10000000 steps
c [bca-2] 70208 out of 77772 literals actually usable 90%
c [bca-2] added 25 blocked clauses in 171662 steps
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-3] removed 1857 variables 4.6% (38885 remain 21%)
c [simplification-3] removed 19679 irredundant clauses 7.0% (261140 remain 31%)
c [simplification-3] maximum reduction of 7% = max (5%, 7%)
c [simplification-3] large reduction 7% >= 5% limit
c [simplification-3] new conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] new conflict limit 6315
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   25.4   38885   261140      5262    2595    464 77248   2 52.6 210.6   25
c i   25.4   38884   261140      5283    2613    466 77248   2 52.6 210.1   25
c i   25.5   38772   261140      5345    2668    466 77254   3 52.4 209.6   25
c i   25.6   38769   261140      5474    2771    471 77263   2 52.4 208.2   25
c i   25.7   38765   261140      5690    2938    493 77274   2 51.2 208.7   25
c i   25.7   38763   261140      5699    2944    493 77276   2 51.1 208.1   25
c i   25.7   38755   261140      5715    2958    494 77276   3 51.0 207.8   25
c i   26.1   38750   261140      6413    3464    522 77321   4 51.5 204.4   26
c i   26.1   38691   261140      6525    3565    522 77325   3 51.2 203.1   26
c 
c [simplification-4] limit of 6699 conflicts hit after 6699 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 38673 free variables schedulable
c [ternres-2] 31 ternary resolvents (0 bin, 31 trn)
c [ternres-2] 7038 variables remain 18% (31635 retained)
c [decomp-7] removed 230 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 22504 literals 29%
c [treelook-2] scheduling used 173308 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 167227 steps
c [treelook-2] 22497 literals remain 29%
c [treelook-2] 21906 variables remain to probed next time 57%
c [treelook-2] removed 0 variables, found 765 hbrs
c [lift-2] limit 689132 with penalty 0 = 0 + 0
c [lift-2] using 33926 probes 88%
c [lift-2] 6 units, 3 impls, 0 eqs in 1 rounds
c [lift-2] 38595 variables remain 100% (9 retained)
c [lift-2] removed 51 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 1, lifted 49
c [unhide-4] limit 229710 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 161 failed, 11074 tauts, 0 hbrs, 13975 literals
c [transred-2] limit 1148554 with penalty 0 = 0 + 0
c [transred-2] removed 121 transitive binary clauses
c [transred-2] found 2 units
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 19
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 18
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 17
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 16
c [cce-3-1] eliminated 5 clauses out of 7 (71%) of length 15
c [cce-3-1] eliminated 6 clauses out of 8 (75%) of length 14
c [cce-3-1] eliminated 6 clauses out of 8 (75%) of length 13
c [cce-3-1] eliminated 6 clauses out of 7 (86%) of length 12
c [cce-3-1] eliminated 5 clauses out of 7 (71%) of length 11
c [cce-3-1] eliminated 7 clauses out of 10 (70%) of length 10
c [cce-3-1] eliminated 8 clauses out of 18 (44%) of length 9
c [cce-3-1] eliminated 10 clauses out of 44 (23%) of length 8
c [cce-3-1] eliminated 26 clauses out of 331 (8%) of length 7
c [cce-3-1] eliminated 38 clauses out of 2316 (2%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 131 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 179211 clauses = 133257 binary + 45954 ternary
c [cce-3] tried to eliminate 569 small clauses 0%
c [cce-3] eliminated 193 small clauses 0%
c [cce-3] eliminated 173 binary clauses 0%
c [cce-3] eliminated 20 ternary clauses 0%
c [cce-3-1] eliminated 2236 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2367 covered clauses in round 1
c [cce-3] eliminated 2367 covered clauses in TOTAL during 1 rounds
c [elim-4] 15010 variables 39% will be scheduled this time
c [elim-4] scheduled 15010 variables 39%
c [elim-4] limit of 22971082 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 363 variables 1% in round 1 in 15662844 steps
c [elim-4-1] backward subsumption/strengthening limit 7308238
c [elim-4-1] subsumed 1 and strengthened 0 clauses in 7308242 steps
c [elim-4] incomplete 5 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 363 = 1% variables out of 38274
c [bca-3] limit of 10000000 steps
c [bca-3] 66939 out of 75824 literals actually usable 88%
c [bca-3] added 11 blocked clauses in 164399 steps
c [phase-5] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-4] removed 762 variables 2.0% (37911 remain 21%)
c [simplification-4] removed 6083 irredundant clauses 2.3% (255057 remain 31%)
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 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] new conflict limit 33365
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   29.8   37910   255057      7454    4210    561 96848   2 52.9 201.9   27
c i   29.8   37906   255057      7653    4361    567 96857   2 53.0 201.1   28
c -   29.9   37902   255057      7849    2519    570 96862   3 53.1 199.5   26
c i   30.6   37901   255057      9075    3520    604 96918   2 54.0 199.7   26
c i   30.6   37845   255057      9077    3520    605 96918   2 54.0 199.7   26
c i   30.6   37786   255057      9078    3520    605 96918   2 54.0 199.7   26
c i   30.7   37715   255057      9314    3712    620 96928   2 53.3 198.7   26
c i   31.2   37713   255057     11037    4926    631 96942   2 62.2 200.8   28
c i   31.4   37708   255057     11817    5412    632 96954   3 64.4 200.6   29
c R   31.4   37705   255057     11851    5442    633 96957   3 64.3 200.7   29
c -   31.6   37705   255057     12128    3169    643 96977   3 63.6 199.1   26
c i   32.2   37704   255057     13282    4165    665 97000   5 64.3 198.7   27
c i   32.6   37673   255057     14198    4921    685 97029   3 65.6 199.6   28
c i   33.5   37658   255057     16046    6472    725 97108   4 64.7 196.5   29
c i   33.5   37655   255057     16047    6472    725 97108   4 64.7 196.5   29
c i   33.5   37652   255057     16054    6472    725 97114   4 64.6 196.4   29
c -   33.7   37588   255057     16612    3924    725 97115   4 67.4 197.3   26
c i   33.9   37587   255057     17194    4414    726 97116   3 69.9 198.7   27
c i   34.3   37585   255057     17806    4935    752 97147   3 68.5 197.9   27
c i   34.4   37582   255057     18094    5189    757 97152   4 67.9 197.1   27
c i   34.5   37577   255057     18283    5326    774 97160   3 67.5 196.6   27
c i   34.6   37520   255057     18473    5495    778 97166   3 67.5 196.8   27
c i   34.8   37519   255057     18705    5696    784 97172   2 67.5 197.2   27
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   35.5   37514   255057     20030    6873    791 97188   2 69.3 199.0   29
c -   36.3   37514   255057     21518    4573    832 97236   4 69.4 199.7   26
c R   37.5   37514   255057     26321    7438    844 97243   3 85.7 202.9   31
c i   38.0   37513   255057     27099    8074    868 97284   3 84.9 202.5   31
c i   38.1   37510   255057     27345    8248    869 97285   5 85.2 202.5   32
c -   38.7   37508   255057     28667    5177    894 97319   4 85.8 200.6   26
c i   40.5   37507   255057     32161    7883    952 97368   3 92.6 202.3   30
c i   41.6   37482   255057     34055    9465    977 97424   4 92.8 202.6   32
c i   41.9   37478   255057     34453    9783    979 97425   3 92.7 202.0   32
c 
c [simplification-5] limit of 35087 conflicts hit after 35087 conflicts
c [ternres-3] limit 5156365 with penalty 0 = 0 + 0
c [ternres-3] 6833 schedulable variables 18%
c [ternres-3] 292 ternary resolvents (0 bin, 292 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 37 xors of average arity 2.6
c [gauss-2] connected 98 occurrences of 67 variables (average 1.5)
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 21 variables
c [basicprobe-2] limit 5156365 penalty 0 = 0 + 0
c [basicprobe-2-0] 8563 probes remain 23% after last round
c [basicprobe-2-0] 61 units = 61 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 572 variables, found 35259 hbrs
c [bate-1] eliminated 57 asymmetric tautologies during probing
c [cgrclsr-2] limit 257818 penalty 1 = 1 + 0
c [cgrclsr-2] all 36879 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 1 variables
c [lift-3] limit 3093819 with penalty 0 = 0 + 0
c [lift-3] using 33017 probes 90%
c [lift-3] 43 units, 14 impls, 0 eqs in 1 rounds
c [lift-3] 36652 variables remain 100% (55 retained)
c [lift-3] removed 171 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 28
c [unhide-5] limit 1031273 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 69 failed, 5944 tauts, 0 hbrs, 76263 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 194 transitive binary clauses
c [transred-3] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 36553 variables 100%
c [block-3] limit of 25781828 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 487 blocked clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-4-1] eliminated 1 clauses out of 21 (5%) of length 8
c [cce-4-1] eliminated 4 clauses out of 196 (2%) of length 7
c [cce-4-1] eliminated 124 clauses out of 2170 (6%) of length 6
c [cce-4-1] eliminated 9 clauses out of 7714 (0%) of length 5
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 162 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 165414 clauses = 123708 binary + 41706 ternary
c [cce-4] tried to eliminate 860 small clauses 1%
c [cce-4] eliminated 294 small clauses 0%
c [cce-4] eliminated 237 binary clauses 0%
c [cce-4] eliminated 57 ternary clauses 0%
c [cce-4-1] eliminated 294 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 456 covered clauses in round 1
c [cce-4] eliminated 456 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 36519 variables 100%
c [elim-5] limit of 103127315 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 1462 variables 4% in round 1 in 19629442 steps
c [elim-5-1] backward subsumption/strengthening limit 39258884
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 7315249 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1462 = 4% variables out of 36519
c [bca-4] limit of 10000000 steps
c [bca-4] 57444 out of 70116 literals actually usable 82%
c [bca-4] added 98 blocked clauses in 140565 steps
c [rephase-1] after 35087 conflicts (new increment 20000, next 55087)
c [flushphases] 19 phases reset
c [phase-6] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-5] removed 2415 variables 6.4% (35057 remain 19%)
c [simplification-5] removed 17929 irredundant clauses 7.0% (237128 remain 28%)
c [simplification-5] maximum reduction of 7% = max (6%, 7%)
c [simplification-5] large reduction 7% >= 5% limit
c [simplification-5] new conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] new conflict limit 37087
c 
c [simplification-6] limit of 37141 conflicts hit after 37141 conflicts
c [ternres-4] limit 5417807 with penalty 0 = 0 + 0
c [ternres-4] all 35057 free variables schedulable
c [ternres-4] 197 ternary resolvents (0 bin, 197 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 677225 penalty 2 = 2 + 0
c [card-3] found 8425 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 677225 for elimination
c [card-3] 8425 out of 8425 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 29 variables
c [simpleprobe-3] 29753 schedulable variables 85%
c [simpleprobe-3] limit 21671229 penalty 0 = 0 + 0
c [decomp-11] removed 791 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 791 variables, found 48163 hbrs, 354 units
c [cgrclsr-3] limit 541780 penalty 0 = 0 + 0
c [cgrclsr-3] all 34237 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-4] limit 3250684 with penalty 0 = 0 + 0
c [lift-4] using 30845 probes 90%
c [lift-4] 59 units, 7 impls, 0 eqs in 1 rounds
c [lift-4] 34042 variables remain 100% (107 retained)
c [lift-4] removed 88 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 0, lifted 13
c [unhide-6] limit 1083561 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 61 failed, 23749 tauts, 0 hbrs, 28784 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 260 transitive binary clauses
c [transred-4] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 33976 variables 100%
c [block-4] limit of 54178072 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 28 blocked clauses
c [block-4] 28 < 1/1000 * 229723 = 229 considered unsuccessful
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-5-1] eliminated 2 clauses out of 3 (67%) 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 37
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 32
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 2 clauses out of 3 (67%) of length 29
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 18
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 11
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-5-1] eliminated 2 clauses out of 10 (20%) of length 9
c [cce-5-1] eliminated 1 clauses out of 22 (5%) of length 8
c [cce-5-1] eliminated 2 clauses out of 192 (1%) of length 7
c [cce-5-1] eliminated 2 clauses out of 2037 (0%) of length 6
c [cce-5-1] eliminated 7 clauses out of 7676 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 65 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 156683 clauses = 118618 binary + 38065 ternary
c [cce-5] tried to eliminate 952 small clauses 1%
c [cce-5] eliminated 316 small clauses 0%
c [cce-5] eliminated 266 binary clauses 0%
c [cce-5] eliminated 50 ternary clauses 0%
c [cce-5-1] eliminated 316 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 381 covered clauses in round 1
c [cce-5] eliminated 381 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 33975 variables 100%
c [elim-6] limit of 108356145 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 528 variables 2% in round 1 in 19892640 steps
c [elim-6-1] backward subsumption/strengthening limit 39785280
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 7086988 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 528 = 2% variables out of 33975
c [bca-5] limit of 10000000 steps
c [bca-5] 54062 out of 66896 literals actually usable 81%
c [bca-5] added 27 blocked clauses in 133924 steps
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 1610 variables 4.6% (33447 remain 18%)
c [simplification-6] removed 10181 irredundant clauses 4.3% (226947 remain 27%)
c [simplification-6] maximum reduction of 5% = max (5%, 4%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] new conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] new conflict limit 39141
c 
c [simplification-7] limit of 39191 conflicts hit after 39194 conflicts
c [ternres-5] limit 5685876 with penalty 0 = 0 + 0
c [ternres-5] all 33447 free variables schedulable
c [ternres-5] 162 ternary resolvents (0 bin, 162 trn)
c [ternres-5] fully completed ternary resolution
c [lift-5] limit 3411525 with penalty 0 = 0 + 0
c [lift-5] using 30242 probes 90%
c [lift-5] 68 units, 10 impls, 0 eqs in 1 rounds
c [lift-5] 33094 variables remain 99% (172 retained)
c [lift-5] removed 181 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 0, lifted 8
c [unhide-7] limit 1137175 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 7 failed, 4004 tauts, 0 hbrs, 35742 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 251 transitive binary clauses
c [transred-5] found 1 units
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 51
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 50
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 49
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 45
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 41
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 40
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 37
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 35
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 33
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 32
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 31
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 29
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 28
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 19
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 18
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 17
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 14
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 13
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 12
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 11
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 10
c [cce-6-1] eliminated 3 clauses out of 13 (23%) of length 9
c [cce-6-1] eliminated 3 clauses out of 24 (12%) of length 8
c [cce-6-1] eliminated 4 clauses out of 191 (2%) of length 7
c [cce-6-1] eliminated 13 clauses out of 2051 (1%) of length 6
c [cce-6-1] eliminated 1 clauses out of 7679 (0%) of length 5
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 104 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 151164 clauses = 114054 binary + 37110 ternary
c [cce-6] tried to eliminate 871 small clauses 1%
c [cce-6] eliminated 272 small clauses 0%
c [cce-6] eliminated 225 binary clauses 0%
c [cce-6] eliminated 47 ternary clauses 0%
c [cce-6-1] eliminated 375 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 479 covered clauses in round 1
c [cce-6] eliminated 479 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 33247 variables 100%
c [elim-7] limit of 113717531 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 255 variables 1% in round 1 in 18760267 steps
c [elim-7-1] backward subsumption/strengthening limit 37520534
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 6882071 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 255 = 1% variables out of 33247
c [bca-6] limit of 10000000 steps
c [bca-6] 53148 out of 65986 literals actually usable 81%
c [bca-6] added 22 blocked clauses in 132076 steps
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 455 variables 1.4% (32992 remain 18%)
c [simplification-7] removed 5138 irredundant clauses 2.3% (221809 remain 27%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-7] new conflict interval 35554
c [simplification-7] penalized conflict interval 35554 = 1 * 35554
c [simplification-7] new conflict limit 74748
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   56.5   32991   221809     39311    8593   1392 177445   6 92.9 203.0   31
c i   56.6   32990   221809     39440    8707   1396 177449   3 92.7 202.8   31
c i   56.6   32988   221809     39441    8707   1396 177449   3 92.7 202.8   31
c i   57.0   32911   221809     40011    9210   1402 177458   4 92.3 202.7   31
c -   57.7   32911   221809     41349    5776   1419 177468   3 92.4 202.9   27
c i   58.0   32910   221809     42070    6310   1425 177479   4 92.0 202.1   27
c i   58.9   32909   221809     44265    8129   1458 177503   4 91.4 202.3   29
c i   59.7   32792   221809     46020    9504   1472 177525   3 91.3 202.0   31
c i   59.9   32789   221809     46446    9835   1485 177537   4 91.3 201.6   31
c i   60.3   32733   221809     47203   10501   1499 177543   5 91.0 201.4   32
c i   60.4   32732   221809     47369   10625   1500 177543   5 91.0 201.5   33
c i   60.6   32731   221809     47705   10903   1511 177552   4 90.7 201.3   33
c i   60.6   32675   221809     47732   10929   1511 177552   5 90.7 201.2   33
c -   60.9   32674   221809     48819    6614   1517 177552   5 91.4 201.3   27
c i   62.8   32673   221809     55541    9962   1537 177605   6 105.1 204.0   36
c i   62.9   32672   221809     55971   10200   1538 177608   8 105.0 203.9   36
c i   63.0   32671   221809     56377   10426   1538 177608   7 105.5 203.9   36
c R   63.5   32671   221809     57873   11448   1542 177613   4 108.4 205.1   38
c i   63.7   32670   221809     58088   11631   1549 177617   4 108.3 205.4   39
c -   64.3   32668   221809     59220    7111   1569 177635   5 107.3 204.5   27
c i   65.1   32667   221809     61196    8730   1599 177656   4 106.4 203.8   28
c i   65.5   32666   221809     61713    9157   1605 177672   4 106.1 203.4   29
c i   65.5   32665   221809     61837    9271   1609 177673   5 106.0 203.2   29
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   65.9   32654   221809     63069   10160   1621 177682   3 106.2 203.7   31
c i   66.1   32653   221809     63377   10403   1624 177684   3 106.1 203.5   31
c i   66.9   32549   221809     64829   11653   1656 177692   5 105.3 202.6   32
c -   68.2   32549   221809     67752    7922   1695 177726   6 104.6 201.4   26
c i   68.7   32548   221809     69778    9251   1705 177728   4 107.1 202.2   30
c i   70.6   32543   221809     73171   11874   1749 177768   4 105.5 200.1   32
c 
c [simplification-8] limit of 75910 conflicts hit after 75910 conflicts
c [ternres-6] limit 10413549 with penalty 0 = 0 + 0
c [ternres-6] all 32495 free variables schedulable
c [ternres-6] 65 ternary resolvents (0 bin, 65 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 520677 penalty 2 = 2 + 0
c [gauss-3] extracted 18 xors of average arity 2.4
c [gauss-3] connected 44 occurrences of 42 variables (average 1.0)
c [gauss-3] limit 520677 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 25 variables
c [cgrclsr-4] limit 520677 penalty 1 = 1 + 0
c [cgrclsr-4] all 32470 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-6] limit 6248129 with penalty 0 = 0 + 0
c [lift-6] using 29585 probes 91%
c [lift-6] 69 units, 28 impls, 0 eqs in 1 rounds
c [lift-6] 32107 variables remain 99% (269 retained)
c [lift-6] removed 94 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 0, lifted 12
c [unhide-8] limit 2082709 with penalty 0 = 0 + 0
c [unhide-8-9] 2 units, 105 failed, 16067 tauts, 0 hbrs, 105285 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 185 transitive binary clauses
c [transred-6] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 32256 variables 100%
c [block-5] limit of 52067749 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1 blocked clauses
c [block-5] 1 < 1/1000 * 214535 = 214 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 41
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 40
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 39
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 37
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 35
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 32
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 29
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 28
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 27
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 25
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 23
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 21
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 19
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 18
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 17
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 15
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 14
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 13
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 12
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 11
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 10
c [cce-7-1] eliminated 3 clauses out of 13 (23%) of length 9
c [cce-7-1] eliminated 3 clauses out of 25 (12%) of length 8
c [cce-7-1] eliminated 3 clauses out of 155 (2%) of length 7
c [cce-7-1] eliminated 10 clauses out of 1960 (1%) of length 6
c [cce-7-1] eliminated 4 clauses out of 7120 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 77 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 152249 clauses = 109791 binary + 42458 ternary
c [cce-7] tried to eliminate 870 small clauses 1%
c [cce-7] eliminated 263 small clauses 0%
c [cce-7] eliminated 199 binary clauses 0%
c [cce-7] eliminated 64 ternary clauses 0%
c [cce-7-1] eliminated 263 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 340 covered clauses in round 1
c [cce-7] eliminated 340 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 32256 variables 100%
c [elim-8] limit of 208270998 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 357 variables 1% in round 1 in 18387480 steps
c [elim-8-1] backward subsumption/strengthening limit 36774960
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 6576256 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 357 = 1% variables out of 32256
c [bca-7] limit of 10000000 steps
c [bca-7] 48984 out of 63800 literals actually usable 77%
c [bca-7] added 36 blocked clauses in 125591 steps
c [rephase-2] after 75910 conflicts (new increment 40000, next 115910)
c [flushphases] 0 phases reset
c [simplification-8] removed 596 variables 1.8% (31899 remain 18%)
c [simplification-8] removed 8341 irredundant clauses 3.8% (213468 remain 26%)
c [simplification-8] maximum reduction of 4% = max (2%, 4%)
c [simplification-8] geometric conflict interval increment 7110 = 35554 / 5
c [simplification-8] new conflict interval 42664
c [simplification-8] penalized conflict interval 42664 = 1 * 42664
c [simplification-8] new conflict limit 118574
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   77.3   31898   213468     77460   13640   1661 182644   2 105.4 199.0   33
c -   78.2   31898   213468     79084    8494   1686 182663   3 104.7 198.3   27
c i   79.2   31897   213468     82723   10631   1691 182678   7 104.1 198.4   31
c i   81.0   31896   213468     86782   13204   1726 182722   5 103.3 197.3   33
c i   81.0   31878   213468     86789   13208   1727 182722   4 103.2 197.3   33
c i   81.0   31862   213468     86792   13210   1727 182722   4 103.2 197.3   33
c i   81.5   31859   213468     87723   13975   1735 182732   4 103.0 197.1   34
c -   82.9   31752   213468     90695    9203   1767 182751   3 102.8 196.4   27
c i   83.0   31751   213468     90866    9349   1779 182751   5 102.8 196.3   28
c i   83.0   31673   213468     90867    9349   1779 182751   5 102.8 196.3   28
c i   83.0   31672   213468     90868    9349   1779 182751   5 102.8 196.3   28
c i   83.0   31671   213468     90869    9349   1779 182751   5 102.8 196.3   28
c i   83.0   31668   213468     90870    9349   1779 182751   5 102.8 196.3   28
c i   83.0   31665   213468     90889    9365   1781 182751   4 102.7 196.3   28
c i   83.9   31664   213468     92724   10936   1807 182763   4 103.2 196.9   30
c i   84.3   31576   213468     93383   11487   1817 182780   3 103.0 196.5   31
c i   86.0   31546   213468     97680   14323   1847 182801   4 103.0 195.7   33
c -   87.9   31546   213468    101895   10036   1883 182826   3 103.0 195.1   27
c i   90.8   31545   213468    109153   15059   1950 182872   4 102.7 194.0   34
c -   92.5   31545   213468    114650   10859   1965 182883   3 110.0 197.3   27
c i   93.7   31544   213468    118396   13815   1968 182886   7 116.3 199.3   38
c 
c [simplification-9] limit of 119466 conflicts hit after 119466 conflicts
c [ternres-7] limit 15854784 with penalty 0 = 0 + 0
c [ternres-7] all 31542 free variables schedulable
c [ternres-7] 71 ternary resolvents (0 bin, 71 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-14] removed 394 variables
c [treelook-3] limit 198184 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 24341 literals 39%
c [treelook-3] scheduling used 198304 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 198184 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 212586 steps
c [treelook-3] 24334 literals remain 39%
c [treelook-3] 16526 variables remain to probed next time 52%
c [treelook-3] removed 0 variables, found 1063 hbrs
c [lift-7] limit 9512870 with penalty 0 = 0 + 0
c [lift-7] using 28753 probes 91%
c [lift-7] 170 units, 51 impls, 1 eqs in 1 rounds
c [lift-7] 30832 variables remain 99% (451 retained)
c [lift-7] removed 222 variables
c [cliff-7] limit of 12683827 steps penalty 0 = 0 + 0
c [cliff-7] failed 4, lifted 17
c [unhide-9] limit 3170956 with penalty 0 = 0 + 0
c [unhide-9-12] 1 units, 41 failed, 11514 tauts, 0 hbrs, 224926 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 185 transitive binary clauses
c [cce-8] limit of 31709568 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 56
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 55
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 54
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 53
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 52
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 50
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 48
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 46
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 44
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 42
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 40
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 39
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 38
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 35
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 33
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 31
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 28
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 27
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 26
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 24
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 23
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 22
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 19
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 18
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 17
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 16
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 15
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 14
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 13
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 12
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 11
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 10
c [cce-8-1] eliminated 3 clauses out of 13 (23%) of length 9
c [cce-8-1] eliminated 6 clauses out of 26 (23%) of length 8
c [cce-8-1] eliminated 4 clauses out of 144 (3%) of length 7
c [cce-8-1] eliminated 5 clauses out of 1946 (0%) of length 6
c [cce-8-1] eliminated 6 clauses out of 6608 (0%) of length 5
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 138 large clauses in 31709569 steps
c [cce-8-1] allowing another 15854784 steps for small clauses
c [cce-8] scheduling 140810 clauses = 106173 binary + 34637 ternary
c [cce-8] tried to eliminate 767 small clauses 1%
c [cce-8] eliminated 221 small clauses 0%
c [cce-8] eliminated 176 binary clauses 0%
c [cce-8] eliminated 45 ternary clauses 0%
c [cce-8-1] eliminated 392 small clauses in 31709569 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 530 covered clauses in round 1
c [cce-8] eliminated 530 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 31183 variables 100%
c [elim-9] limit of 317095685 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 417 variables 1% in round 1 in 18471090 steps
c [elim-9-1] backward subsumption/strengthening limit 36942180
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 6312864 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 417 = 1% variables out of 31183
c [bca-8] limit of 10000000 steps
c [bca-8] 47279 out of 61534 literals actually usable 77%
c [bca-8] added 37 blocked clauses in 119925 steps
c [rephase-3] after 119466 conflicts (new increment 80000, next 199466)
c [flushphases] 0 phases reset
c [simplification-9] removed 776 variables 2.5% (30766 remain 17%)
c [simplification-9] removed 7792 irredundant clauses 3.7% (205676 remain 25%)
c [simplification-9] maximum reduction of 4% = max (2%, 4%)
c [simplification-9] geometric conflict interval increment 8532 = 42664 / 5
c [simplification-9] new conflict interval 51196
c [simplification-9] penalized conflict interval 51196 = 1 * 51196
c [simplification-9] new conflict limit 170662
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  102.5   30766   205676    130923   11091   1957 196769   3 121.2 201.7   28
c -  105.8   30766   205676    143812   11552   1964 196775   4 125.2 204.0   28
c i  107.0   30765   205676    148800   15245   1966 196780   4 127.2 205.1   37
c i  107.1   30764   205676    149258   15501   1968 196780   5 127.1 205.1   37
c -  110.7   30764   205676    163034   12091   1973 196788   7 130.0 206.0   28
c 
c [simplification-10] limit of 170756 conflicts hit after 170757 conflicts
c [ternres-8] limit 20426202 with penalty 0 = 0 + 0
c [ternres-8] all 30764 free variables schedulable
c [ternres-8] 120 ternary resolvents (0 bin, 120 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1276637 penalty 3 = 3 + 0
c [card-4] found 9518 at-most-one constraints of average size 3.9
c [card-4] found 1734 at-most-two constraints of average size 5.0
c [card-4] using previous limit 1276637 for elimination
c [card-4] 11230 out of 11252 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-16] removed 3 variables
c [basicprobe-3] limit 20426202 penalty 0 = 0 + 0
c [basicprobe-3-0] 6789 probes remain 22% after last round
c [basicprobe-3-0] 234 units = 230 failed (98%) + 4 lifted (2%)
c [basicprobe-3-0] removed 389 variables, found 124708 hbrs
c [bate-2] eliminated 387 asymmetric tautologies during probing
c [lift-8] limit 12255721 with penalty 0 = 0 + 0
c [lift-8] using 27647 probes 91%
c [lift-8] 112 units, 69 impls, 23 eqs in 1 rounds
c [lift-8] 29467 variables remain 98% (692 retained)
c [lift-8] removed 215 variables
c [cliff-8] limit of 16340962 steps penalty 0 = 0 + 0
c [cliff-8] failed 0, lifted 31
c [unhide-10] limit 4085240 with penalty 0 = 0 + 0
c [unhide-10-15] 1 units, 62 failed, 22934 tauts, 0 hbrs, 56099 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 112 transitive binary clauses
c [transred-8] found 1 units
c [cce-9] limit of 40852405 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 60
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 59
c [cce-9-1] eliminated 4 clauses out of 5 (80%) of length 58
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 57
c [cce-9-1] eliminated 4 clauses out of 5 (80%) of length 56
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 55
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 54
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 53
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 52
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 49
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 48
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 47
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 45
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 44
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 43
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 42
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 41
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 39
c [cce-9-1] eliminated 4 clauses out of 9 (44%) of length 38
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 37
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 36
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 35
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 34
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 33
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 32
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 31
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 30
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 28
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 26
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-9-1] eliminated 4 clauses out of 8 (50%) of length 24
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-9-1] eliminated 4 clauses out of 9 (44%) of length 22
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 20
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 19
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 18
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 17
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 16
c [cce-9-1] eliminated 5 clauses out of 7 (71%) of length 15
c [cce-9-1] eliminated 7 clauses out of 16 (44%) of length 14
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 13
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 12
c [cce-9-1] eliminated 5 clauses out of 9 (56%) of length 11
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 10
c [cce-9-1] eliminated 6 clauses out of 16 (38%) of length 9
c [cce-9-1] eliminated 3 clauses out of 23 (13%) of length 8
c [cce-9-1] eliminated 6 clauses out of 139 (4%) of length 7
c [cce-9-1] eliminated 4 clauses out of 1933 (0%) of length 6
c [cce-9-1] eliminated 571 clauses out of 6361 (9%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 756 large clauses in 40852406 steps
c [cce-9-1] allowing another 20426203 steps for small clauses
c [cce-9] scheduling 136134 clauses = 103815 binary + 32319 ternary
c [cce-9] tried to eliminate 1137 small clauses 1%
c [cce-9] eliminated 275 small clauses 0%
c [cce-9] eliminated 213 binary clauses 0%
c [cce-9] eliminated 62 ternary clauses 0%
c [cce-9-1] eliminated 364 small clauses in 40852406 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1120 covered clauses in round 1
c [cce-9] eliminated 1120 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 30078 variables 100%
c [elim-10] limit of 408524053 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 813 variables 3% in round 1 in 18114629 steps
c [elim-10-1] backward subsumption/strengthening limit 36229258
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 5966750 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 813 = 3% variables out of 30078
c [bca-9] limit of 10000000 steps
c [bca-9] 45811 out of 58532 literals actually usable 78%
c [bca-9] added 40 blocked clauses in 111310 steps
c [simplification-10] removed 1499 variables 4.9% (29265 remain 16%)
c [simplification-10] removed 9497 irredundant clauses 4.6% (196179 remain 23%)
c [simplification-10] maximum reduction of 5% = max (5%, 5%)
c [simplification-10] large reduction 5% >= 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 172757
c 
c [simplification-11] limit of 172763 conflicts hit after 172764 conflicts
c [ternres-9] limit 20593395 with penalty 0 = 0 + 0
c [ternres-9] all 29265 free variables schedulable
c [ternres-9] 200 ternary resolvents (3 bin, 197 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-17] removed 20 variables
c [simpleprobe-4] all 29245 free variables schedulable
c [simpleprobe-4] limit 82373583 penalty 0 = 0 + 0
c [decomp-18] removed 121 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 121 variables, found 23072 hbrs, 73 units
c [cgrclsr-5] limit 514834 penalty 2 = 2 + 0
c [cgrclsr-5] all 29124 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-9] limit 12356037 with penalty 0 = 0 + 0
c [lift-9] using 26432 probes 91%
c [lift-9] 88 units, 60 impls, 2 eqs in 1 rounds
c [lift-9] 28073 variables remain 97% (933 retained)
c [lift-9] removed 118 variables
c [cliff-9] limit of 16474716 steps penalty 0 = 0 + 0
c [cliff-9] failed 0, lifted 25
c [unhide-11] limit 4118679 with penalty 0 = 0 + 0
c [unhide-11-18] 3 units, 18 failed, 18877 tauts, 0 hbrs, 73200 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 222 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 28962 variables 100%
c [block-6] limit of 51483489 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 9 blocked clauses
c [block-6] 9 < 1/1000 * 192099 = 192 considered unsuccessful
c [cce-10] limit of 41186791 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 68
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 67
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 62
c [cce-10-1] eliminated 5 clauses out of 6 (83%) of length 61
c [cce-10-1] eliminated 3 clauses out of 5 (60%) of length 60
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 59
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 54
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 52
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 51
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 50
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 49
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 48
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 47
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 46
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 45
c [cce-10-1] eliminated 4 clauses out of 6 (67%) of length 44
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 43
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 42
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 41
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 40
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 39
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 38
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 37
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 36
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 35
c [cce-10-1] eliminated 3 clauses out of 9 (33%) of length 34
c [cce-10-1] eliminated 3 clauses out of 5 (60%) of length 33
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 32
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 30
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 28
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 26
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 22
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 21
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 20
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 19
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 18
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 17
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 16
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 15
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 14
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 13
c [cce-10-1] eliminated 1 clauses out of 8 (12%) of length 12
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 11
c [cce-10-1] eliminated 1 clauses out of 11 (9%) of length 10
c [cce-10-1] eliminated 4 clauses out of 8 (50%) of length 9
c [cce-10-1] eliminated 2 clauses out of 13 (15%) of length 8
c [cce-10-1] eliminated 6 clauses out of 72 (8%) of length 7
c [cce-10-1] eliminated 4 clauses out of 1978 (0%) of length 6
c [cce-10-1] eliminated 91 clauses out of 5903 (2%) of length 5
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 209 large clauses in 41186792 steps
c [cce-10-1] allowing another 20593396 steps for small clauses
c [cce-10] scheduling 131184 clauses = 99998 binary + 31186 ternary
c [cce-10] tried to eliminate 1368 small clauses 1%
c [cce-10] eliminated 341 small clauses 0%
c [cce-10] eliminated 270 binary clauses 0%
c [cce-10] eliminated 71 ternary clauses 0%
c [cce-10-1] eliminated 341 small clauses in 41186792 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 550 covered clauses in round 1
c [cce-10] eliminated 550 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 28962 variables 100%
c [elim-11] limit of 411867916 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 190 variables 1% in round 1 in 15948460 steps
c [elim-11-1] backward subsumption/strengthening limit 31896920
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 5738683 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 190 = 1% variables out of 28962
c [bca-10] limit of 10000000 steps
c [bca-10] 44603 out of 57546 literals actually usable 78%
c [bca-10] added 21 blocked clauses in 109633 steps
c [simplification-11] removed 493 variables 1.7% (28772 remain 16%)
c [simplification-11] removed 5042 irredundant clauses 2.6% (191137 remain 23%)
c [simplification-11] maximum reduction of 3% = max (2%, 3%)
c [simplification-11] geometric conflict interval increment 12799 = 51196 / 4
c [simplification-11] new conflict interval 63995
c [simplification-11] penalized conflict interval 63995 = 1 * 63995
c [simplification-11] new conflict limit 236759
c [tabula-rasa-2] number clauses 191137 drops below limit 194792
c [flush-cache] 0 binary, 0 ternary, 9713 large
c [flushphases] 28772 phases reset fully
c [phase-9] phase bias: 1519 positive 19%, 6387 negative 81%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] new conflict limit 192764
c [tabula-rasa-2] new variable limit 7193 and clause limit 95568
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  127.1   28772   191137    178200    2066   2293 338515   6 132.8 209.5   30
c -  128.2   28772   191137    182545    2627   2306 338515   5 135.1 210.8   29
c -  129.5   28772   191137    188804    3240   2327 338518   3 134.8 210.9   29
c 
c [simplification-12] limit of 192796 conflicts hit after 192798 conflicts
c [ternres-10] limit 22277882 with penalty 0 = 0 + 0
c [ternres-10] all 28772 free variables schedulable
c [ternres-10] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 556947 penalty 3 = 3 + 0
c [gauss-4] extracted 9 xors of average arity 3.0
c [gauss-4] connected 27 occurrences of 27 variables (average 1.0)
c [gauss-4] limit 556947 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 13 variables
c [lift-10] limit 13366729 with penalty 0 = 0 + 0
c [lift-10] using 25813 probes 90%
c [lift-10] 79 units, 77 impls, 34 eqs in 1 rounds
c [lift-10] 27419 variables remain 96% (1199 retained)
c [lift-10] removed 141 variables
c [cliff-10] limit of 17822305 steps penalty 0 = 0 + 0
c [cliff-10] failed 0, lifted 18
c [unhide-12] limit 4455576 with penalty 0 = 0 + 0
c [unhide-12-21] 1 units, 31 failed, 15179 tauts, 0 hbrs, 33823 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 134 transitive binary clauses
c [transred-10] found 1 units
c [cce-11] limit of 44555764 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 3 clauses out of 7 (43%) of length 17
c [cce-11-1] eliminated 3 clauses out of 8 (38%) of length 16
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 15
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 14
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 13
c [cce-11-1] eliminated 2 clauses out of 1979 (0%) of length 6
c [cce-11-1] eliminated 21 clauses out of 5830 (0%) of length 5
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 35 large clauses in 44555765 steps
c [cce-11-1] allowing another 22277882 steps for small clauses
c [cce-11] scheduling 129311 clauses = 98909 binary + 30402 ternary
c [cce-11] tried to eliminate 1360 small clauses 1%
c [cce-11] eliminated 351 small clauses 0%
c [cce-11] eliminated 273 binary clauses 0%
c [cce-11] eliminated 78 ternary clauses 0%
c [cce-11-1] eliminated 403 small clauses in 44555765 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 438 covered clauses in round 1
c [cce-11] eliminated 438 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 28580 variables 100%
c [elim-12] limit of 445557649 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 193 variables 1% in round 1 in 16231247 steps
c [elim-12-1] backward subsumption/strengthening limit 32462494
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 5649302 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 193 = 1% variables out of 28580
c [bca-11] limit of 10000000 steps
c [bca-11] 51104 out of 56776 literals actually usable 90%
c [bca-11] added 32 blocked clauses in 119922 steps
c [rephase-4] after 192798 conflicts (new increment 20000, next 212798)
c [flushphases] 687 phases reset
c [phase-10] phase bias: 3 positive 50%, 3 negative 50%
c [simplification-12] removed 385 variables 1.3% (28387 remain 16%)
c [simplification-12] removed 2788 irredundant clauses 1.5% (188349 remain 23%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-12] new conflict interval 30000
c [simplification-12] penalized conflict interval 30000 = 1 * 30000
c [simplification-12] new conflict limit 222798
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  136.2   28387   188349    195745    3739   2385 354902   6 134.9 211.6   30
c -  138.2   28387   188349    202025    4365   2398 354914   3 139.9 215.4   30
c -  140.7   28387   188349    209298    4956   2404 354925   3 146.6 219.9   30
c -  143.3   28387   188349    217482    5643   2409 354930   4 152.2 223.0   30
c 
c [simplification-13] limit of 222862 conflicts hit after 222862 conflicts
c [ternres-11] limit 25517745 with penalty 0 = 0 + 0
c [ternres-11] all 28387 free variables schedulable
c [ternres-11] 87 ternary resolvents (0 bin, 87 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-20] removed 11 variables
c [lift-11] limit 15310647 with penalty 0 = 0 + 0
c [lift-11] using 25187 probes 89%
c [lift-11] 80 units, 89 impls, 1 eqs in 1 rounds
c [lift-11] 26778 variables remain 95% (1509 retained)
c [lift-11] removed 89 variables
c [cliff-11] limit of 20414196 steps penalty 0 = 0 + 0
c [cliff-11] failed 0, lifted 13
c [unhide-13] limit 5103549 with penalty 0 = 0 + 0
c [unhide-13-25] 0 units, 11 failed, 8947 tauts, 0 hbrs, 407928 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 97 transitive binary clauses
c [transred-11] found 1 units
c [cce-12] limit of 51035490 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 1 (100%) of length 76
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 75
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 65
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-12-1] eliminated 2 clauses out of 5 (40%) of length 63
c [cce-12-1] eliminated 3 clauses out of 5 (60%) of length 62
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 61
c [cce-12-1] eliminated 2 clauses out of 3 (67%) of length 60
c [cce-12-1] eliminated 1 clauses out of 4 (25%) of length 59
c [cce-12-1] eliminated 4 clauses out of 9 (44%) of length 13
c [cce-12-1] eliminated 2 clauses out of 10 (20%) of length 12
c [cce-12-1] eliminated 6 clauses out of 11 (55%) of length 11
c [cce-12-1] eliminated 2 clauses out of 10 (20%) of length 10
c [cce-12-1] eliminated 5 clauses out of 11 (45%) of length 9
c [cce-12-1] eliminated 4 clauses out of 13 (31%) of length 8
c [cce-12-1] eliminated 4 clauses out of 71 (6%) of length 7
c [cce-12-1] eliminated 8 clauses out of 1983 (0%) of length 6
c [cce-12-1] eliminated 32 clauses out of 5833 (1%) of length 5
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 84 large clauses in 51035491 steps
c [cce-12-1] allowing another 25517745 steps for small clauses
c [cce-12] scheduling 127361 clauses = 97626 binary + 29735 ternary
c [cce-12] tried to eliminate 1616 small clauses 1%
c [cce-12] eliminated 381 small clauses 0%
c [cce-12] eliminated 308 binary clauses 0%
c [cce-12] eliminated 73 ternary clauses 0%
c [cce-12-1] eliminated 412 small clauses in 51035491 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 496 covered clauses in round 1
c [cce-12] eliminated 496 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 28261 variables 100%
c [elim-13] limit of 510354902 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 141 variables 0% in round 1 in 15610740 steps
c [elim-13-1] backward subsumption/strengthening limit 31221480
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 5542589 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 141 = 0% variables out of 28261
c [bca-12] limit of 10000000 steps
c [bca-12] 48852 out of 56242 literals actually usable 87%
c [bca-12] added 27 blocked clauses in 118253 steps
c [rephase-5] after 222862 conflicts (new increment 40000, next 262862)
c [flushphases] 293 phases reset
c [phase-11] phase bias: 0 positive 0%, 4 negative 100%
c [simplification-13] removed 267 variables 0.9% (28120 remain 15%)
c [simplification-13] removed 2629 irredundant clauses 1.4% (185720 remain 22%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-13] new conflict interval 45000
c [simplification-13] penalized conflict interval 45000 = 1 * 45000
c [simplification-13] new conflict limit 267862
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  152.6   28120   185720    227563    6046   2515 363158   7 155.1 225.2   30
c -  156.4   28120   185720    245079    6541   2541 363174   6 152.5 224.0   30
c i  158.1   28119   185720    253481    9950   2552 363187   5 150.8 223.4   35
c -  159.7   28117   185720    259943    7168   2557 363190   3 153.0 224.6   31
c 
c [simplification-14] limit of 267994 conflicts hit after 267994 conflicts
c [ternres-12] limit 29081645 with penalty 0 = 0 + 0
c [ternres-12] all 28117 free variables schedulable
c [ternres-12] 99 ternary resolvents (0 bin, 99 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-21] removed 4 variables
c [lift-12] limit 17448987 with penalty 0 = 0 + 0
c [lift-12] using 24622 probes 88%
c [lift-12] 59 units, 80 impls, 3 eqs in 1 rounds
c [lift-12] 26139 variables remain 93% (1895 retained)
c [lift-12] removed 82 variables
c [cliff-12] limit of 23265316 steps penalty 0 = 0 + 0
c [cliff-12] failed 0, lifted 11
c [unhide-14] limit 5816329 with penalty 0 = 0 + 0
c [unhide-14-29] 0 units, 9 failed, 8194 tauts, 0 hbrs, 212873 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 83 transitive binary clauses
c [cce-13] limit of 58163290 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2 clauses out of 3 (67%) of length 70
c [cce-13-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-13-1] eliminated 11 clauses out of 5816 (0%) of length 5
c [cce-13-1] incomplete large round (ACCE)
c [cce-13-1] eliminated 14 large clauses in 58163291 steps
c [cce-13-1] allowing another 29081645 steps for small clauses
c [cce-13] scheduling 125581 clauses = 96470 binary + 29111 ternary
c [cce-13] tried to eliminate 1887 small clauses 2%
c [cce-13] eliminated 427 small clauses 0%
c [cce-13] eliminated 352 binary clauses 0%
c [cce-13] eliminated 75 ternary clauses 0%
c [cce-13-1] eliminated 437 small clauses in 58163291 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 451 covered clauses in round 1
c [cce-13] eliminated 451 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 28010 variables 100%
c [elim-14] limit of 581632909 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 125 variables 0% in round 1 in 15275637 steps
c [elim-14-1] backward subsumption/strengthening limit 30551274
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 5459322 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 125 = 0% variables out of 28010
c [bca-13] limit of 10000000 steps
c [bca-13] 46845 out of 55772 literals actually usable 84%
c [bca-13] added 28 blocked clauses in 115207 steps
c [rephase-6] after 267994 conflicts (new increment 80000, next 347994)
c [flushphases] 80 phases reset
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-14] removed 232 variables 0.8% (27885 remain 15%)
c [simplification-14] removed 2212 irredundant clauses 1.2% (183508 remain 22%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-14] new conflict interval 67500
c [simplification-14] penalized conflict interval 67500 = 1 * 67500
c [simplification-14] new conflict limit 335494
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  171.0   27885   183508    276548    7636   2655 379216   5 155.5 226.7   31
c -  174.5   27885   183508    291593    8098   2672 379223   4 156.2 227.0   31
c -  179.9   27885   183508    315863    8974   2700 379251   5 153.3 225.1   31
c 
c [simplification-15] limit of 335636 conflicts hit after 335640 conflicts
c [ternres-13] limit 34717396 with penalty 0 = 0 + 0
c [ternres-13] all 27885 free variables schedulable
c [ternres-13] 39 ternary resolvents (1 bin, 38 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1084918 penalty 4 = 4 + 0
c [card-5] found 8916 at-most-one constraints of average size 3.8
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1084918 for elimination
c [card-5] 8916 out of 8916 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-22] removed 6 variables
c [treelook-4] limit 216983 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 25831 literals 46%
c [treelook-4] scheduling used 218110 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 216983 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 451800 steps
c [treelook-4] 25825 literals remain 46%
c [treelook-4] 14082 variables remain to probed next time 51%
c [treelook-4] removed 0 variables, found 3068 hbrs
c [cgrclsr-6] limit 433967 penalty 3 = 3 + 0
c [cgrclsr-6] all 27879 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 24002 probes 86%
c [lift-13] 73 units, 72 impls, 6 eqs in 1 rounds
c [lift-13] 25410 variables remain 91% (2361 retained)
c [lift-13] removed 108 variables
c [cliff-13] limit of 27773917 steps penalty 0 = 0 + 0
c [cliff-13] failed 0, lifted 8
c [unhide-15] limit 6943479 with penalty 0 = 0 + 0
c [unhide-15-34] 0 units, 4 failed, 10187 tauts, 0 hbrs, 137410 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 75 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 27759 variables 100%
c [block-7] limit of 43396745 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2 blocked clauses
c [block-7] 2 < 1/1000 * 181967 = 181 considered unsuccessful
c [cce-14] limit of 69434793 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 3 clauses out of 1983 (0%) of length 6
c [cce-14-1] eliminated 21 clauses out of 5823 (0%) of length 5
c [cce-14-1] incomplete large round (ACCE)
c [cce-14-1] eliminated 24 large clauses in 69434794 steps
c [cce-14-1] allowing another 34717397 steps for small clauses
c [cce-14] scheduling 123986 clauses = 95462 binary + 28524 ternary
c [cce-14] tried to eliminate 2488 small clauses 2%
c [cce-14] eliminated 530 small clauses 0%
c [cce-14] eliminated 423 binary clauses 0%
c [cce-14] eliminated 107 ternary clauses 0%
c [cce-14-1] eliminated 530 small clauses in 69434794 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 554 covered clauses in round 1
c [cce-14] eliminated 554 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 27759 variables 100%
c [elim-15] limit of 694347930 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 149 variables 1% in round 1 in 15461351 steps
c [elim-15-1] backward subsumption/strengthening limit 30922702
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 5383283 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 149 = 1% variables out of 27759
c [bca-14] limit of 10000000 steps
c [bca-14] 45683 out of 55222 literals actually usable 83%
c [bca-14] added 26 blocked clauses in 115238 steps
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-15] removed 275 variables 1.0% (27610 remain 15%)
c [simplification-15] removed 2299 irredundant clauses 1.3% (181209 remain 22%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 33750 = 67500 / 2
c [simplification-15] new conflict interval 101250
c [simplification-15] penalized conflict interval 101250 = 1 * 101250
c [simplification-15] new conflict limit 436890
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  194.1   27610   181209    343099    9472   2760 402879   3 153.8 225.7   32
c -  197.8   27610   181209    358286   10038   2777 402897   4 155.2 227.3   32
c -  201.8   27610   181209    375313   10597   2789 402898   3 157.8 228.6   32
c -  206.0   27610   181209    394144   11155   2797 402900   3 161.0 230.1   33
c -  211.2   27610   181209    415184   11734   2805 402904   4 164.4 231.4   33
c -  215.8   27610   181209    433071   12228   2812 402928   3 166.5 233.0   32
c i  216.6   27609   181209    435879   14131   2812 402929   8 166.6 233.3   38
c 
c [simplification-16] limit of 437052 conflicts hit after 437052 conflicts
c [ternres-14] limit 43713803 with penalty 0 = 0 + 0
c [ternres-14] all 27608 free variables schedulable
c [ternres-14] 48 ternary resolvents (0 bin, 48 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-24] removed 5 variables
c [basicprobe-4] limit 43713803 penalty 0 = 0 + 0
c [basicprobe-4-0] 3393 probes remain 12% after last round
c [basicprobe-4-0] 320 units = 313 failed (98%) + 7 lifted (2%)
c [basicprobe-4-0] removed 445 variables, found 150339 hbrs
c [bate-3] eliminated 712 asymmetric tautologies during probing
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 22879 probes 84%
c [lift-14] 67 units, 93 impls, 77 eqs in 1 rounds
c [lift-14] 24160 variables remain 89% (2847 retained)
c [lift-14] removed 153 variables
c [cliff-14] limit of 34971042 steps penalty 0 = 0 + 0
c [cliff-14] failed 0, lifted 20
c [unhide-16] limit 8742760 with penalty 0 = 0 + 0
c [unhide-16-39] 0 units, 7 failed, 26709 tauts, 0 hbrs, 122066 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 70 transitive binary clauses
c [cce-15] limit of 87427607 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 79
c [cce-15-1] eliminated 2 clauses out of 3 (67%) of length 78
c [cce-15-1] eliminated 1 clauses out of 3 (33%) of length 77
c [cce-15-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-15-1] eliminated 2 clauses out of 4 (50%) of length 74
c [cce-15-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-15-1] eliminated 1 clauses out of 3 (33%) of length 72
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 67
c [cce-15-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 65
c [cce-15-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 32
c [cce-15-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 30
c [cce-15-1] eliminated 2 clauses out of 11 (18%) of length 9
c [cce-15-1] eliminated 4 clauses out of 10 (40%) of length 8
c [cce-15-1] eliminated 1 clauses out of 65 (2%) of length 7
c [cce-15-1] eliminated 4 clauses out of 1962 (0%) of length 6
c [cce-15-1] eliminated 67 clauses out of 5765 (1%) of length 5
c [cce-15-1] incomplete large round (ACCE)
c [cce-15-1] eliminated 101 large clauses in 87427608 steps
c [cce-15-1] allowing another 43713804 steps for small clauses
c [cce-15] scheduling 120647 clauses = 93671 binary + 26976 ternary
c [cce-15] tried to eliminate 3503 small clauses 3%
c [cce-15] eliminated 768 small clauses 1%
c [cce-15] eliminated 625 binary clauses 1%
c [cce-15] eliminated 143 ternary clauses 1%
c [cce-15-1] eliminated 774 small clauses in 87427608 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 875 covered clauses in round 1
c [cce-15] eliminated 875 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 26981 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 437 variables 2% in round 1 in 16396013 steps
c [elim-16-1] backward subsumption/strengthening limit 32792026
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 5082269 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 437 = 2% variables out of 26981
c [bca-15] limit of 10000000 steps
c [bca-15] 42573 out of 53090 literals actually usable 80%
c [bca-15] added 38 blocked clauses in 108107 steps
c [rephase-7] after 437052 conflicts (new increment 160000, next 597052)
c [flushphases] 20 phases reset
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-16] removed 1064 variables 3.9% (26544 remain 15%)
c [simplification-16] removed 8476 irredundant clauses 4.7% (172733 remain 21%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] new conflict interval 4370 = min (437052/100, 101250)
c [simplification-16] penalized conflict interval 4370 = 1 * 4370
c [simplification-16] new conflict limit 441422
c 
c [simplification-17] limit of 441432 conflicts hit after 441433 conflicts
c [ternres-15] limit 44098178 with penalty 0 = 0 + 0
c [ternres-15] all 26544 free variables schedulable
c [ternres-15] 226 ternary resolvents (3 bin, 223 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 551227 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 551227 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 13 variables
c [simpleprobe-5] all 26531 free variables schedulable
c [simpleprobe-5] limit 176392713 penalty 0 = 0 + 0
c [decomp-26] removed 55 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 55 variables, found 29635 hbrs, 35 units
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 21634 probes 82%
c [lift-15] 47 units, 77 impls, 0 eqs in 1 rounds
c [lift-15] 23117 variables remain 87% (3306 retained)
c [lift-15] removed 53 variables
c [cliff-15] limit of 35278542 steps penalty 0 = 0 + 0
c [cliff-15] failed 0, lifted 15
c [unhide-17] limit 8819635 with penalty 0 = 0 + 0
c [unhide-17-45] 0 units, 10 failed, 30302 tauts, 0 hbrs, 86648 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 93 transitive binary clauses
c [cce-16] limit of 88196356 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 3 (33%) of length 68
c [cce-16-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-16-1] eliminated 1 clauses out of 6 (17%) of length 18
c [cce-16-1] eliminated 1 clauses out of 5 (20%) of length 17
c [cce-16-1] eliminated 2 clauses out of 11 (18%) of length 16
c [cce-16-1] eliminated 1 clauses out of 10 (10%) of length 15
c [cce-16-1] eliminated 4 clauses out of 10 (40%) of length 14
c [cce-16-1] eliminated 2 clauses out of 8 (25%) of length 13
c [cce-16-1] eliminated 4 clauses out of 10 (40%) of length 12
c [cce-16-1] eliminated 1 clauses out of 7 (14%) of length 11
c [cce-16-1] eliminated 2 clauses out of 12 (17%) of length 10
c [cce-16-1] eliminated 2 clauses out of 12 (17%) of length 9
c [cce-16-1] eliminated 4 clauses out of 11 (36%) of length 8
c [cce-16-1] eliminated 5 clauses out of 70 (7%) of length 7
c [cce-16-1] eliminated 6 clauses out of 1974 (0%) of length 6
c [cce-16-1] eliminated 10 clauses out of 5813 (0%) of length 5
c [cce-16-1] incomplete large round (ACCE)
c [cce-16-1] eliminated 47 large clauses in 88196357 steps
c [cce-16-1] allowing another 44098178 steps for small clauses
c [cce-16] scheduling 123593 clauses = 91721 binary + 31872 ternary
c [cce-16] tried to eliminate 3354 small clauses 3%
c [cce-16] eliminated 654 small clauses 1%
c [cce-16] eliminated 528 binary clauses 1%
c [cce-16] eliminated 126 ternary clauses 0%
c [cce-16-1] eliminated 675 small clauses in 88196357 steps
c [cce-16-1] incomplete small round (ACCE)
c [cce-16-1] eliminated 722 covered clauses in round 1
c [cce-16] eliminated 722 covered clauses in TOTAL during 1 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 26399 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 138 variables 1% in round 1 in 14506566 steps
c [elim-17-1] backward subsumption/strengthening limit 29013132
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 4982660 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 138 = 1% variables out of 26399
c [bca-16] limit of 10000000 steps
c [bca-16] 41377 out of 52524 literals actually usable 79%
c [bca-16] added 21 blocked clauses in 107221 steps
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-17] removed 283 variables 1.1% (26261 remain 14%)
c [simplification-17] removed 2690 irredundant clauses 1.6% (170043 remain 20%)
c [simplification-17] maximum reduction of 2% = max (1%, 2%)
c [simplification-17] geometric conflict interval increment 33750 = 101250 / 3
c [simplification-17] new conflict interval 135000
c [simplification-17] penalized conflict interval 135000 = 1 * 135000
c [simplification-17] new conflict limit 576433
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  243.6   26261   170043    460004   12687   3533 494986  10 169.4 236.2   35
c -  249.6   26261   170043    483128   13202   3549 494993   3 172.7 238.8   34
c -  256.6   26261   170043    507846   13750   3571 495012   6 174.2 240.3   34
c -  264.5   26261   170043    531816   14399   3582 495027   3 178.8 244.1   34
c -  272.7   26261   170043    556475   14944   3596 495042   3 183.0 246.8   34
c 
c [simplification-18] limit of 576571 conflicts hit after 576572 conflicts
c [ternres-16] limit 57846694 with penalty 0 = 0 + 0
c [ternres-16] all 26261 free variables schedulable
c [ternres-16] 82 ternary resolvents (2 bin, 80 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-27] removed 11 variables
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 20920 probes 80%
c [lift-16] 24 units, 81 impls, 0 eqs in 1 rounds
c [lift-16] 22408 variables remain 85% (3805 retained)
c [lift-16] removed 37 variables
c [cliff-16] limit of 46277355 steps penalty 0 = 0 + 0
c [cliff-16] failed 0, lifted 1
c [unhide-18] limit 11569338 with penalty 0 = 0 + 0
c [unhide-18-52] 0 units, 5 failed, 10987 tauts, 0 hbrs, 442578 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 65 transitive binary clauses
c [cce-17] limit of 115693389 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 2 clauses out of 8 (25%) of length 13
c [cce-17-1] eliminated 1 clauses out of 8 (12%) of length 12
c [cce-17-1] eliminated 1 clauses out of 8 (12%) of length 11
c [cce-17-1] eliminated 2 clauses out of 13 (15%) of length 10
c [cce-17-1] eliminated 1 clauses out of 1970 (0%) of length 6
c [cce-17-1] eliminated 139 clauses out of 5803 (2%) of length 5
c [cce-17-1] eliminated 1377 clauses out of 13017 (11%) of length 4
c [cce-17-1] incomplete large round (ACCE)
c [cce-17-1] eliminated 1523 large clauses in 115693390 steps
c [cce-17-1] allowing another 57846695 steps for small clauses
c [cce-17] scheduling 122218 clauses = 90820 binary + 31398 ternary
c [cce-17] tried to eliminate 4371 small clauses 4%
c [cce-17] eliminated 760 small clauses 1%
c [cce-17] eliminated 592 binary clauses 1%
c [cce-17] eliminated 168 ternary clauses 1%
c [cce-17-1] eliminated 760 small clauses in 115693390 steps
c [cce-17-1] incomplete small round (ACCE)
c [cce-17-1] eliminated 2283 covered clauses in round 1
c [cce-17] eliminated 2283 covered clauses in TOTAL during 1 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 26208 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 636 variables 2% in round 1 in 14586165 steps
c [elim-18-1] backward subsumption/strengthening limit 29172330
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 4881757 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 636 = 2% variables out of 26208
c [bca-17] limit of 10000000 steps
c [bca-17] 39122 out of 51146 literals actually usable 76%
c [bca-17] added 70 blocked clauses in 109738 steps
c [simplification-18] removed 689 variables 2.6% (25572 remain 14%)
c [simplification-18] removed 3451 irredundant clauses 2.0% (166592 remain 20%)
c [simplification-18] maximum reduction of 3% = max (3%, 2%)
c [simplification-18] geometric conflict interval increment 33750 = 135000 / 4
c [simplification-18] new conflict interval 168750
c [simplification-18] penalized conflict interval 168750 = 1 * 168750
c [simplification-18] new conflict limit 745322
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  298.6   25572   166592    593426   15583   3678 481384   5 184.1 248.2   35
c -  304.7   25572   166592    619773   16070   3687 481384   5 180.2 246.9   34
c -  312.8   25572   166592    658545   16623   3697 481384   4 177.1 245.4   36
c -  322.1   25572   166592    698412   17027   3709 481384   7 177.6 245.5   34
c -  330.7   25572   166592    742254   17694   3716 481384   4 174.5 243.5   34
c 
c [simplification-19] limit of 745332 conflicts hit after 745333 conflicts
c [ternres-17] limit 71436976 with penalty 0 = 0 + 0
c [ternres-17] all 25572 free variables schedulable
c [ternres-17] 50 ternary resolvents (2 bin, 48 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-28] removed 1 variables
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 20141 probes 79%
c [lift-17] 21 units, 93 impls, 1 eqs in 1 rounds
c [lift-17] 21220 variables remain 83% (4322 retained)
c [lift-17] removed 29 variables
c [cliff-17] limit of 57149581 steps penalty 0 = 0 + 0
c [cliff-17] failed 0, lifted 3
c [unhide-19] limit 14287395 with penalty 0 = 0 + 0
c [unhide-19-61] 0 units, 1 failed, 7565 tauts, 0 hbrs, 55197 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 54 transitive binary clauses
c [cce-18] limit of 142873953 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 85
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 84
c [cce-18-1] eliminated 2 clauses out of 3 (67%) of length 83
c [cce-18-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-18-1] eliminated 1 clauses out of 3 (33%) of length 81
c [cce-18-1] eliminated 2 clauses out of 3 (67%) of length 80
c [cce-18-1] eliminated 1 clauses out of 3 (33%) of length 79
c [cce-18-1] eliminated 2 clauses out of 2 (100%) of length 78
c [cce-18-1] eliminated 1 clauses out of 3 (33%) of length 77
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 76
c [cce-18-1] eliminated 2 clauses out of 7 (29%) of length 14
c [cce-18-1] eliminated 1 clauses out of 8 (12%) of length 13
c [cce-18-1] eliminated 1 clauses out of 9 (11%) of length 12
c [cce-18-1] eliminated 2 clauses out of 5 (40%) of length 11
c [cce-18-1] eliminated 1 clauses out of 14 (7%) of length 10
c [cce-18-1] eliminated 2 clauses out of 12 (17%) of length 9
c [cce-18-1] eliminated 1 clauses out of 8 (12%) of length 8
c [cce-18-1] eliminated 3 clauses out of 65 (5%) of length 7
c [cce-18-1] eliminated 52 clauses out of 1973 (3%) of length 6
c [cce-18-1] eliminated 392 clauses out of 6046 (6%) of length 5
c [cce-18-1] eliminated 1206 clauses out of 12080 (10%) of length 4
c [cce-18-1] incomplete large round (ACCE)
c [cce-18-1] eliminated 1676 large clauses in 142873954 steps
c [cce-18-1] allowing another 71436977 steps for small clauses
c [cce-18] scheduling 119749 clauses = 88786 binary + 30963 ternary
c [cce-18] tried to eliminate 5488 small clauses 5%
c [cce-18] eliminated 990 small clauses 1%
c [cce-18] eliminated 789 binary clauses 1%
c [cce-18] eliminated 201 ternary clauses 1%
c [cce-18-1] eliminated 990 small clauses in 142873954 steps
c [cce-18-1] incomplete small round (ACCE)
c [cce-18-1] eliminated 2666 covered clauses in round 1
c [cce-18] eliminated 2666 covered clauses in TOTAL during 1 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 25537 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 258 variables 1% in round 1 in 14401735 steps
c [elim-19-1] backward subsumption/strengthening limit 28803470
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 4674518 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 258 = 1% variables out of 25537
c [bca-18] limit of 10000000 steps
c [bca-18] 39873 out of 50560 literals actually usable 79%
c [bca-18] added 139 blocked clauses in 104869 steps
c [rephase-8] after 745333 conflicts (new increment 320000, next 1065333)
c [flushphases] 0 phases reset
c [simplification-19] removed 293 variables 1.1% (25279 remain 14%)
c [simplification-19] removed 3756 irredundant clauses 2.3% (162836 remain 19%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 56250 = 168750 / 3
c [simplification-19] new conflict interval 225000
c [simplification-19] penalized conflict interval 225000 = 1 * 225000
c [simplification-19] new conflict limit 970333
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  344.1   25278   162836    753076   18891   3847 465722   7 174.5 243.8   43
c -  352.4   25276   162836    780813   18343   3892 465746   4 178.9 249.0   35
c -  358.2   25276   162836    803773   18693   3893 465749   7 179.2 251.3   35
c -  364.9   25276   162836    831222   19409   3911 465757   5 181.2 254.8   35
c -  372.6   25276   162836    860367   19906   3927 465762   5 183.6 259.1   35
c -  378.0   25276   162836    885528   20423   3940 465771   3 184.7 262.3   35
c -  383.8   25276   162836    912032   20961   3946 465773   4 186.4 265.8   35
c -  390.3   25276   162836    938982   21445   3954 465774   4 187.8 269.0   35
c -  396.9   25276   162836    965279   22016   3956 465776   3 188.9 272.1   35
c 
c [simplification-20] limit of 970469 conflicts hit after 970470 conflicts
c [ternres-18] limit 91068457 with penalty 0 = 0 + 0
c [ternres-18] all 25276 free variables schedulable
c [ternres-18] 68 ternary resolvents (3 bin, 65 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-29] removed 6 variables
c [cgrclsr-7] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-7] all 25273 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [lift-18] limit 20000000 with penalty 0 = 0 + 0
c [lift-18] using 19331 probes 76%
c [lift-18] 30 units, 92 impls, 2 eqs in 1 rounds
c [lift-18] 20337 variables remain 81% (4842 retained)
c [lift-18] removed 94 variables
c [cliff-18] limit of 72854765 steps penalty 0 = 0 + 0
c [cliff-18] failed 5, lifted 33
c [unhide-20] limit 18213691 with penalty 0 = 0 + 0
c [unhide-20-72] 0 units, 6 failed, 18365 tauts, 0 hbrs, 285021 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 54 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 25121 variables 100%
c [block-8] limit of 50000000 steps penalty 4 = 4 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 2 blocked clauses
c [block-8] 2 < 1/1000 * 161191 = 161 considered unsuccessful
c [cce-19] limit of 182136914 steps penalty 0 = 0 + 0
c [cce-19-1] eliminated 1 clauses out of 1 (100%) of length 82
c [cce-19-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-19-1] eliminated 2 clauses out of 3 (67%) of length 80
c [cce-19-1] eliminated 4 clauses out of 64 (6%) of length 7
c [cce-19-1] eliminated 13 clauses out of 1933 (1%) of length 6
c [cce-19-1] eliminated 55 clauses out of 5688 (1%) of length 5
c [cce-19-1] eliminated 1368 clauses out of 10888 (13%) of length 4
c [cce-19-1] incomplete large round (ACCE)
c [cce-19-1] eliminated 1444 large clauses in 182136915 steps
c [cce-19-1] allowing another 91068457 steps for small clauses
c [cce-19] scheduling 112642 clauses = 87533 binary + 25109 ternary
c [cce-19] tried to eliminate 7339 small clauses 7%
c [cce-19] eliminated 1255 small clauses 1%
c [cce-19] eliminated 980 binary clauses 1%
c [cce-19] eliminated 275 ternary clauses 1%
c [cce-19-1] eliminated 1255 small clauses in 182136915 steps
c [cce-19-1] incomplete small round (ACCE)
c [cce-19-1] eliminated 2699 covered clauses in round 1
c [cce-19] eliminated 2699 covered clauses in TOTAL during 1 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 25121 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20-1] eliminated 281 variables 1% in round 1 in 13311435 steps
c [elim-20-1] backward subsumption/strengthening limit 26622870
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 4438158 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 281 = 1% variables out of 25121
c [bca-19] limit of 10000000 steps
c [bca-19] 37376 out of 49682 literals actually usable 75%
c [bca-19] added 139 blocked clauses in 109708 steps
c [simplification-20] removed 436 variables 1.7% (24840 remain 14%)
c [simplification-20] removed 4699 irredundant clauses 2.9% (158137 remain 19%)
c [simplification-20] maximum reduction of 3% = max (2%, 3%)
c [simplification-20] geometric conflict interval increment 56250 = 225000 / 4
c [simplification-20] new conflict interval 281250
c [simplification-20] penalized conflict interval 281250 = 1 * 281250
c [simplification-20] new conflict limit 1251720
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  415.1   24839   158137    971587   26512   4081 457452   4 188.6 273.0   47
c i  416.4   24838   158137    976996   29444   4089 457457   5 188.9 273.4   53
c -  425.6   24813   158137   1015474   22456   4102 457462   6 186.7 271.2   36
c -  443.7   24813   158137   1090976   23029   4125 457474   4 183.8 267.5   36
c -  458.9   24813   158137   1149968   23845   4158 457500   6 185.2 267.6   36
c i  462.7   24812   158137   1170582   30862   4161 457502   4 184.7 267.0   51
c -  471.9   24712   158137   1205320   24344   4203 457524  11 184.2 266.5   35
c 
c [simplification-21] limit of 1251926 conflicts hit after 1251926 conflicts
c [ternres-19] limit 116753534 with penalty 0 = 0 + 0
c [ternres-19] all 24712 free variables schedulable
c [ternres-19] 98 ternary resolvents (3 bin, 95 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 3648547 penalty 4 = 4 + 0
c [card-6] found 9368 at-most-one constraints of average size 3.7
c [card-6] found 1244 at-most-two constraints of average size 4.7
c [card-6] using previous limit 3648547 for elimination
c [card-6] 10541 out of 10612 constraints (99%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-30] removed 129 variables
c [lift-19] limit 20000000 with penalty 0 = 0 + 0
c [lift-19] using 18282 probes 74%
c [lift-19] 31 units, 80 impls, 2 eqs in 1 rounds
c [lift-19] 19342 variables remain 78% (5329 retained)
c [lift-19] removed 40 variables
c [cliff-19] limit of 93402827 steps penalty 0 = 0 + 0
c [cliff-19] failed 5, lifted 10
c [unhide-21] limit 20000000 with penalty 0 = 0 + 0
c [unhide-21-83] 0 units, 3 failed, 25915 tauts, 0 hbrs, 602859 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 52 transitive binary clauses
c [cce-20] limit of 233507069 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 94
c [cce-20-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 92
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 90
c [cce-20-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-20-1] eliminated 1 clauses out of 7 (14%) of length 21
c [cce-20-1] eliminated 1 clauses out of 10 (10%) of length 20
c [cce-20-1] eliminated 3 clauses out of 9 (33%) of length 19
c [cce-20-1] eliminated 4 clauses out of 7 (57%) of length 18
c [cce-20-1] eliminated 3 clauses out of 9 (33%) of length 17
c [cce-20-1] eliminated 4 clauses out of 12 (33%) of length 16
c [cce-20-1] eliminated 6 clauses out of 15 (40%) of length 15
c [cce-20-1] eliminated 4 clauses out of 14 (29%) of length 14
c [cce-20-1] eliminated 5 clauses out of 12 (42%) of length 13
c [cce-20-1] eliminated 3 clauses out of 11 (27%) of length 12
c [cce-20-1] eliminated 4 clauses out of 10 (40%) of length 11
c [cce-20-1] eliminated 6 clauses out of 15 (40%) of length 10
c [cce-20-1] eliminated 6 clauses out of 22 (27%) of length 9
c [cce-20-1] eliminated 9 clauses out of 16 (56%) of length 8
c [cce-20-1] eliminated 8 clauses out of 72 (11%) of length 7
c [cce-20-1] eliminated 6 clauses out of 1944 (0%) of length 6
c [cce-20-1] eliminated 28 clauses out of 5451 (1%) of length 5
c [cce-20-1] eliminated 646 clauses out of 9339 (7%) of length 4
c [cce-20-1] completed large round (ACCE)
c [cce-20-1] eliminated 753 large clauses in 191936555 steps
c [cce-20-1] allowing another 95968277 steps for small clauses
c [cce-20] scheduling 110343 clauses = 85948 binary + 24395 ternary
c [cce-20] tried to eliminate 10968 small clauses 10%
c [cce-20] eliminated 1795 small clauses 2%
c [cce-20] eliminated 1392 binary clauses 2%
c [cce-20] eliminated 403 ternary clauses 2%
c [cce-20-1] eliminated 1795 small clauses in 233507070 steps
c [cce-20-1] incomplete small round (ACCE)
c [cce-20-1] eliminated 2548 covered clauses in round 1
c [cce-20] eliminated 2548 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 24647 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21-1] eliminated 268 variables 1% in round 1 in 12727174 steps
c [elim-21-1] backward subsumption/strengthening limit 25454348
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 4214411 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 268 = 1% variables out of 24647
c [bca-20] limit of 10000000 steps
c [bca-20] 34603 out of 48760 literals actually usable 71%
c [bca-20] added 127 blocked clauses in 113707 steps
c [rephase-9] after 1251926 conflicts (new increment 640000, next 1891926)
c [flushphases] 0 phases reset
c [simplification-21] removed 333 variables 1.3% (24379 remain 13%)
c [simplification-21] removed 4780 irredundant clauses 3.0% (153357 remain 18%)
c [simplification-21] maximum reduction of 3% = max (1%, 3%)
c [simplification-21] geometric conflict interval increment 70312 = 281250 / 4
c [simplification-21] new conflict interval 351562
c [simplification-21] penalized conflict interval 351562 = 1 * 351562
c [simplification-21] new conflict limit 1603488
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  513.2   24379   153357   1274250   24911   4443 450071   6 186.6 267.5   34
c -  530.1   24379   153357   1327634   25433   4455 450077   5 190.9 270.1   34
c -  544.2   24379   153357   1372786   25971   4479 450084   5 193.4 272.9   34
c -  560.6   24379   153357   1426481   26580   4498 450097   6 196.0 274.9   34
c -  574.5   24379   153357   1472764   27209   4518 450105   4 198.2 277.2   34
c -  589.4   24379   153357   1518491   27633   4535 450113   4 201.0 280.6   52
c -  605.2   24379   153357   1571667   28203   4554 450116   6 204.3 283.3   52
c 
c [simplification-22] limit of 1603594 conflicts hit after 1603595 conflicts
c [ternres-20] limit 152857753 with penalty 0 = 0 + 0
c [ternres-20] all 24379 free variables schedulable
c [ternres-20] 302 ternary resolvents (3 bin, 299 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-31] removed 2 variables
c [treelook-5] limit 477680 penalty 4 = 4 + 0 boost 1
c [treelook-5] scheduled 32261 literals 66%
c [treelook-5] scheduling used 477721 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 477680 penalty 4 = 4 + 0 boost 1
c [treelook-5] used 504272 steps
c [treelook-5] 32250 literals remain 66%
c [treelook-5] 11881 variables remain to probed next time 49%
c [treelook-5] removed 0 variables, found 1478 hbrs
c [lift-20] limit 20000000 with penalty 0 = 0 + 0
c [lift-20] using 17401 probes 71%
c [lift-20] 45 units, 90 impls, 0 eqs in 1 rounds
c [lift-20] 18501 variables remain 76% (5829 retained)
c [lift-20] removed 47 variables
c [cliff-20] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-20] failed 3, lifted 7
c [unhide-22] limit 20000000 with penalty 0 = 0 + 0
c [unhide-22-94] 0 units, 3 failed, 12089 tauts, 0 hbrs, 1126668 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 48 transitive binary clauses
c [cce-21] limit of 305715506 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 1 clauses out of 1 (100%) of length 69
c [cce-21-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-21-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-21-1] eliminated 2 clauses out of 6 (33%) of length 42
c [cce-21-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 38
c [cce-21-1] eliminated 1 clauses out of 4 (25%) of length 37
c [cce-21-1] eliminated 1 clauses out of 4 (25%) of length 36
c [cce-21-1] eliminated 2 clauses out of 7 (29%) of length 35
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 34
c [cce-21-1] eliminated 2 clauses out of 7 (29%) of length 33
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-21-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 30
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-21-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-21-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-21-1] eliminated 2 clauses out of 6 (33%) of length 26
c [cce-21-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-21-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-21-1] eliminated 1 clauses out of 8 (12%) of length 23
c [cce-21-1] eliminated 2 clauses out of 8 (25%) of length 22
c [cce-21-1] eliminated 1 clauses out of 7 (14%) of length 21
c [cce-21-1] eliminated 2 clauses out of 8 (25%) of length 20
c [cce-21-1] eliminated 1 clauses out of 10 (10%) of length 19
c [cce-21-1] eliminated 2 clauses out of 7 (29%) of length 18
c [cce-21-1] eliminated 1 clauses out of 9 (11%) of length 17
c [cce-21-1] eliminated 1 clauses out of 9 (11%) of length 16
c [cce-21-1] eliminated 4 clauses out of 12 (33%) of length 15
c [cce-21-1] eliminated 2 clauses out of 11 (18%) of length 14
c [cce-21-1] eliminated 2 clauses out of 14 (14%) of length 13
c [cce-21-1] eliminated 5 clauses out of 15 (33%) of length 12
c [cce-21-1] eliminated 4 clauses out of 9 (44%) of length 11
c [cce-21-1] eliminated 4 clauses out of 15 (27%) of length 10
c [cce-21-1] eliminated 4 clauses out of 22 (18%) of length 9
c [cce-21-1] eliminated 5 clauses out of 13 (38%) of length 8
c [cce-21-1] eliminated 4 clauses out of 67 (6%) of length 7
c [cce-21-1] eliminated 7 clauses out of 1958 (0%) of length 6
c [cce-21-1] eliminated 11 clauses out of 5392 (0%) of length 5
c [cce-21-1] eliminated 59 clauses out of 8803 (1%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 149 large clauses in 185218901 steps
c [cce-21-1] allowing another 92609450 steps for small clauses
c [cce-21] scheduling 112411 clauses = 84112 binary + 28299 ternary
c [cce-21] tried to eliminate 16451 small clauses 15%
c [cce-21] eliminated 2276 small clauses 2%
c [cce-21] eliminated 1761 binary clauses 2%
c [cce-21] eliminated 515 ternary clauses 2%
c [cce-21-1] eliminated 2276 small clauses in 305715507 steps
c [cce-21-1] incomplete small round (ACCE)
c [cce-21-1] eliminated 2425 covered clauses in round 1
c [cce-21] eliminated 2425 covered clauses in TOTAL during 1 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 24313 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22-1] eliminated 159 variables 1% in round 1 in 12077606 steps
c [elim-22-1] backward subsumption/strengthening limit 24155212
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 4077516 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 159 = 1% variables out of 24313
c [bca-21] limit of 10000000 steps
c [bca-21] 34099 out of 48310 literals actually usable 71%
c [bca-21] added 98 blocked clauses in 115397 steps
c [simplification-22] removed 225 variables 0.9% (24154 remain 13%)
c [simplification-22] removed 3353 irredundant clauses 2.2% (150004 remain 18%)
c [simplification-22] maximum reduction of 2% = max (1%, 2%)
c [simplification-22] geometric conflict interval increment 117187 = 351562 / 3
c [simplification-22] new conflict interval 468749
c [simplification-22] penalized conflict interval 468749 = 1 * 468749
c [simplification-22] new conflict limit 2072344
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  642.5   24153   150004   1605694   40544   5091 452261   6 206.3 284.9   61
c -  651.6   24150   150004   1640910   28582   5111 452283   5 205.6 284.2   34
c -  667.7   24150   150004   1702593   29141   5134 452296   7 204.6 283.2   34
c -  685.0   24150   150004   1765587   29848   5151 452315   8 204.0 282.8   34
c -  705.8   24150   150004   1837420   30315   5171 452321   5 204.4 282.7   34
c -  721.1   24150   150004   1894842   30874   5188 452342   6 204.5 283.2   34
c -  736.8   24150   150004   1953331   31540   5201 452348   7 204.0 282.9   52
c -  754.6   24150   150004   2015825   32057   5217 452358   6 205.4 284.4   52
c 
c [simplification-23] limit of 2072590 conflicts hit after 2072590 conflicts
c [ternres-21] limit 197115094 with penalty 0 = 0 + 0
c [ternres-21] all 24150 free variables schedulable
c [ternres-21] 108 ternary resolvents (2 bin, 106 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 2463938 penalty 4 = 4 + 0
c [gauss-6] extracted 19 xors of average arity 3.0
c [gauss-6] connected 57 occurrences of 42 variables (average 1.4)
c [gauss-6] limit 2463938 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-5] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 4690 sched 20%, 172 failed, 5 lifted, 59828 hbrs
c [decomp-34] removed 194 variables
c [basicprobe-5-1] 3423 probes remain 14% after last round
c [basicprobe-5-1] 218 units = 213 failed (98%) + 5 lifted (2%)
c [basicprobe-5-1] removed 241 variables, found 75422 hbrs
c [bate-4] eliminated 573 asymmetric tautologies during probing
c [lift-21] limit 20000000 with penalty 0 = 0 + 0
c [lift-21] using 16379 probes 69%
c [lift-21] 15 units, 66 impls, 2 eqs in 1 rounds
c [lift-21] 17535 variables remain 73% (6357 retained)
c [lift-21] removed 17 variables
c [cliff-21] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-21] failed 0, lifted 4
c [unhide-23] limit 20000000 with penalty 0 = 0 + 0
c [unhide-23-104] 0 units, 1 failed, 23087 tauts, 0 hbrs, 1132832 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 59 transitive binary clauses
c [cce-22] limit of 394230188 steps penalty 0 = 0 + 0
c [cce-22-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-22-1] eliminated 1 clauses out of 1 (100%) of length 102
c [cce-22-1] eliminated 2 clauses out of 2 (100%) of length 101
c [cce-22-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-22-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-22-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-22-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-22-1] eliminated 2 clauses out of 2 (100%) of length 96
c [cce-22-1] eliminated 1 clauses out of 1 (100%) of length 94
c [cce-22-1] eliminated 3 clauses out of 13 (23%) of length 10
c [cce-22-1] eliminated 2 clauses out of 19 (11%) of length 9
c [cce-22-1] eliminated 2 clauses out of 9 (22%) of length 8
c [cce-22-1] eliminated 1 clauses out of 67 (1%) of length 7
c [cce-22-1] eliminated 4 clauses out of 1961 (0%) of length 6
c [cce-22-1] eliminated 16 clauses out of 5371 (0%) of length 5
c [cce-22-1] eliminated 43 clauses out of 8548 (1%) of length 4
c [cce-22-1] completed large round (ACCE)
c [cce-22-1] eliminated 83 large clauses in 175044873 steps
c [cce-22-1] allowing another 87522436 steps for small clauses
c [cce-22] scheduling 104547 clauses = 82250 binary + 22297 ternary
c [cce-22] tried to eliminate 25849 small clauses 25%
c [cce-22] eliminated 3273 small clauses 3%
c [cce-22] eliminated 2500 binary clauses 3%
c [cce-22] eliminated 773 ternary clauses 3%
c [cce-22-1] eliminated 3273 small clauses in 394230189 steps
c [cce-22-1] incomplete small round (ACCE)
c [cce-22-1] eliminated 3356 covered clauses in round 1
c [cce-22] eliminated 3356 covered clauses in TOTAL during 1 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 23886 variables 100%
c [elim-23] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-23-1] eliminated 346 variables 1% in round 1 in 11409934 steps
c [elim-23-1] backward subsumption/strengthening limit 22819868
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 3821612 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 346 = 1% variables out of 23886
c [bca-22] limit of 10000000 steps
c [bca-22] 32136 out of 47082 literals actually usable 68%
c [bca-22] added 34 blocked clauses in 123818 steps
c [rephase-10] after 2072590 conflicts (new increment 1280000, next 3352590)
c [flushphases] 0 phases reset
c [simplification-23] removed 610 variables 2.5% (23540 remain 13%)
c [simplification-23] removed 6975 irredundant clauses 4.6% (143029 remain 17%)
c [simplification-23] maximum reduction of 5% = max (3%, 5%)
c [simplification-23] large reduction 5% >= 5% limit
c [simplification-23] new conflict interval 20725 = min (2072590/100, 468749)
c [simplification-23] penalized conflict interval 20725 = 1 * 20725
c [simplification-23] new conflict limit 2093315
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  813.8   23540   143029   2085946   32509   5880 463645   6 206.7 286.4   37
c 
c [simplification-24] limit of 2093331 conflicts hit after 2093331 conflicts
c [ternres-22] limit 199031063 with penalty 0 = 0 + 0
c [ternres-22] all 23540 free variables schedulable
c [ternres-22] 301 ternary resolvents (9 bin, 292 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-35] removed 1 variables
c [simpleprobe-6] all 23539 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-36] removed 2 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 2 variables, found 19199 hbrs, 1 units
c [lift-22] limit 20000000 with penalty 0 = 0 + 0
c [lift-22] using 15403 probes 65%
c [lift-22] 16 units, 80 impls, 2 eqs in 1 rounds
c [lift-22] 16576 variables remain 70% (6943 retained)
c [lift-22] removed 18 variables
c [cliff-22] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-22] failed 0, lifted 7
c [unhide-24] limit 20000000 with penalty 0 = 0 + 0
c [unhide-24-115] 0 units, 2 failed, 24385 tauts, 0 hbrs, 311858 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 88 transitive binary clauses
c [cce-23] limit of 398062126 steps penalty 0 = 0 + 0
c [cce-23-1] eliminated 5 clauses out of 16 (31%) of length 10
c [cce-23-1] eliminated 4 clauses out of 1976 (0%) of length 6
c [cce-23-1] eliminated 17 clauses out of 5430 (0%) of length 5
c [cce-23-1] eliminated 82 clauses out of 8732 (1%) of length 4
c [cce-23-1] completed large round (ACCE)
c [cce-23-1] eliminated 108 large clauses in 175574552 steps
c [cce-23-1] allowing another 87787276 steps for small clauses
c [cce-23] scheduling 104892 clauses = 79098 binary + 25794 ternary
c [cce-23] tried to eliminate 24270 small clauses 23%
c [cce-23] eliminated 2343 small clauses 2%
c [cce-23] eliminated 1770 binary clauses 2%
c [cce-23] eliminated 573 ternary clauses 2%
c [cce-23-1] eliminated 2343 small clauses in 398062127 steps
c [cce-23-1] incomplete small round (ACCE)
c [cce-23-1] eliminated 2451 covered clauses in round 1
c [cce-23] eliminated 2451 covered clauses in TOTAL during 1 rounds
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 23509 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24-1] eliminated 147 variables 1% in round 1 in 10787395 steps
c [elim-24-1] backward subsumption/strengthening limit 21574790
c [elim-24-1] subsumed 0 and strengthened 0 clauses in 3705965 steps
c [elim-24] fully completed in 1 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 147 = 1% variables out of 23509
c [bca-23] limit of 10000000 steps
c [bca-23] 32241 out of 46726 literals actually usable 69%
c [bca-23] added 30 blocked clauses in 108111 steps
c [simplification-24] removed 178 variables 0.8% (23362 remain 13%)
c [simplification-24] removed 2985 irredundant clauses 2.1% (140044 remain 17%)
c [simplification-24] maximum reduction of 2% = max (1%, 2%)
c [simplification-24] geometric conflict interval increment 156249 = 468749 / 3
c [simplification-24] new conflict interval 624998
c [simplification-24] penalized conflict interval 624998 = 1 * 624998
c [simplification-24] new conflict limit 2718329
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  862.4   23362   140044   2175522   32974   6420 462657   5 205.6 284.6   34
c -  887.9   23362   140044   2280519   33586   6444 462666   4 201.5 280.6   34
c -  908.6   23362   140044   2377245   34108   6458 462670   5 197.3 276.7   52
c -  927.7   23362   140044   2461911   34812   6476 462683   5 194.5 273.9   52
c -  946.4   23362   140044   2531510   35358   6490 462689   5 194.2 273.6   52
c -  968.4   23362   140044   2612869   35981   6514 462702   6 193.5 272.6   52
c -  994.7   23362   140044   2713741   36394   6530 462710   6 193.0 271.2   52
c 
c [simplification-25] limit of 2718469 conflicts hit after 2718469 conflicts
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 23362 free variables schedulable
c [ternres-23] 115 ternary resolvents (5 bin, 110 trn)
c [ternres-23] fully completed ternary resolution
c [lift-23] limit 20000000 with penalty 0 = 0 + 0
c [lift-23] using 14591 probes 62%
c [lift-23] 9 units, 88 impls, 0 eqs in 1 rounds
c [lift-23] 15807 variables remain 68% (7545 retained)
c [lift-23] removed 10 variables
c [cliff-23] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-23] failed 1, lifted 1
c [unhide-25] limit 20000000 with penalty 0 = 0 + 0
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1729 basic ate = 1375 trn 80% + 354 lrg 20% in 4 updates
c bcas: 23 count, 1544 added (71 skipped), 2876099 steps
c bkwd: tried 4535544 clauses, 9071070 lits, 2.00 lits/clause
c bkwd: checked 100693847 occs, 22.20 occs/clause, 11.10 occs/lit
c bkwd: subsumed 0 binary, 16 ternary, 2 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 5 large (0% self)
c blkd: 8 bces, 8751 removed, 5921411 resolutions, 20192130 steps
c blkd: 13178 blocking literals 3%, 37 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 0 am1, 16777122 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 164715 subsumed
c card: 76577 at-most-one constraints found, average size 4.27
c card: 76577 at-most-one constraints used 100%, average size 4.27
c card: 3297 at-most-two constraints found, average size 4.95
c card: 3200 at-most-two constraints used 97%, average size 4.97
c cces: 23 cces, 56127 eliminated, 54200 ate 97%, 1927 abce 3%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 7 count, 2969342 esteps, 180673 csteps
c cgrs: 1 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: 4150 extracted (3928 ands 95%, 221 xors 5%, 1 ites 0%)
c clff: 23 cliffs, 774 lifted, 46 failed
c clff: 126037 decisions, 935548656 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2788378 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 228 gcs, 0 rescored clauses, 1422 rescored vars
c dcps: 37 decompositions, 49192 equivalent 26%
c deco: 1386580 decision-only clauses 51%, 60% reduction
c decs: 6186171 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 51232 flipped 0.828% (in 301 phases)
c elms: 24 elims, 57924 eliminated 31%
c elms: 48 rounds, 2.0 rounds/bve
c elms: 37451 small 65%, 20436 large 35%
c elms: 179569 tried small, 37451 succeeded 21%, 142118 failed 79%
c elms: 29718 subsumed, 83525 strengthened, 1684 blocked
c elms: 18814667 copies, 17961027 resolutions, 5558304 ipos
c elms: 4525181 subchks, 4474912 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 6 extractions, 210 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 14188440 steps, 7094220 extr 50%, 1813 elim 0%
c glue: 192.9 orig avg, 170.0 real avg, 9.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 1169659 = 136567 simple + 1030464 trn 12% + 2628 lrg 88%, 2640 sub 0%
c hght: 271 average, 1.41 height/glue
c ints: 67044 luby (18987967 steps), 0 inout (0 steps)
c lift: 23 phases, 48053 probed (16573 level1 34%, 31480 level2 66%)
c lift: 1228 units, 156 equivalences, 1405 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2703251 clauses, 264.2 length
c lrnd: 1020590 uips 38%, 1561568 flips 58%
c mega: 0 count, 0 failed, 0 rounds
c mins: 714107658 learned lits, 44% minimized
c mins: 1283783 mins 47%, 2136 bin 0%, 30752 size 1%, 1386580 deco 51%
c move: moved 2703251, 24091 bin 1%, 9158 trn 0%, 0 lrg 0%
c otfs: str 60135 dyn (60079 red, 56 irr) 15218 drv 25%, 44917 rst 75%
c otfs: sub 949 dyn (949 red, 0 irr)
c phas: 15 computed, 67489 set, 14616 pos (22%), 52873 neg (78%)
c prbs: 5 basic, 29076 probed, 827 failed, 16 lifted
c prbs: 6 simple, 574692 probed, 524 failed, 1784 eqs
c prbs: 5 treelook, 35 probed, 0 failed, 0 lifted
c prps: 2899316909 props, 438 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c psns: 90472881 searches, 15204172 hits, 17% 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: 79 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 79 arith 100%, 0 double 0%
c rmbd: 25447 removed, 4109 red 16%
c rphs: 10 recomputed phases
c rsts: 4024 restarts 6%, 63020 skipped 94%
c rsts: 62949 saturating 100%, 4 agile 0%, 67 reuse 0%
c rsts: 660.0 avg interval, 660.0 scaled, 1.0 factor
c rsts: 924 kept 23.0% average 22.4%
c simp: 25 count (25 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2703251 count (3731886 tried 1.4), 1399700 sub out of 2698102 (51.9%)
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: 58990 fixed 31%, 136 its, 19988.74 confs/it
c trvs: 48343221105 traversals, 97% srch, 4% simp, 0% lkhd
c trvs: 17.3 search traversals per propagation, 17259.1 per conflict
c trvs: 1.8 search traversals per search visit
c trds: 22 transitive reductions, 2599 removed, 18 failed
c trds: 20740 nodes, 79078 edges, 41974035 steps
c trim: 91162165 words, 347.8 MB
c trnr: 23 count, 36 bin, 2853 trn, 132855748 steps
c unhd: 25 count, 116 rounds, 210096670 steps
c unhd: 486 non-trivial sccs of average size 2.8
c unhd: 14 units, 14 bin, 0 trn, 0 lrg
c unhd: 1406 failed, 1334 stamp, 0 lits, 28 bin, 9 trn, 0 lrg
c unhd: 350384 tauts, 12819 bin 4%, 7432 trn 2%, 262 lrg 0%
c unhd: 350384 tauts, 329871 stamp 94%, 320457 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5603110 str, 14 bin 0%, 2521 trn 0%, 5600575 lrg 100%, 5589129 red 100%
c vars: 23350 remaining 12% and 166106 removed 88% out of 189456
c vars: 58990 fixed 31%, 57924 eliminated 31%, 49192 equivalent 26%
c vsts: 27258757476 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 9.5 search visits per propagation, 9503.1 per conflict
c wchs: 3467616529 pushed, 40144592 enlarged, 318 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2698102 100   1192868 100 142502893 100  23003961 100   1177696 100
c 
c  0       7625   0         0   0  18759264  13    871193   4     17553   1 
c  1       4628   0         0   0  15724793  11    729070   3     14393   1 
c  2      16646   1         0   0  51231261  36   3004252  13     71919   6 
c  3      67253   2     33845   3  25149505  18<  3758154  16    149651  13 
c  4      91914   3     85404   7   7511334   5   2146726   9    107007   9 
c  5     137971   5    133221  11   6601748   5   2215845  10    129938  11 
c  6     166486   6    123604  10   4910937   3   1851187   8<   119234  10 
c  7     166738   6    110816   9   3537040   2   1470205   6     98803   8<
c  8     156489   6    101878   9<  2370589   2   1109663   5     79474   7 
c  9     138835   5     83801   7   1502985   1    784990   3     54423   5 
c 10     283844  11<   140879  12   1798599   1   1206426   5     85618   7 
c 11     619314  23    177147  15   1653666   1   1723426   7    112250  10 
c 12     825995  31    197558  17   1723873   1   2096812   9    134202  11 
c 13      14364   1      4715   0     27299   0     36012   0      3231   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             9.5           8.4           2.8           5.7           6.8
c std             2.8           2.8           2.5           3.6           3.4
c 
c  132.080  13% analysis
c   88.408   9% cce
c   85.675   9% unhide
c   32.722   3% bump
c   29.712   3% cliff
c   19.068   2% elim
c   15.984   2% lift
c   15.781   2% gc
c   14.027   1% probe
c    6.809   1% decomp
c    5.993   1% decide
c    4.544   0% mincls
c    4.247   0% defrag
c    3.611   0% backward
c    2.617   0% transred
c    2.404   0% bca
c    1.725   0% block
c    1.558   0% reduce
c    1.435   0% restart
c    1.113   0% cgrclsr
c    1.030   0% gauss
c    0.856   0% card
c    0.810   0% ternres
c    0.710   0% phase
c    0.093   0% tabularasa
c    0.012   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    4.140   0% probe simple     30%
c    8.625   1% probe basic      61%
c    1.262   0% probe tree-look   9%
c ==================================
c    4.252   0% preprocessing     2%
c  266.093  27% inprocessing     98%
c ==================================
c  270.345  27% simplifying
c  729.231  73% search
c ==================================
c  999.580 100% all
c 
c 6186171 decisions, 6188.8 decisions/sec
c 2718469 conflicts, 2719.6 conflicts/sec
c 2899316909 propagations, 2.9 megaprops/sec
c 999.6 seconds, 160.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
