c launch: /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c host: atom14
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/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c no embedded options
c found 'p cnf 52444 217642' header
c read 52444 variables, 217642 clauses, 547043 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 50629 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   50629   210196         0       0      0     0   2  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 4365 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] 4365 out of 4365 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 16367 variables
c [simpleprobe-1] all 36077 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 5434 variables
c [simpleprobe-1] 66 variables remain 0% (30577 retained)
c [simpleprobe-1] removed 5434 variables, found 35300 hbrs, 697 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 9 units, 6 failed, 323 tauts, 0 hbrs, 619 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 30620 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 19242 variables 63% in round 1 in 22541355 steps
c [elim-1-1] backward subsumption/strengthening limit 45082710
c [elim-1-1] subsumed 0 and strengthened 48 clauses in 45083655 steps
c [elim-1-1] rescheduled 148 variables 0% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 57565 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 19296 = 63% variables out of 30620
c [phase-1] phase bias: 4802 positive 42%, 6522 negative 58%
c [simplification-1] removed 34825 variables 75.5% (11324 remain 22%)
c [simplification-1] removed 130761 irredundant clauses 62.2% (79435 remain 38%)
c [simplification-1] maximum reduction of 75% = max (75%, 62%)
c [simplification-1] large reduction 75% >= 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] 47432, max 73553, min4 41292 at 75%, min10 16985 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number variables 11324 drops below limit 12657
c [tabula-rasa-1] number clauses 79435 drops below limit 105098
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 11324 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 2831 and clause limit 39717
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.7   11324    79435         5       4      1  7530   7  3.6 242.5    7
c R    2.8   11324    79435        20      16      3  7531   8  3.6 236.4    7
c R    2.8   11324    79435        61      45     11  7535   8  3.2 218.2    7
c R    2.8   11324    79435       161     127     22  7539   8  3.8 188.7    7
c i    2.8   11323    79435       204     158     28  7544   8  3.8 181.6    7
c i    2.8   11314    79435       205     158     28  7544   8  3.8 181.6    7
c i    2.8   11310    79435       252     195     32  7546   8  3.8 199.0    7
c i    2.8   11308    79435       284     218     37  7549   8  3.7 195.3    7
c i    2.8   11307    79435       285     218     37  7549   8  3.7 195.2    7
c R    2.8   11307    79435       412     324     42  7553   8  4.1 194.4    7
c i    2.8   11306    79435       645     510     59  7568   6  4.4 170.1    7
c R    2.9   11304    79435       984     795     92  7581   6  4.7 156.3    7
c i    2.9   11303    79434      1219     992    106  7589   6  4.8 144.5    7
c 
c [simplification-2] limit of 1252 conflicts hit after 1252 conflicts
c [decomp-3] removed 53 variables
c [simpleprobe-2] 19 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 6 variables
c [simpleprobe-2] 283 variables remain 3% (10982 retained)
c [simpleprobe-2] removed 6 variables, found 303 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 22530 literals 100%
c [treelook-1] scheduling used 258832 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304367 steps
c [treelook-1] 22445 literals remain 100%
c [treelook-1] 11265 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 456 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6417 probes remain 57% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 98 variables, found 1173 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 4 units, 19 failed, 428 tauts, 0 hbrs, 4621 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 11115 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 142 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 41 clauses out of 41 (100%) of length 15
c [cce-1-1] eliminated 26 clauses out of 27 (96%) of length 14
c [cce-1-1] eliminated 17 clauses out of 18 (94%) of length 13
c [cce-1-1] eliminated 14 clauses out of 269 (5%) of length 12
c [cce-1-1] eliminated 36 clauses out of 664 (5%) of length 11
c [cce-1-1] eliminated 14 clauses out of 332 (4%) of length 10
c [cce-1-1] eliminated 98 clauses out of 1074 (9%) of length 9
c [cce-1-1] eliminated 46 clauses out of 1516 (3%) of length 8
c [cce-1-1] eliminated 153 clauses out of 3036 (5%) of length 7
c [cce-1-1] eliminated 455 clauses out of 4679 (10%) of length 6
c [cce-1-1] eliminated 866 clauses out of 6187 (14%) of length 5
c [cce-1-1] eliminated 1135 clauses out of 7234 (16%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2901 large clauses in 59652880 steps
c [cce-1-1] allowing another 29826440 steps for small clauses
c [cce-1] scheduling 45171 clauses = 38807 binary + 6364 ternary
c [cce-1] tried to eliminate 45171 small clauses 100%
c [cce-1] eliminated 4207 small clauses 9%
c [cce-1] eliminated 3641 binary clauses 9%
c [cce-1] eliminated 566 ternary clauses 9%
c [cce-1-1] eliminated 4207 small clauses in 154413218 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7108 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 40964 clauses = 35166 binary + 5798 ternary
c [cce-1] tried to eliminate 40964 small clauses 100%
c [cce-1] eliminated 2561 small clauses 6%
c [cce-1] eliminated 2541 binary clauses 7%
c [cce-1] eliminated 20 ternary clauses 0%
c [cce-1-2] eliminated 2561 small clauses in 107616860 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 2561 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 38403 clauses = 32625 binary + 5778 ternary
c [cce-1] tried to eliminate 13701 small clauses 36%
c [cce-1] eliminated 431 small clauses 1%
c [cce-1] eliminated 428 binary clauses 1%
c [cce-1] eliminated 3 ternary clauses 0%
c [cce-1-3] eliminated 431 small clauses in 37969923 steps
c [cce-1-3] incomplete small round (ACCE)
c [cce-1-3] eliminated 431 covered clauses in round 3
c [cce-1] eliminated 10100 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 11111 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 713 variables 6% in round 1 in 15027829 steps
c [elim-2-1] backward subsumption/strengthening limit 4972171
c [elim-2-1] subsumed 0 and strengthened 40 clauses in 4972409 steps
c [elim-2] incomplete 82 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 713 = 6% variables out of 11111
c [bca-1] limit of 10000000 steps
c [bca-1] 17662 out of 20798 literals actually usable 85%
c [bca-1] added 162 blocked clauses in 51784 steps
c [phase-3] phase bias: 4 positive 100%, 0 negative 0%
c [simplification-2] removed 898 variables 7.9% (10398 remain 21%)
c [simplification-2] removed 13799 irredundant clauses 17.4% (65635 remain 31%)
c [simplification-2] maximum reduction of 17% = max (8%, 17%)
c [simplification-2] large reduction 17% >= 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 3252
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   12.2   10398    65635      2289    1765    674 12374   7  5.2 129.6    7
c 
c [simplification-3] limit of 3396 conflicts hit after 3396 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 10398 free variables schedulable
c [ternres-1] 4103 ternary resolvents (278 bin, 3825 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1091 at-most-one constraints of average size 3.0
c [card-2] found 9 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1100 out of 1100 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 4 at-most-one constraints, 2 used 50%
c [card-2] exported 2 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 3957 xors of average arity 2.9
c [gauss-1] connected 11421 occurrences of 566 variables (average 20.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 103 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 20590 literals 100%
c [treelook-2] scheduling used 251968 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300512 steps
c [treelook-2] 20397 literals remain 99%
c [treelook-2] 10292 variables remain to probed next time 100%
c [decomp-7] removed 2 variables
c [treelook-2] removed 5 variables, found 286 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 10290 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 3 variables
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 7202 probes 70%
c [lift-1] 5 units, 13 impls, 1 eqs in 1 rounds
c [lift-1] 10106 variables remain 98% (173 retained)
c [lift-1] removed 8 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 46, lifted 37
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 1 failed, 291 tauts, 0 hbrs, 1192 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 89 transitive binary clauses
c [transred-1] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 10165 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 41 blocked clauses
c [block-2] 41 < 1/1000 * 64694 = 64 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 6 clauses out of 417 (1%) of length 11
c [cce-2-1] eliminated 9 clauses out of 294 (3%) of length 10
c [cce-2-1] eliminated 56 clauses out of 1092 (5%) of length 9
c [cce-2-1] eliminated 18 clauses out of 1455 (1%) of length 8
c [cce-2-1] eliminated 57 clauses out of 2746 (2%) of length 7
c [cce-2-1] eliminated 377 clauses out of 4175 (9%) of length 6
c [cce-2-1] eliminated 22 clauses out of 5131 (0%) of length 5
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] eliminated 545 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 36492 clauses = 31050 binary + 5442 ternary
c [cce-2] tried to eliminate 5460 small clauses 15%
c [cce-2] eliminated 244 small clauses 1%
c [cce-2] eliminated 213 binary clauses 1%
c [cce-2] eliminated 31 ternary clauses 1%
c [cce-2-1] eliminated 244 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ACCE)
c [cce-2-1] eliminated 789 covered clauses in round 1
c [cce-2] eliminated 789 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 10161 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 175 variables 2% in round 1 in 11407896 steps
c [elim-3-1] backward subsumption/strengthening limit 8592104
c [elim-3-1] subsumed 0 and strengthened 21 clauses in 8592657 steps
c [elim-3] incomplete 55 not tried 1% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 175 = 2% variables out of 10161
c [bca-2] limit of 10000000 steps
c [bca-2] 14498 out of 19974 literals actually usable 73%
c [bca-2] added 77 blocked clauses in 43209 steps
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-3] removed 412 variables 4.0% (9986 remain 20%)
c [simplification-3] removed 2578 irredundant clauses 3.9% (63057 remain 30%)
c [simplification-3] maximum reduction of 4% = max (4%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] new conflict limit 27396
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   14.7    9986    63057      5209    4143   3322 15501  11  5.4 110.3    7
c i   14.8    9985    63057      5901    4748   3351 15516   6  5.5 106.1    7
c i   14.8    9983    63057      5902    4748   3351 15516   6  5.5 106.1    7
c -   14.9    9967    63057      7032    3749   3403 15539   6  5.6 100.9    7
c i   15.0    9966    63057      8345    4910   3445 15587   6  5.6  96.0    7
c i   15.1    9965    63057      8812    5314   3474 15590   6  5.6  95.1    7
c i   15.1    9964    63057      8816    5315   3475 15590   6  5.6  95.1    7
c -   15.3    9964    63057     11620    5269   3585 15621   8  7.1  97.8    7
c R   15.3    9964    63057     11725    5346   3592 15622   8  7.1  97.9    7
c i   15.4    9963    63057     13177    6619   3664 15646   6  7.1  94.5    7
c i   15.5    9962    63057     14441    7716   3718 15663   6  7.0  93.2    7
c i   15.6    9961    63057     14601    7841   3728 15671   6  7.0  92.7    7
c i   15.6    9959    63057     15530    8633   3771 15683   6  7.0  90.9    7
c i   15.7    9942    63057     15729    8810   3778 15688   6  7.0  90.4    8
c i   15.7    9941    63057     16482    9447   3803 15698   7  7.1  90.7    8
c -   15.8    9941    63057     16833    6743   3815 15701   6  7.1  90.4    7
c i   16.0    9940    63057     18716    8435   3863 15731   5  7.1  87.7    7
c i   16.1    9937    63057     20250    9807   3929 15745   6  7.1  86.8    7
c -   16.3    9930    63057     22478    8276   3973 15766   8  7.8  86.5    7
c R   16.6    9930    63057     26132   11054   4019 15789   8  9.2  85.4    8
c i   16.8    9929    63057     28063   12796   4073 15811   7  9.1  83.3    8
c i   16.8    9928    63057     28132   12859   4077 15811   7  9.1  83.2    8
c 
c [simplification-4] limit of 28294 conflicts hit after 28294 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 9928 free variables schedulable
c [ternres-2] 380 ternary resolvents (16 bin, 364 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-8] removed 125 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 4538 probes remain 46% after last round
c [basicprobe-2-0] 41 units = 26 failed (63%) + 15 lifted (37%)
c [basicprobe-2-0] removed 31 variables, found 658 hbrs
c [bate-1] eliminated 16 asymmetric tautologies during probing
c [cgrclsr-2] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-2] all 9830 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 6 variables
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 6883 probes 70%
c [lift-2] 13 units, 12 impls, 8 eqs in 1 rounds
c [lift-2] 9487 variables remain 97% (316 retained)
c [lift-2] removed 21 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 21, lifted 35
c [unhide-4] limit 130667 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 4 failed, 2425 tauts, 0 hbrs, 10807 literals
c [transred-2] limit 653339 with penalty 0 = 0 + 0
c [transred-2] removed 325 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 91 (2%) of length 12
c [cce-3-1] eliminated 2 clauses out of 367 (1%) of length 11
c [cce-3-1] eliminated 12 clauses out of 279 (4%) of length 10
c [cce-3-1] eliminated 25 clauses out of 949 (3%) of length 9
c [cce-3-1] eliminated 46 clauses out of 1288 (4%) of length 8
c [cce-3-1] eliminated 73 clauses out of 2517 (3%) of length 7
c [cce-3-1] eliminated 68 clauses out of 3898 (2%) of length 6
c [cce-3-1] eliminated 155 clauses out of 4949 (3%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 383 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 35362 clauses = 29640 binary + 5722 ternary
c [cce-3] tried to eliminate 6089 small clauses 17%
c [cce-3] eliminated 321 small clauses 1%
c [cce-3] eliminated 237 binary clauses 1%
c [cce-3] eliminated 84 ternary clauses 1%
c [cce-3-1] eliminated 344 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 727 covered clauses in round 1
c [cce-3] eliminated 727 covered clauses in TOTAL during 1 rounds
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 9738 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 264 variables 3% in round 1 in 11963396 steps
c [elim-4-1] backward subsumption/strengthening limit 8036604
c [elim-4-1] subsumed 0 and strengthened 19 clauses in 8037216 steps
c [elim-4] incomplete 43 not tried 0% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 264 = 3% variables out of 9738
c [bca-3] limit of 10000000 steps
c [bca-3] 10844 out of 18950 literals actually usable 57%
c [bca-3] added 41 blocked clauses in 40764 steps
c [rephase-1] after 28294 conflicts (new increment 20000, next 48294)
c [flushphases] 0 phases reset
c [simplification-4] removed 454 variables 4.6% (9474 remain 19%)
c [simplification-4] removed 3442 irredundant clauses 5.5% (59615 remain 28%)
c [simplification-4] maximum reduction of 5% = max (5%, 5%)
c [simplification-4] large reduction 5% >= 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 30294
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   19.2    9474    59615     29462    9005   3647 14154   7  9.0  82.4    8
c i   19.3    9473    59615     29874    9364   3663 14161   6  9.0  82.1    8
c 
c [simplification-5] limit of 30344 conflicts hit after 30345 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 9473 free variables schedulable
c [ternres-3] 222 ternary resolvents (1 bin, 221 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1524 xors of average arity 2.9
c [gauss-2] connected 4436 occurrences of 492 variables (average 9.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 50 variables
c [simpleprobe-3] 242 schedulable variables 3%
c [simpleprobe-3] limit 2852950 penalty 0 = 0 + 0
c [decomp-10] removed 50 variables
c [simpleprobe-3] 758 variables remain 8% (8615 retained)
c [simpleprobe-3] removed 50 variables, found 287 hbrs, 0 units
c [cgrclsr-3] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-3] all 9373 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 4 variables
c [lift-3] limit 500000 with penalty 0 = 0 + 0
c [lift-3] using 6430 probes 69%
c [lift-3] 2 units, 12 impls, 2 eqs in 1 rounds
c [lift-3] 8892 variables remain 95% (473 retained)
c [lift-3] removed 4 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 6, lifted 2
c [unhide-5] limit 142647 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 94 tauts, 0 hbrs, 2111 literals
c [transred-3] limit 713237 with penalty 0 = 0 + 0
c [transred-3] removed 480 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 9357 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 11 blocked clauses
c [block-3] 11 < 1/1000 * 58991 = 58 considered unsuccessful
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 2 clauses out of 367 (1%) of length 11
c [cce-4-1] eliminated 6 clauses out of 291 (2%) of length 10
c [cce-4-1] eliminated 12 clauses out of 659 (2%) of length 9
c [cce-4-1] eliminated 16 clauses out of 1333 (1%) of length 8
c [cce-4-1] eliminated 17 clauses out of 2617 (1%) of length 7
c [cce-4-1] eliminated 88 clauses out of 3862 (2%) of length 6
c [cce-4-1] eliminated 53 clauses out of 4837 (1%) of length 5
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 194 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 33778 clauses = 28282 binary + 5496 ternary
c [cce-4] tried to eliminate 5975 small clauses 18%
c [cce-4] eliminated 279 small clauses 1%
c [cce-4] eliminated 211 binary clauses 1%
c [cce-4] eliminated 68 ternary clauses 1%
c [cce-4-1] eliminated 279 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 473 covered clauses in round 1
c [cce-4] eliminated 473 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 9357 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 96 variables 1% in round 1 in 15957115 steps
c [elim-5-1] backward subsumption/strengthening limit 4042885
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 3323564 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 96 = 1% variables out of 9357
c [bca-4] limit of 10000000 steps
c [bca-4] 10657 out of 18524 literals actually usable 58%
c [bca-4] added 20 blocked clauses in 38047 steps
c [simplification-5] removed 212 variables 2.2% (9261 remain 18%)
c [simplification-5] removed 1443 irredundant clauses 2.4% (58172 remain 28%)
c [simplification-5] maximum reduction of 2% = max (2%, 2%)
c [simplification-5] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-5] new conflict interval 32000
c [simplification-5] penalized conflict interval 32000 = 1 * 32000
c [simplification-5] new conflict limit 62345
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   22.1    9261    58172     36655   10497   3884 14709   9  8.9  80.4    7
c i   22.2    9260    58172     38372   12029   3916 14720   7  9.4  80.6    8
c -   22.8    9245    58172     43770   11938   4054 14752   7  9.3  79.0    7
c i   22.8    9244    58172     43829   11990   4057 14753   7  9.3  78.9    8
c i   22.8    9238    58172     43862   12016   4058 14754   7  9.3  78.9    8
c -   23.5    9229    58172     51581   13420   4193 14786   8  9.5  77.5    8
c R   24.0    9229    58172     57483   18319   4239 14796   7  9.9  76.4    9
c -   24.3    9229    58172     59768   14431   4282 14810   8  9.9  75.7    8
c i   24.4    9228    58172     60527   15121   4297 14813   8  9.8  75.4    8
c 
c [simplification-6] limit of 62687 conflicts hit after 62689 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 9213 free variables schedulable
c [ternres-4] 663 ternary resolvents (8 bin, 655 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1091 at-most-one constraints of average size 3.0
c [card-3] found 59 at-most-two constraints of average size 4.1
c [card-3] using previous limit 500000 for elimination
c [card-3] 1150 out of 1150 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 2231 xors of average arity 2.9
c [gauss-3] connected 6473 occurrences of 532 variables (average 12.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 45 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 18336 literals 100%
c [treelook-3] scheduling used 265956 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 301167 steps
c [treelook-3] 18141 literals remain 99%
c [treelook-3] 9168 variables remain to probed next time 100%
c [decomp-12] removed 5 variables
c [treelook-3] removed 5 variables, found 259 hbrs
c [cgrclsr-4] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-4] all 9163 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [cgrclsr-4] removed 4 variables
c [lift-4] limit 913184 with penalty 0 = 0 + 0
c [lift-4] using 6285 probes 69%
c [lift-4] 6 units, 20 impls, 3 eqs in 1 rounds
c [lift-4] 8363 variables remain 91% (779 retained)
c [lift-4] removed 17 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 10, lifted 9
c [transred-4] limit 1521974 with penalty 0 = 0 + 0
c [transred-4] removed 1240 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 329 (0%) of length 11
c [cce-5-1] eliminated 7 clauses out of 264 (3%) of length 10
c [cce-5-1] eliminated 19 clauses out of 617 (3%) of length 9
c [cce-5-1] eliminated 36 clauses out of 1275 (3%) of length 8
c [cce-5-1] eliminated 34 clauses out of 2632 (1%) of length 7
c [cce-5-1] eliminated 52 clauses out of 3742 (1%) of length 6
c [cce-5-1] eliminated 156 clauses out of 4729 (3%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 305 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 32677 clauses = 27366 binary + 5311 ternary
c [cce-5] tried to eliminate 6257 small clauses 19%
c [cce-5] eliminated 279 small clauses 1%
c [cce-5] eliminated 223 binary clauses 1%
c [cce-5] eliminated 56 ternary clauses 1%
c [cce-5-1] eliminated 421 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 726 covered clauses in round 1
c [cce-5] eliminated 726 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 9121 variables 100%
c [elim-6] limit of 30439481 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 105 variables 1% in round 1 in 12705072 steps
c [elim-6-1] backward subsumption/strengthening limit 17734409
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 3193205 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 105 = 1% variables out of 9121
c [bca-5] limit of 10000000 steps
c [bca-5] 9169 out of 18034 literals actually usable 51%
c [bca-5] added 7 blocked clauses in 40729 steps
c [rephase-2] after 62689 conflicts (new increment 40000, next 102689)
c [flushphases] 0 phases reset
c [simplification-6] removed 197 variables 2.1% (9016 remain 18%)
c [simplification-6] removed 1735 irredundant clauses 3.0% (56437 remain 27%)
c [simplification-6] maximum reduction of 3% = max (2%, 3%)
c [simplification-6] geometric conflict interval increment 8000 = 32000 / 4
c [simplification-6] new conflict interval 40000
c [simplification-6] penalized conflict interval 40000 = 1 * 40000
c [simplification-6] new conflict limit 102689
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   27.5    9016    56437     69230   15716   4732 14711  10  9.9  73.6    8
c i   28.4    9015    56437     77616   23308   4893 14747   7  9.9  71.6    9
c i   28.4    9010    56437     77667   23349   4896 14748   7  9.9  71.5    9
c -   28.5    9010    56437     78819   17396   4911 14755   8  9.9  71.2    8
c -   29.5    9010    56437     88965   19097   5025 14778   9  9.9  70.4    8
c -   30.7    9010    56437     99721   20830   5173 14816   7 10.0  68.8    8
c 
c [simplification-7] limit of 102997 conflicts hit after 102998 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 9010 free variables schedulable
c [ternres-5] 895 ternary resolvents (15 bin, 880 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-13] removed 48 variables
c [basicprobe-3] limit 2618477 penalty 0 = 0 + 0
c [basicprobe-3-0] 2040 probes remain 23% after last round
c [basicprobe-3-0] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 16 variables, found 892 hbrs
c [bate-2] eliminated 15 asymmetric tautologies during probing
c [cgrclsr-5] limit 261847 penalty 0 = 0 + 0
c [cgrclsr-5] all 8952 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [cgrclsr-5] removed 5 variables
c [lift-5] limit 1571086 with penalty 0 = 0 + 0
c [lift-5] using 5930 probes 66%
c [lift-5] 8 units, 33 impls, 7 eqs in 1 rounds
c [lift-5] 7742 variables remain 87% (1190 retained)
c [lift-5] removed 15 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 5, lifted 4
c [unhide-6] limit 261847 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 0 failed, 1581 tauts, 0 hbrs, 12238 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 774 transitive binary clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 325 (0%) of length 11
c [cce-6-1] eliminated 4 clauses out of 256 (2%) of length 10
c [cce-6-1] eliminated 19 clauses out of 595 (3%) of length 9
c [cce-6-1] eliminated 17 clauses out of 1031 (2%) of length 8
c [cce-6-1] eliminated 28 clauses out of 2642 (1%) of length 7
c [cce-6-1] eliminated 47 clauses out of 3731 (1%) of length 6
c [cce-6-1] eliminated 72 clauses out of 4505 (2%) of length 5
c [cce-6-1] eliminated 3 clauses out of 6195 (0%) of length 4
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 191 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 31433 clauses = 26614 binary + 4819 ternary
c [cce-6] tried to eliminate 6621 small clauses 21%
c [cce-6] eliminated 291 small clauses 1%
c [cce-6] eliminated 245 binary clauses 1%
c [cce-6] eliminated 46 ternary clauses 1%
c [cce-6-1] eliminated 291 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 482 covered clauses in round 1
c [cce-6] eliminated 482 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 8923 variables 100%
c [elim-7] limit of 52369542 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 154 variables 2% in round 1 in 15186174 steps
c [elim-7-1] backward subsumption/strengthening limit 30372348
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 3118236 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 154 = 2% variables out of 8923
c [bca-6] limit of 10000000 steps
c [bca-6] 8470 out of 17540 literals actually usable 48%
c [bca-6] added 28 blocked clauses in 44789 steps
c [rephase-3] after 102998 conflicts (new increment 80000, next 182998)
c [flushphases] 0 phases reset
c [simplification-7] removed 241 variables 2.7% (8769 remain 17%)
c [simplification-7] removed 1328 irredundant clauses 2.4% (55109 remain 26%)
c [simplification-7] maximum reduction of 3% = max (3%, 2%)
c [simplification-7] geometric conflict interval increment 10000 = 40000 / 4
c [simplification-7] new conflict interval 50000
c [simplification-7] penalized conflict interval 50000 = 1 * 50000
c [simplification-7] new conflict limit 152998
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.2    8769    55109    112091   21772   5655 14074   9 10.2  68.4    9
c -   35.2    8769    55109    123643   22772   5710 14087   7 10.7  69.0    9
c R   35.3    8769    55109    125492   24279   5721 14089   8 10.8  68.9   13
c -   36.6    8769    55109    136063   24500   5847 14113   9 10.7  67.4    9
c i   37.1    8768    55109    141200   29251   5904 14132   7 10.6  67.0   10
c -   38.0    8768    55109    149047   26414   5975 14157   8 10.7  66.4    9
c 
c [simplification-8] limit of 153200 conflicts hit after 153201 conflicts
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 8768 free variables schedulable
c [ternres-6] 526 ternary resolvents (4 bin, 522 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 1327 xors of average arity 3.0
c [gauss-4] connected 3915 occurrences of 452 variables (average 8.7)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 20 variables
c [simpleprobe-4] 676 schedulable variables 8%
c [simpleprobe-4] limit 15890411 penalty 0 = 0 + 0
c [decomp-15] removed 285 variables
c [simpleprobe-4] 444 variables remain 5% (8019 retained)
c [simpleprobe-4] removed 285 variables, found 3147 hbrs, 12 units
c [cgrclsr-6] limit 397260 penalty 0 = 0 + 0
c [cgrclsr-6] all 8463 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 1 variables
c [lift-6] limit 2383561 with penalty 0 = 0 + 0
c [lift-6] using 5441 probes 64%
c [lift-6] 1 units, 45 impls, 6 eqs in 1 rounds
c [lift-6] 6672 variables remain 79% (1783 retained)
c [lift-6] removed 7 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 8, lifted 1
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1999 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8439 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 21 blocked clauses
c [block-4] 21 < 1/1000 * 53439 = 53 considered unsuccessful
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 311 (1%) of length 11
c [cce-7-1] eliminated 5 clauses out of 242 (2%) of length 10
c [cce-7-1] eliminated 29 clauses out of 568 (5%) of length 9
c [cce-7-1] eliminated 10 clauses out of 975 (1%) of length 8
c [cce-7-1] eliminated 12 clauses out of 2552 (0%) of length 7
c [cce-7-1] eliminated 45 clauses out of 3637 (1%) of length 6
c [cce-7-1] eliminated 54 clauses out of 4403 (1%) of length 5
c [cce-7-1] eliminated 22 clauses out of 6146 (0%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 179 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 29350 clauses = 24624 binary + 4726 ternary
c [cce-7] tried to eliminate 6778 small clauses 23%
c [cce-7] eliminated 205 small clauses 1%
c [cce-7] eliminated 173 binary clauses 1%
c [cce-7] eliminated 32 ternary clauses 1%
c [cce-7-1] eliminated 205 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 384 covered clauses in round 1
c [cce-7] eliminated 384 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8439 variables 100%
c [elim-8] limit of 79452059 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 67 variables 1% in round 1 in 11782300 steps
c [elim-8-1] backward subsumption/strengthening limit 23564600
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 2890910 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 67 = 1% variables out of 8439
c [bca-7] limit of 10000000 steps
c [bca-7] 7793 out of 16746 literals actually usable 47%
c [bca-7] added 8 blocked clauses in 50376 steps
c [simplification-8] removed 396 variables 4.5% (8372 remain 17%)
c [simplification-8] removed 2352 irredundant clauses 4.3% (52757 remain 25%)
c [simplification-8] maximum reduction of 5% = max (5%, 4%)
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 155201
c 
c [simplification-9] limit of 155209 conflicts hit after 155209 conflicts
c [ternres-7] limit 4036383 with penalty 0 = 0 + 0
c [ternres-7] all 8372 free variables schedulable
c [ternres-7] 283 ternary resolvents (7 bin, 276 trn)
c [ternres-7] 7863 variables remain 94% (509 retained)
c [decomp-16] removed 7 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 16730 literals 100%
c [treelook-4] scheduling used 286815 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 301912 steps
c [treelook-4] 16527 literals remain 99%
c [treelook-4] 8365 variables remain to probed next time 100%
c [treelook-4] removed 0 variables, found 59 hbrs
c [cgrclsr-7] limit 403638 penalty 0 = 0 + 0
c [cgrclsr-7] all 8365 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [cgrclsr-7] removed 3 variables
c [lift-7] limit 2421829 with penalty 0 = 0 + 0
c [lift-7] using 4728 probes 57%
c [lift-7] 1 units, 41 impls, 6 eqs in 1 rounds
c [lift-7] 5934 variables remain 71% (2421 retained)
c [lift-7] removed 7 variables
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 2, lifted 0
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1173 transitive binary clauses
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 309 (1%) of length 11
c [cce-8-1] eliminated 2 clauses out of 238 (1%) of length 10
c [cce-8-1] eliminated 5 clauses out of 542 (1%) of length 9
c [cce-8-1] eliminated 3 clauses out of 848 (0%) of length 8
c [cce-8-1] eliminated 8 clauses out of 2589 (0%) of length 7
c [cce-8-1] eliminated 16 clauses out of 3662 (0%) of length 6
c [cce-8-1] eliminated 30 clauses out of 4347 (1%) of length 5
c [cce-8-1] eliminated 7 clauses out of 6156 (0%) of length 4
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 73 large clauses in 30000001 steps
c [cce-8-1] allowing another 15000000 steps for small clauses
c [cce-8] scheduling 28907 clauses = 24242 binary + 4665 ternary
c [cce-8] tried to eliminate 7031 small clauses 24%
c [cce-8] eliminated 174 small clauses 1%
c [cce-8] eliminated 143 binary clauses 1%
c [cce-8] eliminated 31 ternary clauses 1%
c [cce-8-1] eliminated 189 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 262 covered clauses in round 1
c [cce-8] eliminated 262 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8353 variables 100%
c [elim-9] limit of 80727666 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 38 variables 0% in round 1 in 11455073 steps
c [elim-9-1] backward subsumption/strengthening limit 22910146
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 2866306 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 38 = 0% variables out of 8353
c [bca-8] limit of 10000000 steps
c [bca-8] 7704 out of 16632 literals actually usable 46%
c [bca-8] added 8 blocked clauses in 51158 steps
c [simplification-9] removed 57 variables 0.7% (8315 remain 16%)
c [simplification-9] removed 399 irredundant clauses 0.8% (52358 remain 25%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 25000 = 50000 / 2
c [simplification-9] new conflict interval 75000
c [simplification-9] penalized conflict interval 75000 = 1 * 75000
c [simplification-9] new conflict limit 230209
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   44.0    8315    52358    163714   27300   6557 14612   9 10.8  65.2    9
c -   45.5    8315    52358    177679   29079   6693 14628  10 10.9  64.1   13
c -   47.1    8315    52358    192017   30231   6781 14643   7 11.1  63.1   13
c -   48.8    8315    52358    207097   31839   6913 14666   8 11.2  62.0    9
c -   50.6    8315    52358    222647   33277   7028 14684   9 11.3  61.2   13
c 
c [simplification-10] limit of 230395 conflicts hit after 230397 conflicts
c [ternres-8] limit 6457855 with penalty 0 = 0 + 0
c [ternres-8] 7814 schedulable variables 94%
c [ternres-8] 1916 ternary resolvents (22 bin, 1894 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 403615 penalty 3 = 3 + 0
c [card-4] found 1236 at-most-one constraints of average size 3.0
c [card-4] found 83 at-most-two constraints of average size 4.0
c [card-4] using previous limit 403615 for elimination
c [card-4] 1318 out of 1319 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-18] removed 4 variables
c [basicprobe-4] limit 6457855 penalty 0 = 0 + 0
c [basicprobe-4-0] 1793 sched 22%, 7 failed, 0 lifted, 572 hbrs
c [decomp-19] removed 9 variables
c [basicprobe-4-1] 2085 probes remain 25% after last round
c [basicprobe-4-1] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-4-1] removed 12 variables, found 912 hbrs
c [bate-3] eliminated 10 asymmetric tautologies during probing
c [cgrclsr-8] limit 645785 penalty 0 = 0 + 0
c [cgrclsr-8] all 8299 free variables schedulable
c [cgrclsr-8] fully completed congruence closure
c [cgrclsr-8] removed 5 variables
c [lift-8] limit 3874713 with penalty 0 = 0 + 0
c [lift-8] using 4106 probes 50%
c [lift-8] 0 units, 65 impls, 8 eqs in 1 rounds
c [lift-8] 4925 variables remain 59% (3361 retained)
c [lift-8] removed 8 variables
c [cliff-8] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-8] failed 2, lifted 0
c [unhide-7] limit 322892 with penalty 2 = 2 + 0
c [unhide-7-7] 0 units, 0 failed, 111 tauts, 0 hbrs, 17459 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 935 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 3 clauses out of 37 (8%) of length 12
c [cce-9-1] eliminated 1 clauses out of 305 (0%) of length 11
c [cce-9-1] eliminated 8 clauses out of 239 (3%) of length 10
c [cce-9-1] eliminated 10 clauses out of 535 (2%) of length 9
c [cce-9-1] eliminated 14 clauses out of 834 (2%) of length 8
c [cce-9-1] eliminated 13 clauses out of 2556 (1%) of length 7
c [cce-9-1] eliminated 32 clauses out of 3604 (1%) of length 6
c [cce-9-1] eliminated 25 clauses out of 4274 (1%) of length 5
c [cce-9-1] eliminated 10 clauses out of 6139 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 116 large clauses in 30000001 steps
c [cce-9-1] allowing another 15000000 steps for small clauses
c [cce-9] scheduling 28553 clauses = 23928 binary + 4625 ternary
c [cce-9] tried to eliminate 5808 small clauses 20%
c [cce-9] eliminated 157 small clauses 1%
c [cce-9] eliminated 144 binary clauses 1%
c [cce-9] eliminated 13 ternary clauses 0%
c [cce-9-1] eliminated 157 small clauses in 30000001 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 273 covered clauses in round 1
c [cce-9] eliminated 273 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8284 variables 100%
c [elim-10] limit of 129157106 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 78 variables 1% in round 1 in 11488084 steps
c [elim-10-1] backward subsumption/strengthening limit 22976168
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 2798219 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 78 = 1% variables out of 8284
c [bca-9] limit of 10000000 steps
c [bca-9] 7419 out of 16414 literals actually usable 45%
c [bca-9] added 10 blocked clauses in 58155 steps
c [rephase-4] after 230397 conflicts (new increment 160000, next 390397)
c [flushphases] 0 phases reset
c [simplification-10] removed 109 variables 1.3% (8206 remain 16%)
c [simplification-10] removed 637 irredundant clauses 1.2% (51721 remain 25%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 37500 = 75000 / 2
c [simplification-10] new conflict interval 112500
c [simplification-10] penalized conflict interval 112500 = 1 * 112500
c [simplification-10] new conflict limit 342897
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   55.4    8206    51721    241610   34190   8861 14545   6 11.4  60.3   10
c -   57.3    8206    51721    259560   35372   8925 14561   8 12.1  59.9   15
c R   58.8    8206    51721    271987   45251   8954 14565  11 12.7  60.0   20
c -   59.6    8206    51721    277959   36631   9003 14570   7 12.7  59.5   11
c -   61.9    8206    51721    296397   38480   9175 14584   9 12.8  58.7   11
c -   64.4    8206    51721    314520   39838   9310 14599   8 12.9  58.0   11
c -   66.6    8206    51721    333724   41395   9473 14621   8 12.9  57.7   11
c 
c [simplification-11] limit of 343051 conflicts hit after 343057 conflicts
c [ternres-9] limit 10488444 with penalty 0 = 0 + 0
c [ternres-9] all 8206 free variables schedulable
c [ternres-9] 4217 ternary resolvents (42 bin, 4175 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 524422 penalty 2 = 2 + 0
c [gauss-5] extracted 492 xors of average arity 3.0
c [gauss-5] connected 1467 occurrences of 381 variables (average 3.9)
c [gauss-5] limit 524422 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 9 variables
c [simpleprobe-5] 424 schedulable variables 5%
c [simpleprobe-5] limit 41953776 penalty 0 = 0 + 0
c [decomp-21] removed 29 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 29 variables, found 2191 hbrs, 4 units
c [cgrclsr-9] limit 1048844 penalty 0 = 0 + 0
c [cgrclsr-9] all 8168 free variables schedulable
c [cgrclsr-9] fully completed congruence closure
c [cgrclsr-9] removed 1 variables
c [lift-9] limit 6293066 with penalty 0 = 0 + 0
c [lift-9] using 3232 probes 40%
c [lift-9] 6 units, 91 impls, 12 eqs in 1 rounds
c [lift-9] 3606 variables remain 44% (4543 retained)
c [lift-9] removed 18 variables
c [cliff-9] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-9] failed 11, lifted 2
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1426 transitive binary clauses
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 12 clauses out of 321 (4%) of length 11
c [cce-10-1] eliminated 8 clauses out of 229 (3%) of length 10
c [cce-10-1] eliminated 21 clauses out of 544 (4%) of length 9
c [cce-10-1] eliminated 3 clauses out of 805 (0%) of length 8
c [cce-10-1] eliminated 22 clauses out of 2493 (1%) of length 7
c [cce-10-1] eliminated 29 clauses out of 3571 (1%) of length 6
c [cce-10-1] eliminated 51 clauses out of 4240 (1%) of length 5
c [cce-10-1] eliminated 3 clauses out of 6142 (0%) of length 4
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 149 large clauses in 30000001 steps
c [cce-10-1] allowing another 15000000 steps for small clauses
c [cce-10] scheduling 27962 clauses = 23415 binary + 4547 ternary
c [cce-10] tried to eliminate 6489 small clauses 23%
c [cce-10] eliminated 167 small clauses 1%
c [cce-10] eliminated 146 binary clauses 1%
c [cce-10] eliminated 21 ternary clauses 0%
c [cce-10-1] eliminated 262 small clauses in 30000001 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 411 covered clauses in round 1
c [cce-10] eliminated 411 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8136 variables 100%
c [elim-11] limit of 209768882 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 62 variables 1% in round 1 in 13445570 steps
c [elim-11-1] backward subsumption/strengthening limit 26891140
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 2739055 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 62 = 1% variables out of 8136
c [bca-10] limit of 10000000 steps
c [bca-10] 5905 out of 16150 literals actually usable 37%
c [bca-10] added 11 blocked clauses in 63881 steps
c [simplification-11] removed 132 variables 1.6% (8074 remain 16%)
c [simplification-11] removed 833 irredundant clauses 1.6% (50888 remain 24%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 37500 = 112500 / 3
c [simplification-11] new conflict interval 150000
c [simplification-11] penalized conflict interval 150000 = 1 * 150000
c [simplification-11] new conflict limit 493057
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   71.9    8074    50888    355253   42740  13193 15862  12 13.0  57.0   12
c -   74.8    8074    50888    375028   44400  13338 15879   8 13.1  56.5   12
c -   77.6    8074    50888    397779   45862  13415 15891   9 13.6  56.4   12
c -   80.8    8074    50888    418702   47332  13552 15904   8 13.6  55.6   12
c -   84.1    8074    50888    440994   49044  13692 15918   9 13.8  54.9   12
c -   87.7    8074    50888    463837   50374  13810 15927   7 14.0  54.6   18
c -   91.2    8074    50888    486369   51917  13927 15936   8 14.0  54.1   12
c 
c [simplification-12] limit of 493193 conflicts hit after 493194 conflicts
c [ternres-10] limit 17625268 with penalty 0 = 0 + 0
c [ternres-10] all 8074 free variables schedulable
c [ternres-10] 1434 ternary resolvents (13 bin, 1421 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-22] removed 6 variables
c [cgrclsr-10] limit 1762526 penalty 0 = 0 + 0
c [cgrclsr-10] all 8068 free variables schedulable
c [cgrclsr-10] fully completed congruence closure
c [cgrclsr-10] removed 20 variables
c [lift-10] limit 10575161 with penalty 0 = 0 + 0
c [lift-10] using 2014 probes 25%
c [lift-10] 19 units, 160 impls, 13 eqs in 1 rounds
c [lift-10] 1733 variables remain 22% (6282 retained)
c [lift-10] removed 33 variables
c [cliff-10] limit of 14100214 steps penalty 0 = 0 + 0
c [cliff-10] failed 4, lifted 6
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1136 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 8005 variables 100%
c [block-5] limit of 22031585 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2 blocked clauses
c [block-5] 2 < 1/1000 * 50554 = 50 considered unsuccessful
c [cce-11] limit of 35250537 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 4 clauses out of 312 (1%) of length 11
c [cce-11-1] eliminated 2 clauses out of 212 (1%) of length 10
c [cce-11-1] eliminated 7 clauses out of 530 (1%) of length 9
c [cce-11-1] eliminated 4 clauses out of 796 (1%) of length 8
c [cce-11-1] eliminated 40 clauses out of 2433 (2%) of length 7
c [cce-11-1] eliminated 40 clauses out of 3490 (1%) of length 6
c [cce-11-1] eliminated 44 clauses out of 4177 (1%) of length 5
c [cce-11-1] eliminated 95 clauses out of 6156 (2%) of length 4
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 236 large clauses in 35250538 steps
c [cce-11-1] allowing another 17625269 steps for small clauses
c [cce-11] scheduling 27893 clauses = 22902 binary + 4991 ternary
c [cce-11] tried to eliminate 7914 small clauses 28%
c [cce-11] eliminated 302 small clauses 1%
c [cce-11] eliminated 221 binary clauses 1%
c [cce-11] eliminated 81 ternary clauses 2%
c [cce-11-1] eliminated 302 small clauses in 35250538 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 538 covered clauses in round 1
c [cce-11] eliminated 538 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8005 variables 100%
c [elim-12] limit of 352505374 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 80 variables 1% in round 1 in 11155400 steps
c [elim-12-1] backward subsumption/strengthening limit 22310800
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 2672690 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 80 = 1% variables out of 8005
c [bca-11] limit of 10000000 steps
c [bca-11] 5097 out of 15852 literals actually usable 32%
c [bca-11] added 15 blocked clauses in 68979 steps
c [rephase-5] after 493194 conflicts (new increment 320000, next 813194)
c [flushphases] 0 phases reset
c [simplification-12] removed 149 variables 1.8% (7925 remain 16%)
c [simplification-12] removed 1156 irredundant clauses 2.3% (49732 remain 24%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 50000 = 150000 / 3
c [simplification-12] new conflict interval 200000
c [simplification-12] penalized conflict interval 200000 = 1 * 200000
c [simplification-12] new conflict limit 693194
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   97.8    7925    49732    511913   52589  14423 16513  10 14.1  53.6   14
c -  102.5    7925    49732    542172   53794  14502 16525  10 15.3  54.0   13
c -  107.6    7925    49732    575145   55172  14589 16538  10 16.3  54.3   13
c R  109.3    7925    49732    585720   62519  14614 16540  13 16.6  54.3   19
c -  112.2    7925    49732    602187   56466  14693 16548   7 16.5  53.8   14
c -  116.6    7925    49732    627795   57960  14839 16557   7 16.5  53.3   14
c -  121.4    7925    49732    655147   59863  14976 16574  17 16.6  53.0   14
c -  126.2    7925    49732    682188   61073  15102 16584   9 16.5  52.4   14
c 
c [simplification-13] limit of 693328 conflicts hit after 693328 conflicts
c [ternres-11] limit 29311278 with penalty 0 = 0 + 0
c [ternres-11] all 7925 free variables schedulable
c [ternres-11] 11852 ternary resolvents (74 bin, 11778 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-23] removed 7 variables
c [treelook-5] limit 732781 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 15836 literals 100%
c [treelook-5] scheduling used 428088 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 732781 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 735652 steps
c [treelook-5] 15643 literals remain 99%
c [treelook-5] 7918 variables remain to probed next time 100%
c [decomp-24] removed 11 variables
c [treelook-5] removed 11 variables, found 269 hbrs
c [cgrclsr-11] limit 2931127 penalty 0 = 0 + 0
c [cgrclsr-11] all 7907 free variables schedulable
c [cgrclsr-11] fully completed congruence closure
c [cgrclsr-11] removed 7 variables
c [lift-11] limit 17586766 with penalty 0 = 0 + 0
c [lift-11] using 277 probes 4%
c [lift-11-1] found 4 units 33 impls in round 1
c [lift-11-2] found 0 units 20 impls in round 2
c [lift-11-3] found 2 units 27 impls in round 3
c [lift-11-4] found 0 units 22 impls in round 4
c [lift-11-5] found 0 units 17 impls in round 5
c [lift-11] 6 units, 119 impls, 11 eqs in 6 rounds
c [lift-11] 1417 variables remain 18% (6466 retained)
c [lift-11] removed 17 variables
c [cliff-11] limit of 23449022 steps penalty 0 = 0 + 0
c [cliff-11] failed 5, lifted 0
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1100 transitive binary clauses
c [cce-12] limit of 58622556 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 306 (0%) of length 11
c [cce-12-1] eliminated 5 clauses out of 210 (2%) of length 10
c [cce-12-1] eliminated 29 clauses out of 537 (5%) of length 9
c [cce-12-1] eliminated 4 clauses out of 806 (0%) of length 8
c [cce-12-1] eliminated 35 clauses out of 2319 (2%) of length 7
c [cce-12-1] eliminated 37 clauses out of 3480 (1%) of length 6
c [cce-12-1] eliminated 41 clauses out of 4123 (1%) of length 5
c [cce-12-1] eliminated 411 clauses out of 6112 (7%) of length 4
c [cce-12-1] completed large round (ACCE)
c [cce-12-1] eliminated 563 large clauses in 41449964 steps
c [cce-12-1] allowing another 20724982 steps for small clauses
c [cce-12] scheduling 27296 clauses = 22448 binary + 4848 ternary
c [cce-12] tried to eliminate 16616 small clauses 61%
c [cce-12] eliminated 632 small clauses 2%
c [cce-12] eliminated 495 binary clauses 2%
c [cce-12] eliminated 137 ternary clauses 3%
c [cce-12-1] eliminated 663 small clauses in 58622557 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 1226 covered clauses in round 1
c [cce-12] eliminated 1226 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7878 variables 100%
c [elim-13] limit of 586225566 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 102 variables 1% in round 1 in 10847882 steps
c [elim-13-1] backward subsumption/strengthening limit 21695764
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 2549811 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 102 = 1% variables out of 7878
c [bca-12] limit of 10000000 steps
c [bca-12] 4214 out of 15554 literals actually usable 27%
c [bca-12] added 16 blocked clauses in 79424 steps
c [simplification-13] removed 149 variables 1.9% (7776 remain 15%)
c [simplification-13] removed 1602 irredundant clauses 3.2% (48130 remain 23%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 50000 = 200000 / 4
c [simplification-13] new conflict interval 250000
c [simplification-13] penalized conflict interval 250000 = 1 * 250000
c [simplification-13] new conflict limit 943328
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  134.9    7776    48130    711393   61658  26332 18163   8 16.5  52.0   16
c -  140.2    7776    48130    738969   63234  26475 18173   7 16.4  51.5   15
c -  146.1    7776    48130    766910   64624  26584 18179   5 16.3  50.9   15
c -  152.2    7776    48130    795900   66131  26676 18186   9 16.3  50.4   15
c -  158.7    7776    48130    824822   67237  26742 18193   8 16.2  49.8   15
c -  164.6    7776    48130    855366   68296  26793 18195   8 16.2  49.5   15
c i  171.3    7775    48130    884451   93641  26869 18208   9 16.1  48.8   24
c -  171.9    7524    48130    886701   69592  26892 18210   9 16.1  48.8   23
c i  174.1    7523    48130    897965   79938  26995 18239   8 16.1  48.8   19
c i  178.4    7519    48130    917628   97626  27135 18287   8 16.0  48.8   25
c -  179.0    7519    48130    919721   73027  27164 18296   8 16.0  48.8   17
c i  181.4    7518    48130    931838   84132  27285 18322   8 16.0  48.7   21
c i  182.4    7517    48130    935893   87838  27329 18341   8 16.0  48.7   22
c i  182.7    7516    48130    937181   89060  27338 18347   9 16.0  48.7   22
c i  182.8    7515    48130    937611   89461  27341 18347   8 16.0  48.7   22
c i  183.9    7514    48130    943668   94726  27375 18358   9 16.0  48.7   24
c 
c [simplification-14] limit of 943838 conflicts hit after 943838 conflicts
c [ternres-12] limit 48564432 with penalty 0 = 0 + 0
c [ternres-12] all 7514 free variables schedulable
c [ternres-12] 1498 ternary resolvents (9 bin, 1489 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-25] removed 478 variables
c [basicprobe-5] limit 48564432 penalty 0 = 0 + 0
c [basicprobe-5-0] 1823 sched 25%, 17 failed, 0 lifted, 4519 hbrs
c [decomp-26] removed 26 variables
c [basicprobe-5-1] 3495 sched 48%, 16 failed, 0 lifted, 3315 hbrs
c [decomp-27] removed 20 variables
c [basicprobe-5-2] 3430 sched 47%, 3 failed, 0 lifted, 481 hbrs
c [decomp-28] removed 3 variables
c [basicprobe-5-3] 3428 sched 47%, 1 failed, 0 lifted, 235 hbrs
c [decomp-29] removed 2 variables
c [basicprobe-5-4] 679 probes remain 9% after last round
c [basicprobe-5-4] 38 units = 38 failed (100%) + 0 lifted (0%)
c [basicprobe-5-4] removed 52 variables, found 8641 hbrs
c [bate-4] eliminated 27 asymmetric tautologies during probing
c [cgrclsr-12] limit 4856443 penalty 0 = 0 + 0
c [cgrclsr-12] all 7246 free variables schedulable
c [cgrclsr-12] fully completed congruence closure
c [cgrclsr-12] removed 13 variables
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 171 probes 2%
c [lift-12-1] found 0 units 9 impls in round 1
c [lift-12-2] found 0 units 15 impls in round 2
c [lift-12-3] found 0 units 8 impls in round 3
c [lift-12-4] found 0 units 9 impls in round 4
c [lift-12-5] found 0 units 8 impls in round 5
c [lift-12] 0 units, 49 impls, 7 eqs in 6 rounds
c [lift-12] 1171 variables remain 16% (6055 retained)
c [lift-12] removed 7 variables
c [cliff-12] limit of 38851546 steps penalty 0 = 0 + 0
c [cliff-12] failed 0, lifted 0
c [unhide-8] limit 1214110 with penalty 3 = 3 + 0
c [unhide-8-8] 0 units, 0 failed, 8524 tauts, 0 hbrs, 162288 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1610 transitive binary clauses
c [cce-13] limit of 97128865 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-13-1] eliminated 8 clauses out of 237 (3%) of length 11
c [cce-13-1] eliminated 12 clauses out of 124 (10%) of length 10
c [cce-13-1] eliminated 36 clauses out of 500 (7%) of length 9
c [cce-13-1] eliminated 26 clauses out of 851 (3%) of length 8
c [cce-13-1] eliminated 54 clauses out of 1676 (3%) of length 7
c [cce-13-1] eliminated 97 clauses out of 3118 (3%) of length 6
c [cce-13-1] eliminated 133 clauses out of 3950 (3%) of length 5
c [cce-13-1] eliminated 246 clauses out of 5567 (4%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 613 large clauses in 19179016 steps
c [cce-13-1] allowing another 9589508 steps for small clauses
c [cce-13] scheduling 24285 clauses = 20487 binary + 3798 ternary
c [cce-13] tried to eliminate 24285 small clauses 100%
c [cce-13] eliminated 995 small clauses 4%
c [cce-13] eliminated 829 binary clauses 4%
c [cce-13] eliminated 166 ternary clauses 4%
c [cce-13-1] eliminated 995 small clauses in 42320682 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 1608 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 23290 clauses = 19658 binary + 3632 ternary
c [cce-13] tried to eliminate 23290 small clauses 100%
c [cce-13] eliminated 7 small clauses 0%
c [cce-13] eliminated 5 binary clauses 0%
c [cce-13] eliminated 2 ternary clauses 0%
c [cce-13-2] eliminated 7 small clauses in 30281481 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 7 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 0 steps for small clauses
c [cce-13] scheduling 23283 clauses = 19653 binary + 3630 ternary
c [cce-13] tried to eliminate 18880 small clauses 81%
c [cce-13-3] incomplete small round (ACCE)
c [cce-13-3] eliminated 0 covered clauses in round 3
c [cce-13] eliminated 1615 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 7226 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 470 variables 7% in round 1 in 8462331 steps
c [elim-14-1] backward subsumption/strengthening limit 16924662
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 1807527 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 470 = 7% variables out of 7226
c [bca-13] limit of 10000000 steps
c [bca-13] 3344 out of 13514 literals actually usable 25%
c [bca-13] added 45 blocked clauses in 64825 steps
c [rephase-6] after 943838 conflicts (new increment 640000, next 1583838)
c [flushphases] 0 phases reset
c [simplification-14] removed 758 variables 10.1% (6756 remain 13%)
c [simplification-14] removed 6583 irredundant clauses 13.7% (41547 remain 20%)
c [simplification-14] maximum reduction of 14% = max (10%, 14%)
c [simplification-14] large reduction 14% >= 5% limit
c [simplification-14] new conflict interval 9438 = min (943838/100, 250000)
c [simplification-14] penalized conflict interval 9438 = 1 * 9438
c [simplification-14] new conflict limit 953276
c 
c [simplification-15] limit of 953326 conflicts hit after 953326 conflicts
c [ternres-13] limit 49261584 with penalty 0 = 0 + 0
c [ternres-13] all 6756 free variables schedulable
c [ternres-13] 4687 ternary resolvents (39 bin, 4648 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1539424 penalty 4 = 4 + 0
c [card-5] found 1193 at-most-one constraints of average size 3.1
c [card-5] found 367 at-most-two constraints of average size 4.4
c [card-5] using previous limit 1539424 for elimination
c [card-5] 1559 out of 1560 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-6] limit 1231539 penalty 3 = 3 + 0
c [gauss-6] extracted 809 xors of average arity 3.0
c [gauss-6] connected 2399 occurrences of 337 variables (average 7.1)
c [gauss-6] limit 1231539 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 15 variables
c [simpleprobe-6] all 6741 free variables schedulable
c [simpleprobe-6] limit 197046337 penalty 0 = 0 + 0
c [decomp-31] removed 21 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 21 variables, found 8726 hbrs, 0 units
c [cgrclsr-13] limit 4926158 penalty 0 = 0 + 0
c [cgrclsr-13] all 6720 free variables schedulable
c [cgrclsr-13] fully completed congruence closure
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 143 probes 2%
c [lift-13-1] found 0 units 14 impls in round 1
c [lift-13-2] found 1 units 13 impls in round 2
c [lift-13-3] found 0 units 12 impls in round 3
c [lift-13-4] found 0 units 12 impls in round 4
c [lift-13-5] found 0 units 13 impls in round 5
c [lift-13] 1 units, 64 impls, 3 eqs in 6 rounds
c [lift-13] 903 variables remain 13% (5813 retained)
c [lift-13] removed 4 variables
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2912 transitive binary clauses
c [cce-14] limit of 98523168 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 10 clauses out of 247 (4%) of length 11
c [cce-14-1] eliminated 5 clauses out of 113 (4%) of length 10
c [cce-14-1] eliminated 30 clauses out of 484 (6%) of length 9
c [cce-14-1] eliminated 27 clauses out of 833 (3%) of length 8
c [cce-14-1] eliminated 34 clauses out of 1569 (2%) of length 7
c [cce-14-1] eliminated 53 clauses out of 3102 (2%) of length 6
c [cce-14-1] eliminated 65 clauses out of 3858 (2%) of length 5
c [cce-14-1] eliminated 121 clauses out of 5444 (2%) of length 4
c [cce-14-1] completed large round (ACCE)
c [cce-14-1] eliminated 345 large clauses in 19082335 steps
c [cce-14-1] allowing another 9541167 steps for small clauses
c [cce-14] scheduling 21727 clauses = 18135 binary + 3592 ternary
c [cce-14] tried to eliminate 21727 small clauses 100%
c [cce-14] eliminated 289 small clauses 1%
c [cce-14] eliminated 210 binary clauses 1%
c [cce-14] eliminated 79 ternary clauses 2%
c [cce-14-1] eliminated 289 small clauses in 39419167 steps
c [cce-14-1] completed small round (ACCE)
c [cce-14-1] eliminated 634 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 21438 clauses = 17925 binary + 3513 ternary
c [cce-14] tried to eliminate 21438 small clauses 100%
c [cce-14] eliminated 7 small clauses 0%
c [cce-14] eliminated 6 binary clauses 0%
c [cce-14] eliminated 1 ternary clauses 0%
c [cce-14-2] eliminated 7 small clauses in 29470590 steps
c [cce-14-2] completed small round (ACCE)
c [cce-14-2] eliminated 7 covered clauses in round 2
c [cce-14-3] completed large round (ACCE)
c [cce-14-3] allowing another 0 steps for small clauses
c [cce-14] scheduling 21431 clauses = 17919 binary + 3512 ternary
c [cce-14] tried to eliminate 21431 small clauses 100%
c [cce-14-3] completed small round (ACCE)
c [cce-14-3] eliminated 0 covered clauses in round 3
c [cce-14] eliminated 641 covered clauses in TOTAL during 3 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 6716 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 102 variables 2% in round 1 in 7092831 steps
c [elim-15-1] backward subsumption/strengthening limit 14185662
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 1746874 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 102 = 2% variables out of 6716
c [bca-14] limit of 10000000 steps
c [bca-14] 3007 out of 13230 literals actually usable 23%
c [bca-14] added 48 blocked clauses in 71588 steps
c [simplification-15] removed 142 variables 2.1% (6614 remain 13%)
c [simplification-15] removed 953 irredundant clauses 2.3% (40594 remain 19%)
c [simplification-15] maximum reduction of 2% = max (2%, 2%)
c [simplification-15] geometric conflict interval increment 83333 = 250000 / 3
c [simplification-15] new conflict interval 333333
c [simplification-15] penalized conflict interval 333333 = 1 * 333333
c [simplification-15] new conflict limit 1286659
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  202.9    6614    40594    979184   59468  22358 26103   9 16.0  48.5   15
c -  210.9    6614    40594   1013059   61800  22542 26159   9 16.1  48.2   15
c -  219.0    6614    40594   1047312   64222  22701 26194   8 16.1  47.9   15
c i  219.9    6613    40594   1051299   67938  22728 26204   9 16.1  47.8   18
c i  222.6    6612    40594   1061828   77722  22781 26219   9 16.0  47.7   20
c i  226.8    6611    40594   1077277   91494  22824 26234   8 16.0  47.6   24
c -  227.9    6611    40594   1081478   66619  22836 26241   8 16.1  47.6   16
c i  228.2    6610    40594   1082417   67502  22845 26245   8 16.1  47.6   17
c -  235.8    6610    40594   1118367   68551  22955 26287  14 16.3  47.6   16
c -  244.0    6610    40594   1156896   69945  23027 26293  12 16.5  47.5   16
c -  251.9    6610    40594   1195663   71133  23062 26302   8 16.7  47.5   23
c -  259.2    6610    40594   1230596   72343  23107 26307  12 16.7  47.3   18
c R  264.1    6610    40594   1254508   94245  23141 26309  11 16.7  47.1   27
c i  264.8    6609    40594   1256216   95850  23148 26311   9 16.7  47.1   27
c i  267.1    6605    40594   1262834  101869  23172 26322   9 16.7  47.0   33
c i  267.2    6604    40594   1262996  102024  23172 26322   9 16.7  47.0   33
c -  268.2    6604    40594   1266460   73927  23180 26324  12 16.7  47.0   18
c 
c [simplification-16] limit of 1287241 conflicts hit after 1287243 conflicts
c [ternres-14] limit 78920051 with penalty 0 = 0 + 0
c [ternres-14] all 6604 free variables schedulable
c [ternres-14] 3013 ternary resolvents (27 bin, 2986 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-32] removed 16 variables
c [treelook-6] limit 3946002 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 13196 literals 100%
c [treelook-6] scheduling used 469721 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3946002 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3947443 steps
c [treelook-6] 12547 literals remain 95%
c [treelook-6] 6593 variables remain to probed next time 100%
c [decomp-33] removed 6 variables
c [treelook-6] removed 8 variables, found 3910 hbrs
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 43 probes 1%
c [lift-14-1] found 2 units 4 impls in round 1
c [lift-14-2] found 0 units 5 impls in round 2
c [lift-14-3] found 1 units 6 impls in round 3
c [lift-14-4] found 1 units 1 impls in round 4
c [lift-14-5] found 0 units 5 impls in round 5
c [lift-14] 4 units, 21 impls, 1 eqs in 6 rounds
c [lift-14] 829 variables remain 13% (5756 retained)
c [lift-14] removed 5 variables
c [cliff-13] limit of 31568020 steps penalty 1 = 1 + 0
c [cliff-13] failed 11, lifted 6
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 2451 transitive binary clauses
c [transred-14] found 1 units
c [cce-15] limit of 157840103 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 3 clauses out of 3 (100%) of length 17
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 16
c [cce-15-1] eliminated 1 clauses out of 4 (25%) of length 15
c [cce-15-1] eliminated 2 clauses out of 6 (33%) of length 14
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-15-1] eliminated 4 clauses out of 102 (4%) of length 10
c [cce-15-1] eliminated 19 clauses out of 454 (4%) of length 9
c [cce-15-1] eliminated 16 clauses out of 808 (2%) of length 8
c [cce-15-1] eliminated 35 clauses out of 1494 (2%) of length 7
c [cce-15-1] eliminated 39 clauses out of 3001 (1%) of length 6
c [cce-15-1] eliminated 54 clauses out of 3773 (1%) of length 5
c [cce-15-1] eliminated 58 clauses out of 5377 (1%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 234 large clauses in 18964640 steps
c [cce-15-1] allowing another 9482320 steps for small clauses
c [cce-15] scheduling 21563 clauses = 17617 binary + 3946 ternary
c [cce-15] tried to eliminate 21563 small clauses 100%
c [cce-15] eliminated 358 small clauses 2%
c [cce-15] eliminated 193 binary clauses 1%
c [cce-15] eliminated 165 ternary clauses 4%
c [cce-15-1] eliminated 477 small clauses in 39123182 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 711 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 21205 clauses = 17424 binary + 3781 ternary
c [cce-15] tried to eliminate 21205 small clauses 100%
c [cce-15] eliminated 2 small clauses 0%
c [cce-15] eliminated 2 binary clauses 0%
c [cce-15-2] eliminated 2 small clauses in 29090644 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 2 covered clauses in round 2
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] allowing another 0 steps for small clauses
c [cce-15] scheduling 21203 clauses = 17422 binary + 3781 ternary
c [cce-15] tried to eliminate 21203 small clauses 100%
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 0 covered clauses in round 3
c [cce-15] eliminated 713 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 6567 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 72 variables 1% in round 1 in 6508860 steps
c [elim-16-1] backward subsumption/strengthening limit 13017720
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 1686382 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 72 = 1% variables out of 6567
c [bca-15] limit of 10000000 steps
c [bca-15] 2551 out of 12992 literals actually usable 20%
c [bca-15] added 16 blocked clauses in 94348 steps
c [simplification-16] removed 109 variables 1.7% (6495 remain 13%)
c [simplification-16] removed 1018 irredundant clauses 2.5% (39576 remain 19%)
c [simplification-16] maximum reduction of 3% = max (2%, 3%)
c [simplification-16] geometric conflict interval increment 83333 = 333333 / 4
c [simplification-16] new conflict interval 416666
c [simplification-16] penalized conflict interval 416666 = 1 * 416666
c [simplification-16] new conflict limit 1703909
c [tabula-rasa-2] number clauses 39576 drops below limit 39717
c [flush-cache] 0 binary, 0 ternary, 87747 large
c [flushphases] 6495 phases reset fully
c [phase-5] phase bias: 412 positive 40%, 627 negative 60%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] new conflict limit 1307243
c [tabula-rasa-2] new variable limit 1623 and clause limit 19788
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  279.2    6495    39576   1293236    3524  25419 30136   6 16.6  46.8   11
c -  279.7    6495    39576   1297466    4935  25494 30161  13 16.5  46.8   12
c -  280.2    6495    39576   1302072    6266  25556 30176   8 16.5  46.8   12
c -  280.8    6495    39576   1307105    7438  25593 30180  10 16.5  46.8   12
c 
c [simplification-17] limit of 1307359 conflicts hit after 1307359 conflicts
c [ternres-15] limit 79735307 with penalty 0 = 0 + 0
c [ternres-15] all 6495 free variables schedulable
c [ternres-15] 943 ternary resolvents (17 bin, 926 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-34] removed 9 variables
c [basicprobe-6] limit 79735307 penalty 0 = 0 + 0
c [basicprobe-6-0] 712 sched 11%, 2 failed, 0 lifted, 549 hbrs
c [decomp-35] removed 3 variables
c [basicprobe-6-1] 2837 sched 44%, 2 failed, 0 lifted, 1430 hbrs
c [decomp-36] removed 3 variables
c [basicprobe-6-2] 2820 sched 44%, 0 failed, 0 lifted, 195 hbrs
c [basicprobe-6-3] 2820 sched 44%, 0 failed, 0 lifted, 65 hbrs
c [basicprobe-6-4] 2823 sched 44%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-6-5] 2823 sched 44%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-6-6] 2823 sched 44%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-6-7] 2823 sched 44%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-6-8] 2823 sched 44%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-6-9] 2823 sched 44%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-6-9] round limit 9 hit
c [basicprobe-6-9] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-6-9] removed 6 variables, found 2328 hbrs
c [bate-5] eliminated 1 asymmetric tautologies during probing
c [cgrclsr-14] limit 3986765 penalty 1 = 1 + 0
c [cgrclsr-14] all 6480 free variables schedulable
c [cgrclsr-14] fully completed congruence closure
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 19 probes 0%
c [lift-15-1] found 0 units 0 impls in round 1
c [lift-15-2] found 0 units 2 impls in round 2
c [lift-15-3] found 0 units 1 impls in round 3
c [lift-15-4] found 0 units 1 impls in round 4
c [lift-15-5] found 0 units 3 impls in round 5
c [lift-15] 0 units, 7 impls, 0 eqs in 6 rounds
c [lift-15] 781 variables remain 12% (5699 retained)
c [cliff-14] limit of 63788245 steps penalty 0 = 0 + 0
c [cliff-14] failed 0, lifted 0
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1874 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 6480 variables 100%
c [block-6] limit of 49834566 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 159470614 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 4 clauses out of 244 (2%) of length 11
c [cce-16-1] eliminated 4 clauses out of 111 (4%) of length 10
c [cce-16-1] eliminated 11 clauses out of 439 (3%) of length 9
c [cce-16-1] eliminated 6 clauses out of 812 (1%) of length 8
c [cce-16-1] eliminated 10 clauses out of 1434 (1%) of length 7
c [cce-16-1] eliminated 12 clauses out of 2941 (0%) of length 6
c [cce-16-1] eliminated 18 clauses out of 3711 (0%) of length 5
c [cce-16-1] eliminated 46 clauses out of 5368 (1%) of length 4
c [cce-16-1] completed large round (ACCE)
c [cce-16-1] eliminated 111 large clauses in 18916389 steps
c [cce-16-1] allowing another 9458194 steps for small clauses
c [cce-16] scheduling 21032 clauses = 17276 binary + 3756 ternary
c [cce-16] tried to eliminate 21032 small clauses 100%
c [cce-16] eliminated 98 small clauses 0%
c [cce-16] eliminated 72 binary clauses 0%
c [cce-16] eliminated 26 ternary clauses 1%
c [cce-16-1] eliminated 98 small clauses in 39256233 steps
c [cce-16-1] completed small round (ACCE)
c [cce-16-1] eliminated 209 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 20934 clauses = 17204 binary + 3730 ternary
c [cce-16] tried to eliminate 20934 small clauses 100%
c [cce-16] eliminated 4 small clauses 0%
c [cce-16] eliminated 3 binary clauses 0%
c [cce-16] eliminated 1 ternary clauses 0%
c [cce-16-2] eliminated 4 small clauses in 29551741 steps
c [cce-16-2] completed small round (ACCE)
c [cce-16-2] eliminated 4 covered clauses in round 2
c [cce-16-3] completed large round (ACCE)
c [cce-16-3] allowing another 0 steps for small clauses
c [cce-16] scheduling 20930 clauses = 17201 binary + 3729 ternary
c [cce-16] tried to eliminate 20930 small clauses 100%
c [cce-16-3] completed small round (ACCE)
c [cce-16-3] eliminated 0 covered clauses in round 3
c [cce-16] eliminated 213 covered clauses in TOTAL during 3 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 6480 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 18 variables 0% in round 1 in 6381232 steps
c [elim-17-1] backward subsumption/strengthening limit 12762464
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 1666819 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 18 = 0% variables out of 6480
c [bca-16] limit of 10000000 steps
c [bca-16] 6471 out of 12926 literals actually usable 50%
c [bca-16] added 7 blocked clauses in 24428 steps
c [rephase-7] after 1307359 conflicts (new increment 20000, next 1327359)
c [flushphases] 1 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-17] removed 33 variables 0.5% (6462 remain 13%)
c [simplification-17] removed 293 irredundant clauses 0.7% (39283 remain 19%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-17] new conflict interval 30000
c [simplification-17] penalized conflict interval 30000 = 1 * 30000
c [simplification-17] new conflict limit 1337359
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  288.2    6462    39283   1313121    8218  26241 30802   9 16.5  46.8    9
c -  289.1    6462    39283   1319421    9602  26323 30815   9 16.5  46.8    9
c -  290.0    6462    39283   1326459   11229  26378 30828  11 16.5  46.8    9
c -  291.1    6462    39283   1333838   12643  26451 30841   9 16.4  46.7    9
c 
c [simplification-18] limit of 1337449 conflicts hit after 1337451 conflicts
c [ternres-16] limit 81188234 with penalty 0 = 0 + 0
c [ternres-16] all 6462 free variables schedulable
c [ternres-16] 769 ternary resolvents (14 bin, 755 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-44] removed 3 variables
c [simpleprobe-7] all 6459 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-45] removed 9 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 9 variables, found 6969 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 2872 transitive binary clauses
c [cce-17] limit of 162376469 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 6 clauses out of 425 (1%) of length 9
c [cce-17-1] eliminated 6 clauses out of 797 (1%) of length 8
c [cce-17-1] eliminated 1 clauses out of 1404 (0%) of length 7
c [cce-17-1] eliminated 7 clauses out of 2926 (0%) of length 6
c [cce-17-1] eliminated 7 clauses out of 3711 (0%) of length 5
c [cce-17-1] eliminated 9 clauses out of 5333 (0%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 36 large clauses in 19262666 steps
c [cce-17-1] allowing another 9631333 steps for small clauses
c [cce-17] scheduling 20877 clauses = 17142 binary + 3735 ternary
c [cce-17] tried to eliminate 20877 small clauses 100%
c [cce-17] eliminated 34 small clauses 0%
c [cce-17] eliminated 24 binary clauses 0%
c [cce-17] eliminated 10 ternary clauses 0%
c [cce-17-1] eliminated 34 small clauses in 40076047 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 70 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 20843 clauses = 17118 binary + 3725 ternary
c [cce-17] tried to eliminate 20843 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 70 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 6450 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 20 variables 0% in round 1 in 6380911 steps
c [elim-18-1] backward subsumption/strengthening limit 12761822
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 1661834 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 20 = 0% variables out of 6450
c [bca-17] limit of 10000000 steps
c [bca-17] 5215 out of 12862 literals actually usable 41%
c [bca-17] added 3 blocked clauses in 29333 steps
c [rephase-8] after 1337451 conflicts (new increment 40000, next 1377451)
c [flushphases] 0 phases reset
c [simplification-18] removed 32 variables 0.5% (6430 remain 13%)
c [simplification-18] removed 130 irredundant clauses 0.3% (39153 remain 19%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 30000
c [simplification-18] new conflict interval 60000
c [simplification-18] penalized conflict interval 60000 = 1 * 60000
c [simplification-18] new conflict limit 1397451
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  294.9    6430    39153   1341949   13845  27185 34767  11 16.4  46.7   10
c -  296.2    6430    39153   1350504   15265  27248 34775  11 16.4  46.6   10
c -  297.8    6430    39153   1359556   16841  27306 34789  10 16.4  46.6   10
c -  299.1    6430    39153   1369473   18364  27392 34797  11 16.3  46.6   10
c -  300.5    6430    39153   1379888   19632  27435 34798   9 16.4  46.7   10
c -  302.4    6430    39153   1390574   21122  27494 34812  10 16.3  46.7   10
c 
c [simplification-19] limit of 1397567 conflicts hit after 1397567 conflicts
c [ternres-17] limit 84842229 with penalty 0 = 0 + 0
c [ternres-17] all 6430 free variables schedulable
c [ternres-17] 979 ternary resolvents (16 bin, 963 trn)
c [ternres-17] fully completed ternary resolution
c [treelook-7] limit 4242111 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 12858 literals 100%
c [treelook-7] scheduling used 345209 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 4242111 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 4255175 steps
c [treelook-7] 12498 literals remain 97%
c [treelook-7] 6427 variables remain to probed next time 100%
c [decomp-47] removed 1 variables
c [treelook-7] removed 1 variables, found 3748 hbrs
c [lift-16] limit 10000000 with penalty 1 = 1 + 0
c [lift-16] using 44 probes 1%
c [lift-16-1] found 0 units 10 impls in round 1
c [lift-16-2] found 0 units 6 impls in round 2
c [lift-16-3] found 0 units 2 impls in round 3
c [lift-16-4] found 0 units 8 impls in round 4
c [lift-16-5] found 0 units 9 impls in round 5
c [lift-16] 0 units, 35 impls, 0 eqs in 6 rounds
c [lift-16] 729 variables remain 11% (5700 retained)
c [cliff-15] limit of 33936891 steps penalty 1 = 1 + 0
c [cliff-15] failed 0, lifted 1
c [unhide-9] limit 1060527 with penalty 4 = 4 + 0
c [unhide-9-10] 0 units, 0 failed, 9737 tauts, 0 hbrs, 75393 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1878 transitive binary clauses
c [cce-18] limit of 169684459 steps penalty 0 = 0 + 0
c [cce-18-1] eliminated 5 clauses out of 230 (2%) of length 11
c [cce-18-1] eliminated 1 clauses out of 309 (0%) of length 9
c [cce-18-1] eliminated 4 clauses out of 796 (1%) of length 8
c [cce-18-1] eliminated 8 clauses out of 1311 (1%) of length 7
c [cce-18-1] eliminated 9 clauses out of 2715 (0%) of length 6
c [cce-18-1] eliminated 21 clauses out of 3880 (1%) of length 5
c [cce-18-1] eliminated 29 clauses out of 5369 (1%) of length 4
c [cce-18-1] completed large round (ACCE)
c [cce-18-1] eliminated 77 large clauses in 17789495 steps
c [cce-18-1] allowing another 8894747 steps for small clauses
c [cce-18] scheduling 20595 clauses = 17110 binary + 3485 ternary
c [cce-18] tried to eliminate 20595 small clauses 100%
c [cce-18] eliminated 161 small clauses 1%
c [cce-18] eliminated 107 binary clauses 1%
c [cce-18] eliminated 54 ternary clauses 2%
c [cce-18-1] eliminated 161 small clauses in 37557965 steps
c [cce-18-1] completed small round (ACCE)
c [cce-18-1] eliminated 238 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 20434 clauses = 17003 binary + 3431 ternary
c [cce-18] tried to eliminate 20434 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 238 covered clauses in TOTAL during 2 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 6428 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19-1] eliminated 100 variables 2% in round 1 in 6320733 steps
c [elim-19-1] backward subsumption/strengthening limit 12641466
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 1639218 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 100 = 2% variables out of 6428
c [bca-18] limit of 10000000 steps
c [bca-18] 4450 out of 12658 literals actually usable 35%
c [bca-18] added 4 blocked clauses in 36869 steps
c [rephase-9] after 1397567 conflicts (new increment 80000, next 1477567)
c [flushphases] 0 phases reset
c [simplification-19] removed 102 variables 1.6% (6328 remain 12%)
c [simplification-19] removed 417 irredundant clauses 1.1% (38736 remain 18%)
c [simplification-19] maximum reduction of 2% = max (2%, 1%)
c [simplification-19] geometric conflict interval increment 20000 = 60000 / 3
c [simplification-19] new conflict interval 80000
c [simplification-19] penalized conflict interval 80000 = 1 * 80000
c [simplification-19] new conflict limit 1477567
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  308.4    6328    38736   1403632   22031  25113 29904  12 16.3  46.6   11
c -  310.5    6328    38736   1415256   23496  25182 29919  11 16.3  46.5   10
c -  312.8    6328    38736   1427737   25207  25257 29934   9 16.2  46.4   10
c -  315.2    6328    38736   1440824   26651  25309 29941  10 16.2  46.4   11
c i  317.5    6327    38736   1452753   37668  25360 29953   8 16.2  46.3   15
c -  317.9    6327    38736   1454526   28321  25370 29955   9 16.2  46.3   11
c -  320.6    6327    38736   1468605   29856  25436 29966   7 16.2  46.2   11
c 
c [simplification-20] limit of 1477717 conflicts hit after 1477717 conflicts
c [ternres-18] limit 90404801 with penalty 0 = 0 + 0
c [ternres-18] all 6327 free variables schedulable
c [ternres-18] 2590 ternary resolvents (33 bin, 2557 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-7] limit 1130060 penalty 4 = 4 + 0
c [gauss-7] extracted 507 xors of average arity 3.0
c [gauss-7] connected 1519 occurrences of 339 variables (average 4.5)
c [gauss-7] limit 1130060 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-48] removed 1 variables
c [basicprobe-7] limit 90404801 penalty 0 = 0 + 0
c [basicprobe-7-0] 2639 sched 42%, 3 failed, 0 lifted, 1278 hbrs
c [decomp-49] removed 3 variables
c [basicprobe-7-1] 2627 sched 42%, 1 failed, 0 lifted, 94 hbrs
c [decomp-50] removed 1 variables
c [basicprobe-7-2] 2627 sched 42%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-7-3] 2626 sched 42%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-7-4] 2626 sched 42%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-5] 2626 sched 42%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-7-6] 2626 sched 42%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-7-7] 2626 sched 42%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-8] 2626 sched 42%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-9] 2626 sched 42%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-9] round limit 9 hit
c [basicprobe-7-9] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-7-9] removed 4 variables, found 1447 hbrs
c [cgrclsr-15] limit 2000000 penalty 2 = 2 + 0
c [cgrclsr-15] all 6322 free variables schedulable
c [cgrclsr-15] fully completed congruence closure
c [cliff-16] limit of 72323841 steps penalty 0 = 0 + 0
c [cliff-16] failed 0, lifted 0
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 1444 transitive binary clauses
c [cce-19] limit of 180809602 steps penalty 0 = 0 + 0
c [cce-19-1] eliminated 1 clauses out of 83 (1%) of length 10
c [cce-19-1] eliminated 11 clauses out of 313 (4%) of length 9
c [cce-19-1] eliminated 21 clauses out of 791 (3%) of length 8
c [cce-19-1] eliminated 15 clauses out of 1303 (1%) of length 7
c [cce-19-1] eliminated 23 clauses out of 2723 (1%) of length 6
c [cce-19-1] eliminated 34 clauses out of 3940 (1%) of length 5
c [cce-19-1] eliminated 22 clauses out of 5343 (0%) of length 4
c [cce-19-1] completed large round (ACCE)
c [cce-19-1] eliminated 127 large clauses in 18046266 steps
c [cce-19-1] allowing another 9023133 steps for small clauses
c [cce-19] scheduling 20519 clauses = 16698 binary + 3821 ternary
c [cce-19] tried to eliminate 20519 small clauses 100%
c [cce-19] eliminated 79 small clauses 0%
c [cce-19] eliminated 48 binary clauses 0%
c [cce-19] eliminated 31 ternary clauses 1%
c [cce-19-1] eliminated 79 small clauses in 37409789 steps
c [cce-19-1] completed small round (ACCE)
c [cce-19-1] eliminated 206 covered clauses in round 1
c [cce-19-2] completed large round (ACCE)
c [cce-19-2] allowing another 0 steps for small clauses
c [cce-19] scheduling 20440 clauses = 16650 binary + 3790 ternary
c [cce-19] tried to eliminate 20440 small clauses 100%
c [cce-19-2] completed small round (ACCE)
c [cce-19-2] eliminated 0 covered clauses in round 2
c [cce-19] eliminated 206 covered clauses in TOTAL during 2 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 6322 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20-1] eliminated 21 variables 0% in round 1 in 5930411 steps
c [elim-20-1] backward subsumption/strengthening limit 11860822
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 1616958 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 21 = 0% variables out of 6322
c [bca-19] limit of 10000000 steps
c [bca-19] 4060 out of 12604 literals actually usable 32%
c [bca-19] added 3 blocked clauses in 48087 steps
c [rephase-10] after 1477717 conflicts (new increment 160000, next 1637717)
c [flushphases] 0 phases reset
c [simplification-20] removed 26 variables 0.4% (6301 remain 12%)
c [simplification-20] removed 273 irredundant clauses 0.7% (38463 remain 18%)
c [simplification-20] maximum reduction of 1% = max (0%, 1%)
c [simplification-20] geometric conflict interval increment 40000 = 80000 / 2
c [simplification-20] new conflict interval 120000
c [simplification-20] penalized conflict interval 120000 = 1 * 120000
c [simplification-20] new conflict limit 1597717
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  331.1    6301    38463   1484007   31240  27910 29968   9 16.1  46.1   12
c -  333.4    6301    38463   1499507   32729  27951 29973  10 16.1  46.2   12
c -  336.0    6301    38463   1516736   34070  27995 29979  11 16.2  46.3   12
c -  339.4    6301    38463   1534244   35283  28047 29982  10 16.2  46.2   12
c -  342.9    6301    38463   1550958   36861  28115 29993  11 16.2  46.1   12
c -  346.7    6301    38463   1567967   38154  28183 29999   9 16.2  46.0   12
c -  351.2    6301    38463   1588164   39451  28251 30006   9 16.3  46.0   12
c 
c [simplification-21] limit of 1597813 conflicts hit after 1597813 conflicts
c [ternres-19] limit 99544077 with penalty 0 = 0 + 0
c [ternres-19] all 6301 free variables schedulable
c [ternres-19] 1803 ternary resolvents (25 bin, 1778 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 3110752 penalty 4 = 4 + 0
c [card-6] found 1488 at-most-one constraints of average size 3.2
c [card-6] found 375 at-most-two constraints of average size 4.3
c [card-6] using previous limit 3110752 for elimination
c [card-6] 1863 out of 1863 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [simpleprobe-8] all 6301 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 10 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 10 variables, found 8743 hbrs, 0 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 2491 transitive binary clauses
c [cce-20] limit of 199088154 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 7 clauses out of 302 (2%) of length 9
c [cce-20-1] eliminated 2 clauses out of 767 (0%) of length 8
c [cce-20-1] eliminated 6 clauses out of 2695 (0%) of length 6
c [cce-20-1] eliminated 2 clauses out of 3913 (0%) of length 5
c [cce-20-1] eliminated 12 clauses out of 5334 (0%) of length 4
c [cce-20-1] completed large round (ACCE)
c [cce-20-1] eliminated 29 large clauses in 18978051 steps
c [cce-20-1] allowing another 9489025 steps for small clauses
c [cce-20] scheduling 20360 clauses = 16566 binary + 3794 ternary
c [cce-20] tried to eliminate 20360 small clauses 100%
c [cce-20] eliminated 32 small clauses 0%
c [cce-20] eliminated 31 binary clauses 0%
c [cce-20] eliminated 1 ternary clauses 0%
c [cce-20-1] eliminated 32 small clauses in 39504097 steps
c [cce-20-1] completed small round (ACCE)
c [cce-20-1] eliminated 61 covered clauses in round 1
c [cce-20-2] completed large round (ACCE)
c [cce-20-2] allowing another 0 steps for small clauses
c [cce-20] scheduling 20328 clauses = 16535 binary + 3793 ternary
c [cce-20] tried to eliminate 20328 small clauses 100%
c [cce-20-2] completed small round (ACCE)
c [cce-20-2] eliminated 0 covered clauses in round 2
c [cce-20] eliminated 61 covered clauses in TOTAL during 2 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 6291 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21-1] eliminated 7 variables 0% in round 1 in 5909930 steps
c [elim-21-1] backward subsumption/strengthening limit 11819860
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 1611753 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 7 = 0% variables out of 6291
c [bca-20] limit of 10000000 steps
c [bca-20] 3776 out of 12570 literals actually usable 30%
c [bca-20] added 2 blocked clauses in 58089 steps
c [simplification-21] removed 17 variables 0.3% (6284 remain 12%)
c [simplification-21] removed 105 irredundant clauses 0.3% (38358 remain 18%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 120000
c [simplification-21] new conflict interval 240000
c [simplification-21] penalized conflict interval 240000 = 1 * 240000
c [simplification-21] new conflict limit 1837813
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  358.5    6284    38358   1606444   40950  30092 36270  13 16.3  45.9   14
c -  362.7    6284    38358   1625231   42157  30153 36281   9 16.3  45.8   14
c -  367.1    6284    38358   1645973   43436  30209 36289  10 16.4  45.8   14
c -  372.0    6284    38358   1666713   44833  30271 36299  10 16.4  45.7   14
c -  377.0    6284    38358   1687407   46303  30328 36309  10 16.4  45.6   14
c -  381.8    6284    38358   1708435   47820  30384 36317   8 16.3  45.5   14
c -  387.5    6284    38358   1730280   49112  30453 36329   6 16.3  45.3   14
c i  392.9    6283    38358   1750933   68094  30500 36339   8 16.3  45.2   23
c -  393.4    6281    38358   1752443   50465  30504 36340   9 16.3  45.2   14
c -  398.7    6281    38358   1776844   51726  30541 36344  12 16.4  45.1   21
c -  403.9    6281    38358   1800444   52737  30560 36349  12 16.4  45.0   14
c -  409.2    6281    38358   1826947   53680  30592 36355  10 16.5  45.0   14
c 
c [simplification-22] limit of 1837985 conflicts hit after 1837985 conflicts
c [ternres-20] limit 121765479 with penalty 0 = 0 + 0
c [ternres-20] all 6281 free variables schedulable
c [ternres-20] 2143 ternary resolvents (31 bin, 2112 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-60] removed 4 variables
c [treelook-8] limit 6088273 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 12558 literals 100%
c [treelook-8] scheduling used 438928 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 6088273 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 6088937 steps
c [treelook-8] 11500 literals remain 92%
c [treelook-8] 6269 variables remain to probed next time 100%
c [decomp-61] removed 8 variables
c [treelook-8] removed 8 variables, found 3739 hbrs
c [lift-17] limit 5000000 with penalty 2 = 2 + 0
c [lift-17] using 58 probes 1%
c [lift-17-1] found 0 units 8 impls in round 1
c [lift-17-2] found 0 units 1 impls in round 2
c [lift-17-3] found 0 units 2 impls in round 3
c [lift-17-4] found 0 units 4 impls in round 4
c [lift-17-5] found 0 units 2 impls in round 5
c [lift-17] 0 units, 17 impls, 1 eqs in 6 rounds
c [lift-17] 643 variables remain 10% (5628 retained)
c [lift-17] removed 1 variables
c [cliff-17] limit of 48706191 steps penalty 1 = 1 + 0
c [cliff-17] failed 0, lifted 1
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 2055 transitive binary clauses
c [cce-21] limit of 243530958 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 3 clauses out of 294 (1%) of length 9
c [cce-21-1] eliminated 5 clauses out of 761 (1%) of length 8
c [cce-21-1] eliminated 4 clauses out of 1274 (0%) of length 7
c [cce-21-1] eliminated 10 clauses out of 2677 (0%) of length 6
c [cce-21-1] eliminated 6 clauses out of 3910 (0%) of length 5
c [cce-21-1] eliminated 9 clauses out of 5332 (0%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 37 large clauses in 19169083 steps
c [cce-21-1] allowing another 9584541 steps for small clauses
c [cce-21] scheduling 19939 clauses = 16502 binary + 3437 ternary
c [cce-21] tried to eliminate 19939 small clauses 100%
c [cce-21] eliminated 53 small clauses 0%
c [cce-21] eliminated 33 binary clauses 0%
c [cce-21] eliminated 20 ternary clauses 1%
c [cce-21-1] eliminated 59 small clauses in 39573557 steps
c [cce-21-1] completed small round (ACCE)
c [cce-21-1] eliminated 96 covered clauses in round 1
c [cce-21-2] completed large round (ACCE)
c [cce-21-2] allowing another 0 steps for small clauses
c [cce-21] scheduling 19886 clauses = 16469 binary + 3417 ternary
c [cce-21] tried to eliminate 19886 small clauses 100%
c [cce-21] eliminated 2 small clauses 0%
c [cce-21] eliminated 1 binary clauses 0%
c [cce-21] eliminated 1 ternary clauses 0%
c [cce-21-2] eliminated 2 small clauses in 29873186 steps
c [cce-21-2] completed small round (ACCE)
c [cce-21-2] eliminated 2 covered clauses in round 2
c [cce-21-3] completed large round (ACCE)
c [cce-21-3] allowing another 0 steps for small clauses
c [cce-21] scheduling 19884 clauses = 16468 binary + 3416 ternary
c [cce-21] tried to eliminate 19884 small clauses 100%
c [cce-21-3] completed small round (ACCE)
c [cce-21-3] eliminated 0 covered clauses in round 3
c [cce-21] eliminated 98 covered clauses in TOTAL during 3 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 6270 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22-1] eliminated 3 variables 0% in round 1 in 5808592 steps
c [elim-22-1] backward subsumption/strengthening limit 11617184
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 1599617 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 3 = 0% variables out of 6270
c [elim-22] 3 < 1/1000 * 6270 = 6 considered unsuccessful
c [bca-21] limit of 10000000 steps
c [bca-21] 3609 out of 12536 literals actually usable 29%
c [bca-21] added 2 blocked clauses in 71605 steps
c [rephase-11] after 1837985 conflicts (new increment 320000, next 2157985)
c [flushphases] 0 phases reset
c [simplification-22] removed 14 variables 0.2% (6267 remain 12%)
c [simplification-22] removed 167 irredundant clauses 0.4% (38191 remain 18%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 240000
c [simplification-22] new conflict interval 480000
c [simplification-22] penalized conflict interval 480000 = 1 * 480000
c [simplification-22] new conflict limit 2317985
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  420.6    6267    38191   1852389   54508  32598 39326  11 16.5  44.9   16
c -  427.7    6267    38191   1876891   56011  32661 39337   9 16.5  44.7   16
c -  434.6    6267    38191   1903811   57429  32728 39348   7 16.5  44.6   16
c -  442.0    6267    38191   1930126   59051  32794 39355  11 16.5  44.5   17
c -  449.2    6267    38191   1956838   60224  32839 39363  12 16.5  44.3   17
c -  457.0    6267    38191   1983852   61566  32880 39371  10 16.5  44.2   17
c -  465.5    6267    38191   2011942   62974  32941 39381  10 16.5  44.1   17
c -  473.7    6267    38191   2040919   64349  32990 39387  10 16.5  43.9   25
c -  482.3    6267    38191   2069101   65719  33037 39398   8 16.5  43.8   17
c -  489.4    6267    38191   2099335   67039  33067 39401   9 16.5  43.7   17
c -  498.7    6267    38191   2132537   68189  33101 39414   9 16.6  43.6   24
c -  508.3    6267    38191   2163587   69636  33144 39425  10 16.6  43.4   24
c -  518.0    6267    38191   2195037   70848  33193 39436   9 16.6  43.3   17
c i  525.6    6266    38191   2217886   91829  33239 39450   8 16.6  43.2   27
c -  528.4    6265    38191   2227214   72340  33252 39452  11 16.6  43.2   17
c -  539.3    6265    38191   2261568   73662  33311 39463  10 16.6  43.1   25
c -  549.8    6265    38191   2293940   75063  33372 39469  11 16.6  42.9   18
c 
c [simplification-23] limit of 2318249 conflicts hit after 2318250 conflicts
c [ternres-21] limit 177590372 with penalty 0 = 0 + 0
c [ternres-21] all 6265 free variables schedulable
c [ternres-21] 5534 ternary resolvents (57 bin, 5477 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-62] removed 6 variables
c [basicprobe-8] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 2546 sched 41%, 13 failed, 0 lifted, 1208 hbrs
c [decomp-63] removed 15 variables
c [basicprobe-8-1] 2534 sched 41%, 0 failed, 0 lifted, 177 hbrs
c [basicprobe-8-2] 2533 sched 41%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-8-3] 2533 sched 41%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-8-4] 2533 sched 41%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-8-5] 2533 sched 41%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-8-6] 2533 sched 41%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-7] 2533 sched 41%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-8-8] 2092 probes remain 33% after last round
c [basicprobe-8-8] 13 units = 13 failed (100%) + 0 lifted (0%)
c [basicprobe-8-8] removed 15 variables, found 1472 hbrs
c [bate-6] eliminated 5 asymmetric tautologies during probing
c [cliff-18] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-18] failed 1, lifted 0
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 1652 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 6245 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 0 blocked clauses
c [cce-22] limit of 355180745 steps penalty 0 = 0 + 0
c [cce-22-1] eliminated 1 clauses out of 291 (0%) of length 9
c [cce-22-1] eliminated 1 clauses out of 756 (0%) of length 8
c [cce-22-1] eliminated 1 clauses out of 1254 (0%) of length 7
c [cce-22-1] eliminated 7 clauses out of 2645 (0%) of length 6
c [cce-22-1] eliminated 8 clauses out of 3901 (0%) of length 5
c [cce-22-1] eliminated 4 clauses out of 5305 (0%) of length 4
c [cce-22-1] completed large round (ACCE)
c [cce-22-1] eliminated 22 large clauses in 19479646 steps
c [cce-22-1] allowing another 9739823 steps for small clauses
c [cce-22] scheduling 20164 clauses = 16387 binary + 3777 ternary
c [cce-22] tried to eliminate 20164 small clauses 100%
c [cce-22] eliminated 31 small clauses 0%
c [cce-22] eliminated 20 binary clauses 0%
c [cce-22] eliminated 11 ternary clauses 0%
c [cce-22-1] eliminated 31 small clauses in 40284069 steps
c [cce-22-1] completed small round (ACCE)
c [cce-22-1] eliminated 53 covered clauses in round 1
c [cce-22-2] completed large round (ACCE)
c [cce-22-2] allowing another 0 steps for small clauses
c [cce-22] scheduling 20133 clauses = 16367 binary + 3766 ternary
c [cce-22] tried to eliminate 20133 small clauses 100%
c [cce-22-2] completed small round (ACCE)
c [cce-22-2] eliminated 0 covered clauses in round 2
c [cce-22] eliminated 53 covered clauses in TOTAL during 2 rounds
c [bca-22] limit of 10000000 steps
c [bca-22] 3254 out of 12492 literals actually usable 26%
c [bca-22] added 1 blocked clauses in 105234 steps
c [rephase-12] after 2318250 conflicts (new increment 640000, next 2958250)
c [flushphases] 0 phases reset
c [simplification-23] removed 20 variables 0.3% (6245 remain 12%)
c [simplification-23] removed 193 irredundant clauses 0.5% (37998 remain 18%)
c [simplification-23] maximum reduction of 1% = max (0%, 1%)
c [simplification-23] geometric conflict interval increment 240000 = 480000 / 2
c [simplification-23] new conflict interval 720000
c [simplification-23] penalized conflict interval 720000 = 1 * 720000
c [simplification-23] new conflict limit 3038250
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  571.2    6245    37998   2327604   76173  38749 39584   8 16.6  42.8   20
c -  582.6    6245    37998   2363613   77424  38790 39589   8 16.7  42.7   21
c -  592.9    6245    37998   2405142   78551  38836 39592   9 16.9  42.7   23
c -  605.5    6245    37998   2463748   79469  38884 39599  10 17.4  42.8   32
c -  618.6    6245    37998   2516271   80525  38920 39606   9 17.7  42.9   30
c -  629.7    6245    37998   2558408   81527  38943 39610  10 17.8  42.8   20
c -  640.7    6245    37998   2599541   82528  38980 39617  10 17.9  42.8   20
c -  652.4    6245    37998   2638411   83519  39015 39617  10 17.9  42.7   29
c R  662.7    6245    37998   2673664  114472  39034 39619  10 17.9  42.6   47
c -  664.2    6245    37998   2676915   84430  39037 39619   9 17.9  42.6   29
c -  678.9    6245    37998   2715238   85763  39076 39630   7 17.9  42.5   22
c -  693.5    6245    37998   2755791   87044  39120 39635   9 17.9  42.3   22
c -  706.8    6245    37998   2798935   88407  39180 39641  13 18.0  42.3   22
c -  721.7    6245    37998   2839207   89572  39244 39645   8 18.0  42.1   31
c -  737.1    6245    37998   2878674   90925  39292 39652   8 18.0  42.0   31
c -  751.5    6245    37998   2921335   92072  39324 39657   9 18.0  41.8   21
c -  766.4    6245    37998   2963624   93115  39359 39669  11 18.0  41.8   31
c -  783.3    6245    37998   3006886   94417  39408 39676   7 18.0  41.6   31
c 
c [simplification-24] limit of 3038414 conflicts hit after 3038421 conflicts
c [ternres-22] limit 200000000 with penalty 0 = 0 + 0
c [ternres-22] all 6245 free variables schedulable
c [ternres-22] 3940 ternary resolvents (51 bin, 3889 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-71] removed 3 variables
c [simpleprobe-9] all 6242 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-72] removed 3 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 3 variables, found 8796 hbrs, 0 units
c [cgrclsr-16] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-16] all 6239 free variables schedulable
c [cgrclsr-16] fully completed congruence closure
c [lift-18] limit 10000000 with penalty 1 = 1 + 0
c [lift-18] using 31 probes 0%
c [lift-18-1] found 1 units 4 impls in round 1
c [lift-18-2] found 0 units 5 impls in round 2
c [lift-18-3] found 0 units 2 impls in round 3
c [lift-18-4] found 0 units 2 impls in round 4
c [lift-18-5] found 0 units 3 impls in round 5
c [lift-18] 1 units, 16 impls, 0 eqs in 6 rounds
c [lift-18] 609 variables remain 10% (5629 retained)
c [lift-18] removed 1 variables
c [cliff-19] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-19] failed 5, lifted 1
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 2608 transitive binary clauses
c [cce-23] limit of 547620467 steps penalty 0 = 0 + 0
c [cce-23-1] eliminated 2 clauses out of 753 (0%) of length 8
c [cce-23-1] eliminated 1 clauses out of 1250 (0%) of length 7
c [cce-23-1] eliminated 7 clauses out of 2622 (0%) of length 6
c [cce-23-1] eliminated 4 clauses out of 3890 (0%) of length 5
c [cce-23-1] eliminated 7 clauses out of 5304 (0%) of length 4
c [cce-23-1] completed large round (ACCE)
c [cce-23-1] eliminated 21 large clauses in 20244727 steps
c [cce-23-1] allowing another 10122363 steps for small clauses
c [cce-23] scheduling 20097 clauses = 16337 binary + 3760 ternary
c [cce-23] tried to eliminate 20097 small clauses 100%
c [cce-23] eliminated 29 small clauses 0%
c [cce-23] eliminated 25 binary clauses 0%
c [cce-23] eliminated 4 ternary clauses 0%
c [cce-23-1] eliminated 77 small clauses in 41755620 steps
c [cce-23-1] completed small round (ACCE)
c [cce-23-1] eliminated 98 covered clauses in round 1
c [cce-23-2] completed large round (ACCE)
c [cce-23-2] allowing another 0 steps for small clauses
c [cce-23] scheduling 20068 clauses = 16312 binary + 3756 ternary
c [cce-23] tried to eliminate 20068 small clauses 100%
c [cce-23-2] completed small round (ACCE)
c [cce-23-2] eliminated 0 covered clauses in round 2
c [cce-23] eliminated 98 covered clauses in TOTAL during 2 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 6231 variables 100%
c [elim-23] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-23-1] eliminated 18 variables 0% in round 1 in 5873324 steps
c [elim-23-1] backward subsumption/strengthening limit 11746648
c [elim-23-1] subsumed 0 and strengthened 0 clauses in 1584691 steps
c [elim-23] fully completed in 1 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 18 = 0% variables out of 6231
c [bca-23] limit of 10000000 steps
c [bca-23] 3180 out of 12428 literals actually usable 26%
c [bca-23] added 0 blocked clauses in 126221 steps
c [rephase-13] after 3038421 conflicts (new increment 1280000, next 4318421)
c [flushphases] 0 phases reset
c [simplification-24] removed 32 variables 0.5% (6213 remain 12%)
c [simplification-24] removed 147 irredundant clauses 0.4% (37851 remain 18%)
c [simplification-24] maximum reduction of 1% = max (1%, 0%)
c [simplification-24] geometric conflict interval increment 360000 = 720000 / 2
c [simplification-24] conflict interval soft limit 1000000 reached
c [simplification-24] new conflict interval 1000000
c [simplification-24] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-24] new conflict limit 4038421
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  810.7    6213    37851   3053875   94419  42883 46820  10 18.0  41.5   27
c -  826.8    6213    37851   3098180   95831  42921 46823  10 18.0  41.4   27
c -  845.3    6213    37851   3143889   97058  42962 46826   8 18.0  41.3   24
c -  863.2    6213    37851   3188191   98498  42993 46830  11 18.0  41.1   34
c -  876.5    6213    37851   3236676   99319  43013 46831  16 18.0  41.0   34
c -  894.1    6213    37851   3282264  100351  43039 46832   8 18.0  40.9   24
c -  913.7    6213    37851   3329356  101607  43079 46841   9 18.0  40.8   24
c -  932.7    6213    37851   3376491  102931  43130 46846  14 18.0  40.6   35
c -  952.0    6213    37851   3423975  104071  43168 46854   9 18.0  40.5   35
c -  972.5    6213    37851   3472870  105436  43207 46860  11 18.1  40.4   35
c -  990.7    6213    37851   3521647  106548  43238 46865  11 18.1  40.3   24
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 74 basic ate = 49 trn 66% + 25 lrg 34% in 6 updates
c bcas: 23 count, 534 added (0 skipped), 1361922 steps
c bkwd: tried 894274 clauses, 1788420 lits, 2.00 lits/clause
c bkwd: checked 67174548 occs, 75.12 occs/clause, 37.56 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 126 large (0% self)
c blkd: 7 bces, 217 removed, 1780473 resolutions, 5255778 steps
c blkd: 3920 blocking literals 4%, 8 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 2 am1, 10955296 steps
c card: 72 rescheduled, 624 eliminated, 5867 resolved, 22869 subsumed
c card: 10464 at-most-one constraints found, average size 3.04
c card: 10464 at-most-one constraints used 100%, average size 3.04
c card: 893 at-most-two constraints found, average size 4.31
c card: 891 at-most-two constraints used 100%, average size 4.31
c cces: 23 cces, 19918 eliminated, 15043 ate 76%, 4875 abce 24%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 16 count, 16227383 esteps, 5988362 csteps
c cgrs: 13 eqs, 5 units
c cgrs: 43 matched (43 ands 100%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 44036 extracted (38035 ands 86%, 4140 xors 9%, 1861 ites 4%)
c clff: 19 cliffs, 105 lifted, 137 failed
c clff: 884969 decisions, 616823195 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 764685 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 205 gcs, 0 rescored clauses, 1857 rescored vars
c dcps: 72 decompositions, 15449 equivalent 29%
c deco: 378670 decision-only clauses 11%, 76% reduction
c decs: 9775016 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 250256 flipped 2.560% (in 5245 phases)
c elms: 23 elims, 22015 eliminated 42%
c elms: 46 rounds, 2.0 rounds/bve
c elms: 19168 small 87%, 2839 large 13%
c elms: 28787 tried small, 19168 succeeded 67%, 9619 failed 33%
c elms: 6116 subsumed, 21277 strengthened, 674 blocked
c elms: 5950451 copies, 7619969 resolutions, 647043 ipos
c elms: 3043811 subchks, 3997972 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 7 extractions, 10847 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 17565314 steps, 8782657 extr 50%, 396638 elim 2%
c glue: 18.0 orig avg, 17.4 real avg, 3.8 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 132853 = 74462 simple + 51755 trn 56% + 6636 lrg 39%, 5143 sub 5%
c hght: 40 average, 2.23 height/glue
c ints: 90658 luby (26058416 steps), 0 inout (0 steps)
c lift: 18 phases, 62241 probed (20938 level1 34%, 41303 level2 66%)
c lift: 73 units, 89 equivalences, 820 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3531029 clauses, 63.6 length
c lrnd: 889242 uips 25%, 2271413 flips 64%
c mega: 0 count, 0 failed, 0 rounds
c mins: 224590272 learned lits, 43% minimized
c mins: 3119725 mins 88%, 1435 bin 0%, 31199 size 1%, 378670 deco 11%
c move: moved 3531029, 10781 bin 0%, 1913 trn 0%, 0 lrg 0%
c otfs: str 71442 dyn (70630 red, 812 irr) 17044 drv 24%, 54398 rst 76%
c otfs: sub 397 dyn (396 red, 1 irr)
c phas: 6 computed, 12367 set, 5218 pos (42%), 7149 neg (58%)
c prbs: 8 basic, 192426 probed, 120 failed, 15 lifted
c prbs: 9 simple, 186289 probed, 713 failed, 12505 eqs
c prbs: 8 treelook, 2919 probed, 5 failed, 0 lifted
c prps: 1668505540 props, 162 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c psns: 401939513 searches, 78741476 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: 141 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 141 arith 100%, 0 double 0%
c rmbd: 9834 removed, 9031 red 92%
c rphs: 13 recomputed phases
c rsts: 89327 restarts 99%, 1331 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 1331 reuse 100%
c rsts: 38.9 avg interval, 38.9 scaled, 1.0 factor
c rsts: 33028 kept 37.0% average 15.8%
c simp: 24 count (24 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3531029 count (5613290 tried 1.6), 428522 sub out of 3517891 (12.2%)
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: 8767 fixed 17%, 48 its, 73918.19 confs/it
c trvs: 56643013105 traversals, 98% srch, 2% simp, 0% lkhd
c trvs: 35.2 search traversals per propagation, 15684.2 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 22 transitive reductions, 34524 removed, 2 failed
c trds: 260942 nodes, 642467 edges, 36053035 steps
c trim: 10216377 words, 39.0 MB
c trnr: 22 count, 799 bin, 53591 trn, 379494489 steps
c unhd: 9 count, 10 rounds, 7291262 steps
c unhd: 223 non-trivial sccs of average size 2.0
c unhd: 14 units, 14 bin, 0 trn, 0 lrg
c unhd: 30 failed, 28 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 23514 tauts, 402 bin 2%, 6370 trn 27%, 2630 lrg 11%
c unhd: 23514 tauts, 14112 stamp 60%, 23110 red 98%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 286728 str, 14 bin 0%, 1317 trn 0%, 285397 lrg 100%, 276692 red 96%
c vars: 6213 remaining 12% and 46231 removed 88% out of 52444
c vars: 8767 fixed 17%, 22015 eliminated 42%, 15449 equivalent 29%
c vsts: 36474771451 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 22.4 search visits per propagation, 9999.9 per conflict
c wchs: 7993912928 pushed, 41154424 enlarged, 372 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3517891 100   2797510 100 309494752 100  71116750 100   2533546 100
c 
c  0     138987   4         0   0 215228250  70< 38780235  55    888017  35 
c  1     135714   4     42481   2  76651395  25  19538660  27<   647153  26 
c  2     534756  15    510403  18   7639323   2   3764473   5    230333   9<
c  3     852998  24    810029  29   5200203   2   3744932   5    299037  12 
c  4     798543  23<   739188  26<  2612140   1   2571495   4    233737   9 
c  5     541521  15    507285  18   1298035   0   1532334   2    149413   6 
c  6     237470   7    117510   4    455865   0    590110   1     47618   2 
c  7     138786   4     34700   1    210194   0    302512   0     19719   1 
c  8      83204   2     20688   1    119747   0    175283   0     11145   0 
c  9      40890   1     10694   0     58908   0     86125   0      5423   0 
c 10      14244   0      4225   0     19679   0     29056   0      1853   0 
c 11        754   0       291   0       970   0      1482   0        88   0 
c 12         24   0        16   0        43   0        53   0        10   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.7
c std             1.8           1.3           0.8           1.4           1.8
c 
c   96.007  10% analysis
c   43.499   4% cce
c   36.901   4% mincls
c   17.454   2% cliff
c   16.542   2% bump
c   15.103   2% probe
c   11.372   1% decide
c    8.579   1% elim
c    5.712   1% restart
c    5.090   1% gc
c    4.267   0% ternres
c    4.250   0% decomp
c    3.208   0% lift
c    2.802   0% backward
c    2.549   0% transred
c    1.568   0% defrag
c    1.546   0% reduce
c    1.515   0% cgrclsr
c    1.124   0% unhide
c    0.815   0% bca
c    0.551   0% block
c    0.426   0% gauss
c    0.411   0% card
c    0.055   0% phase
c    0.022   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    2.473   0% probe simple     16%
c   11.580   1% probe basic      77%
c    1.050   0% probe tree-look   7%
c ==================================
c    2.734   0% preprocessing     3%
c   98.805  10% inprocessing     97%
c ==================================
c  101.539  10% simplifying
c  898.370  90% search
c ==================================
c  999.911 100% all
c 
c 9775016 decisions, 9775.9 decisions/sec
c 3548073 conflicts, 3548.4 conflicts/sec
c 1668505540 propagations, 1.7 megaprops/sec
c 999.9 seconds, 63.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
