c launch: /data/cnf/sc2014/app/SAT_dat.k35-31_2_rule_2.cnf.bz2
c host: atom28
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/SAT_dat.k35-31_2_rule_2.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k35-31_2_rule_2.cnf.bz2
c no embedded options
c found 'p cnf 51465 228571' header
c read 51465 variables, 228571 clauses, 579146 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 51010 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   51010   228116         0       0      0     0   0  0.0   0.0    9
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 5480 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5480 out of 5480 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 1 used 100%
c [card-1] exported 1 binary clauses, 1.0 per/constraint
c [decomp-1] removed 16615 variables
c [simpleprobe-1] all 34850 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 6161 variables
c [simpleprobe-1] 1359 variables remain 5% (27330 retained)
c [simpleprobe-1] removed 6161 variables, found 49013 hbrs, 632 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 52 units, 19 failed, 1314 tauts, 0 hbrs, 4017 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 28470 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 18152 variables 64% in round 1 in 21408921 steps
c [elim-1-1] backward subsumption/strengthening limit 42817842
c [elim-1-1] subsumed 0 and strengthened 311 clauses in 42818549 steps
c [elim-1-1] rescheduled 254 variables 1% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 390514 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 18176 = 64% variables out of 28470
c [phase-1] phase bias: 4836 positive 47%, 5458 negative 53%
c [simplification-1] removed 34016 variables 76.8% (10294 remain 20%)
c [simplification-1] removed 153966 irredundant clauses 67.5% (74150 remain 33%)
c [simplification-1] maximum reduction of 77% = max (77%, 67%)
c [simplification-1] large reduction 77% >= 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] 7784, max 11951, min4 5539 at 72%, min10 4223 at 87%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number variables 10294 drops below limit 12752
c [tabula-rasa-1] number clauses 74150 drops below limit 114058
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 10294 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 2573 and clause limit 37075
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.6   10294    74150         5       4      1  8352   8  5.6  39.4    6
c R    2.6   10294    74150        20      15      4  8353   8  4.0  42.8    6
c R    2.6   10294    74150        64      47     11  8353   8  4.0  61.2    6
c R    2.7   10294    74150       167     131     19  8359   8  4.1  64.9    6
c R    2.7   10294    74150       412     338     39  8366   8  5.1  63.4    6
c i    2.7   10293    74150       700     560     74  8379   7  4.9  58.2    6
c i    2.7   10292    74150       723     570     78  8383   6  4.8  58.4    6
c i    2.7    9933    74150       901     700    106  8396   5  4.7  57.5    7
c R    2.7    9933    74150       992     772    117  8401   6  4.9  58.8    7
c 
c [simplification-2] limit of 1158 conflicts hit after 1159 conflicts
c [decomp-3] removed 568 variables
c [simpleprobe-2] 1010 schedulable variables 10%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 198 variables
c [simpleprobe-2] 99 variables remain 1% (9429 retained)
c [simpleprobe-2] removed 198 variables, found 1867 hbrs, 43 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19056 literals 100%
c [treelook-1] scheduling used 233800 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303479 steps
c [treelook-1] 18960 literals remain 100%
c [treelook-1] 9521 variables remain to probed next time 100%
c [decomp-5] removed 7 variables
c [treelook-1] removed 14 variables, found 826 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 4307 probes remain 46% after last round
c [basicprobe-1-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 156 variables, found 2426 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 7 failed, 1253 tauts, 0 hbrs, 4628 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9343 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 588 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 2 clauses out of 113 (2%) of length 13
c [cce-1-1] eliminated 31 clauses out of 197 (16%) of length 12
c [cce-1-1] eliminated 19 clauses out of 399 (5%) of length 11
c [cce-1-1] eliminated 8 clauses out of 629 (1%) of length 10
c [cce-1-1] eliminated 55 clauses out of 713 (8%) of length 9
c [cce-1-1] eliminated 54 clauses out of 1437 (4%) of length 8
c [cce-1-1] eliminated 163 clauses out of 2177 (7%) of length 7
c [cce-1-1] eliminated 345 clauses out of 3584 (10%) of length 6
c [cce-1-1] eliminated 616 clauses out of 4539 (14%) of length 5
c [cce-1-1] eliminated 880 clauses out of 6002 (15%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2173 large clauses in 38787777 steps
c [cce-1-1] allowing another 19393888 steps for small clauses
c [cce-1] scheduling 39763 clauses = 34132 binary + 5631 ternary
c [cce-1] tried to eliminate 39763 small clauses 100%
c [cce-1] eliminated 6428 small clauses 16%
c [cce-1] eliminated 5937 binary clauses 17%
c [cce-1] eliminated 491 ternary clauses 9%
c [cce-1-1] eliminated 6428 small clauses in 91438137 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 8601 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 33335 clauses = 28195 binary + 5140 ternary
c [cce-1] tried to eliminate 33335 small clauses 100%
c [cce-1] eliminated 2465 small clauses 7%
c [cce-1] eliminated 2393 binary clauses 8%
c [cce-1] eliminated 72 ternary clauses 1%
c [cce-1-2] eliminated 2465 small clauses in 58597113 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 2465 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 0 steps for small clauses
c [cce-1] scheduling 30870 clauses = 25802 binary + 5068 ternary
c [cce-1] tried to eliminate 30870 small clauses 100%
c [cce-1] eliminated 1710 small clauses 6%
c [cce-1] eliminated 1689 binary clauses 7%
c [cce-1] eliminated 21 ternary clauses 0%
c [cce-1-3] eliminated 1710 small clauses in 54110152 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 1710 covered clauses in round 3
c [cce-1-4] completed large round (ACCE)
c [cce-1-4] allowing another 0 steps for small clauses
c [cce-1] scheduling 29160 clauses = 24113 binary + 5047 ternary
c [cce-1] tried to eliminate 29160 small clauses 100%
c [cce-1] eliminated 4 small clauses 0%
c [cce-1] eliminated 3 binary clauses 0%
c [cce-1] eliminated 1 ternary clauses 0%
c [cce-1-4] eliminated 4 small clauses in 49205593 steps
c [cce-1-4] completed small round (ACCE)
c [cce-1-4] eliminated 4 covered clauses in round 4
c [cce-1-5] completed large round (ACCE)
c [cce-1-5] allowing another 0 steps for small clauses
c [cce-1] scheduling 29156 clauses = 24110 binary + 5046 ternary
c [cce-1] tried to eliminate 27689 small clauses 95%
c [cce-1] eliminated 4 small clauses 0%
c [cce-1] eliminated 3 binary clauses 0%
c [cce-1] eliminated 1 ternary clauses 0%
c [cce-1-5] eliminated 4 small clauses in 46649006 steps
c [cce-1-5] incomplete small round (ACCE)
c [cce-1-5] eliminated 4 covered clauses in round 5
c [cce-1] eliminated 12784 covered clauses in TOTAL during 5 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9341 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 1397 variables 15% in round 1 in 19138482 steps
c [elim-2-1] backward subsumption/strengthening limit 861518
c [elim-2-1] subsumed 0 and strengthened 127 clauses in 861546 steps
c [elim-2] incomplete 139 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1398 = 15% variables out of 9341
c [bca-1] limit of 10000000 steps
c [bca-1] 13897 out of 15888 literals actually usable 87%
c [bca-1] added 38 blocked clauses in 43369 steps
c [phase-3] phase bias: 1 positive 50%, 1 negative 50%
c [simplification-2] removed 1990 variables 20.0% (7943 remain 16%)
c [simplification-2] removed 24461 irredundant clauses 33.0% (49689 remain 22%)
c [simplification-2] maximum reduction of 33% = max (20%, 33%)
c [simplification-2] large reduction 33% >= 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 3159
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   11.8    7942    49689      1208     633    472 11329   5  4.8  62.4    6
c i   11.8    7940    49689      1209     633    472 11329   5  4.8  62.4    6
c i   11.8    7937    49689      1212     634    472 11330   5  4.8  62.4    6
c i   11.9    7915    49689      1427     793    505 11343   6  4.8  62.6    6
c i   11.9    7913    49689      1540     870    527 11352   5  4.8  62.4    6
c R   11.9    7910    49689      2307    1530    578 11372   9  5.0  66.9    6
c i   12.0    7909    49689      3348    2342    683 11417   7  4.9  62.6    6
c i   12.0    7908    49689      3434    2400    695 11422   7  4.9  62.1    6
c 
c [simplification-3] limit of 3471 conflicts hit after 3471 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 7904 free variables schedulable
c [ternres-1] 1921 ternary resolvents (122 bin, 1799 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1062 at-most-one constraints of average size 3.1
c [card-2] found 8 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1070 out of 1070 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 27 at-most-one constraints, 5 used 19%
c [card-2] exported 5 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2111 xors of average arity 2.9
c [gauss-1] connected 6143 occurrences of 526 variables (average 11.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-6] removed 87 variables
c [gauss-1] exported 0 unary, 5 binary and 1 ternary equations
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15634 literals 100%
c [treelook-2] scheduling used 195892 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300060 steps
c [treelook-2] 15472 literals remain 99%
c [treelook-2] 7817 variables remain to probed next time 100%
c [decomp-8] removed 2 variables
c [treelook-2] removed 2 variables, found 224 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 7815 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 5770 probes 74%
c [lift-1] 32 units, 29 impls, 11 eqs in 1 rounds
c [lift-1] 7339 variables remain 94% (428 retained)
c [lift-1] removed 48 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 39, lifted 45
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1 failed, 288 tauts, 0 hbrs, 1515 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 237 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7669 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 46 blocked clauses
c [block-2] 46 < 1/1000 * 48063 = 48 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 7 (57%) of length 16
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-2-1] eliminated 20 clauses out of 35 (57%) of length 14
c [cce-2-1] eliminated 23 clauses out of 50 (46%) of length 13
c [cce-2-1] eliminated 17 clauses out of 42 (40%) of length 12
c [cce-2-1] eliminated 15 clauses out of 86 (17%) of length 11
c [cce-2-1] eliminated 28 clauses out of 609 (5%) of length 10
c [cce-2-1] eliminated 38 clauses out of 949 (4%) of length 9
c [cce-2-1] eliminated 82 clauses out of 1473 (6%) of length 8
c [cce-2-1] eliminated 142 clauses out of 2034 (7%) of length 7
c [cce-2-1] eliminated 391 clauses out of 2975 (13%) of length 6
c [cce-2-1] eliminated 285 clauses out of 3851 (7%) of length 5
c [cce-2-1] eliminated 456 clauses out of 5314 (9%) of length 4
c [cce-2-1] completed large round (ACCE)
c [cce-2-1] eliminated 1503 large clauses in 27168075 steps
c [cce-2-1] allowing another 13584037 steps for small clauses
c [cce-2] scheduling 26367 clauses = 21840 binary + 4527 ternary
c [cce-2] tried to eliminate 10927 small clauses 41%
c [cce-2] eliminated 604 small clauses 2%
c [cce-2] eliminated 372 binary clauses 2%
c [cce-2] eliminated 232 ternary clauses 5%
c [cce-2-1] eliminated 604 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ACCE)
c [cce-2-1] eliminated 2107 covered clauses in round 1
c [cce-2] eliminated 2107 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 7668 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 392 variables 5% in round 1 in 12974714 steps
c [elim-3-1] backward subsumption/strengthening limit 7025286
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 2198268 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 392 = 5% variables out of 7668
c [bca-2] limit of 10000000 steps
c [bca-2] 10470 out of 14554 literals actually usable 72%
c [bca-2] added 40 blocked clauses in 32818 steps
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-3] removed 628 variables 7.9% (7276 remain 14%)
c [simplification-3] removed 4702 irredundant clauses 9.5% (44987 remain 20%)
c [simplification-3] maximum reduction of 9% = max (8%, 9%)
c [simplification-3] large reduction 9% >= 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 5471
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   14.2    7275    44987      3727    2206   1901 12492   6  4.9  61.0    6
c R   14.3    7275    44987      5251    3519   1969 12516   8  5.3  65.8    6
c i   14.3    7274    44987      5272    3530   1973 12517   8  5.3  65.6    6
c i   14.3    7273    44987      5475    3705   1984 12520   7  5.3  64.6    6
c 
c [simplification-4] limit of 5601 conflicts hit after 5601 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7272 free variables schedulable
c [ternres-2] 129 ternary resolvents (5 bin, 124 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 1536 xors of average arity 2.9
c [gauss-2] connected 4492 occurrences of 588 variables (average 7.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 63 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 990 probes remain 14% after last round
c [basicprobe-2-0] 24 units = 23 failed (96%) + 1 lifted (4%)
c [basicprobe-2-0] removed 28 variables, found 663 hbrs
c [bate-1] eliminated 10 asymmetric tautologies during probing
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 4907 probes 68%
c [lift-2] 25 units, 26 impls, 16 eqs in 1 rounds
c [lift-2] 6298 variables remain 88% (834 retained)
c [lift-2] removed 49 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 11, lifted 5
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 2209 tauts, 0 hbrs, 3669 literals
c [transred-2] limit 107222 with penalty 0 = 0 + 0
c [transred-2] removed 172 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 16
c [cce-3-1] eliminated 12 clauses out of 16 (75%) of length 15
c [cce-3-1] eliminated 12 clauses out of 29 (41%) of length 14
c [cce-3-1] eliminated 19 clauses out of 40 (48%) of length 13
c [cce-3-1] eliminated 11 clauses out of 40 (28%) of length 12
c [cce-3-1] eliminated 17 clauses out of 86 (20%) of length 11
c [cce-3-1] eliminated 17 clauses out of 483 (4%) of length 10
c [cce-3-1] eliminated 54 clauses out of 910 (6%) of length 9
c [cce-3-1] eliminated 34 clauses out of 1361 (2%) of length 8
c [cce-3-1] eliminated 40 clauses out of 1843 (2%) of length 7
c [cce-3-1] eliminated 56 clauses out of 2614 (2%) of length 6
c [cce-3-1] eliminated 76 clauses out of 3455 (2%) of length 5
c [cce-3-1] eliminated 134 clauses out of 4828 (3%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 485 large clauses in 23348694 steps
c [cce-3-1] allowing another 11674347 steps for small clauses
c [cce-3] scheduling 24157 clauses = 20316 binary + 3841 ternary
c [cce-3] tried to eliminate 12811 small clauses 53%
c [cce-3] eliminated 554 small clauses 2%
c [cce-3] eliminated 448 binary clauses 2%
c [cce-3] eliminated 106 ternary clauses 3%
c [cce-3-1] eliminated 554 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1039 covered clauses in round 1
c [cce-3] eliminated 1039 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7111 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 281 variables 4% in round 1 in 10832482 steps
c [elim-4-1] backward subsumption/strengthening limit 9167518
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 2053354 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 281 = 4% variables out of 7111
c [bca-3] limit of 10000000 steps
c [bca-3] 8830 out of 13662 literals actually usable 65%
c [bca-3] added 12 blocked clauses in 28655 steps
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 442 variables 6.1% (6830 remain 13%)
c [simplification-4] removed 2587 irredundant clauses 5.8% (42400 remain 19%)
c [simplification-4] maximum reduction of 6% = max (6%, 6%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] new conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] new conflict limit 7601
c 
c [simplification-5] limit of 7663 conflicts hit after 7663 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 6830 free variables schedulable
c [ternres-3] 170 ternary resolvents (1 bin, 169 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-10] removed 36 variables
c [simpleprobe-3] 30 schedulable variables 0%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-11] removed 113 variables
c [simpleprobe-3] 49 variables remain 1% (6632 retained)
c [simpleprobe-3] removed 113 variables, found 1265 hbrs, 0 units
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 6681 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 500000 with penalty 0 = 0 + 0
c [lift-3] using 4353 probes 65%
c [lift-3] 0 units, 21 impls, 5 eqs in 1 rounds
c [lift-3] 5484 variables remain 82% (1192 retained)
c [lift-3] removed 5 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 9, lifted 1
c [transred-3] limit 143322 with penalty 0 = 0 + 0
c [transred-3] removed 381 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 6665 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 13 blocked clauses
c [block-3] 13 < 1/1000 * 41628 = 41 considered unsuccessful
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-4-1] eliminated 2 clauses out of 5 (40%) of length 15
c [cce-4-1] eliminated 4 clauses out of 18 (22%) of length 14
c [cce-4-1] eliminated 6 clauses out of 31 (19%) of length 13
c [cce-4-1] eliminated 5 clauses out of 17 (29%) of length 12
c [cce-4-1] eliminated 3 clauses out of 83 (4%) of length 11
c [cce-4-1] eliminated 17 clauses out of 325 (5%) of length 10
c [cce-4-1] eliminated 19 clauses out of 763 (2%) of length 9
c [cce-4-1] eliminated 29 clauses out of 1401 (2%) of length 8
c [cce-4-1] eliminated 59 clauses out of 1960 (3%) of length 7
c [cce-4-1] eliminated 33 clauses out of 2605 (1%) of length 6
c [cce-4-1] eliminated 50 clauses out of 3429 (1%) of length 5
c [cce-4-1] eliminated 127 clauses out of 4745 (3%) of length 4
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] eliminated 355 large clauses in 22682612 steps
c [cce-4-1] allowing another 11341306 steps for small clauses
c [cce-4] scheduling 22097 clauses = 18576 binary + 3521 ternary
c [cce-4] tried to eliminate 14481 small clauses 66%
c [cce-4] eliminated 424 small clauses 2%
c [cce-4] eliminated 352 binary clauses 2%
c [cce-4] eliminated 72 ternary clauses 2%
c [cce-4-1] eliminated 424 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 779 covered clauses in round 1
c [cce-4] eliminated 779 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 6665 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 98 variables 1% in round 1 in 8777541 steps
c [elim-5-1] backward subsumption/strengthening limit 11222459
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 1901404 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 98 = 1% variables out of 6665
c [bca-4] limit of 10000000 steps
c [bca-4] 7540 out of 13136 literals actually usable 57%
c [bca-4] added 13 blocked clauses in 26063 steps
c [simplification-5] removed 263 variables 3.9% (6567 remain 13%)
c [simplification-5] removed 1841 irredundant clauses 4.3% (40559 remain 18%)
c [simplification-5] maximum reduction of 4% = max (4%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 24000
c [simplification-5] penalized conflict interval 24000 = 1 * 24000
c [simplification-5] new conflict limit 31663
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   18.4    6567    40559      8825    3792   2029 11445   8  5.5  61.4    6
c i   18.5    6566    40559      9888    4742   2074 11453   9  5.5  60.6    6
c i   18.5    6556    40559     10744    5505   2121 11458   9  5.6  61.7    6
c R   18.6    6553    40559     11820    6542   2131 11461  16  6.1  62.9    6
c -   18.7    6553    40559     13223    5266   2199 11493   9  6.0  61.6    6
c i   18.7    6552    40559     13226    5268   2199 11493   9  6.0  61.6    6
c i   18.8    6551    40559     14703    6564   2254 11505   7  6.1  61.3    6
c i   18.8    6542    40559     14712    6571   2254 11506   7  6.1  61.2    6
c i   18.8    6540    40559     14719    6572   2257 11508   7  6.1  61.2    6
c i   19.1    6538    40559     17846    9332   2401 11553  10  6.2  61.0    6
c i   19.1    6537    40559     17847    9332   2401 11553  10  6.2  61.0    6
c -   19.1    6537    40559     18576    6974   2428 11559   9  6.2  60.6    6
c i   19.2    6536    40559     19406    7706   2451 11567   8  6.3  60.5    6
c i   19.3    6533    40559     20633    8794   2498 11575   9  6.5  60.9    6
c i   19.5    6526    40559     23790   11598   2577 11618  13  6.8  61.9    9
c -   19.6    6525    40559     24521    8751   2589 11620  12  6.8  61.9    8
c R   19.7    6525    40559     26190   10314   2610 11626  16  7.0  62.0    9
c -   20.1    6525    40559     30692   10300   2764 11689   9  7.0  60.4    8
c 
c [simplification-6] limit of 32347 conflicts hit after 32347 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6525 free variables schedulable
c [ternres-4] 238 ternary resolvents (6 bin, 232 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 839 at-most-one constraints of average size 3.1
c [card-3] found 42 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 881 out of 881 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 1143 xors of average arity 2.8
c [gauss-3] connected 3201 occurrences of 459 variables (average 7.0)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 58 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 12934 literals 100%
c [treelook-3] scheduling used 187956 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 300637 steps
c [treelook-3] 12781 literals remain 99%
c [treelook-3] 6467 variables remain to probed next time 100%
c [decomp-13] removed 14 variables
c [treelook-3] removed 14 variables, found 180 hbrs
c [lift-4] limit 500000 with penalty 0 = 0 + 0
c [lift-4] using 3960 probes 61%
c [lift-4] 11 units, 17 impls, 5 eqs in 1 rounds
c [lift-4] 4984 variables remain 77% (1453 retained)
c [lift-4] removed 16 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 13, lifted 15
c [unhide-5] limit 59622 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 192 tauts, 0 hbrs, 5613 literals
c [transred-4] limit 596229 with penalty 0 = 0 + 0
c [transred-4] removed 1363 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 19 (5%) of length 12
c [cce-5-1] eliminated 2 clauses out of 76 (3%) of length 11
c [cce-5-1] eliminated 27 clauses out of 279 (10%) of length 10
c [cce-5-1] eliminated 13 clauses out of 690 (2%) of length 9
c [cce-5-1] eliminated 58 clauses out of 1321 (4%) of length 8
c [cce-5-1] eliminated 77 clauses out of 1882 (4%) of length 7
c [cce-5-1] eliminated 65 clauses out of 2559 (3%) of length 6
c [cce-5-1] eliminated 87 clauses out of 3339 (3%) of length 5
c [cce-5-1] eliminated 73 clauses out of 4602 (2%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 403 large clauses in 20281476 steps
c [cce-5-1] allowing another 10140738 steps for small clauses
c [cce-5] scheduling 21467 clauses = 17598 binary + 3869 ternary
c [cce-5] tried to eliminate 16581 small clauses 77%
c [cce-5] eliminated 497 small clauses 2%
c [cce-5] eliminated 372 binary clauses 2%
c [cce-5] eliminated 125 ternary clauses 3%
c [cce-5-1] eliminated 497 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 900 covered clauses in round 1
c [cce-5] eliminated 900 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6408 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 116 variables 2% in round 1 in 7893382 steps
c [elim-6-1] backward subsumption/strengthening limit 12106618
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 1758307 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 116 = 2% variables out of 6408
c [bca-5] limit of 10000000 steps
c [bca-5] 4927 out of 12586 literals actually usable 39%
c [bca-5] added 3 blocked clauses in 24062 steps
c [rephase-1] after 32347 conflicts (new increment 20000, next 52347)
c [flushphases] 0 phases reset
c [simplification-6] removed 233 variables 3.6% (6292 remain 12%)
c [simplification-6] removed 2053 irredundant clauses 5.1% (38506 remain 17%)
c [simplification-6] maximum reduction of 5% = max (4%, 5%)
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 34347
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   22.2    6291    38506     32617   11291   2857 11011   9  7.0  60.1    7
c 
c [simplification-7] limit of 34415 conflicts hit after 34415 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6291 free variables schedulable
c [ternres-5] 123 ternary resolvents (6 bin, 117 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-14] removed 27 variables
c [basicprobe-3] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-3-0] 879 sched 14%, 5 failed, 0 lifted, 165 hbrs
c [decomp-15] removed 7 variables
c [basicprobe-3-1] 2929 probes remain 47% after last round
c [basicprobe-3-1] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 7 variables, found 218 hbrs
c [bate-2] eliminated 5 asymmetric tautologies during probing
c [lift-5] limit 500000 with penalty 0 = 0 + 0
c [lift-5] using 3553 probes 57%
c [lift-5] 2 units, 10 impls, 2 eqs in 1 rounds
c [lift-5] 4496 variables remain 72% (1758 retained)
c [lift-5] removed 4 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 4, lifted 1
c [transred-5] limit 643292 with penalty 0 = 0 + 0
c [transred-5] removed 893 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 3 clauses out of 216 (1%) of length 10
c [cce-6-1] eliminated 16 clauses out of 649 (2%) of length 9
c [cce-6-1] eliminated 17 clauses out of 1280 (1%) of length 8
c [cce-6-1] eliminated 32 clauses out of 1826 (2%) of length 7
c [cce-6-1] eliminated 31 clauses out of 2539 (1%) of length 6
c [cce-6-1] eliminated 40 clauses out of 3254 (1%) of length 5
c [cce-6-1] eliminated 54 clauses out of 4530 (1%) of length 4
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] eliminated 193 large clauses in 19161986 steps
c [cce-6-1] allowing another 9580993 steps for small clauses
c [cce-6] scheduling 20212 clauses = 16904 binary + 3308 ternary
c [cce-6] tried to eliminate 17346 small clauses 86%
c [cce-6] eliminated 208 small clauses 1%
c [cce-6] eliminated 148 binary clauses 1%
c [cce-6] eliminated 60 ternary clauses 2%
c [cce-6-1] eliminated 248 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 441 covered clauses in round 1
c [cce-6] eliminated 441 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6248 variables 100%
c [elim-7] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 60 variables 1% in round 1 in 7215192 steps
c [elim-7-1] backward subsumption/strengthening limit 12784808
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 1713577 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 60 = 1% variables out of 6248
c [bca-6] limit of 10000000 steps
c [bca-6] 4546 out of 12378 literals actually usable 37%
c [bca-6] added 3 blocked clauses in 24209 steps
c [simplification-7] removed 103 variables 1.6% (6188 remain 12%)
c [simplification-7] removed 669 irredundant clauses 1.7% (37837 remain 17%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-7] new conflict interval 32000
c [simplification-7] penalized conflict interval 32000 = 1 * 32000
c [simplification-7] new conflict limit 66415
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   24.1    6187    37837     34446   12422   2950 10476   8  7.0  59.7    7
c -   24.4    6187    37837     38817   11743   3086 10520   8  7.1  59.1    7
c i   24.5    6186    37837     40120   12917   3126 10535   9  7.1  58.9    7
c i   24.8    6185    37837     43521   15961   3245 10566  10  7.1  58.5    7
c i   24.8    6184    37837     43522   15961   3244 10567  10  7.1  58.5    7
c i   24.8    6171    37837     43523   15960   3245 10567  10  7.1  58.5    7
c -   25.1    6164    37837     46561   13674   3329 10606   9  7.1  58.0    7
c i   25.1    6163    37837     46854   13939   3338 10609   9  7.1  57.8    7
c -   25.7    6163    37837     54664   15125   3448 10660   7  8.0  57.9    7
c i   25.9    6162    37837     57405   17248   3524 10692  10  8.1  57.6    7
c R   25.9    6160    37837     57518   17357   3524 10692  11  8.1  57.6    7
c i   25.9    6159    37837     57653   17478   3528 10695   9  8.1  57.6    7
c i   26.0    6158    37837     58138   17894   3557 10704  10  8.1  57.4    7
c i   26.1    6157    37837     59316   18947   3595 10725   9  8.1  57.3    7
c i   26.2    6153    37837     60445   19993   3623 10736  10  8.1  57.1    7
c i   26.4    6151    37837     61951   21344   3662 10753  10  8.0  56.8    8
c -   26.6    6149    37837     64432   17502   3737 10811   9  8.0  56.3    7
c i   26.6    6148    37837     64632   17672   3746 10817   9  8.0  56.3    7
c i   26.9    6144    37837     66989   19778   3822 10847   9  7.9  55.9    7
c i   26.9    6140    37837     67135   19907   3827 10848   9  7.9  55.9    7
c 
c [simplification-8] limit of 67333 conflicts hit after 67336 conflicts
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6138 free variables schedulable
c [ternres-6] 663 ternary resolvents (6 bin, 657 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-16] removed 85 variables
c [simpleprobe-4] 48 schedulable variables 1%
c [simpleprobe-4] limit 5475819 penalty 0 = 0 + 0
c [decomp-17] removed 45 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 45 variables, found 267 hbrs, 0 units
c [cgrclsr-3] limit 50000 penalty 2 = 2 + 0
c [cgrclsr-3] all 6058 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-6] limit 821372 with penalty 0 = 0 + 0
c [lift-6] using 3211 probes 53%
c [lift-6] 12 units, 26 impls, 7 eqs in 1 rounds
c [lift-6] 4072 variables remain 67% (1963 retained)
c [lift-6] removed 23 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 14, lifted 5
c [transred-6] limit 1368954 with penalty 0 = 0 + 0
c [transred-6] removed 1269 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6013 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16 blocked clauses
c [block-4] 16 < 1/1000 * 36928 = 36 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 5 clauses out of 205 (2%) of length 10
c [cce-7-1] eliminated 22 clauses out of 601 (4%) of length 9
c [cce-7-1] eliminated 41 clauses out of 1201 (3%) of length 8
c [cce-7-1] eliminated 69 clauses out of 1726 (4%) of length 7
c [cce-7-1] eliminated 44 clauses out of 2435 (2%) of length 6
c [cce-7-1] eliminated 65 clauses out of 3138 (2%) of length 5
c [cce-7-1] eliminated 71 clauses out of 4493 (2%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 317 large clauses in 18038881 steps
c [cce-7-1] allowing another 9019440 steps for small clauses
c [cce-7] scheduling 19305 clauses = 16204 binary + 3101 ternary
c [cce-7] tried to eliminate 17874 small clauses 93%
c [cce-7] eliminated 309 small clauses 2%
c [cce-7] eliminated 276 binary clauses 2%
c [cce-7] eliminated 33 ternary clauses 1%
c [cce-7-1] eliminated 309 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 626 covered clauses in round 1
c [cce-7] eliminated 626 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6013 variables 100%
c [elim-8] limit of 27379097 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 97 variables 2% in round 1 in 7281036 steps
c [elim-8-1] backward subsumption/strengthening limit 14562072
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 1586290 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 97 = 2% variables out of 6013
c [bca-7] limit of 10000000 steps
c [bca-7] 3423 out of 11834 literals actually usable 29%
c [bca-7] added 2 blocked clauses in 27676 steps
c [rephase-2] after 67336 conflicts (new increment 40000, next 107336)
c [flushphases] 0 phases reset
c [simplification-8] removed 222 variables 3.6% (5916 remain 12%)
c [simplification-8] removed 1893 irredundant clauses 5.0% (35944 remain 16%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] new conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] new conflict limit 69336
c [tabula-rasa-2] number clauses 35944 drops below limit 37075
c [flush-cache] 0 binary, 0 ternary, 19095 large
c [flushphases] 5916 phases reset fully
c [phase-6] phase bias: 428 positive 51%, 405 negative 49%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] conflict limit 20000 does not change
c [tabula-rasa-2] new variable limit 1479 and clause limit 17972
c 
c [simplification-9] limit of 69368 conflicts hit after 69369 conflicts
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 5916 free variables schedulable
c [ternres-7] 156 ternary resolvents (12 bin, 144 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 338 xors of average arity 2.9
c [gauss-4] connected 992 occurrences of 223 variables (average 4.4)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 11 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 11810 literals 100%
c [treelook-4] scheduling used 158067 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 302721 steps
c [treelook-4] 11756 literals remain 100%
c [treelook-4] 5905 variables remain to probed next time 100%
c [decomp-19] removed 2 variables
c [treelook-4] removed 2 variables, found 359 hbrs
c [lift-7] limit 837880 with penalty 0 = 0 + 0
c [lift-7] using 2880 probes 49%
c [lift-7] 1 units, 25 impls, 2 eqs in 1 rounds
c [lift-7] 3572 variables remain 61% (2328 retained)
c [lift-7] removed 3 variables
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 0, lifted 0
c [unhide-6] limit 69823 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 0 failed, 1426 tauts, 0 hbrs, 5375 literals
c [transred-7] limit 1396467 with penalty 0 = 0 + 0
c [transred-7] removed 730 transitive binary clauses
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 4 clauses out of 71 (6%) of length 11
c [cce-8-1] eliminated 14 clauses out of 186 (8%) of length 10
c [cce-8-1] eliminated 26 clauses out of 510 (5%) of length 9
c [cce-8-1] eliminated 43 clauses out of 1006 (4%) of length 8
c [cce-8-1] eliminated 89 clauses out of 1591 (6%) of length 7
c [cce-8-1] eliminated 54 clauses out of 2516 (2%) of length 6
c [cce-8-1] eliminated 34 clauses out of 3119 (1%) of length 5
c [cce-8-1] eliminated 54 clauses out of 4462 (1%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 318 large clauses in 14247691 steps
c [cce-8-1] allowing another 7123845 steps for small clauses
c [cce-8] scheduling 19315 clauses = 15771 binary + 3544 ternary
c [cce-8] tried to eliminate 19315 small clauses 100%
c [cce-8] eliminated 368 small clauses 2%
c [cce-8] eliminated 300 binary clauses 2%
c [cce-8] eliminated 68 ternary clauses 2%
c [cce-8-1] eliminated 368 small clauses in 26856151 steps
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 686 covered clauses in round 1
c [cce-8-2] completed large round (ACCE)
c [cce-8-2] allowing another 0 steps for small clauses
c [cce-8] scheduling 18947 clauses = 15471 binary + 3476 ternary
c [cce-8] tried to eliminate 3051 small clauses 16%
c [cce-8-2] incomplete small round (ACCE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 686 covered clauses in TOTAL during 2 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 5900 variables 100%
c [elim-9] limit of 27929346 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 143 variables 2% in round 1 in 7092695 steps
c [elim-9-1] backward subsumption/strengthening limit 14185390
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 1520095 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 143 = 2% variables out of 5900
c [bca-8] limit of 10000000 steps
c [bca-8] 7695 out of 11516 literals actually usable 67%
c [bca-8] added 25 blocked clauses in 22568 steps
c [rephase-3] after 69369 conflicts (new increment 20000, next 89369)
c [flushphases] 2 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 159 variables 2.7% (5757 remain 11%)
c [simplification-9] removed 987 irredundant clauses 2.7% (34957 remain 15%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 25000
c [simplification-9] penalized conflict interval 25000 = 1 * 25000
c [simplification-9] new conflict limit 94369
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   30.7    5756    34957     71382    3569   3830 12075   9  7.9  55.9    6
c -   30.9    5756    34957     73755    3733   3908 12098  10  7.8  55.8    5
c i   31.0    5755    34957     74881    4774   3924 12102  10  7.9  55.9    6
c -   31.3    5755    34957     78246    5334   4029 12140   8  7.9  55.5    6
c i   31.6    5754    34957     82489    9201   4106 12160  11  8.0  56.1    6
c -   31.6    5754    34957     83472    7142   4114 12163  13  8.0  56.1    6
c i   31.8    5753    34957     85634    9075   4178 12188   9  8.0  55.8    8
c i   32.0    5752    34957     87209   10498   4225 12200   9  8.0  55.8    8
c -   32.2    5751    34957     89270    8803   4285 12212  10  8.4  55.9    8
c 
c [simplification-10] limit of 94821 conflicts hit after 94824 conflicts
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 5751 free variables schedulable
c [ternres-8] 580 ternary resolvents (5 bin, 575 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 569 at-most-one constraints of average size 3.1
c [card-4] found 83 at-most-two constraints of average size 4.1
c [card-4] using previous limit 250000 for elimination
c [card-4] 650 out of 652 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-20] removed 27 variables
c [basicprobe-4] limit 1922354 penalty 0 = 0 + 0
c [basicprobe-4-0] 1140 probes remain 20% after last round
c [basicprobe-4-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 10 variables, found 1793 hbrs
c [bate-3] eliminated 5 asymmetric tautologies during probing
c [lift-8] limit 1153412 with penalty 0 = 0 + 0
c [lift-8] using 2459 probes 43%
c [lift-8] 1 units, 20 impls, 5 eqs in 1 rounds
c [lift-8] 3097 variables remain 54% (2617 retained)
c [lift-8] removed 6 variables
c [transred-8] limit 1922354 with penalty 0 = 0 + 0
c [transred-8] removed 868 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 13 (8%) of length 13
c [cce-9-1] eliminated 2 clauses out of 68 (3%) of length 11
c [cce-9-1] eliminated 9 clauses out of 169 (5%) of length 10
c [cce-9-1] eliminated 20 clauses out of 491 (4%) of length 9
c [cce-9-1] eliminated 24 clauses out of 973 (2%) of length 8
c [cce-9-1] eliminated 47 clauses out of 1474 (3%) of length 7
c [cce-9-1] eliminated 58 clauses out of 2466 (2%) of length 6
c [cce-9-1] eliminated 36 clauses out of 3099 (1%) of length 5
c [cce-9-1] eliminated 72 clauses out of 4445 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 269 large clauses in 13171253 steps
c [cce-9-1] allowing another 6585626 steps for small clauses
c [cce-9] scheduling 18511 clauses = 15089 binary + 3422 ternary
c [cce-9] tried to eliminate 18511 small clauses 100%
c [cce-9] eliminated 169 small clauses 1%
c [cce-9] eliminated 142 binary clauses 1%
c [cce-9] eliminated 27 ternary clauses 1%
c [cce-9-1] eliminated 169 small clauses in 25029811 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 438 covered clauses in round 1
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] allowing another 0 steps for small clauses
c [cce-9] scheduling 18342 clauses = 14947 binary + 3395 ternary
c [cce-9] tried to eliminate 5023 small clauses 27%
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 0 covered clauses in round 2
c [cce-9] eliminated 438 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 5714 variables 100%
c [elim-10] limit of 38447080 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 67 variables 1% in round 1 in 6168307 steps
c [elim-10-1] backward subsumption/strengthening limit 12336614
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 1467532 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 67 = 1% variables out of 5714
c [bca-9] limit of 10000000 steps
c [bca-9] 3538 out of 11296 literals actually usable 31%
c [bca-9] added 0 blocked clauses in 21957 steps
c [rephase-4] after 94824 conflicts (new increment 40000, next 134824)
c [flushphases] 0 phases reset
c [simplification-10] removed 104 variables 1.8% (5647 remain 11%)
c [simplification-10] removed 772 irredundant clauses 2.2% (34185 remain 15%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 8333 = 25000 / 3
c [simplification-10] new conflict interval 33333
c [simplification-10] penalized conflict interval 33333 = 1 * 33333
c [simplification-10] new conflict limit 128157
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   34.1    5646    34185     95046   13473   4759 13260  13  8.4  55.3    8
c i   34.2    5645    34185     95968   14290   4775 13265  10  8.5  55.2    8
c -   34.2    5643    34185     96065   10371   4780 13265   9  8.5  55.2    7
c i   34.3    5642    34185     97038   11237   4818 13271  10  8.4  55.1    7
c -   34.9    5642    34185    103469   12521   4968 13312   8  8.5  54.7    7
c -   35.7    5642    34185    111749   14236   5087 13348  12  9.3  54.6    7
c -   36.5    5642    34185    120428   15443   5134 13356  12 10.9  55.5    7
c R   36.9    5642    34185    125268   19522   5146 13359  13 11.6  55.9    9
c i   37.2    5641    34185    127705   21732   5182 13373  12 11.6  55.6    9
c 
c [simplification-11] limit of 128451 conflicts hit after 128451 conflicts
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 5641 free variables schedulable
c [ternres-9] 361 ternary resolvents (17 bin, 344 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-21] removed 16 variables
c [simpleprobe-5] all 5631 free variables schedulable
c [simpleprobe-5] limit 11313337 penalty 0 = 0 + 0
c [decomp-22] removed 39 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 39 variables, found 3629 hbrs, 3 units
c [lift-9] limit 1697000 with penalty 0 = 0 + 0
c [lift-9] using 2125 probes 38%
c [lift-9] 4 units, 33 impls, 9 eqs in 1 rounds
c [lift-9] 2614 variables remain 47% (2965 retained)
c [lift-9] removed 13 variables
c [cliff-8] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-8] failed 3, lifted 0
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2089 transitive binary clauses
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 13 (8%) of length 13
c [cce-10-1] eliminated 1 clauses out of 12 (8%) of length 12
c [cce-10-1] eliminated 3 clauses out of 67 (4%) of length 11
c [cce-10-1] eliminated 5 clauses out of 168 (3%) of length 10
c [cce-10-1] eliminated 13 clauses out of 474 (3%) of length 9
c [cce-10-1] eliminated 23 clauses out of 940 (2%) of length 8
c [cce-10-1] eliminated 16 clauses out of 1404 (1%) of length 7
c [cce-10-1] eliminated 27 clauses out of 2411 (1%) of length 6
c [cce-10-1] eliminated 31 clauses out of 3060 (1%) of length 5
c [cce-10-1] eliminated 47 clauses out of 4362 (1%) of length 4
c [cce-10-1] completed large round (ACCE)
c [cce-10-1] eliminated 167 large clauses in 12948280 steps
c [cce-10-1] allowing another 6474140 steps for small clauses
c [cce-10] scheduling 17629 clauses = 14652 binary + 2977 ternary
c [cce-10] tried to eliminate 17629 small clauses 100%
c [cce-10] eliminated 207 small clauses 1%
c [cce-10] eliminated 135 binary clauses 1%
c [cce-10] eliminated 72 ternary clauses 2%
c [cce-10-1] eliminated 228 small clauses in 24494929 steps
c [cce-10-1] completed small round (ACCE)
c [cce-10-1] eliminated 395 covered clauses in round 1
c [cce-10-2] completed large round (ACCE)
c [cce-10-2] allowing another 0 steps for small clauses
c [cce-10] scheduling 17422 clauses = 14517 binary + 2905 ternary
c [cce-10] tried to eliminate 5524 small clauses 32%
c [cce-10] eliminated 1 small clauses 0%
c [cce-10] eliminated 1 binary clauses 0%
c [cce-10-2] eliminated 1 small clauses in 5505072 steps
c [cce-10-2] incomplete small round (ACCE)
c [cce-10-2] eliminated 1 covered clauses in round 2
c [cce-10] eliminated 396 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 5576 variables 100%
c [elim-11] limit of 56566689 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 44 variables 1% in round 1 in 6053405 steps
c [elim-11-1] backward subsumption/strengthening limit 12106810
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 1427246 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 44 = 1% variables out of 5576
c [simplification-11] removed 109 variables 1.9% (5532 remain 11%)
c [simplification-11] removed 736 irredundant clauses 2.2% (33449 remain 15%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 11111 = 33333 / 3
c [simplification-11] new conflict interval 44444
c [simplification-11] penalized conflict interval 44444 = 1 * 44444
c [simplification-11] new conflict limit 172895
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   39.1    5532    33449    130057   16622   5324 16913  13 11.6  55.4    8
c -   40.2    5532    33449    139469   18734   5474 16959  13 11.6  54.8    7
c -   41.4    5532    33449    149208   20632   5605 16989  12 11.7  54.4    7
c -   42.6    5532    33449    159410   22218   5735 17028  12 11.8  53.8    8
c -   44.0    5532    33449    170166   24155   5851 17079  10 11.9  53.4    8
c 
c [simplification-12] limit of 173211 conflicts hit after 173211 conflicts
c [ternres-10] limit 4465489 with penalty 0 = 0 + 0
c [ternres-10] all 5532 free variables schedulable
c [ternres-10] 477 ternary resolvents (8 bin, 469 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-23] removed 10 variables
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11044 literals 100%
c [treelook-5] scheduling used 224239 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 304669 steps
c [treelook-5] 11000 literals remain 100%
c [treelook-5] 5521 variables remain to probed next time 100%
c [decomp-24] removed 1 variables
c [treelook-5] removed 2 variables, found 367 hbrs
c [cgrclsr-4] limit 55818 penalty 3 = 3 + 0
c [cgrclsr-4] all 5520 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-10] limit 2679293 with penalty 0 = 0 + 0
c [lift-10] using 1734 probes 31%
c [lift-10] 4 units, 51 impls, 5 eqs in 1 rounds
c [lift-10] 2059 variables remain 37% (3449 retained)
c [lift-10] removed 12 variables
c [cliff-9] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-9] failed 4, lifted 5
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1709 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5499 variables 100%
c [block-5] limit of 6250000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 65 (2%) of length 11
c [cce-11-1] eliminated 2 clauses out of 156 (1%) of length 10
c [cce-11-1] eliminated 6 clauses out of 455 (1%) of length 9
c [cce-11-1] eliminated 9 clauses out of 910 (1%) of length 8
c [cce-11-1] eliminated 13 clauses out of 1360 (1%) of length 7
c [cce-11-1] eliminated 14 clauses out of 2353 (1%) of length 6
c [cce-11-1] eliminated 43 clauses out of 3072 (1%) of length 5
c [cce-11-1] eliminated 28 clauses out of 4361 (1%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 116 large clauses in 13007594 steps
c [cce-11-1] allowing another 6503797 steps for small clauses
c [cce-11] scheduling 17239 clauses = 14380 binary + 2859 ternary
c [cce-11] tried to eliminate 17239 small clauses 100%
c [cce-11] eliminated 80 small clauses 0%
c [cce-11] eliminated 65 binary clauses 0%
c [cce-11] eliminated 15 ternary clauses 1%
c [cce-11-1] eliminated 80 small clauses in 24622118 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 196 covered clauses in round 1
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] allowing another 0 steps for small clauses
c [cce-11] scheduling 17159 clauses = 14315 binary + 2844 ternary
c [cce-11] tried to eliminate 5030 small clauses 29%
c [cce-11-2] incomplete small round (ACCE)
c [cce-11-2] eliminated 0 covered clauses in round 2
c [cce-11] eliminated 196 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5499 variables 100%
c [elim-12] limit of 89309793 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 26 variables 0% in round 1 in 5690637 steps
c [elim-12-1] backward subsumption/strengthening limit 11381274
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 1404670 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 26 = 0% variables out of 5499
c [bca-10] limit of 10000000 steps
c [bca-10] 2682 out of 10948 literals actually usable 24%
c [bca-10] added 2 blocked clauses in 33089 steps
c [rephase-5] after 173211 conflicts (new increment 80000, next 253211)
c [flushphases] 0 phases reset
c [simplification-12] removed 59 variables 1.1% (5473 remain 11%)
c [simplification-12] removed 388 irredundant clauses 1.2% (33061 remain 14%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 22222 = 44444 / 2
c [simplification-12] new conflict interval 66666
c [simplification-12] penalized conflict interval 66666 = 1 * 66666
c [simplification-12] new conflict limit 239877
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   47.4    5473    33061    181825   25532   6122 18555   9 12.1  53.3    8
c -   49.1    5473    33061    193699   27505   6280 18597  10 12.0  52.7    9
c i   49.5    5472    33061    196067   29651   6312 18607  10 12.0  52.6   10
c -   51.0    5471    33061    205878   29375   6405 18631  11 12.0  52.3    9
c -   52.8    5471    33061    218129   30760   6495 18651  11 12.2  51.9    9
c -   55.0    5471    33061    231681   32703   6626 18681  13 12.3  51.4    9
c 
c [simplification-13] limit of 240171 conflicts hit after 240171 conflicts
c [ternres-11] limit 7513013 with penalty 0 = 0 + 0
c [ternres-11] all 5471 free variables schedulable
c [ternres-11] 665 ternary resolvents (13 bin, 652 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-5] limit 250000 penalty 3 = 3 + 0
c [gauss-5] extracted 157 xors of average arity 2.9
c [gauss-5] connected 462 occurrences of 169 variables (average 2.7)
c [gauss-5] limit 250000 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 14 variables
c [basicprobe-5] limit 7513013 penalty 0 = 0 + 0
c [basicprobe-5-0] 1040 sched 19%, 2 failed, 0 lifted, 1012 hbrs
c [decomp-26] removed 2 variables
c [basicprobe-5-1] 796 probes remain 15% after last round
c [basicprobe-5-1] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-5-1] removed 3 variables, found 1783 hbrs
c [bate-4] eliminated 2 asymmetric tautologies during probing
c [lift-11] limit 4507808 with penalty 0 = 0 + 0
c [lift-11] using 1225 probes 22%
c [lift-11] 2 units, 58 impls, 9 eqs in 1 rounds
c [lift-11] 1250 variables remain 23% (4193 retained)
c [lift-11] removed 11 variables
c [cliff-10] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-10] failed 0, lifted 0
c [unhide-7] limit 187825 with penalty 3 = 3 + 0
c [unhide-7-7] 0 units, 0 failed, 206 tauts, 0 hbrs, 50404 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1320 transitive binary clauses
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 6 clauses out of 157 (4%) of length 10
c [cce-12-1] eliminated 4 clauses out of 418 (1%) of length 9
c [cce-12-1] eliminated 10 clauses out of 893 (1%) of length 8
c [cce-12-1] eliminated 15 clauses out of 1317 (1%) of length 7
c [cce-12-1] eliminated 23 clauses out of 2338 (1%) of length 6
c [cce-12-1] eliminated 24 clauses out of 3014 (1%) of length 5
c [cce-12-1] eliminated 22 clauses out of 4358 (1%) of length 4
c [cce-12-1] completed large round (ACCE)
c [cce-12-1] eliminated 104 large clauses in 12982552 steps
c [cce-12-1] allowing another 6491276 steps for small clauses
c [cce-12] scheduling 17523 clauses = 14240 binary + 3283 ternary
c [cce-12] tried to eliminate 17523 small clauses 100%
c [cce-12] eliminated 136 small clauses 1%
c [cce-12] eliminated 97 binary clauses 1%
c [cce-12] eliminated 39 ternary clauses 1%
c [cce-12-1] eliminated 136 small clauses in 24843987 steps
c [cce-12-1] completed small round (ACCE)
c [cce-12-1] eliminated 240 covered clauses in round 1
c [cce-12-2] completed large round (ACCE)
c [cce-12-2] allowing another 0 steps for small clauses
c [cce-12] scheduling 17387 clauses = 14143 binary + 3244 ternary
c [cce-12] tried to eliminate 4937 small clauses 28%
c [cce-12] eliminated 1 small clauses 0%
c [cce-12] eliminated 1 binary clauses 0%
c [cce-12-2] eliminated 1 small clauses in 5156014 steps
c [cce-12-2] incomplete small round (ACCE)
c [cce-12-2] eliminated 1 covered clauses in round 2
c [cce-12] eliminated 241 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5443 variables 100%
c [elim-13] limit of 150260278 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 40 variables 1% in round 1 in 5577569 steps
c [elim-13-1] backward subsumption/strengthening limit 11155138
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 1380952 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 40 = 1% variables out of 5443
c [bca-11] limit of 10000000 steps
c [bca-11] 2400 out of 10808 literals actually usable 22%
c [bca-11] added 1 blocked clauses in 45231 steps
c [simplification-13] removed 68 variables 1.2% (5403 remain 11%)
c [simplification-13] removed 437 irredundant clauses 1.3% (32624 remain 14%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 33333 = 66666 / 2
c [simplification-13] new conflict interval 99999
c [simplification-13] penalized conflict interval 99999 = 1 * 99999
c [simplification-13] new conflict limit 340170
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   59.1    5403    32624    245941   33666   7081 19653  18 12.4  51.5   10
c -   60.9    5403    32624    260021   34793   7118 19656  10 12.6  51.5   10
c R   62.3    5403    32624    271507   43976   7149 19660  12 13.1  51.6   14
c -   63.2    5403    32624    275985   36189   7188 19672  13 13.1  51.3   10
c -   65.7    5403    32624    291301   37908   7310 19699  12 13.2  50.8   10
c i   67.7    5402    32624    303721   49539   7389 19716   9 13.2  50.6   15
c -   68.4    5399    32624    307131   39760   7402 19722  10 13.2  50.4   10
c -   71.0    5399    32624    323950   41764   7497 19743  15 13.2  50.0   10
c 
c [simplification-14] limit of 340376 conflicts hit after 340376 conflicts
c [ternres-12] limit 12624469 with penalty 0 = 0 + 0
c [ternres-12] all 5399 free variables schedulable
c [ternres-12] 1093 ternary resolvents (15 bin, 1078 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-27] removed 8 variables
c [simpleprobe-6] all 5395 free variables schedulable
c [simpleprobe-6] limit 50497877 penalty 0 = 0 + 0
c [decomp-28] removed 6 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 6 variables, found 4200 hbrs, 0 units
c [lift-12] limit 7574681 with penalty 0 = 0 + 0
c [lift-12] using 489 probes 9%
c [lift-12-1] found 1 units 33 impls in round 1
c [lift-12] 4 units, 55 impls, 11 eqs in 2 rounds
c [lift-12] 749 variables remain 14% (4625 retained)
c [lift-12] removed 15 variables
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2083 transitive binary clauses
c [cce-13] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-13-1] eliminated 1 clauses out of 142 (1%) of length 10
c [cce-13-1] eliminated 4 clauses out of 414 (1%) of length 9
c [cce-13-1] eliminated 14 clauses out of 886 (2%) of length 8
c [cce-13-1] eliminated 9 clauses out of 1270 (1%) of length 7
c [cce-13-1] eliminated 11 clauses out of 2312 (0%) of length 6
c [cce-13-1] eliminated 16 clauses out of 2976 (1%) of length 5
c [cce-13-1] eliminated 20 clauses out of 4374 (0%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 76 large clauses in 13214402 steps
c [cce-13-1] allowing another 6607201 steps for small clauses
c [cce-13] scheduling 16799 clauses = 13969 binary + 2830 ternary
c [cce-13] tried to eliminate 16799 small clauses 100%
c [cce-13] eliminated 79 small clauses 0%
c [cce-13] eliminated 57 binary clauses 0%
c [cce-13] eliminated 22 ternary clauses 1%
c [cce-13-1] eliminated 79 small clauses in 25087461 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 155 covered clauses in round 1
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] allowing another 0 steps for small clauses
c [cce-13] scheduling 16720 clauses = 13912 binary + 2808 ternary
c [cce-13] tried to eliminate 4605 small clauses 28%
c [cce-13-2] incomplete small round (ACCE)
c [cce-13-2] eliminated 0 covered clauses in round 2
c [cce-13] eliminated 155 covered clauses in TOTAL during 2 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5374 variables 100%
c [elim-14] limit of 252489386 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 19 variables 0% in round 1 in 5361244 steps
c [elim-14-1] backward subsumption/strengthening limit 10722488
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 1364473 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 19 = 0% variables out of 5374
c [bca-12] limit of 10000000 steps
c [bca-12] 2054 out of 10712 literals actually usable 19%
c [bca-12] added 0 blocked clauses in 60473 steps
c [rephase-6] after 340376 conflicts (new increment 160000, next 500376)
c [flushphases] 0 phases reset
c [simplification-14] removed 44 variables 0.8% (5355 remain 10%)
c [simplification-14] removed 310 irredundant clauses 1.0% (32314 remain 14%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 49999 = 99999 / 2
c [simplification-14] new conflict interval 149998
c [simplification-14] penalized conflict interval 149998 = 1 * 149998
c [simplification-14] new conflict limit 490374
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   76.0    5355    32314    342035   43078   8386 22437  11 13.3  49.7   12
c -   79.1    5355    32314    359744   44829   8480 22456  11 13.4  49.4   12
c -   82.5    5355    32314    377879   46692   8564 22471  13 13.5  48.9   12
c -   85.0    5355    32314    396346   47857   8596 22473  19 13.7  48.7   11
c -   88.6    5355    32314    415095   49485   8677 22492  12 13.7  48.3   12
c -   92.4    5355    32314    434673   51237   8750 22507  14 13.7  48.0   12
c -   96.3    5355    32314    455549   52882   8842 22527   9 13.8  47.7   12
c -  100.6    5355    32314    475784   54575   8938 22549  11 13.8  47.4   13
c 
c [simplification-15] limit of 490594 conflicts hit after 490595 conflicts
c [ternres-13] limit 21968950 with penalty 0 = 0 + 0
c [ternres-13] all 5355 free variables schedulable
c [ternres-13] 800 ternary resolvents (18 bin, 782 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 686529 penalty 4 = 4 + 0
c [card-5] found 953 at-most-one constraints of average size 3.1
c [card-5] found 131 at-most-two constraints of average size 4.1
c [card-5] using previous limit 686529 for elimination
c [card-5] 1083 out of 1084 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-29] removed 4 variables
c [treelook-6] limit 1098447 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10702 literals 100%
c [treelook-6] scheduling used 337854 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1098447 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1103441 steps
c [treelook-6] 10570 literals remain 99%
c [treelook-6] 5351 variables remain to probed next time 100%
c [decomp-30] removed 1 variables
c [treelook-6] removed 1 variables, found 1124 hbrs
c [lift-13] limit 13181370 with penalty 0 = 0 + 0
c [lift-13] using 43 probes 1%
c [lift-13-1] found 2 units 5 impls in round 1
c [lift-13-2] found 0 units 2 impls in round 2
c [lift-13-3] found 0 units 5 impls in round 3
c [lift-13-4] found 0 units 7 impls in round 4
c [lift-13-5] found 0 units 3 impls in round 5
c [lift-13] 2 units, 22 impls, 1 eqs in 6 rounds
c [lift-13] 703 variables remain 13% (4644 retained)
c [lift-13] removed 3 variables
c [cliff-11] limit of 8787580 steps penalty 1 = 1 + 0
c [cliff-11] failed 0, lifted 0
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1436 transitive binary clauses
c [cce-14] limit of 43937901 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 142 (1%) of length 10
c [cce-14-1] eliminated 3 clauses out of 407 (1%) of length 9
c [cce-14-1] eliminated 4 clauses out of 858 (0%) of length 8
c [cce-14-1] eliminated 8 clauses out of 1265 (1%) of length 7
c [cce-14-1] eliminated 9 clauses out of 2298 (0%) of length 6
c [cce-14-1] eliminated 9 clauses out of 2972 (0%) of length 5
c [cce-14-1] eliminated 5 clauses out of 4356 (0%) of length 4
c [cce-14-1] completed large round (ACCE)
c [cce-14-1] eliminated 40 large clauses in 13284689 steps
c [cce-14-1] allowing another 6642344 steps for small clauses
c [cce-14] scheduling 17119 clauses = 13900 binary + 3219 ternary
c [cce-14] tried to eliminate 17119 small clauses 100%
c [cce-14] eliminated 43 small clauses 0%
c [cce-14] eliminated 28 binary clauses 0%
c [cce-14] eliminated 15 ternary clauses 0%
c [cce-14-1] eliminated 43 small clauses in 25714897 steps
c [cce-14-1] completed small round (ACCE)
c [cce-14-1] eliminated 83 covered clauses in round 1
c [cce-14-2] completed large round (ACCE)
c [cce-14-2] allowing another 0 steps for small clauses
c [cce-14] scheduling 17076 clauses = 13872 binary + 3204 ternary
c [cce-14] tried to eliminate 16339 small clauses 96%
c [cce-14-2] incomplete small round (ACCE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 83 covered clauses in TOTAL during 2 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 5347 variables 100%
c [elim-15] limit of 439379016 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 15 variables 0% in round 1 in 5337447 steps
c [elim-15-1] backward subsumption/strengthening limit 10674894
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 1357736 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 15 = 0% variables out of 5347
c [simplification-15] removed 23 variables 0.4% (5332 remain 10%)
c [simplification-15] removed 126 irredundant clauses 0.4% (32188 remain 14%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 149998
c [simplification-15] new conflict interval 299996
c [simplification-15] penalized conflict interval 299996 = 1 * 299996
c [simplification-15] new conflict limit 790591
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  107.5    5332    32188    498197   56211   9605 23910  12 13.8  47.1   13
c -  111.1    5332    32188    519931   57629   9656 23919  12 13.9  47.2   13
c -  115.1    5332    32188    545945   58805   9701 23927  16 14.5  47.4   13
c -  119.4    5332    32188    571085   59777   9722 23928  13 14.8  47.4   19
c R  121.7    5332    32188    585180   72936   9728 23929  13 14.8  47.3   21
c -  123.9    5332    32188    593618   60881   9753 23933  12 14.8  47.1   14
c -  129.1    5332    32188    617392   62486   9811 23944  11 14.9  46.9   14
c -  134.3    5332    32188    642325   64280   9876 23958  10 14.9  46.8   14
c -  140.1    5332    32188    666869   65947   9952 23982  13 14.9  46.4   14
c -  146.3    5332    32188    692326   67498  10029 24003  11 14.9  46.2   15
c -  152.1    5332    32188    721953   68871  10080 24010  15 15.2  46.0   15
c -  158.5    5332    32188    748393   70377  10167 24030  16 15.2  45.7   14
c -  164.8    5332    32188    776682   71785  10238 24042  11 15.3  45.6   20
c 
c [simplification-16] limit of 790851 conflicts hit after 790852 conflicts
c [ternres-14] limit 44125080 with penalty 0 = 0 + 0
c [ternres-14] all 5332 free variables schedulable
c [ternres-14] 1907 ternary resolvents (28 bin, 1879 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-31] removed 8 variables
c [basicprobe-6] limit 44125080 penalty 0 = 0 + 0
c [basicprobe-6-0] 770 sched 14%, 1 failed, 0 lifted, 1052 hbrs
c [decomp-32] removed 2 variables
c [basicprobe-6-1] 2475 sched 47%, 2 failed, 0 lifted, 1566 hbrs
c [decomp-33] removed 2 variables
c [basicprobe-6-2] 2465 sched 46%, 0 failed, 0 lifted, 251 hbrs
c [basicprobe-6-3] 2464 sched 46%, 0 failed, 0 lifted, 105 hbrs
c [basicprobe-6-4] 2464 sched 46%, 0 failed, 0 lifted, 72 hbrs
c [basicprobe-6-5] 2155 probes remain 41% after last round
c [basicprobe-6-5] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-6-5] removed 4 variables, found 3047 hbrs
c [bate-5] eliminated 2 asymmetric tautologies during probing
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 22 probes 0%
c [lift-14-1] found 0 units 1 impls in round 1
c [lift-14-2] found 0 units 2 impls in round 2
c [lift-14-3] found 0 units 0 impls in round 3
c [lift-14-4] found 0 units 1 impls in round 4
c [lift-14-5] found 0 units 3 impls in round 5
c [lift-14] 0 units, 7 impls, 0 eqs in 6 rounds
c [lift-14] 680 variables remain 13% (4640 retained)
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1334 transitive binary clauses
c [cce-15] limit of 88250161 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 6 clauses out of 388 (2%) of length 9
c [cce-15-1] eliminated 9 clauses out of 859 (1%) of length 8
c [cce-15-1] eliminated 4 clauses out of 1269 (0%) of length 7
c [cce-15-1] eliminated 5 clauses out of 2284 (0%) of length 6
c [cce-15-1] eliminated 2 clauses out of 2977 (0%) of length 5
c [cce-15-1] eliminated 8 clauses out of 4359 (0%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 34 large clauses in 14015065 steps
c [cce-15-1] allowing another 7007532 steps for small clauses
c [cce-15] scheduling 16595 clauses = 13819 binary + 2776 ternary
c [cce-15] tried to eliminate 16595 small clauses 100%
c [cce-15] eliminated 42 small clauses 0%
c [cce-15] eliminated 32 binary clauses 0%
c [cce-15] eliminated 10 ternary clauses 0%
c [cce-15-1] eliminated 42 small clauses in 26657958 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 76 covered clauses in round 1
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] allowing another 0 steps for small clauses
c [cce-15] scheduling 16553 clauses = 13787 binary + 2766 ternary
c [cce-15] tried to eliminate 16553 small clauses 100%
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 0 covered clauses in round 2
c [cce-15] eliminated 76 covered clauses in TOTAL during 2 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 5320 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 11 variables 0% in round 1 in 5386899 steps
c [elim-16-1] backward subsumption/strengthening limit 10773798
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 1351961 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 11 = 0% variables out of 5320
c [bca-13] limit of 10000000 steps
c [bca-13] 1751 out of 10620 literals actually usable 16%
c [bca-13] added 0 blocked clauses in 88906 steps
c [rephase-7] after 790852 conflicts (new increment 320000, next 1110852)
c [flushphases] 0 phases reset
c [simplification-16] removed 23 variables 0.4% (5309 remain 10%)
c [simplification-16] removed 143 irredundant clauses 0.4% (32045 remain 14%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 299996
c [simplification-16] new conflict interval 599992
c [simplification-16] penalized conflict interval 599992 = 1 * 599992
c [simplification-16] new conflict limit 1390844
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  175.4    5309    32045    804539   73215  11983 25678  13 15.3  45.4   16
c -  181.2    5309    32045    832780   74552  12018 25686  16 15.4  45.2   16
c -  187.0    5309    32045    863271   75600  12063 25689  13 15.6  45.1   19
c -  194.5    5309    32045    892706   77026  12126 25699  13 15.6  44.9   17
c -  202.3    5309    32045    924178   78512  12189 25706  10 15.7  44.7   17
c -  210.2    5309    32045    955211   80173  12253 25718  11 15.8  44.5   17
c -  217.7    5309    32045    989147   81878  12331 25726  13 15.9  44.4   17
c -  226.3    5309    32045   1020060   83325  12405 25735  11 15.9  44.1   18
c -  235.1    5309    32045   1054242   84846  12470 25751  12 16.0  44.0   18
c -  243.9    5309    32045   1086296   86326  12531 25760  12 16.0  43.8   24
c -  250.5    5309    32045   1120200   87458  12550 25762  16 16.1  43.7   17
c -  257.9    5309    32045   1156567   88681  12581 25766  11 16.1  43.5   24
c -  267.1    5309    32045   1195548   89834  12619 25775  10 16.3  43.3   18
c -  274.8    5309    32045   1233608   90935  12641 25778  13 16.3  43.1   18
c R  278.9    5309    32045   1254198  108490  12673 25780  13 16.4  43.0   34
c -  284.3    5309    32045   1270400   92396  12711 25790  12 16.4  42.9   18
c -  294.2    5309    32045   1305902   94038  12769 25807  14 16.3  42.7   18
c -  304.8    5309    32045   1343391   95441  12827 25827  11 16.4  42.5   19
c -  313.8    5309    32045   1381276   96858  12879 25840  11 16.4  42.4   25
c 
c [simplification-17] limit of 1391104 conflicts hit after 1391108 conflicts
c [ternres-15] limit 98088822 with penalty 0 = 0 + 0
c [ternres-15] all 5309 free variables schedulable
c [ternres-15] 3217 ternary resolvents (37 bin, 3180 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-37] removed 2 variables
c [simpleprobe-7] all 5307 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 7 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 7 variables, found 5555 hbrs, 0 units
c [cgrclsr-5] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-5] all 5300 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1907 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5300 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [cce-16] limit of 196177645 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 379 (0%) of length 9
c [cce-16-1] eliminated 11 clauses out of 842 (1%) of length 8
c [cce-16-1] eliminated 4 clauses out of 1259 (0%) of length 7
c [cce-16-1] eliminated 9 clauses out of 2278 (0%) of length 6
c [cce-16-1] eliminated 12 clauses out of 2991 (0%) of length 5
c [cce-16-1] eliminated 29 clauses out of 4364 (1%) of length 4
c [cce-16-1] completed large round (ACCE)
c [cce-16-1] eliminated 66 large clauses in 15164558 steps
c [cce-16-1] allowing another 7582279 steps for small clauses
c [cce-16] scheduling 16913 clauses = 13740 binary + 3173 ternary
c [cce-16] tried to eliminate 16913 small clauses 100%
c [cce-16] eliminated 91 small clauses 1%
c [cce-16] eliminated 75 binary clauses 1%
c [cce-16] eliminated 16 ternary clauses 1%
c [cce-16-1] eliminated 91 small clauses in 29532487 steps
c [cce-16-1] completed small round (ACCE)
c [cce-16-1] eliminated 157 covered clauses in round 1
c [cce-16-2] completed large round (ACCE)
c [cce-16-2] allowing another 0 steps for small clauses
c [cce-16] scheduling 16822 clauses = 13665 binary + 3157 ternary
c [cce-16] tried to eliminate 16822 small clauses 100%
c [cce-16-2] completed small round (ACCE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 157 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 5300 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 15 variables 0% in round 1 in 5487901 steps
c [elim-17-1] backward subsumption/strengthening limit 10975802
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 1339347 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 15 = 0% variables out of 5300
c [rephase-8] after 1391108 conflicts (new increment 640000, next 2031108)
c [flushphases] 0 phases reset
c [simplification-17] removed 24 variables 0.5% (5285 remain 10%)
c [simplification-17] removed 211 irredundant clauses 0.7% (31834 remain 14%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 299996 = 599992 / 2
c [simplification-17] new conflict interval 899988
c [simplification-17] penalized conflict interval 899988 = 1 * 899988
c [simplification-17] new conflict limit 2291096
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  327.7    5285    31834   1419478   98212  16099 29481  10 16.4  42.3   21
c -  338.9    5285    31834   1457651   99672  16154 29491  10 16.4  42.1   21
c -  350.0    5285    31834   1496850  101205  16194 29502  12 16.5  42.0   21
c -  359.8    5285    31834   1537747  102413  16229 29514  12 16.6  41.9   21
c -  372.2    5285    31834   1576834  103736  16283 29523  12 16.6  41.8   21
c -  384.0    5285    31834   1617425  105100  16330 29532  15 16.6  41.7   22
c -  395.0    5285    31834   1657788  106378  16381 29547  12 16.6  41.5   22
c -  408.6    5285    31834   1698441  107864  16440 29561  11 16.6  41.3   22
c -  421.2    5285    31834   1739910  109259  16486 29573  10 16.6  41.2   22
c -  432.5    5285    31834   1783086  110474  16518 29578  10 16.6  41.1   29
c -  444.0    5285    31834   1833574  111743  16549 29582  15 16.7  41.1   22
c -  458.3    5285    31834   1877212  113066  16605 29587  12 16.7  40.9   30
c -  472.4    5285    31834   1920830  114459  16650 29594  10 16.7  40.8   30
c -  486.1    5285    31834   1967572  115776  16675 29607  10 16.8  40.7   22
c -  501.8    5285    31834   2012610  117247  16728 29619   9 16.8  40.5   23
c -  516.7    5285    31834   2058278  118919  16796 29632  12 16.8  40.4   32
c -  530.4    5285    31834   2107850  120335  16822 29639  12 16.9  40.4   30
c -  546.7    5285    31834   2155072  121758  16878 29653  11 16.9  40.3   24
c -  563.1    5285    31834   2202817  123239  16923 29667  11 16.9  40.1   24
c -  577.6    5285    31834   2249235  124438  16950 29675  11 16.9  40.0   31
c 
c [simplification-18] limit of 2291422 conflicts hit after 2291423 conflicts
c [ternres-16] limit 198129211 with penalty 0 = 0 + 0
c [ternres-16] all 5285 free variables schedulable
c [ternres-16] 3878 ternary resolvents (45 bin, 3833 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 2476615 penalty 4 = 4 + 0
c [gauss-6] extracted 619 xors of average arity 3.0
c [gauss-6] connected 1853 occurrences of 217 variables (average 8.5)
c [gauss-6] limit 2476615 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 2 variables
c [treelook-7] limit 9906460 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 10566 literals 100%
c [treelook-7] scheduling used 603886 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 9906460 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 9919363 steps
c [treelook-7] 8876 literals remain 84%
c [treelook-7] 5207 variables remain to probed next time 99%
c [decomp-40] removed 16 variables
c [treelook-7] removed 19 variables, found 8673 hbrs
c [lift-15] limit 10000000 with penalty 1 = 1 + 0
c [lift-15] using 112 probes 2%
c [lift-15-1] found 0 units 8 impls in round 1
c [lift-15-2] found 0 units 12 impls in round 2
c [lift-15-3] found 0 units 12 impls in round 3
c [lift-15-4] found 0 units 14 impls in round 4
c [lift-15-5] found 0 units 12 impls in round 5
c [lift-15] 0 units, 58 impls, 1 eqs in 6 rounds
c [lift-15] 560 variables remain 11% (4703 retained)
c [lift-15] removed 1 variables
c [cliff-12] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-12] failed 1, lifted 0
c [unhide-8] limit 1250000 with penalty 4 = 4 + 0
c [unhide-8-8] 0 units, 0 failed, 7642 tauts, 0 hbrs, 430812 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1596 transitive binary clauses
c [cce-17] limit of 396258423 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-17-1] eliminated 2 clauses out of 8 (25%) of length 13
c [cce-17-1] eliminated 1 clauses out of 55 (2%) of length 11
c [cce-17-1] eliminated 5 clauses out of 98 (5%) of length 10
c [cce-17-1] eliminated 13 clauses out of 324 (4%) of length 9
c [cce-17-1] eliminated 18 clauses out of 757 (2%) of length 8
c [cce-17-1] eliminated 12 clauses out of 1161 (1%) of length 7
c [cce-17-1] eliminated 40 clauses out of 2302 (2%) of length 6
c [cce-17-1] eliminated 27 clauses out of 3036 (1%) of length 5
c [cce-17-1] eliminated 48 clauses out of 4382 (1%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 167 large clauses in 15015906 steps
c [cce-17-1] allowing another 7507953 steps for small clauses
c [cce-17] scheduling 16408 clauses = 13585 binary + 2823 ternary
c [cce-17] tried to eliminate 16408 small clauses 100%
c [cce-17] eliminated 199 small clauses 1%
c [cce-17] eliminated 168 binary clauses 1%
c [cce-17] eliminated 31 ternary clauses 1%
c [cce-17-1] eliminated 199 small clauses in 29279871 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 366 covered clauses in round 1
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] allowing another 0 steps for small clauses
c [cce-17] scheduling 16209 clauses = 13417 binary + 2792 ternary
c [cce-17] tried to eliminate 16209 small clauses 100%
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 0 covered clauses in round 2
c [cce-17] eliminated 366 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 5262 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 75 variables 1% in round 1 in 5220283 steps
c [elim-18-1] backward subsumption/strengthening limit 10440566
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 1297412 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 75 = 1% variables out of 5262
c [rephase-9] after 2291423 conflicts (new increment 1280000, next 3571423)
c [flushphases] 0 phases reset
c [simplification-18] removed 98 variables 1.9% (5187 remain 10%)
c [simplification-18] removed 582 irredundant clauses 1.8% (31252 remain 14%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 299996 = 899988 / 3
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] new conflict limit 3291423
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  602.1    5187    31252   2303987  120796  19566 31944  11 16.9  39.9   27
c -  619.5    5187    31252   2352522  122326  19617 31956  14 16.9  39.8   36
c -  633.1    5187    31252   2407065  123549  19642 31959  12 17.0  39.7   36
c -  645.8    5187    31252   2458448  124325  19650 31962  15 16.9  39.5   28
c -  657.9    5187    31252   2511688  125077  19663 31964  11 16.9  39.4   28
c -  676.2    5187    31252   2586834  126422  19674 31969  11 17.2  39.4   38
c -  693.7    5187    31252   2656762  127502  19691 31971  12 17.4  39.4   38
c R  698.0    5187    31252   2675632  142118  19698 31972  11 17.5  39.5   45
c -  712.4    5187    31252   2711301  128775  19735 31978  10 17.5  39.4   25
c -  731.3    5187    31252   2764492  130107  19788 31986  11 17.5  39.2   26
c -  750.1    5187    31252   2818684  131490  19821 31995  12 17.5  39.1   26
c -  769.8    5187    31252   2871761  132866  19850 32006  11 17.5  39.0   26
c -  788.4    5187    31252   2925550  134201  19880 32011  15 17.5  39.0   25
c -  807.7    5187    31252   2981084  135587  19907 32018  15 17.5  38.9   36
c -  830.9    5187    31252   3038213  136984  19947 32022  12 17.5  38.8   26
c -  852.2    5187    31252   3095351  138183  19982 32029  11 17.5  38.7   37
c -  874.3    5187    31252   3151204  139635  20011 32037  14 17.5  38.6   26
c -  892.9    5187    31252   3209254  140722  20037 32046  10 17.5  38.5   37
c -  916.9    5187    31252   3279179  141960  20062 32051  12 17.6  38.4   26
c 
c [simplification-19] limit of 3291581 conflicts hit after 3291584 conflicts
c [ternres-17] limit 200000000 with penalty 0 = 0 + 0
c [ternres-17] all 5187 free variables schedulable
c [ternres-17] 4998 ternary resolvents (46 bin, 4952 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-41] removed 4 variables
c [basicprobe-7] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 2011 sched 39%, 0 failed, 0 lifted, 1908 hbrs
c [decomp-42] removed 1 variables
c [basicprobe-7-1] 2273 sched 44%, 0 failed, 0 lifted, 527 hbrs
c [basicprobe-7-2] 2270 sched 44%, 0 failed, 0 lifted, 145 hbrs
c [basicprobe-7-3] 2270 sched 44%, 0 failed, 0 lifted, 69 hbrs
c [basicprobe-7-4] 2270 sched 44%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-7-5] 2270 sched 44%, 0 failed, 0 lifted, 24 hbrs
c [basicprobe-7-6] 2269 sched 44%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-7-7] 2269 sched 44%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-7-8] 1945 probes remain 38% after last round
c [basicprobe-7-8] removed 1 variables, found 2740 hbrs
c [bate-6] eliminated 1 asymmetric tautologies during probing
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 24 probes 0%
c [lift-16-1] found 0 units 4 impls in round 1
c [lift-16-2] found 0 units 1 impls in round 2
c [lift-16-3] found 0 units 0 impls in round 3
c [lift-16-4] found 0 units 1 impls in round 4
c [lift-16-5] found 0 units 1 impls in round 5
c [lift-16] 0 units, 7 impls, 1 eqs in 6 rounds
c [lift-16] 525 variables remain 10% (4656 retained)
c [lift-16] removed 1 variables
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1491 transitive binary clauses
c [cce-18] limit of 656529625 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 1 clauses out of 12 (8%) of length 12
c [cce-18-1] eliminated 3 clauses out of 311 (1%) of length 9
c [cce-18-1] eliminated 13 clauses out of 741 (2%) of length 8
c [cce-18-1] eliminated 10 clauses out of 1147 (1%) of length 7
c [cce-18-1] eliminated 17 clauses out of 2266 (1%) of length 6
c [cce-18-1] eliminated 11 clauses out of 3043 (0%) of length 5
c [cce-18-1] eliminated 29 clauses out of 4366 (1%) of length 4
c [cce-18-1] completed large round (ACCE)
c [cce-18-1] eliminated 84 large clauses in 15574456 steps
c [cce-18-1] allowing another 7787228 steps for small clauses
c [cce-18] scheduling 15964 clauses = 13221 binary + 2743 ternary
c [cce-18] tried to eliminate 15964 small clauses 100%
c [cce-18] eliminated 58 small clauses 0%
c [cce-18] eliminated 49 binary clauses 0%
c [cce-18] eliminated 9 ternary clauses 0%
c [cce-18-1] eliminated 58 small clauses in 29899205 steps
c [cce-18-1] completed small round (ACCE)
c [cce-18-1] eliminated 142 covered clauses in round 1
c [cce-18-2] completed large round (ACCE)
c [cce-18-2] allowing another 0 steps for small clauses
c [cce-18] scheduling 15906 clauses = 13172 binary + 2734 ternary
c [cce-18] tried to eliminate 15906 small clauses 100%
c [cce-18-2] completed small round (ACCE)
c [cce-18-2] eliminated 0 covered clauses in round 2
c [cce-18] eliminated 142 covered clauses in TOTAL during 2 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 5181 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 17 variables 0% in round 1 in 4996023 steps
c [elim-19-1] backward subsumption/strengthening limit 9992046
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 1281624 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 17 = 0% variables out of 5181
c [bca-14] limit of 10000000 steps
c [bca-14] 1433 out of 10330 literals actually usable 14%
c [bca-14] added 3 blocked clauses in 155693 steps
c [simplification-19] removed 23 variables 0.4% (5164 remain 10%)
c [simplification-19] removed 185 irredundant clauses 0.6% (31067 remain 14%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-19] conflict interval soft limit 1000000 reached
c [simplification-19] new conflict interval 1000000
c [simplification-19] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-19] new conflict limit 4291584
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  948.5    5164    31067   3338523  142807  24813 33179  12 17.6  38.3   29
c -  971.2    5164    31067   3398090  144051  24863 33187  17 17.6  38.2   29
c -  995.2    5164    31067   3457125  145424  24895 33194  12 17.6  38.1   29
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 25 basic ate = 20 trn 80% + 5 lrg 20% in 6 updates
c bcas: 14 count, 142 added (0 skipped), 634769 steps
c bkwd: tried 638640 clauses, 1276928 lits, 2.00 lits/clause
c bkwd: checked 45494535 occs, 71.24 occs/clause, 35.63 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 438 large (0% self)
c blkd: 6 bces, 663 removed, 1257477 resolutions, 3550273 steps
c blkd: 3917 blocking literals 4%, 3 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 6 am1, 5864342 steps
c card: 53 rescheduled, 406 eliminated, 7994 resolved, 25064 subsumed
c card: 8903 at-most-one constraints found, average size 3.03
c card: 8903 at-most-one constraints used 100%, average size 3.03
c card: 264 at-most-two constraints found, average size 4.08
c card: 261 at-most-two constraints used 99%, average size 4.08
c cces: 18 cces, 21551 eliminated, 16741 ate 78%, 4810 abce 22%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 5 count, 905884 esteps, 198526 csteps
c cgrs: 0 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 3240 extracted (2662 ands 82%, 222 xors 7%, 356 ites 11%)
c clff: 12 cliffs, 77 lifted, 98 failed
c clff: 382692 decisions, 128814166 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 807717 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 154 gcs, 0 rescored clauses, 1818 rescored vars
c dcps: 49 decompositions, 15569 equivalent 30%
c deco: 343124 decision-only clauses 10%, 75% reduction
c decs: 9220260 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 309651 flipped 3.358% (in 6440 phases)
c elms: 19 elims, 21068 eliminated 41%
c elms: 38 rounds, 2.0 rounds/bve
c elms: 17226 small 82%, 3839 large 18%
c elms: 23175 tried small, 17226 succeeded 74%, 5949 failed 26%
c elms: 9652 subsumed, 26536 strengthened, 613 blocked
c elms: 4412649 copies, 5858887 resolutions, 447934 ipos
c elms: 1697644 subchks, 2299433 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 6 extractions, 5904 extracted, 2.9 size, 4 max
c gaus: exported 0 units, 5 binary and 1 ternary equations
c gaus: 0 gc, 14013816 steps, 7006908 extr 50%, 219753 elim 2%
c glue: 17.6 orig avg, 17.1 real avg, 3.8 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 114378 = 65796 simple + 42959 trn 58% + 5623 lrg 38%, 3742 sub 5%
c hght: 38 average, 2.16 height/glue
c ints: 89069 luby (25522052 steps), 0 inout (0 steps)
c lift: 16 phases, 39392 probed (13222 level1 34%, 26170 level2 66%)
c lift: 100 units, 90 equivalences, 465 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3456967 clauses, 61.4 length
c lrnd: 754769 uips 22%, 2358755 flips 68%
c mega: 0 count, 0 failed, 0 rounds
c mins: 212270627 learned lits, 40% minimized
c mins: 3090523 mins 89%, 1346 bin 0%, 21974 size 1%, 343124 deco 10%
c move: moved 3456967, 13688 bin 0%, 1654 trn 0%, 0 lrg 0%
c otfs: str 55861 dyn (54980 red, 881 irr) 12872 drv 23%, 42989 rst 77%
c otfs: sub 277 dyn (277 red, 0 irr)
c phas: 7 computed, 11129 set, 5265 pos (47%), 5864 neg (53%)
c prbs: 7 basic, 77395 probed, 75 failed, 1 lifted
c prbs: 7 simple, 162036 probed, 678 failed, 14526 eqs
c prbs: 7 treelook, 2297 probed, 11 failed, 0 lifted
c prps: 1159673188 props, 123 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c psns: 363107168 searches, 72527639 hits, 20% 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: 112 count, 0 reset, 1 acts 1%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 112 arith 100%, 0 double 0%
c rmbd: 14398 removed, 13799 red 96%
c rphs: 9 recomputed phases
c rsts: 88101 restarts 99%, 968 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 968 reuse 100%
c rsts: 38.5 avg interval, 38.5 scaled, 1.0 factor
c rsts: 18294 kept 20.8% average 22.1%
c simp: 19 count (19 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3456967 count (5316203 tried 1.5), 378553 sub out of 3446553 (11.0%)
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: 9664 fixed 19%, 51 its, 68036.06 confs/it
c trvs: 57243894050 traversals, 99% srch, 1% simp, 0% lkhd
c trvs: 50.3 search traversals per propagation, 16404.3 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 17 transitive reductions, 20878 removed, 0 failed
c trds: 136093 nodes, 335012 edges, 23286955 steps
c trim: 7358904 words, 28.1 MB
c trnr: 17 count, 390 bin, 20986 trn, 179722008 steps
c unhd: 8 count, 8 rounds, 5987894 steps
c unhd: 146 non-trivial sccs of average size 2.4
c unhd: 57 units, 57 bin, 0 trn, 0 lrg
c unhd: 27 failed, 26 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 14530 tauts, 250 bin 2%, 1972 trn 14%, 1398 lrg 10%
c unhd: 14530 tauts, 10910 stamp 75%, 13079 red 90%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 506033 str, 57 bin 0%, 456 trn 0%, 505520 lrg 100%, 493824 red 98%
c vars: 5164 remaining 10% and 46301 removed 90% out of 51465
c vars: 9664 fixed 19%, 21068 eliminated 41%, 15569 equivalent 30%
c vsts: 35697800596 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 31.3 search visits per propagation, 10194.7 per conflict
c wchs: 10220338003 pushed, 30201944 enlarged, 316 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3446553 100   2867904 100 299466776 100  64307845 100   2703239 100
c 
c  0     115998   3         0   0 223557716  75< 36454395  57   1020037  38 
c  1     109005   3     42808   1  62430253  21  16627589  26<   703387  26 
c  2     446327  13    436048  15   4870910   2   2528288   4    172613   6<
c  3     835899  24    808635  28   4122201   1   3338486   5    311601  12 
c  4     887393  26<   840862  29<  2468747   1   2705549   4    266501  10 
c  5     583405  17    558646  19   1277283   0   1596276   2    158358   6 
c  6     262595   8    125688   4    454274   0    629084   1     47153   2 
c  7     126913   4     32010   1    178139   0    267579   0     14500   1 
c  8      53183   2     14546   1     71996   0    108734   0      6151   0 
c  9      16945   0      5572   0     22993   0     33927   0      1985   0 
c 10       8162   0      2779   0     11254   0     16444   0       842   0 
c 11        728   0       310   0      1010   0      1494   0       111   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.8           3.7           0.4           0.9           1.6
c std             1.7           1.3           0.8           1.5           1.8
c 
c   79.644   8% analysis
c   32.176   3% mincls
c   26.419   3% cce
c   13.227   1% bump
c   10.881   1% decide
c    9.233   1% probe
c    5.903   1% elim
c    5.609   1% restart
c    4.083   0% cliff
c    3.137   0% gc
c    2.782   0% decomp
c    2.073   0% lift
c    1.754   0% transred
c    1.676   0% backward
c    1.543   0% reduce
c    1.500   0% ternres
c    1.364   0% defrag
c    1.332   0% unhide
c    0.370   0% gauss
c    0.369   0% bca
c    0.354   0% block
c    0.219   0% card
c    0.201   0% cgrclsr
c    0.049   0% phase
c    0.017   0% tabularasa
c    0.003   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    1.367   0% probe simple     15%
c    7.023   1% probe basic      76%
c    0.843   0% probe tree-look   9%
c ==================================
c    2.630   0% preprocessing     5%
c   52.562   5% inprocessing     95%
c ==================================
c   55.191   6% simplifying
c  944.751  94% search
c ==================================
c  999.943 100% all
c 
c 9220260 decisions, 9220.8 decisions/sec
c 3469839 conflicts, 3470.0 conflicts/sec
c 1159673188 propagations, 1.2 megaprops/sec
c 999.9 seconds, 72.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
