c launch: /data/cnf/sc2014/app/6s131-opt.cnf.bz2
c host: atom16
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/6s131-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s131-opt.cnf.bz2
c no embedded options
c found 'p cnf 49325 144226' header
c read 49325 variables, 144226 clauses, 336526 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 49281 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   49281   144225         0       0      0     0   0  0.0   0.0    9
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 84 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] 84 out of 84 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 85 at-most-one constraints, 85 used 100%
c [card-1] exported 90 binary clauses, 1.1 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 49281 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 835 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 835 variables, found 1887 hbrs, 24 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 9 tauts, 0 hbrs, 12 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 48446 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 35863 variables 74% in round 1 in 12353399 steps
c [elim-1-1] backward subsumption/strengthening limit 24706798
c [elim-1-1] subsumed 92 and strengthened 975 clauses in 5800203 steps
c [elim-1-1] rescheduled 1403 variables 3% by backward subsumption
c [elim-1-2] eliminated 3 variables 0% in round 2 in 1097555 steps
c [elim-1-2] backward subsumption/strengthening limit 2195110
c [elim-1-2] subsumed 1 and strengthened 4 clauses in 2195114 steps
c [elim-1-2] rescheduled 11 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 10501 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 35866 = 74% variables out of 48446
c [phase-1] phase bias: 3252 positive 26%, 9328 negative 74%
c [simplification-1] removed 36701 variables 74.5% (12580 remain 26%)
c [simplification-1] removed 74186 irredundant clauses 51.4% (70039 remain 49%)
c [simplification-1] maximum reduction of 74% = max (74%, 51%)
c [simplification-1] large reduction 74% >= 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] 17437, max 30970, min4 3302 at 72%, min10 3302 at 72%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number clauses 70039 drops below limit 72112
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 12580 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 3145 and clause limit 35019
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    1.6   12580    70039         5       2      1   113   0  2.2  12.7    7
c R    1.6   12580    70039        20      11      6   114   2  3.5 111.7    7
c R    1.6   12580    70039        60      32     16   118   7  3.2 350.5    8
c R    1.6   12580    70039       163     109     25   123   7  4.5 375.9    8
c R    1.7   12580    70039       413     312     47   127   4  5.0 508.7    8
c R    1.8   12580    70039       985     747    109   139   3  5.3 447.1    8
c 
c [simplification-2] limit of 1045 conflicts hit after 1045 conflicts
c [decomp-3] removed 5 variables
c [simpleprobe-2] all 12575 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 4 variables
c [simpleprobe-2] 5015 variables remain 40% (7556 retained)
c [simpleprobe-2] removed 4 variables, found 465 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 25142 literals 100%
c [treelook-1] scheduling used 292756 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300825 steps
c [treelook-1] 25032 literals remain 100%
c [treelook-1] 12571 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 3536 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 4324 probes remain 34% after last round
c [basicprobe-1-0] removed 0 variables, found 6498 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 12569 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 2092 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 1 clauses out of 1 (100%) of length 20
c [cce-1-1] eliminated 1 clauses out of 11 (9%) of length 18
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-1-1] eliminated 1 clauses out of 92 (1%) of length 13
c [cce-1-1] eliminated 9 clauses out of 119 (8%) of length 12
c [cce-1-1] eliminated 17 clauses out of 121 (14%) of length 11
c [cce-1-1] eliminated 18 clauses out of 204 (9%) of length 10
c [cce-1-1] eliminated 21 clauses out of 394 (5%) of length 9
c [cce-1-1] eliminated 35 clauses out of 682 (5%) of length 8
c [cce-1-1] eliminated 123 clauses out of 1418 (9%) of length 7
c [cce-1-1] eliminated 250 clauses out of 3159 (8%) of length 6
c [cce-1-1] eliminated 658 clauses out of 6427 (10%) of length 5
c [cce-1-1] eliminated 1086 clauses out of 14705 (7%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2221 large clauses in 36451122 steps
c [cce-1-1] allowing another 18225561 steps for small clauses
c [cce-1] scheduling 22012 clauses = 13491 binary + 8521 ternary
c [cce-1] tried to eliminate 22012 small clauses 100%
c [cce-1] eliminated 512 small clauses 2%
c [cce-1] eliminated 169 binary clauses 1%
c [cce-1] eliminated 343 ternary clauses 4%
c [cce-1-1] eliminated 512 small clauses in 36736411 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 2733 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 21500 clauses = 13322 binary + 8178 ternary
c [cce-1] tried to eliminate 21500 small clauses 100%
c [cce-1] eliminated 103 small clauses 0%
c [cce-1] eliminated 68 binary clauses 1%
c [cce-1] eliminated 35 ternary clauses 0%
c [cce-1-2] eliminated 103 small clauses in 18155470 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 103 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 21398 clauses = 13254 binary + 8144 ternary
c [cce-1] tried to eliminate 21398 small clauses 100%
c [cce-1] eliminated 46 small clauses 0%
c [cce-1] eliminated 22 binary clauses 0%
c [cce-1] eliminated 24 ternary clauses 0%
c [cce-1-3] eliminated 46 small clauses in 103573351 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 46 covered clauses in round 3
c [cce-1-4] completed large round (ACCE)
c [cce-1-4] allowing another 0 steps for small clauses
c [cce-1] scheduling 21352 clauses = 13232 binary + 8120 ternary
c [cce-1] tried to eliminate 21352 small clauses 100%
c [cce-1-4] completed small round (ACCE)
c [cce-1-4] eliminated 0 covered clauses in round 4
c [cce-1] eliminated 2882 covered clauses in TOTAL during 4 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12569 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2-1] eliminated 751 variables 6% in round 1 in 13066973 steps
c [elim-2-1] backward subsumption/strengthening limit 6933027
c [elim-2-1] subsumed 1 and strengthened 39 clauses in 3023218 steps
c [elim-2-1] rescheduled 111 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 513322 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 752 = 6% variables out of 12569
c [bca-1] limit of 10000000 steps
c [bca-1] 21617 out of 23636 literals actually usable 91%
c [bca-1] added 468 blocked clauses in 57598 steps
c [phase-3] phase bias: 7 positive 30%, 16 negative 70%
c [simplification-2] removed 763 variables 6.1% (11817 remain 24%)
c [simplification-2] removed 5769 irredundant clauses 8.2% (64270 remain 45%)
c [simplification-2] maximum reduction of 8% = max (6%, 8%)
c [simplification-2] large reduction 8% >= 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 3045
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   13.9   11817    64270      2293    1657   1414 10337   9  5.2 378.7    8
c 
c [simplification-3] limit of 3081 conflicts hit after 3082 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 11817 free variables schedulable
c [ternres-1] 6765 ternary resolvents (170 bin, 6595 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 370 at-most-one constraints of average size 3.5
c [card-2] found 50 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 417 out of 420 constraints (99%) meet size limits
c [card-2] no units found
c [card-2] generated 10 at-most-one constraints, 5 used 50%
c [card-2] exported 9 binary clauses, 1.8 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5660 xors of average arity 3.1
c [gauss-1] connected 17386 occurrences of 1242 variables (average 14.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-6] removed 27 variables
c [gauss-1] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 23580 literals 100%
c [treelook-2] scheduling used 300002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 424885 steps
c [treelook-2] 23528 literals remain 100%
c [treelook-2] 11788 variables remain to probed next time 100%
c [decomp-8] removed 1 variables
c [treelook-2] removed 3 variables, found 954 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 11787 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 10709 probes 91%
c [lift-1] 0 units, 12 impls, 2 eqs in 1 rounds
c [lift-1] 11356 variables remain 96% (429 retained)
c [lift-1] removed 2 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 1, lifted 4
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 2004 tauts, 0 hbrs, 1503 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 66 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 11780 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 7 blocked clauses
c [block-2] 7 < 1/1000 * 64211 = 64 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-2-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-2-1] eliminated 3 clauses out of 30 (10%) of length 15
c [cce-2-1] eliminated 1 clauses out of 42 (2%) of length 14
c [cce-2-1] eliminated 2 clauses out of 126 (2%) of length 13
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] eliminated 10 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 29466 clauses = 12308 binary + 17158 ternary
c [cce-2] tried to eliminate 718 small clauses 2%
c [cce-2] eliminated 17 small clauses 0%
c [cce-2] eliminated 2 binary clauses 0%
c [cce-2] eliminated 15 ternary clauses 0%
c [cce-2-1] eliminated 17 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ACCE)
c [cce-2-1] eliminated 27 covered clauses in round 1
c [cce-2] eliminated 27 covered clauses in TOTAL during 1 rounds
c [cce-2] 27 < 1/1000 * 64204 = 64 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 11779 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 117 variables 1% in round 1 in 15151647 steps
c [elim-3-1] backward subsumption/strengthening limit 4848353
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 2702729 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 117 = 1% variables out of 11779
c [bca-2] limit of 10000000 steps
c [bca-2] 19356 out of 23326 literals actually usable 83%
c [bca-2] added 8 blocked clauses in 52523 steps
c [phase-4] phase bias: 14 positive 50%, 14 negative 50%
c [simplification-3] removed 155 variables 1.3% (11662 remain 24%)
c [simplification-3] removed 275 irredundant clauses 0.4% (63995 remain 44%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 30000
c [simplification-3] penalized conflict interval 30000 = 1 * 30000
c [simplification-3] new conflict limit 33082
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   17.1   11662    63995      5247    4100   7314 17004  11  6.2 317.9    9
c -   17.3   11662    63995      6588    3287   7368 17018   9  6.3 293.0    8
c i   17.5   11661    63994      8331    4764   7446 17025   5  6.5 280.9    9
c -   17.7   11661    63994     10856    4482   7526 17035  11  6.9 293.0    8
c R   17.8   11661    63994     11788    5372   7532 17035  19  7.9 293.3    9
c -   18.2   11661    63994     15475    5593   7678 17056   9  7.7 271.1    9
c -   19.2   11661    63993     21483    7180   7916 17096   4  7.7 300.9    9
c R   19.4   11661    63993     26181   11384   7965 17114  13  7.8 304.1    9
c -   19.6   11661    63993     27389    8465   8008 17126   9  7.8 300.4    9
c 
c [simplification-4] limit of 33300 conflicts hit after 33300 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 11661 free variables schedulable
c [ternres-2] 1479 ternary resolvents (49 bin, 1430 trn)
c [ternres-2] 4 variables remain 0% (11657 retained)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5404 xors of average arity 3.0
c [gauss-2] connected 16302 occurrences of 1234 variables (average 13.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-9] removed 54 variables
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 10157 probes 88%
c [lift-2] 4 units, 7 impls, 1 eqs in 1 rounds
c [lift-2] 10843 variables remain 93% (759 retained)
c [lift-2] removed 5 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 1, lifted 11
c [transred-2] limit 778211 with penalty 0 = 0 + 0
c [transred-2] removed 572 transitive binary clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 11590 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 37 variables 0% in round 1 in 14294987 steps
c [elim-4-1] backward subsumption/strengthening limit 5705013
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 2706843 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 37 = 0% variables out of 11590
c [bca-3] limit of 10000000 steps
c [bca-3] 12192 out of 23108 literals actually usable 53%
c [bca-3] added 24 blocked clauses in 44444 steps
c [rephase-1] after 33300 conflicts (new increment 20000, next 53300)
c [flushphases] 0 phases reset
c [simplification-4] removed 108 variables 0.9% (11553 remain 23%)
c [simplification-4] removed 414 irredundant clauses 0.6% (63579 remain 44%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-4] new conflict interval 45000
c [simplification-4] penalized conflict interval 45000 = 1 * 45000
c [simplification-4] new conflict limit 78300
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   21.4   11553    63579     34340    9980   9383 17920  10  7.7 283.7    9
c -   22.0   11553    63579     41788   11449   9535 17941  10  7.7 272.9    9
c i   22.1   11552    63579     41996   11619   9538 17942   4  7.7 273.7   10
c i   22.1   11551    63579     42010   11630   9539 17943   5  7.7 273.5   10
c -   22.9   11551    63579     49433   12844   9718 17954  21  7.8 273.4   10
c -   23.2   11551    63579     57320   13891   9813 17962  26  8.4 276.1   10
c R   23.2   11551    63579     57503   14064   9813 17962  27  8.4 276.1   10
c -   24.3   11551    63579     66316   15451  10008 17998   6  8.4 271.5   10
c -   25.2   11551    63579     75721   17068  10149 18027  11  8.3 268.1   11
c 
c [simplification-5] limit of 78490 conflicts hit after 78491 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 4 schedulable variables 0%
c [ternres-3] 1589 ternary resolvents (15 bin, 1574 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 4933 xors of average arity 2.9
c [gauss-3] connected 14532 occurrences of 1143 variables (average 12.7)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 11 ternary equations
c [decomp-10] removed 67 variables
c [basicprobe-2] limit 897583 penalty 1 = 1 + 0
c [basicprobe-2-0] 2698 probes remain 24% after last round
c [basicprobe-2-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 5 variables, found 415 hbrs
c [bate-1] eliminated 7 asymmetric tautologies during probing
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 11479 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 1 variables
c [lift-3] limit 1077100 with penalty 0 = 0 + 0
c [lift-3] using 9750 probes 85%
c [lift-3] 2 units, 13 impls, 7 eqs in 1 rounds
c [lift-3] 10119 variables remain 88% (1350 retained)
c [lift-3] removed 9 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 1, lifted 0
c [transred-3] limit 1795167 with penalty 0 = 0 + 0
c [transred-3] removed 851 transitive binary clauses
c [transred-3] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 11467 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 112 blocked clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 19613 clauses = 11856 binary + 7757 ternary
c [cce-3] tried to eliminate 740 small clauses 4%
c [cce-3] eliminated 6 small clauses 0%
c [cce-3] eliminated 4 binary clauses 0%
c [cce-3] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 6 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6 covered clauses in round 1
c [cce-3] eliminated 6 covered clauses in TOTAL during 1 rounds
c [cce-3] 6 < 1/1000 * 63269 = 63 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 11454 variables 100%
c [elim-5] limit of 35903359 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 39 variables 0% in round 1 in 16335556 steps
c [elim-5-1] backward subsumption/strengthening limit 19567803
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 2699924 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 39 = 0% variables out of 11454
c [bca-4] limit of 10000000 steps
c [bca-4] 9823 out of 22832 literals actually usable 43%
c [bca-4] added 17 blocked clauses in 43525 steps
c [rephase-2] after 78491 conflicts (new increment 40000, next 118491)
c [flushphases] 0 phases reset
c [simplification-5] removed 136 variables 1.2% (11415 remain 23%)
c [simplification-5] removed 512 irredundant clauses 0.8% (63066 remain 44%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-5] new conflict interval 67500
c [simplification-5] penalized conflict interval 67500 = 1 * 67500
c [simplification-5] new conflict limit 145991
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   28.3   11415    63066     85879   18418  11345 18355  12  8.5 272.6   10
c i   28.6   11414    63066     87784   20105  11386 18372   7  8.5 272.9   11
c -   29.4   11414    63066     96112   19627  11476 18388  10  8.5 270.4   10
c -   30.6   11414    63066    107306   21275  11630 18427  21  8.5 266.0   10
c -   31.3   11414    63066    118678   22819  11636 18427  37  8.2 264.0   11
c R   31.7   11414    63066    125305   28791  11648 18428  19  8.2 265.3   17
c -   32.3   11414    63066    130561   24038  11727 18439  15  8.2 265.5   16
c -   33.7   11414    63066    143225   25425  11878 18462  11  8.4 261.9   11
c 
c [simplification-6] limit of 146177 conflicts hit after 146177 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 11414 free variables schedulable
c [ternres-4] 1909 ternary resolvents (91 bin, 1818 trn)
c [ternres-4] 3 variables remain 0% (11411 retained)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 599 at-most-one constraints of average size 3.2
c [card-3] found 90 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 686 out of 689 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 4463 xors of average arity 2.9
c [gauss-4] connected 13141 occurrences of 1095 variables (average 12.0)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-11] removed 67 variables
c [simpleprobe-3] 4519 schedulable variables 40%
c [simpleprobe-3] limit 13966608 penalty 0 = 0 + 0
c [decomp-12] removed 31 variables
c [simpleprobe-3] 307 variables remain 3% (11009 retained)
c [simpleprobe-3] removed 31 variables, found 2629 hbrs, 1 units
c [cgrclsr-3] limit 349165 penalty 0 = 0 + 0
c [cgrclsr-3] all 11316 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 1 variables
c [lift-4] limit 2094991 with penalty 0 = 0 + 0
c [lift-4] using 9039 probes 80%
c [lift-4] 5 units, 31 impls, 8 eqs in 1 rounds
c [lift-4] 8994 variables remain 80% (2308 retained)
c [lift-4] removed 13 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 2, lifted 0
c [unhide-3] limit 174582 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 374 tauts, 0 hbrs, 14975 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1063 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 11300 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 73 blocked clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 11293 variables 100%
c [elim-6] limit of 69833040 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 100 variables 1% in round 1 in 15729223 steps
c [elim-6-1] backward subsumption/strengthening limit 31458446
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 2689264 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 101 = 1% variables out of 11293
c [bca-5] limit of 10000000 steps
c [bca-5] 8879 out of 22386 literals actually usable 40%
c [bca-5] added 8 blocked clauses in 49054 steps
c [rephase-3] after 146177 conflicts (new increment 80000, next 226177)
c [flushphases] 0 phases reset
c [simplification-6] removed 222 variables 1.9% (11192 remain 23%)
c [simplification-6] removed 692 irredundant clauses 1.1% (62374 remain 43%)
c [simplification-6] maximum reduction of 2% = max (2%, 1%)
c [simplification-6] geometric conflict interval increment 22500 = 67500 / 3
c [simplification-6] new conflict interval 90000
c [simplification-6] penalized conflict interval 90000 = 1 * 90000
c [simplification-6] new conflict limit 236177
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   36.7   11192    62374    156817   26503  12694 20177  17  8.3 259.7   12
c i   36.7   11191    62374    157069   26733  12701 20180  12  8.3 259.5   13
c -   38.3   11191    62374    170635   28152  12833 20191  12  8.4 256.0   12
c -   39.3   11191    62374    184152   29250  12891 20200   7  8.7 257.8   17
c -   40.9   11191    62374    198966   30766  13024 20214   7  8.7 257.5   12
c i   41.8   11190    62374    209473   40265  13110 20220  13  8.8 257.9   14
c -   42.5   11190    62374    214455   32250  13164 20233   4  8.8 257.6   12
c i   44.3   11189    62374    228494   45315  13272 20247  13  8.7 254.3   14
c -   44.6   11189    62374    230399   34074  13293 20249  16  8.7 253.6   12
c 
c [simplification-7] limit of 236343 conflicts hit after 236345 conflicts
c [ternres-5] limit 5961771 with penalty 0 = 0 + 0
c [ternres-5] 3 schedulable variables 0%
c [ternres-5] 1831 ternary resolvents (28 bin, 1803 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 3725 xors of average arity 3.0
c [gauss-5] connected 11076 occurrences of 1008 variables (average 11.0)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 31 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 16682 literals 75%
c [treelook-3] scheduling used 300002 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 302345 steps
c [treelook-3] 16560 literals remain 74%
c [treelook-3] 10739 variables remain to probed next time 96%
c [decomp-14] removed 3 variables
c [treelook-3] removed 3 variables, found 253 hbrs
c [cgrclsr-4] limit 596177 penalty 0 = 0 + 0
c [cgrclsr-4] all 11155 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [cgrclsr-4] removed 4 variables
c [lift-5] limit 3577062 with penalty 0 = 0 + 0
c [lift-5] using 7966 probes 71%
c [lift-5] 5 units, 50 impls, 9 eqs in 1 rounds
c [lift-5] 7356 variables remain 66% (3781 retained)
c [lift-5] removed 14 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 1, lifted 0
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 766 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 11136 variables 100%
c [block-5] limit of 59617715 steps penalty 0 = 0 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 49 blocked clauses
c [block-5] 49 < 1/1000 * 62265 = 62 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 11131 variables 100%
c [elim-7] limit of 119235431 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 98 variables 1% in round 1 in 22109725 steps
c [elim-7-1] backward subsumption/strengthening limit 44219450
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 2650746 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 98 = 1% variables out of 11131
c [bca-6] limit of 10000000 steps
c [bca-6] 6591 out of 22068 literals actually usable 30%
c [bca-6] added 5 blocked clauses in 55014 steps
c [rephase-4] after 236345 conflicts (new increment 160000, next 396345)
c [flushphases] 0 phases reset
c [simplification-7] removed 156 variables 1.4% (11033 remain 22%)
c [simplification-7] removed 584 irredundant clauses 0.9% (61790 remain 43%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 45000 = 90000 / 2
c [simplification-7] new conflict interval 135000
c [simplification-7] penalized conflict interval 135000 = 1 * 135000
c [simplification-7] new conflict limit 371345
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   47.0   11033    61790    245981   34844  14246 20360  10  8.8 253.8   13
c -   47.7   11033    61790    261802   35882  14275 20362  28  9.0 255.1   13
c R   47.9   11033    61790    271040   44340  14279 20362  27  8.9 257.4   14
c -   49.1   11033    61790    278803   37004  14343 20372  10  8.9 257.5   13
c i   49.9   11032    61789    285699   43247  14410 20384   8  8.9 257.8   15
c -   51.1   11032    61789    297199   38799  14515 20397  22  9.0 256.7   19
c -   53.5   11032    61789    316242   40543  14690 20428  14  8.9 253.6   13
c -   55.4   11032    61789    335524   42022  14804 20442   9  9.1 251.7   19
c -   57.2   11032    61789    354741   43476  14890 20453  18  9.1 251.7   14
c i   58.4   11031    61788    362944   51017  14942 20461   8  9.1 250.9   15
c i   59.2   11030    61788    369519   57056  14983 20472   9  9.1 250.6   16
c 
c [simplification-8] limit of 371527 conflicts hit after 371527 conflicts
c [ternres-6] limit 9277321 with penalty 0 = 0 + 0
c [ternres-6] all 11030 free variables schedulable
c [ternres-6] 3504 ternary resolvents (130 bin, 3374 trn)
c [ternres-6] 1 variables remain 0% (11029 retained)
c [decomp-15] removed 40 variables
c [basicprobe-3] limit 9277321 penalty 0 = 0 + 0
c [basicprobe-3-0] 2705 sched 25%, 4 failed, 0 lifted, 1141 hbrs
c [decomp-16] removed 8 variables
c [basicprobe-3-1] 6301 sched 57%, 14 failed, 0 lifted, 1069 hbrs
c [decomp-17] removed 26 variables
c [basicprobe-3-2] 2530 probes remain 23% after last round
c [basicprobe-3-2] 18 units = 18 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 34 variables, found 2225 hbrs
c [bate-2] eliminated 12 asymmetric tautologies during probing
c [cgrclsr-5] limit 927732 penalty 0 = 0 + 0
c [cgrclsr-5] all 10959 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [cgrclsr-5] removed 8 variables
c [lift-6] limit 5566393 with penalty 0 = 0 + 0
c [lift-6] using 6342 probes 58%
c [lift-6] 0 units, 64 impls, 8 eqs in 1 rounds
c [lift-6] 4819 variables remain 44% (6124 retained)
c [lift-6] removed 8 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 838 transitive binary clauses
c [cce-4] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 16
c [cce-4-1] eliminated 1 clauses out of 18 (6%) of length 15
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 2 large clauses in 7500001 steps
c [cce-4-1] allowing another 3750000 steps for small clauses
c [cce-4] scheduling 27253 clauses = 11376 binary + 15877 ternary
c [cce-4] tried to eliminate 300 small clauses 1%
c [cce-4] eliminated 13 small clauses 0%
c [cce-4] eliminated 5 binary clauses 0%
c [cce-4] eliminated 8 ternary clauses 0%
c [cce-4-1] eliminated 13 small clauses in 7500001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 15 covered clauses in round 1
c [cce-4] eliminated 15 covered clauses in TOTAL during 1 rounds
c [cce-4] 15 < 1/1000 * 61564 = 61 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 10943 variables 100%
c [elim-8] limit of 185546434 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 58 variables 1% in round 1 in 21880555 steps
c [elim-8-1] backward subsumption/strengthening limit 43761110
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 2628611 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 58 = 1% variables out of 10943
c [bca-7] limit of 10000000 steps
c [bca-7] 4254 out of 21772 literals actually usable 20%
c [bca-7] added 2 blocked clauses in 67205 steps
c [simplification-8] removed 145 variables 1.3% (10885 remain 22%)
c [simplification-8] removed 551 irredundant clauses 0.9% (61237 remain 42%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 67500 = 135000 / 2
c [simplification-8] new conflict interval 202500
c [simplification-8] penalized conflict interval 202500 = 1 * 202500
c [simplification-8] new conflict limit 574027
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   62.4   10885    61237    375812   44615  16774 20841   9  9.1 249.7   15
c -   63.3   10885    61237    396562   45460  16810 20846  11  9.2 248.4   15
c -   66.4   10885    61236    417939   47271  16944 20870  13  9.2 246.3   15
c -   67.8   10885    61236    437915   48075  16962 20870  22 10.2 246.2   22
c -   69.6   10885    61236    460132   49823  17028 20874  38 10.1 245.0   15
c -   71.5   10885    61236    482602   51264  17093 20889  40 10.2 244.7   16
c -   73.8   10885    61236    506917   52594  17095 20889  38 10.1 243.8   23
c -   76.6   10885    61236    533530   53916  17097 20889  34 10.0 242.7   22
c -   78.5   10885    61236    558519   55412  17109 20889  36 10.1 242.0   23
c 
c [simplification-9] limit of 574091 conflicts hit after 574091 conflicts
c [ternres-7] limit 16225337 with penalty 0 = 0 + 0
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 414 ternary resolvents (1 bin, 413 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-6] limit 1622533 penalty 1 = 1 + 0
c [gauss-6] extracted 2519 xors of average arity 3.0
c [gauss-6] connected 7509 occurrences of 918 variables (average 8.2)
c [gauss-6] limit 1622533 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 20 variables
c [simpleprobe-4] 278 schedulable variables 3%
c [simpleprobe-4] limit 64901348 penalty 0 = 0 + 0
c [decomp-19] removed 8 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 8 variables, found 1962 hbrs, 1 units
c [cgrclsr-6] limit 1622533 penalty 0 = 0 + 0
c [cgrclsr-6] all 10857 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 14 variables
c [lift-7] limit 9735202 with penalty 0 = 0 + 0
c [lift-7] using 3918 probes 36%
c [lift-7-1] found 8 units 107 impls in round 1
c [lift-7] 8 units, 110 impls, 13 eqs in 2 rounds
c [lift-7] 848 variables remain 8% (9974 retained)
c [lift-7] removed 21 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1013 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 10822 variables 100%
c [block-6] limit of 81126685 steps penalty 1 = 1 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 123 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 10814 variables 100%
c [elim-9] limit of 324506742 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 55 variables 1% in round 1 in 21585990 steps
c [elim-9-1] backward subsumption/strengthening limit 43171980
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 2615953 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 55 = 1% variables out of 10814
c [bca-8] limit of 10000000 steps
c [bca-8] 5335 out of 21520 literals actually usable 25%
c [bca-8] added 8 blocked clauses in 81540 steps
c [rephase-5] after 574091 conflicts (new increment 320000, next 894091)
c [flushphases] 0 phases reset
c [simplification-9] removed 126 variables 1.2% (10759 remain 22%)
c [simplification-9] removed 508 irredundant clauses 0.8% (60728 remain 42%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 101250 = 202500 / 2
c [simplification-9] new conflict interval 303750
c [simplification-9] penalized conflict interval 303750 = 1 * 303750
c [simplification-9] new conflict limit 877841
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   81.5   10759    60728    583519   55969  16874 21452  21 10.2 242.8   16
c R   81.5   10759    60728    583582   56027  16875 21452  22 10.2 242.8   18
c -   84.9   10759    60728    609083   57660  17021 21462  38 10.2 240.9   16
c -   87.6   10759    60728    635023   58892  17100 21466  30 10.1 239.6   24
c -   90.7   10759    60728    661314   60193  17190 21477   8 10.1 236.3   16
c -   94.5   10759    60728    688380   61835  17310 21494   8 10.1 235.2   16
c -   96.2   10759    60728    715930   62984  17328 21495  34 10.2 234.4   17
c -   98.1   10759    60728    743548   63716  17332 21495  36 10.2 234.9   25
c -  100.2   10759    60728    771843   64551  17336 21495  34 10.2 235.5   25
c -  102.5   10759    60728    800378   65238  17337 21495  32 10.3 236.0   25
c -  104.9   10759    60728    829389   65903  17343 21495  36 10.4 236.5   25
c -  107.4   10759    60728    859019   66562  17346 21495  36 10.5 237.1   25
c 
c [simplification-10] limit of 877875 conflicts hit after 877875 conflicts
c [ternres-8] limit 28070022 with penalty 0 = 0 + 0
c [ternres-8] all 10759 free variables schedulable
c [ternres-8] 3872 ternary resolvents (157 bin, 3715 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1754376 penalty 3 = 3 + 0
c [card-4] found 821 at-most-one constraints of average size 3.2
c [card-4] found 123 at-most-two constraints of average size 4.1
c [card-4] using previous limit 1754376 for elimination
c [card-4] 942 out of 944 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-20] removed 41 variables
c [treelook-4] limit 1403501 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 21052 literals 98%
c [treelook-4] scheduling used 572776 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1403501 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1433768 steps
c [treelook-4] 20741 literals remain 97%
c [treelook-4] 10309 variables remain to probed next time 96%
c [decomp-21] removed 4 variables
c [treelook-4] removed 6 variables, found 630 hbrs
c [cgrclsr-7] limit 2807002 penalty 0 = 0 + 0
c [cgrclsr-7] all 10712 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [cgrclsr-7] removed 20 variables
c [lift-8] limit 16842013 with penalty 0 = 0 + 0
c [lift-8] using 30 probes 0%
c [lift-8-1] found 0 units 3 impls in round 1
c [lift-8-2] found 0 units 0 impls in round 2
c [lift-8-3] found 0 units 1 impls in round 3
c [lift-8-4] found 0 units 2 impls in round 4
c [lift-8-5] found 0 units 3 impls in round 5
c [lift-8] 0 units, 9 impls, 0 eqs in 6 rounds
c [lift-8] 813 variables remain 8% (9879 retained)
c [cliff-7] limit of 11228009 steps penalty 1 = 1 + 0
c [cliff-7] failed 0, lifted 0
c [unhide-4] limit 701750 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 3 failed, 3630 tauts, 0 hbrs, 49573 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 569 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 10691 variables 100%
c [block-7] limit of 280700226 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 40 blocked clauses
c [block-7] 40 < 1/1000 * 60639 = 60 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 10690 variables 100%
c [elim-10] limit of 561400453 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 49 variables 0% in round 1 in 27965483 steps
c [elim-10-1] backward subsumption/strengthening limit 55930966
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 2581957 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 49 = 0% variables out of 10690
c [bca-9] limit of 10000000 steps
c [bca-9] 4365 out of 21284 literals actually usable 21%
c [bca-9] added 1 blocked clauses in 93108 steps
c [simplification-10] removed 118 variables 1.1% (10641 remain 22%)
c [simplification-10] removed 464 irredundant clauses 0.8% (60264 remain 42%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 151875 = 303750 / 2
c [simplification-10] new conflict interval 455625
c [simplification-10] penalized conflict interval 455625 = 1 * 455625
c [simplification-10] new conflict limit 1333500
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  111.6   10640    60264    883033   87715  19260 18879   6 10.6 237.1   23
c -  112.7   10640    60264    889130   66432  19301 18886  11 10.6 236.7   18
c -  116.7   10640    60264    920724   68375  19397 18897  13 10.5 235.3   26
c i  118.5   10639    60264    933304   80055  19451 18901  12 10.5 234.6   20
c i  118.5   10638    60264    933305   80055  19451 18901  12 10.5 234.6   20
c i  118.5   10637    60264    933347   80080  19452 18907  10 10.5 234.6   20
c -  120.9   10637    60264    952957   70158  19461 18907  13 10.5 234.0   17
c -  124.2   10637    60264    983772   71487  19504 18909  39 10.7 233.7   25
c -  127.1   10637    60264   1013980   72168  19506 18909  36 10.9 233.8   25
c -  130.0   10637    60264   1045139   73051  19508 18909  39 11.2 233.9   25
c -  132.9   10637    60264   1076698   73726  19510 18909  40 11.5 234.0   25
c -  136.0   10637    60264   1108715   74477  19510 18909  38 11.7 234.1   25
c -  139.2   10637    60264   1141239   75119  19510 18909  38 11.9 234.2   25
c -  142.4   10637    60264   1174218   75755  19509 18910  40 12.1 234.3   25
c -  146.3   10637    60264   1207971   76636  19510 18910  36 12.4 234.4   25
c -  150.0   10637    60264   1242032   77439  19511 18910  40 12.6 234.5   25
c -  153.7   10637    60264   1276621   78192  19512 18910  38 12.8 234.6   25
c -  157.4   10637    60264   1312021   78954  19514 18910  37 13.0 234.7   25
c 
c [simplification-11] limit of 1333608 conflicts hit after 1333608 conflicts
c [ternres-9] limit 53219445 with penalty 0 = 0 + 0
c [ternres-9] all 10637 free variables schedulable
c [ternres-9] 2235 ternary resolvents (130 bin, 2105 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-22] removed 33 variables
c [basicprobe-4] limit 53219445 penalty 0 = 0 + 0
c [basicprobe-4-0] 2524 sched 24%, 11 failed, 0 lifted, 572 hbrs
c [decomp-23] removed 17 variables
c [basicprobe-4-1] 6078 sched 57%, 9 failed, 0 lifted, 466 hbrs
c [decomp-24] removed 15 variables
c [basicprobe-4-2] 6061 sched 57%, 0 failed, 0 lifted, 39 hbrs
c [basicprobe-4-3] 6061 sched 57%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-4] 6061 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-5] 6061 sched 57%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-6] 6059 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-7] 6059 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-8] 6059 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-9] 6059 sched 57%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-9] round limit 9 hit
c [basicprobe-4-9] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-4-9] removed 32 variables, found 1097 hbrs
c [bate-3] eliminated 7 asymmetric tautologies during probing
c [cgrclsr-8] limit 5321944 penalty 0 = 0 + 0
c [cgrclsr-8] all 10576 free variables schedulable
c [cgrclsr-8] fully completed congruence closure
c [cgrclsr-8] removed 10 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 529 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 10566 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 8 variables 0% in round 1 in 20933812 steps
c [elim-11-1] backward subsumption/strengthening limit 41867624
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 2572479 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 8 = 0% variables out of 10566
c [elim-11] 8 < 1/1000 * 10566 = 10 considered unsuccessful
c [bca-10] limit of 10000000 steps
c [bca-10] 3804 out of 21118 literals actually usable 18%
c [bca-10] added 1 blocked clauses in 108501 steps
c [rephase-6] after 1333608 conflicts (new increment 640000, next 1973608)
c [flushphases] 0 phases reset
c [simplification-11] removed 79 variables 0.7% (10558 remain 21%)
c [simplification-11] removed 257 irredundant clauses 0.4% (60007 remain 42%)
c [simplification-11] maximum reduction of 1% = max (1%, 0%)
c [simplification-11] geometric conflict interval increment 227812 = 455625 / 2
c [simplification-11] new conflict interval 683437
c [simplification-11] penalized conflict interval 683437 = 1 * 683437
c [simplification-11] new conflict limit 2017045
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  165.0   10558    60007   1349052   79913  20538 19030  38 13.0 234.3   20
c -  170.2   10558    60007   1389396   81534  20605 19037  13 13.0 232.7   29
c -  175.4   10558    60007   1430321   83180  20648 19045  38 12.9 232.3   29
c -  181.4   10558    60007   1470966   85331  20780 19057  19 12.8 230.3   20
c -  184.3   10558    60007   1512818   86964  20872 19077  39 12.7 229.7   20
c -  188.7   10558    60007   1554613   87753  20876 19077  37 12.7 230.6   30
c -  193.1   10558    60007   1598272   88582  20876 19077  34 12.7 231.4   30
c -  197.5   10558    60007   1645264   89295  20878 19077  36 12.6 232.0   30
c -  202.2   10558    60007   1691958   89997  20882 19078  34 12.6 232.5   30
c -  207.1   10558    60007   1737854   90639  20884 19078  35 12.7 233.1   30
c -  212.3   10558    60007   1788404   91397  20886 19078  39 12.6 233.7   30
c -  217.2   10558    60007   1841162   92023  20886 19078  37 12.7 234.3   30
c -  222.4   10558    60007   1896308   92627  20886 19078  35 12.7 234.8   30
c -  227.6   10558    60007   1950127   93275  20887 19078  36 12.7 235.3   30
c -  232.6   10558    60007   1996577   94473  20957 19084  35 12.6 233.3   30
c 
c [simplification-12] limit of 2017097 conflicts hit after 2017097 conflicts
c [ternres-10] limit 93411483 with penalty 0 = 0 + 0
c [ternres-10] all 10558 free variables schedulable
c [ternres-10] 1606 ternary resolvents (106 bin, 1500 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-7] limit 4670574 penalty 2 = 2 + 0
c [gauss-7] extracted 4458 xors of average arity 3.1
c [gauss-7] connected 13762 occurrences of 970 variables (average 14.2)
c [gauss-7] limit 4670574 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-32] removed 18 variables
c [simpleprobe-5] all 10540 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-33] removed 6 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 6 variables, found 1906 hbrs, 1 units
c [cgrclsr-9] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-9] all 10534 free variables schedulable
c [cgrclsr-9] fully completed congruence closure
c [cgrclsr-9] removed 14 variables
c [lift-9] limit 10000000 with penalty 1 = 1 + 0
c [lift-9] using 40 probes 0%
c [lift-9-1] found 0 units 1 impls in round 1
c [lift-9-2] found 0 units 1 impls in round 2
c [lift-9-3] found 0 units 1 impls in round 3
c [lift-9-4] found 1 units 3 impls in round 4
c [lift-9-5] found 0 units 0 impls in round 5
c [lift-9] 1 units, 6 impls, 1 eqs in 6 rounds
c [lift-9] 757 variables remain 7% (9761 retained)
c [lift-9] removed 2 variables
c [unhide-5] limit 4670574 with penalty 2 = 2 + 0
c [unhide-5-7] 0 units, 0 failed, 3808 tauts, 0 hbrs, 75928 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 605 transitive binary clauses
c [transred-10] found 1 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 10517 variables 100%
c [block-8] limit of 400000000 steps penalty 1 = 1 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 24 blocked clauses
c [block-8] 24 < 1/1000 * 59937 = 59 considered unsuccessful
c [cce-5] limit of 23352870 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 1 clauses out of 104 (1%) of length 13
c [cce-5-1] eliminated 14 clauses out of 140 (10%) of length 11
c [cce-5-1] eliminated 2 clauses out of 249 (1%) of length 10
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 17 large clauses in 23352871 steps
c [cce-5-1] allowing another 11676435 steps for small clauses
c [cce-5] scheduling 18897 clauses = 11061 binary + 7836 ternary
c [cce-5] tried to eliminate 2332 small clauses 12%
c [cce-5] eliminated 68 small clauses 0%
c [cce-5] eliminated 46 binary clauses 0%
c [cce-5] eliminated 22 ternary clauses 0%
c [cce-5-1] eliminated 68 small clauses in 23352871 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 85 covered clauses in round 1
c [cce-5] eliminated 85 covered clauses in TOTAL during 1 rounds
c [bca-11] limit of 10000000 steps
c [bca-11] 3452 out of 21032 literals actually usable 16%
c [bca-11] added 1 blocked clauses in 120010 steps
c [rephase-7] after 2017097 conflicts (new increment 1280000, next 3297097)
c [flushphases] 0 phases reset
c [simplification-12] removed 43 variables 0.4% (10515 remain 21%)
c [simplification-12] removed 182 irredundant clauses 0.3% (59825 remain 41%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 683437
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 3017097
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  242.3   10515    59825   2043027   94899  21090 18716  34 12.6 231.8   30
c -  247.7   10515    59825   2090578   96398  21113 18717  29 12.5 230.8   30
c -  253.5   10515    59825   2137453   97794  21131 18719  20 12.5 229.6   30
c -  259.9   10515    59825   2191091   99145  21164 18721  38 12.4 227.3   30
c -  267.4   10515    59825   2256523   99891  21180 18723  39 12.3 225.8   30
c -  274.5   10515    59822   2307820  101293  21206 18728  33 12.3 224.7   30
c -  281.3   10515    59817   2359020  102788  21254 18735  35 12.2 223.5   21
c -  285.3   10515    59816   2410959  104224  21285 18745  21 12.2 223.3   31
c i  286.1   10514    59816   2422972  115534  21317 18752  11 12.2 223.5   36
c -  290.8   10514    59816   2466814  105909  21321 18755  25 12.1 222.8   31
c -  296.5   10514    59814   2520387  107519  21324 18756  35 12.1 222.3   31
c -  302.5   10514    59814   2569986  108566  21328 18756  20 12.2 221.9   31
c -  309.1   10514    59814   2619355  109545  21334 18756  33 12.3 221.9   31
c -  316.7   10514    59814   2669468  110368  21337 18756  37 12.4 221.8   31
c -  323.5   10514    59814   2720886  111025  21338 18756  41 12.5 221.5   31
c -  330.3   10514    59814   2773332  111762  21340 18756  37 12.5 221.1   31
c -  337.6   10514    59814   2827348  112444  21340 18756  36 12.6 220.6   34
c -  344.7   10514    59814   2880955  113152  21341 18756  33 12.7 220.0   31
c i  349.2   10513    59814   2917874  137919  21402 18770  34 12.6 219.2   38
c i  352.5   10475    59813   2943253  161242  21421 18788  18 12.6 218.5   40
c i  353.2   10473    59813   2946132  163930  21453 18798  10 12.6 218.3   40
c i  353.5   10472    59813   2946793  164544  21457 18802  12 12.6 218.3   40
c -  353.7   10472    59813   2947740  115440  21457 18802  18 12.6 218.2   31
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  358.2   10471    59813   2973461  139488  21517 18821  12 12.6 217.3   37
c -  363.0   10471    59813   3004188  117851  21558 18837  36 12.5 216.5   22
c 
c [simplification-13] limit of 3017371 conflicts hit after 3017372 conflicts
c [ternres-11] limit 164162259 with penalty 0 = 0 + 0
c [ternres-11] all 10471 free variables schedulable
c [ternres-11] 1345 ternary resolvents (111 bin, 1234 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-34] removed 312 variables
c [treelook-5] limit 8208112 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 20054 literals 98%
c [treelook-5] scheduling used 626649 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 8208112 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 8213200 steps
c [treelook-5] 18399 literals remain 90%
c [treelook-5] 9790 variables remain to probed next time 96%
c [decomp-35] removed 62 variables
c [treelook-5] removed 71 variables, found 21562 hbrs
c [cgrclsr-10] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-10] all 10132 free variables schedulable
c [cgrclsr-10] fully completed congruence closure
c [cgrclsr-10] removed 74 variables
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 107 probes 1%
c [lift-10-1] found 0 units 5 impls in round 1
c [lift-10-2] found 0 units 6 impls in round 2
c [lift-10-3] found 0 units 2 impls in round 3
c [lift-10-4] found 0 units 5 impls in round 4
c [lift-10-5] found 0 units 3 impls in round 5
c [lift-10] 0 units, 21 impls, 4 eqs in 6 rounds
c [lift-10] 637 variables remain 6% (9417 retained)
c [lift-10] removed 4 variables
c [cliff-8] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-8] failed 0, lifted 0
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1947 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 10054 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12-1] eliminated 338 variables 3% in round 1 in 22813054 steps
c [elim-12-1] backward subsumption/strengthening limit 45626108
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 2484793 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 338 = 3% variables out of 10054
c [bca-12] limit of 10000000 steps
c [bca-12] 3919 out of 19434 literals actually usable 20%
c [bca-12] added 17 blocked clauses in 120502 steps
c [simplification-13] removed 755 variables 7.2% (9716 remain 20%)
c [simplification-13] removed 3505 irredundant clauses 5.9% (56308 remain 39%)
c [simplification-13] maximum reduction of 7% = max (7%, 6%)
c [simplification-13] large reduction 7% >= 5% limit
c [simplification-13] new conflict interval 30173 = min (3017372/100, 1000000)
c [simplification-13] penalized conflict interval 30173 = 1 * 30173
c [simplification-13] new conflict limit 3047545
c 
c [simplification-14] limit of 3047545 conflicts hit after 3047545 conflicts
c [ternres-12] limit 166076283 with penalty 0 = 0 + 0
c [ternres-12] all 9716 free variables schedulable
c [ternres-12] 1241 ternary resolvents (94 bin, 1147 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-8] limit 16607628 penalty 1 = 1 + 0
c [gauss-8] extracted 4052 xors of average arity 3.1
c [gauss-8] connected 12498 occurrences of 870 variables (average 14.4)
c [gauss-8] limit 16607628 penalty 1 = 1 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 24 variables
c [basicprobe-5] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 5436 sched 56%, 8 failed, 0 lifted, 542 hbrs
c [decomp-37] removed 15 variables
c [basicprobe-5-1] 5413 sched 56%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-5-2] 5413 sched 56%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-5-3] 5413 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 15 variables, found 575 hbrs
c [bate-4] eliminated 51 asymmetric tautologies during probing
c [cgrclsr-11] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-11] all 9677 free variables schedulable
c [cgrclsr-11] fully completed congruence closure
c [cgrclsr-11] removed 16 variables
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 1 probes 0%
c [lift-11-1] found 0 units 0 impls in round 1
c [lift-11-2] found 0 units 0 impls in round 2
c [lift-11-3] found 0 units 0 impls in round 3
c [lift-11-4] found 0 units 0 impls in round 4
c [lift-11-5] found 0 units 0 impls in round 5
c [lift-11] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-11] 601 variables remain 6% (9060 retained)
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1143 transitive binary clauses
c [cce-6] limit of 83038141 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 1 clauses out of 26 (4%) of length 17
c [cce-6-1] eliminated 2 clauses out of 14 (14%) of length 14
c [cce-6-1] eliminated 1 clauses out of 114 (1%) of length 13
c [cce-6-1] eliminated 2 clauses out of 66 (3%) of length 12
c [cce-6-1] eliminated 4 clauses out of 127 (3%) of length 11
c [cce-6-1] eliminated 32 clauses out of 256 (12%) of length 10
c [cce-6-1] eliminated 22 clauses out of 451 (5%) of length 9
c [cce-6-1] eliminated 42 clauses out of 690 (6%) of length 8
c [cce-6-1] eliminated 41 clauses out of 1379 (3%) of length 7
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 147 large clauses in 83038142 steps
c [cce-6-1] allowing another 41519071 steps for small clauses
c [cce-6] scheduling 18243 clauses = 10628 binary + 7615 ternary
c [cce-6] tried to eliminate 8594 small clauses 47%
c [cce-6] eliminated 389 small clauses 2%
c [cce-6] eliminated 180 binary clauses 2%
c [cce-6] eliminated 209 ternary clauses 3%
c [cce-6-1] eliminated 389 small clauses in 83038142 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 536 covered clauses in round 1
c [cce-6] eliminated 536 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 9661 variables 100%
c [elim-13] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 91 variables 1% in round 1 in 16504419 steps
c [elim-13-1] backward subsumption/strengthening limit 33008838
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 2410352 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 91 = 1% variables out of 9661
c [bca-13] limit of 10000000 steps
c [bca-13] 3554 out of 19142 literals actually usable 19%
c [bca-13] added 6 blocked clauses in 147092 steps
c [simplification-14] removed 146 variables 1.5% (9570 remain 19%)
c [simplification-14] removed 980 irredundant clauses 1.7% (55328 remain 38%)
c [simplification-14] maximum reduction of 2% = max (2%, 2%)
c [simplification-14] geometric conflict interval increment 333333 = 1000000 / 3
c [simplification-14] conflict interval soft limit 1000000 reached
c [simplification-14] new conflict interval 1000000
c [simplification-14] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-14] new conflict limit 4047545
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  380.4    9570    55328   3070490  109518  18229 35332  10 12.5 216.1   36
c i  381.1    9569    55328   3074446  113253  18244 35333  16 12.5 216.0   37
c i  383.5    9568    55328   3087226  125324  18282 35345  16 12.5 215.6   38
c i  384.5    9567    55328   3092780  130514  18302 35351  11 12.5 215.6   39
c -  391.7    9567    55328   3128465  112378  18385 35369  15 12.5 214.3   26
c i  392.2    9566    55327   3130519  114322  18390 35372  15 12.5 214.1   27
c -  401.9    9566    55327   3187076  115012  18500 35396  30 12.4 212.6   37
c -  408.7    9566    55327   3247137  116746  18505 35397  29 12.6 211.8   35
c -  420.2    9566    55324   3306515  119501  18627 35430  28 12.6 210.0   35
c -  432.2    9566    55322   3365949  121916  18728 35451  18 12.5 208.2   24
c -  442.1    9566    55322   3426983  123486  18778 35455  38 12.5 207.6   37
c -  453.0    9566    55321   3489418  125812  18853 35469  30 12.5 206.3   37
c -  464.5    9566    55321   3549493  127834  18883 35475  12 12.5 205.7   37
c i  471.2    9565    55321   3582626  159273  18912 35477  17 12.5 204.8   47
c -  478.1    9565    55321   3610718  130394  18950 35483  24 12.5 203.9   37
c -  492.2    9565    55321   3673164  132540  19017 35497  34 12.5 202.1   37
c -  506.1    9565    55321   3736044  134686  19060 35501  19 12.4 200.3   37
c -  515.2    9565    55320   3797300  136015  19082 35504  34 12.5 199.7   37
c -  523.1    9565    55320   3857781  136570  19082 35504  38 12.6 199.3   41
c -  530.0    9565    55320   3922085  137225  19082 35504  37 12.9 199.0   37
c -  540.3    9565    55319   3986050  138660  19114 35507  37 12.9 197.9   37
c 
c [simplification-15] limit of 4047821 conflicts hit after 4047821 conflicts
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 9565 free variables schedulable
c [ternres-13] 1713 ternary resolvents (90 bin, 1623 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 7423039 penalty 4 = 4 + 0
c [card-5] found 820 at-most-one constraints of average size 3.1
c [card-5] found 116 at-most-two constraints of average size 4.0
c [card-5] using previous limit 7423039 for elimination
c [card-5] 935 out of 936 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-40] removed 79 variables
c [simpleprobe-6] all 9491 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-41] removed 43 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 43 variables, found 6135 hbrs, 4 units
c [cgrclsr-12] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-12] all 9448 free variables schedulable
c [cgrclsr-12] fully completed congruence closure
c [cgrclsr-12] removed 17 variables
c [unhide-6] limit 2500000 with penalty 3 = 3 + 0
c [unhide-6-8] 0 units, 0 failed, 9982 tauts, 0 hbrs, 138532 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1031 transitive binary clauses
c [transred-13] found 2 units
c [block-9] scheduling all variables this time
c [block-9] scheduled 9429 variables 100%
c [block-9] limit of 200000000 steps penalty 2 = 2 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 206 blocked clauses
c [cce-7] limit of 237537253 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 62 (2%) of length 12
c [cce-7-1] eliminated 1 clauses out of 119 (1%) of length 11
c [cce-7-1] eliminated 6 clauses out of 223 (3%) of length 10
c [cce-7-1] eliminated 1 clauses out of 423 (0%) of length 9
c [cce-7-1] eliminated 11 clauses out of 624 (2%) of length 8
c [cce-7-1] eliminated 92 clauses out of 1331 (7%) of length 7
c [cce-7-1] eliminated 266 clauses out of 2668 (10%) of length 6
c [cce-7-1] eliminated 622 clauses out of 5600 (11%) of length 5
c [cce-7-1] eliminated 379 clauses out of 12687 (3%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 1379 large clauses in 237537254 steps
c [cce-7-1] allowing another 118768627 steps for small clauses
c [cce-7] scheduling 23397 clauses = 10227 binary + 13170 ternary
c [cce-7] tried to eliminate 15732 small clauses 67%
c [cce-7] eliminated 696 small clauses 3%
c [cce-7] eliminated 137 binary clauses 1%
c [cce-7] eliminated 559 ternary clauses 4%
c [cce-7-1] eliminated 696 small clauses in 237537254 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 2075 covered clauses in round 1
c [cce-7] eliminated 2075 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 9409 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 302 variables 3% in round 1 in 18090685 steps
c [elim-14-1] backward subsumption/strengthening limit 36181370
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 2242927 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 302 = 3% variables out of 9409
c [bca-14] limit of 10000000 steps
c [bca-14] 2414 out of 18216 literals actually usable 13%
c [bca-14] added 14 blocked clauses in 194922 steps
c [rephase-8] after 4047821 conflicts (new increment 2560000, next 6607821)
c [flushphases] 0 phases reset
c [simplification-15] removed 458 variables 4.8% (9107 remain 18%)
c [simplification-15] removed 3359 irredundant clauses 6.1% (51960 remain 36%)
c [simplification-15] maximum reduction of 6% = max (5%, 6%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] new conflict interval 40478 = min (4047821/100, 1000000)
c [simplification-15] penalized conflict interval 40478 = 1 * 40478
c [simplification-15] new conflict limit 4088299
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  565.1    9107    51960   4054519  136780  18406 29107  12 12.8 196.4   29
c 
c [simplification-16] limit of 4088301 conflicts hit after 4088303 conflicts
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] all 9107 free variables schedulable
c [ternres-14] 1461 ternary resolvents (82 bin, 1379 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-42] removed 8 variables
c [treelook-6] limit 12029412 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 17905 literals 98%
c [treelook-6] scheduling used 774211 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 12029412 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 12037679 steps
c [treelook-6] 15209 literals remain 84%
c [treelook-6] 8675 variables remain to probed next time 95%
c [decomp-43] removed 7 variables
c [treelook-6] removed 9 variables, found 6358 hbrs
c [cgrclsr-13] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-13] all 9090 free variables schedulable
c [cgrclsr-13] fully completed congruence closure
c [lift-12] limit 10000000 with penalty 1 = 1 + 0
c [lift-12] using 33 probes 0%
c [lift-12-1] found 0 units 3 impls in round 1
c [lift-12-2] found 0 units 1 impls in round 2
c [lift-12-3] found 0 units 0 impls in round 3
c [lift-12-4] found 0 units 2 impls in round 4
c [lift-12-5] found 0 units 0 impls in round 5
c [lift-12] 0 units, 6 impls, 0 eqs in 6 rounds
c [lift-12] 516 variables remain 6% (8574 retained)
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1124 transitive binary clauses
c [cce-8] limit of 481176502 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 13 (8%) of length 14
c [cce-8-1] eliminated 1 clauses out of 69 (1%) of length 12
c [cce-8-1] eliminated 1 clauses out of 111 (1%) of length 11
c [cce-8-1] eliminated 3 clauses out of 235 (1%) of length 10
c [cce-8-1] eliminated 7 clauses out of 440 (2%) of length 9
c [cce-8-1] eliminated 12 clauses out of 626 (2%) of length 8
c [cce-8-1] eliminated 27 clauses out of 1300 (2%) of length 7
c [cce-8-1] eliminated 73 clauses out of 2556 (3%) of length 6
c [cce-8-1] eliminated 121 clauses out of 5023 (2%) of length 5
c [cce-8-1] eliminated 668 clauses out of 12280 (5%) of length 4
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] eliminated 914 large clauses in 428267843 steps
c [cce-8-1] allowing another 214133921 steps for small clauses
c [cce-8] scheduling 21772 clauses = 9736 binary + 12036 ternary
c [cce-8] tried to eliminate 21772 small clauses 100%
c [cce-8] eliminated 319 small clauses 1%
c [cce-8] eliminated 85 binary clauses 1%
c [cce-8] eliminated 234 ternary clauses 2%
c [cce-8-1] eliminated 319 small clauses in 373451954 steps
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 1233 covered clauses in round 1
c [cce-8-2] completed large round (ACCE)
c [cce-8-2] allowing another 0 steps for small clauses
c [cce-8] scheduling 21453 clauses = 9651 binary + 11802 ternary
c [cce-8] tried to eliminate 14383 small clauses 67%
c [cce-8] eliminated 8 small clauses 0%
c [cce-8] eliminated 7 binary clauses 0%
c [cce-8] eliminated 1 ternary clauses 0%
c [cce-8-2] eliminated 8 small clauses in 107724549 steps
c [cce-8-2] incomplete small round (ACCE)
c [cce-8-2] eliminated 8 covered clauses in round 2
c [cce-8] eliminated 1241 covered clauses in TOTAL during 2 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 9090 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 164 variables 2% in round 1 in 13881507 steps
c [elim-15-1] backward subsumption/strengthening limit 27763014
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 2145214 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 164 = 2% variables out of 9090
c [bca-15] limit of 10000000 steps
c [bca-15] 2300 out of 17854 literals actually usable 13%
c [bca-15] added 1 blocked clauses in 170966 steps
c [simplification-16] removed 181 variables 2.0% (8926 remain 18%)
c [simplification-16] removed 1549 irredundant clauses 3.0% (50411 remain 35%)
c [simplification-16] maximum reduction of 3% = max (2%, 3%)
c [simplification-16] geometric conflict interval increment 250000 = 1000000 / 4
c [simplification-16] conflict interval soft limit 1000000 reached
c [simplification-16] new conflict interval 1000000
c [simplification-16] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-16] new conflict limit 5088303
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  599.4    8926    50411   4122038  138382  19530 33667  27 12.8 194.7   41
c -  611.7    8926    50411   4189311  139388  19534 33667  31 13.0 194.3   41
c -  628.8    8926    50411   4256371  141667  19585 33674  18 13.0 192.3   41
c -  639.9    8926    50411   4323568  143255  19604 33675  20 13.0 191.4   41
c -  652.1    8926    50411   4389850  144767  19622 33677  32 13.0 190.3   41
c -  662.8    8926    50411   4457556  145746  19624 33677  34 13.0 189.9   41
c -  671.0    8926    50411   4523030  146521  19624 33677  39 13.1 189.5   41
c -  679.9    8926    50411   4588764  147147  19624 33677  37 13.2 189.1   69
c -  689.1    8926    50411   4654856  147859  19624 33677  32 13.3 188.7   65
c -  697.6    8926    50411   4721864  148534  19624 33677  34 13.4 188.3   65
c -  708.2    8926    50411   4791129  149337  19626 33678  18 13.6 187.8   65
c -  722.2    8926    50411   4863785  151001  19651 33679  38 13.5 186.7   65
c -  733.3    8926    50411   4940362  153438  19651 33680  36 13.5 186.2   65
c -  746.2    8926    50411   5014280  155330  19655 33680  33 13.5 185.7   65
c -  760.8    8926    50411   5083108  156245  19657 33680  34 13.6 185.6   65
c 
c [simplification-17] limit of 5088327 conflicts hit after 5088328 conflicts
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 8926 free variables schedulable
c [ternres-15] 234 ternary resolvents (51 bin, 183 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-9] limit 12500000 penalty 2 = 2 + 0
c [gauss-9] extracted 3675 xors of average arity 3.1
c [gauss-9] connected 11445 occurrences of 766 variables (average 14.9)
c [gauss-9] limit 12500000 penalty 2 = 2 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-44] removed 3 variables
c [basicprobe-6] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 5013 sched 56%, 9 failed, 0 lifted, 890 hbrs
c [decomp-45] removed 10 variables
c [basicprobe-6-1] 5000 sched 56%, 2 failed, 0 lifted, 55 hbrs
c [decomp-46] removed 2 variables
c [basicprobe-6-2] 4998 sched 56%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-3] 4999 sched 56%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-6-4] 4999 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-4] fully completed probing
c [basicprobe-6-4] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-6-4] removed 12 variables, found 952 hbrs
c [bate-5] eliminated 6 asymmetric tautologies during probing
c [cliff-9] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-9] failed 0, lifted 0
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1023 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 8911 variables 100%
c [block-10] limit of 400000000 steps penalty 1 = 1 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 94 blocked clauses
c [cce-9] limit of 676056783 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 16
c [cce-9-1] eliminated 2 clauses out of 243 (1%) of length 10
c [cce-9-1] eliminated 3 clauses out of 446 (1%) of length 9
c [cce-9-1] eliminated 8 clauses out of 592 (1%) of length 8
c [cce-9-1] eliminated 21 clauses out of 1327 (2%) of length 7
c [cce-9-1] eliminated 27 clauses out of 2518 (1%) of length 6
c [cce-9-1] eliminated 48 clauses out of 4935 (1%) of length 5
c [cce-9-1] eliminated 58 clauses out of 11629 (0%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 168 large clauses in 370425581 steps
c [cce-9-1] allowing another 185212790 steps for small clauses
c [cce-9] scheduling 16712 clauses = 9502 binary + 7210 ternary
c [cce-9] tried to eliminate 16712 small clauses 100%
c [cce-9] eliminated 223 small clauses 1%
c [cce-9] eliminated 51 binary clauses 1%
c [cce-9] eliminated 172 ternary clauses 2%
c [cce-9-1] eliminated 223 small clauses in 263431790 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 391 covered clauses in round 1
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] allowing another 0 steps for small clauses
c [cce-9] scheduling 16489 clauses = 9451 binary + 7038 ternary
c [cce-9] tried to eliminate 16489 small clauses 100%
c [cce-9] eliminated 2 small clauses 0%
c [cce-9] eliminated 1 binary clauses 0%
c [cce-9] eliminated 1 ternary clauses 0%
c [cce-9-2] eliminated 2 small clauses in 77367251 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 2 covered clauses in round 2
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] allowing another 0 steps for small clauses
c [cce-9] scheduling 16487 clauses = 9450 binary + 7037 ternary
c [cce-9] tried to eliminate 16487 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 393 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 8907 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 49 variables 1% in round 1 in 13336900 steps
c [elim-16-1] backward subsumption/strengthening limit 26673800
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 2104971 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 49 = 1% variables out of 8907
c [bca-16] limit of 10000000 steps
c [bca-16] 2374 out of 17718 literals actually usable 13%
c [bca-16] added 0 blocked clauses in 164634 steps
c [simplification-17] removed 68 variables 0.8% (8858 remain 18%)
c [simplification-17] removed 599 irredundant clauses 1.2% (49812 remain 35%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] new conflict limit 6088328
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  797.6    8858    49812   5157525  157161  19822 33356  27 13.6 185.0   43
c -  807.1    8858    49812   5234100  158552  19829 33356  27 13.7 184.5   43
c -  816.6    8858    49812   5308133  159414  19842 33356  37 13.8 184.0   43
c -  826.9    8858    49812   5384873  160270  19843 33356  35 14.0 183.5   43
c -  839.6    8858    49812   5479918  160941  19843 33357  38 14.4 182.9   48
c -  849.5    8858    49812   5554388  161579  19843 33357  38 14.5 182.5   48
c -  861.2    8858    49812   5636838  162168  19843 33357  29 14.7 182.0   48
c -  873.5    8858    49812   5713277  163242  19852 33359  34 14.7 181.6   43
c -  883.8    8858    49812   5787046  163763  19852 33359  35 14.8 181.5   48
c -  894.6    8858    49812   5861795  164310  19852 33359  32 14.9 181.3   71
c -  905.7    8858    49812   5936895  164882  19853 33359  36 15.0 181.2   71
c -  916.5    8858    49812   6012954  165441  19853 33359  34 15.0 181.0   71
c 
c [simplification-18] limit of 6088334 conflicts hit after 6088335 conflicts
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 8858 free variables schedulable
c [ternres-16] 160 ternary resolvents (45 bin, 115 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-49] removed 1 variables
c [simpleprobe-7] all 8857 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 0 variables, found 3894 hbrs, 0 units
c [cgrclsr-14] limit 4000000 penalty 1 = 1 + 0
c [cgrclsr-14] all 8857 free variables schedulable
c [cgrclsr-14] fully completed congruence closure
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1062 transitive binary clauses
c [block-11] scheduling all variables this time
c [block-11] scheduled 8857 variables 100%
c [block-11] limit of 800000000 steps penalty 0 = 0 + 0
c [block-11] fully completed
c [block-11] transition to [ all 0 rem 0 ] state
c [block-11] eliminated 0 blocked clauses
c [cce-10] limit of 880998827 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 98 (1%) of length 11
c [cce-10-1] eliminated 1 clauses out of 448 (0%) of length 9
c [cce-10-1] eliminated 9 clauses out of 586 (2%) of length 8
c [cce-10-1] eliminated 5 clauses out of 1317 (0%) of length 7
c [cce-10-1] eliminated 8 clauses out of 2507 (0%) of length 6
c [cce-10-1] eliminated 1 clauses out of 4878 (0%) of length 5
c [cce-10-1] eliminated 13 clauses out of 11578 (0%) of length 4
c [cce-10-1] completed large round (ACCE)
c [cce-10-1] eliminated 38 large clauses in 381851288 steps
c [cce-10-1] allowing another 190925644 steps for small clauses
c [cce-10] scheduling 20910 clauses = 9419 binary + 11491 ternary
c [cce-10] tried to eliminate 20910 small clauses 100%
c [cce-10] eliminated 30 small clauses 0%
c [cce-10] eliminated 10 binary clauses 0%
c [cce-10] eliminated 20 ternary clauses 0%
c [cce-10-1] eliminated 30 small clauses in 337174132 steps
c [cce-10-1] completed small round (ACCE)
c [cce-10-1] eliminated 68 covered clauses in round 1
c [cce-10-2] completed large round (ACCE)
c [cce-10-2] allowing another 0 steps for small clauses
c [cce-10] scheduling 20880 clauses = 9409 binary + 11471 ternary
c [cce-10] tried to eliminate 20880 small clauses 100%
c [cce-10-2] completed small round (ACCE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 68 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 8857 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 7 variables 0% in round 1 in 12789932 steps
c [elim-17-1] backward subsumption/strengthening limit 25579864
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 2099696 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 7 = 0% variables out of 8857
c [elim-17] 7 < 1/1000 * 8857 = 8 considered unsuccessful
c [simplification-18] removed 8 variables 0.1% (8850 remain 18%)
c [simplification-18] removed 79 irredundant clauses 0.2% (49733 remain 34%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 1000000
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] new conflict limit 7088335
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  945.5    8850    49733   6089329  165849  19977 36226  39 15.1 180.8   41
c -  964.8    8850    49733   6170176  167913  20000 36229  16 15.1 179.5   51
c -  976.5    8850    49733   6255949  169785  20016 36229  20 15.1 178.8   51
c -  999.7    8850    49733   6337596  172022  20058 36230  35 15.0 177.3   51
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 83 basic ate = 47 trn 57% + 36 lrg 43% in 5 updates
c bcas: 16 count, 581 added (1 skipped), 1570638 steps
c bkwd: tried 1064090 clauses, 2127351 lits, 2.00 lits/clause
c bkwd: checked 28005061 occs, 26.32 occs/clause, 13.16 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 90 large
c bkwd: strengthened 1 binary, 13 ternary (100% self), 1004 large (1% self)
c blkd: 11 bces, 2820 removed, 3571596 resolutions, 10064791 steps
c blkd: 1721 blocking literals 2%, 61 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 99 am1, 12764601 steps
c card: 46 rescheduled, 330 eliminated, 9006 resolved, 12800 subsumed
c card: 2694 at-most-one constraints found, average size 3.20
c card: 2694 at-most-one constraints used 100%, average size 3.20
c card: 379 at-most-two constraints found, average size 4.02
c card: 370 at-most-two constraints used 98%, average size 4.02
c cces: 10 cces, 7328 eliminated, 6480 ate 88%, 848 abce 12%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 14 count, 24843221 esteps, 2221002 csteps
c cgrs: 10 eqs, 0 units
c cgrs: 97 matched (39 ands 40%, 6 xors 6%, 52 ites 54%)
c cgrs: 7 simplified (0 ands 0%, 5 xors 71%, 2 ites 29%)
c cgrs: 53410 extracted (31909 ands 60%, 11150 xors 21%, 10351 ites 19%)
c clff: 9 cliffs, 15 lifted, 6 failed
c clff: 457588 decisions, 108756861 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 480752 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 134 gcs, 0 rescored clauses, 3319 rescored vars
c dcps: 50 decompositions, 1999 equivalent 4%
c deco: 91654 decision-only clauses 1%, 52% reduction
c decs: 21638275 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 537374 flipped 2.483% (in 3520 phases)
c elms: 17 elims, 38190 eliminated 77%
c elms: 35 rounds, 2.1 rounds/bve
c elms: 36486 small 96%, 1643 large 4%
c elms: 74264 tried small, 36486 succeeded 49%, 37778 failed 51%
c elms: 3669 subsumed, 4196 strengthened, 299 blocked
c elms: 5623431 copies, 7643433 resolutions, 2502509 ipos
c elms: 2111809 subchks, 1901187 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 9 extractions, 38889 extracted, 3.0 size, 4 max
c gaus: exported 1 units, 0 binary and 15 ternary equations
c gaus: 0 gc, 46162262 steps, 23081131 extr 50%, 2219867 elim 5%
c glue: 15.0 orig avg, 14.8 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 82205 = 18878 simple + 48918 trn 23% + 14409 lrg 60%, 1569 sub 18%
c hght: 177 average, 11.78 height/glue
c ints: 151035 luby (46214861 steps), 0 inout (0 steps)
c lift: 12 phases, 68286 probed (22816 level1 33%, 45470 level2 67%)
c lift: 25 units, 53 equivalences, 329 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 6310587 clauses, 37.0 length
c lrnd: 1284821 uips 20%, 4555877 flips 72%
c mega: 0 count, 0 failed, 0 rounds
c mins: 233403000 learned lits, 23% minimized
c mins: 6168118 mins 98%, 436 bin 0%, 50379 size 1%, 91654 deco 1%
c move: moved 6310587, 1392 bin 0%, 3079 trn 0%, 0 lrg 0%
c otfs: str 106047 dyn (105586 red, 461 irr) 29227 drv 28%, 76820 rst 72%
c otfs: sub 1670 dyn (1643 red, 27 irr)
c phas: 4 computed, 12631 set, 3273 pos (26%), 9358 neg (74%)
c prbs: 6 basic, 241808 probed, 62 failed, 0 lifted
c prbs: 7 simple, 199055 probed, 32 failed, 1805 eqs
c prbs: 6 treelook, 4899 probed, 13 failed, 0 lifted
c prps: 823874462 props, 37 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c psns: 250415507 searches, 36905125 hits, 15% 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: 146 count, 0 reset, 7 acts 5%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 146 arith 100%, 0 double 0%
c rmbd: 2723 removed, 2583 red 95%
c rphs: 8 recomputed phases
c rsts: 62455 restarts 41%, 88580 skipped 59%
c rsts: 0 saturating 0%, 87213 agile 98%, 1367 reuse 2%
c rsts: 99.9 avg interval, 99.9 scaled, 1.0 factor
c rsts: 25139 kept 40.3% average 22.3%
c simp: 18 count (18 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 6310587 count (5840765 tried 0.9), 509944 sub out of 6303416 (8.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 1 count
c tops: 243 fixed 0%, 25 its, 253592.60 confs/it
c trvs: 69597203018 traversals, 100% srch, 1% simp, 0% lkhd
c trvs: 86.8 search traversals per propagation, 10932.4 per conflict
c trvs: 1.5 search traversals per search visit
c trds: 16 transitive reductions, 14202 removed, 4 failed
c trds: 273133 nodes, 300513 edges, 25431942 steps
c trim: 5112178 words, 19.5 MB
c trnr: 16 count, 1350 bin, 30008 trn, 207018466 steps
c unhd: 6 count, 8 rounds, 12750239 steps
c unhd: 56 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 19807 tauts, 294 bin 1%, 4261 trn 22%, 2196 lrg 11%
c unhd: 19807 tauts, 13056 stamp 66%, 19752 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 280523 str, 0 bin 0%, 373 trn 0%, 280150 lrg 100%, 278175 red 99%
c vars: 8893 remaining 18% and 40432 removed 82% out of 49325
c vars: 243 fixed 0%, 38190 eliminated 77%, 1999 equivalent 4%
c vsts: 46433085807 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 57.8 search visits per propagation, 7278.7 per conflict
c wchs: 11633235718 pushed, 15567038 enlarged, 246 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   6303416 100   5580422 100 177415621 100  67006580 100   3495679 100
c 
c  0     121537   2         0   0 114371382  64  28362283  42   1117864  32 
c  1     187860   3     97170   2  38157614  22< 15201713  23<   772792  22 
c  2    1130668  18   1080622  19  10337676   6   7100621  11    471707  13<
c  3    1907949  30   1742415  31   7893269   4   7605474  11    547195  16 
c  4    1411639  22<  1244598  22<  3886844   2   4602897   7    323125   9 
c  5    1110348  18   1060576  19   2083682   1   3007758   4    173242   5 
c  6     307868   5    281436   5    518499   0    831707   1     70952   2 
c  7      51077   1     38638   1     76706   0    134848   0     13308   0 
c  8      10950   0      7193   0     16414   0     27157   0      2230   0 
c  9      43142   1     17606   0     50068   0     90002   0      2188   0 
c 10      17869   0      8500   0     20157   0     36604   0       840   0 
c 11       2506   0      1666   0      3307   0      5512   0       236   0 
c 12          3   0         2   0         3   0         4   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.5           3.6           0.6           1.4           1.7
c std             1.5           1.3           1.1           1.6           1.7
c 
c   79.570   8% analysis
c   74.989   7% cce
c   29.805   3% decide
c   22.229   2% mincls
c   14.471   1% bump
c    9.345   1% probe
c    8.679   1% elim
c    5.440   1% restart
c    5.229   1% gc
c    4.530   0% decomp
c    3.103   0% cliff
c    2.326   0% ternres
c    2.284   0% reduce
c    2.042   0% cgrclsr
c    1.854   0% transred
c    1.776   0% lift
c    1.768   0% unhide
c    1.757   0% defrag
c    1.432   0% backward
c    1.210   0% block
c    1.022   0% gauss
c    0.866   0% bca
c    0.332   0% card
c    0.036   0% phase
c    0.010   0% tabularasa
c    0.003   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c    1.652   0% probe simple     18%
c    6.522   1% probe basic      70%
c    1.172   0% probe tree-look  13%
c ==================================
c    1.549   0% preprocessing     1%
c  110.112  11% inprocessing     99%
c ==================================
c  111.661  11% simplifying
c  888.339  89% search
c ==================================
c 1000.001 100% all
c 
c 21638275 decisions, 21638.3 decisions/sec
c 6339815 conflicts, 6339.8 conflicts/sec
c 823874462 propagations, 0.8 megaprops/sec
c 1000.0 seconds, 104.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
