c launch: /data/cnf/sc2014/app/post-cbmc-aes-ee-r2-noholes.cnf.bz2
c host: atom03
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/post-cbmc-aes-ee-r2-noholes.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/post-cbmc-aes-ee-r2-noholes.cnf.bz2
c no embedded options
c found 'p cnf 266199 1575975' header
c read 266199 variables, 1575975 clauses, 4240496 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 163710 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  163710  1328859         0       0      0     0  64  0.0   0.0   66
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 145467 variables
c [simpleprobe-1] all 120732 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 2788 variables
c [simpleprobe-1] 69434 variables remain 59% (48510 retained)
c [simpleprobe-1] removed 2788 variables, found 14485 hbrs, 30 units
c [unhide-1] limit 465212 based on 930424 irredundant clauses
c [unhide-1-1] 31 units, 235 failed, 1555 tauts, 0 hbrs, 1916 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 111276 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 102338 variables 92% in round 1 in 124844787 steps
c [elim-1-1] backward subsumption/strengthening limit 249689574
c [elim-1-1] subsumed 7 and strengthened 145842 clauses in 249689626 steps
c [elim-1-1] rescheduled 1751 variables 2% by backward subsumption
c [elim-1-2] eliminated 26 variables 0% in round 2 in 132948 steps
c [elim-1-2] backward subsumption/strengthening limit 265896
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 267107 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 107259 = 96% variables out of 111276
c [phase-1] phase bias: 1070 positive 27%, 2947 negative 73%
c [simplification-1] removed 148687 variables 97.4% (4017 remain 2%)
c [simplification-1] removed 940431 irredundant clauses 70.8% (388428 remain 29%)
c [simplification-1] maximum reduction of 97% = max (97%, 71%)
c [simplification-1] large reduction 97% >= 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] 48620, max 193266, min4 3108 at 34%, min10 2908 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number variables 4017 drops below limit 40927
c [tabula-rasa-1] number clauses 388428 drops below limit 664429
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 4017 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 1004 and clause limit 194214
c 
c [simplification-2] limit of 1008 conflicts hit after 1008 conflicts
c [decomp-3] removed 132 variables
c [simpleprobe-2] 2261 schedulable variables 58%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2281 variables remain 59% (1604 retained)
c [simpleprobe-2] removed 0 variables, found 94 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 1965 literals 25%
c [treelook-1] scheduling used 305673 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 358637 steps
c [treelook-1] 1955 literals remain 25%
c [treelook-1] 1732 variables remain to probed next time 45%
c [treelook-1] removed 0 variables, found 144 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 216 probes remain 6% after last round
c [basicprobe-1-0] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 14 variables, found 2257 hbrs
c [unhide-2] limit 194068 based on 388136 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 175 tauts, 0 hbrs, 540 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 3871 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 11485 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 14 clauses out of 14 (100%) of length 10
c [cce-1-1] eliminated 57743 clauses out of 223352 (26%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 57757 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 5286 clauses = 4410 binary + 876 ternary
c [cce-1] tried to eliminate 5286 small clauses 100%
c [cce-1] eliminated 823 small clauses 16%
c [cce-1] eliminated 693 binary clauses 16%
c [cce-1] eliminated 130 ternary clauses 15%
c [cce-1-1] eliminated 823 small clauses in 208224642 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 58580 covered clauses in round 1
c [cce-1-2] eliminated 453 clauses out of 139252 (0%) of length 8
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] eliminated 453 large clauses in 91775359 steps
c [cce-1-2] allowing another 45887679 steps for small clauses
c [cce-1] scheduling 4463 clauses = 3717 binary + 746 ternary
c [cce-1] tried to eliminate 4013 small clauses 90%
c [cce-1-2] incomplete small round (ATE)
c [cce-1-2] eliminated 453 covered clauses in round 2
c [cce-1] eliminated 59033 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3796 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 1814 not tried 48% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 388 = 10% variables out of 3796
c [bca-1] limit of 10000000 steps
c [bca-1] 6246 out of 6818 literals actually usable 92%
c [bca-1] added 231 blocked clauses in 25774 steps
c [phase-3] phase bias: 158 positive 66%, 83 negative 34%
c [simplification-2] removed 609 variables 15.2% (3408 remain 2%)
c [simplification-2] removed 79414 irredundant clauses 20.4% (308985 remain 23%)
c [simplification-2] maximum reduction of 20% = max (15%, 20%)
c [simplification-2] large reduction 20% >= 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 3008
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   43.2    3407   308969      1785    1437    169  2458  54  8.0 285.9   41
c 
c [simplification-3] limit of 3060 conflicts hit after 3061 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 3407 free variables schedulable
c [ternres-1] 674 ternary resolvents (20 bin, 654 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 68 at-most-one constraints of average size 4.3
c [card-2] found 32 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 100 out of 100 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 7889 xors of average arity 3.2
c [gauss-1] connected 25467 occurrences of 1957 variables (average 13.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 5048 occurrences of 1957 variables (average 2.6)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 4 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 3403 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 2040 probes 60%
c [lift-1] 4 units, 33 impls, 4 eqs in 1 rounds
c [lift-1] 2929 variables remain 86% (466 retained)
c [lift-1] removed 8 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 308921 based on 308921 irredundant clauses
c [transred-1] removed 126 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3395 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] incomplete 123 not tried 4%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 2395 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 162830 (0%) of length 9
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 2 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 7090 clauses = 3413 binary + 3677 ternary
c [cce-2] tried to eliminate 1370 small clauses 19%
c [cce-2] eliminated 101 small clauses 1%
c [cce-2] eliminated 6 binary clauses 0%
c [cce-2] eliminated 95 ternary clauses 3%
c [cce-2-1] eliminated 101 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 103 covered clauses in round 1
c [cce-2] eliminated 103 covered clauses in TOTAL during 1 rounds
c [cce-2] 103 < 1/1000 * 306509 = 306 considered unsuccessful
c [elim-3] 1805 variables 53% will be scheduled this time
c [elim-3] scheduled 1805 variables 53%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 1572 not tried 46% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 33 = 1% variables out of 3383
c [bca-2] limit of 10000000 steps
c [bca-2] 5707 out of 6702 literals actually usable 85%
c [bca-2] added 70 blocked clauses in 25610 steps
c [phase-4] phase bias: 11 positive 61%, 7 negative 39%
c [simplification-3] removed 57 variables 1.7% (3350 remain 2%)
c [simplification-3] removed 8858 irredundant clauses 2.9% (300088 remain 23%)
c [simplification-3] maximum reduction of 3% = max (2%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 25000
c [simplification-3] penalized conflict interval 25000 = 1 * 25000
c [simplification-3] new conflict limit 28061
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   48.7    3350   300033      5371    2403    836  3724  42  9.0 424.5   41
c -   48.9    3350   299938      8725    3048    836  3724  40  9.2 419.7   41
c -   49.0    3350   299915     12552    3688    837  3724  40  9.1 392.9   42
c -   49.3    3350   299877     16994    4229    838  3724  36  9.7 370.0   42
c -   49.6    3350   299827     22027    4780    842  3726  37 10.0 353.4   42
c -   50.0    3350   299792     27556    5297    844  3726  35 10.6 340.9   42
c 
c [simplification-4] limit of 28065 conflicts hit after 28065 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3350 free variables schedulable
c [ternres-2] 97 ternary resolvents (15 bin, 82 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-7] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1243 literals 19%
c [treelook-2] scheduling used 150250 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 193936 steps
c [treelook-2] 1239 literals remain 19%
c [treelook-2] 733 variables remain to probed next time 22%
c [treelook-2] removed 0 variables, found 37 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 1492 probes 45%
c [lift-2] 1 units, 25 impls, 4 eqs in 1 rounds
c [lift-2] 2406 variables remain 72% (933 retained)
c [lift-2] removed 5 variables
c [unhide-3] limit 149883 based on 299767 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 105 tauts, 0 hbrs, 119 literals
c [transred-2] limit 625571 with penalty 0 = 0 + 0
c [transred-2] removed 100 transitive binary clauses
c [block-3] 123 variables 4% will be scheduled this time
c [block-3] scheduled 123 variables 4%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] incomplete 117 not tried 4%
c [block-3] transition to [ all 0 rem 1 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3339 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 1567 not tried 47% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 66 = 2% variables out of 3339
c [bca-3] limit of 10000000 steps
c [bca-3] 5327 out of 6548 literals actually usable 81%
c [bca-3] added 9 blocked clauses in 26859 steps
c [rephase-1] after 28065 conflicts (new increment 20000, next 48065)
c [flushphases] 0 phases reset
c [simplification-4] removed 77 variables 2.3% (3273 remain 2%)
c [simplification-4] removed 1837 irredundant clauses 0.6% (297954 remain 22%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 8333 = 25000 / 3
c [simplification-4] new conflict interval 33333
c [simplification-4] penalized conflict interval 33333 = 1 * 33333
c [simplification-4] new conflict limit 61398
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   53.8    3273   297616     34443    6213    707  3633  40 10.4 301.0   40
c -   55.2    3273   297267     41982    7058    707  3634  34 11.3 261.6   40
c -   56.3    3273   296660     50050    7997    717  3643  17 10.9 194.6   41
c -   56.9    3273   296397     58572    8790    718  3643  40 10.8 203.6   41
c 
c [simplification-5] limit of 61430 conflicts hit after 61430 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3273 free variables schedulable
c [ternres-3] 260 ternary resolvents (12 bin, 248 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 6828 xors of average arity 3.3
c [gauss-2] connected 22244 occurrences of 1750 variables (average 12.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] connected 3438 occurrences of 1750 variables (average 2.0)
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2 variables
c [basicprobe-2] limit 2668315 penalty 0 = 0 + 0
c [basicprobe-2-0] 251 sched 8%, 0 failed, 0 lifted, 94 hbrs
c [basicprobe-2-1] 566 sched 17%, 0 failed, 0 lifted, 140 hbrs
c [basicprobe-2-2] 73 probes remain 2% after last round
c [basicprobe-2-2] removed 0 variables, found 234 hbrs
c [bate-1] eliminated 6 asymmetric tautologies during probing
c [cgrclsr-2] limit 148156 based on 296312 irredundant clauses
c [cgrclsr-2] all 3271 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 1600989 with penalty 0 = 0 + 0
c [lift-3] using 969 probes 30%
c [lift-3-1] found 0 units 48 impls in round 1
c [lift-3] 0 units, 65 impls, 4 eqs in 2 rounds
c [lift-3] 1409 variables remain 43% (1858 retained)
c [lift-3] removed 4 variables
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 167 transitive binary 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 6670 clauses = 3437 binary + 3233 ternary
c [cce-3] tried to eliminate 366 small clauses 5%
c [cce-3] eliminated 24 small clauses 0%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3] eliminated 23 ternary clauses 1%
c [cce-3-1] eliminated 24 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 24 covered clauses in round 1
c [cce-3] eliminated 24 covered clauses in TOTAL during 1 rounds
c [cce-3] 24 < 1/1000 * 296299 = 296 considered unsuccessful
c [elim-5] 1559 variables 48% will be scheduled this time
c [elim-5] scheduled 1559 variables 48%
c [elim-5] limit of 53366318 steps penalty 0 = 0 + 0
c [elim-5] incomplete 1295 not tried 40% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 37 = 1% variables out of 3267
c [bca-4] limit of 10000000 steps
c [bca-4] 4243 out of 6462 literals actually usable 66%
c [bca-4] added 0 blocked clauses in 28027 steps
c [rephase-2] after 61430 conflicts (new increment 40000, next 101430)
c [flushphases] 0 phases reset
c [simplification-5] removed 43 variables 1.3% (3230 remain 2%)
c [simplification-5] removed 5758 irredundant clauses 1.9% (290566 remain 22%)
c [simplification-5] maximum reduction of 2% = max (1%, 2%)
c [simplification-5] geometric conflict interval increment 11111 = 33333 / 3
c [simplification-5] new conflict interval 44444
c [simplification-5] penalized conflict interval 44444 = 1 * 44444
c [simplification-5] new conflict limit 105874
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   61.7    3230   289958     69909   10068    946  3859  43 10.4 194.6   40
c -   62.9    3230   289563     80930   11046    952  3875  43 10.2 185.4   41
c -   63.4    3230   289407     90140   11657    952  3878  41 10.0 181.0   41
c -   64.0    3230   289309     99920   12222    952  3878  39 10.2 177.1   41
c 
c [simplification-6] limit of 105912 conflicts hit after 105912 conflicts
c [ternres-4] limit 4439516 with penalty 0 = 0 + 0
c [ternres-4] all 3230 free variables schedulable
c [ternres-4] 58 ternary resolvents (11 bin, 47 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 554939 penalty 2 = 2 + 0
c [card-3] found 62 at-most-one constraints of average size 4.7
c [card-3] found 46 at-most-two constraints of average size 4.0
c [card-3] using previous limit 554939 for elimination
c [card-3] 108 out of 108 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 4 variables
c [lift-4] limit 2663709 with penalty 0 = 0 + 0
c [lift-4] using 16 probes 0%
c [lift-4-1] found 0 units 2 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 0 impls in round 5
c [lift-4] 0 units, 2 impls, 1 eqs in 6 rounds
c [lift-4] 1392 variables remain 43% (1833 retained)
c [lift-4] removed 1 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 126 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3225 variables 100%
c [block-4] limit of 25000000 steps penalty 1 = 1 + 0
c [block-4] incomplete 126 not tried 4%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 2 blocked clauses
c [block-4] 2 < 1/1000 * 289271 = 289 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 3225 variables 100%
c [elim-6] limit of 88790327 steps penalty 0 = 0 + 0
c [elim-6] incomplete 929 not tried 29% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 59 = 2% variables out of 3225
c [rephase-3] after 105912 conflicts (new increment 80000, next 185912)
c [flushphases] 0 phases reset
c [simplification-6] removed 64 variables 2.0% (3166 remain 2%)
c [simplification-6] removed 1978 irredundant clauses 0.7% (287305 remain 22%)
c [simplification-6] maximum reduction of 2% = max (2%, 1%)
c [simplification-6] geometric conflict interval increment 14814 = 44444 / 3
c [simplification-6] new conflict interval 59258
c [simplification-6] penalized conflict interval 59258 = 1 * 59258
c [simplification-6] new conflict limit 165170
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   68.1    3166   287061    112456   12653    959  3696  39 10.2 169.3   41
c -   69.4    3166   286916    124142   13303    961  3709  37 10.7 159.0   41
c -   71.1    3166   286857    136242   13865    968  3725  35 11.3 149.3   41
c -   72.7    3166   286767    149128   14490    982  3765  34 11.6 140.7   41
c -   74.3    3166   286719    162827   15076    985  3778  32 11.9 132.3   40
c 
c [simplification-7] limit of 165342 conflicts hit after 165342 conflicts
c [ternres-5] limit 7789624 with penalty 0 = 0 + 0
c [ternres-5] all 3166 free variables schedulable
c [ternres-5] 56 ternary resolvents (7 bin, 49 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 1831 schedulable variables 58%
c [simpleprobe-3] limit 15579249 penalty 1 = 1 + 0
c [simpleprobe-3] 1877 variables remain 59% (1289 retained)
c [simpleprobe-3] removed 0 variables, found 197 hbrs, 0 units
c [lift-5] limit 4673774 with penalty 0 = 0 + 0
c [lift-5] using 11 probes 0%
c [lift-5-1] found 0 units 5 impls in round 1
c [lift-5-2] found 0 units 0 impls in round 2
c [lift-5-3] found 0 units 0 impls in round 3
c [lift-5-4] found 0 units 2 impls in round 4
c [lift-5-5] found 0 units 1 impls in round 5
c [lift-5] 0 units, 8 impls, 0 eqs in 6 rounds
c [lift-5] 1381 variables remain 44% (1785 retained)
c [unhide-4] limit 389481 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 541 tauts, 0 hbrs, 343 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 112 transitive binary clauses
c [elim-7] 921 variables 29% will be scheduled this time
c [elim-7] scheduled 921 variables 29%
c [elim-7] limit of 155792497 steps penalty 0 = 0 + 0
c [elim-7] incomplete 740 not tried 23% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 0 = 0% variables out of 3166
c [bca-5] limit of 10000000 steps
c [bca-5] 4505 out of 6334 literals actually usable 71%
c [bca-5] added 0 blocked clauses in 36712 steps
c [simplification-7] removed 0 variables 0.0% (3166 remain 2%)
c [simplification-7] removed 2436 irredundant clauses 0.8% (284276 remain 21%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 29629 = 59258 / 2
c [simplification-7] new conflict interval 88887
c [simplification-7] penalized conflict interval 88887 = 1 * 88887
c [simplification-7] new conflict limit 254229
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   77.9    3166   284216    176518   15567    810  3693  35 12.2 125.8   40
c -   78.9    3166   284121    190804   16184    810  3694  38 12.5 120.2   40
c -   79.8    3166   284036    205980   16947    813  3695  37 12.7 114.8   40
c -   81.0    3166   283948    222158   17698    814  3697  36 12.9 109.7   40
c -   82.6    3166   283911    239539   18407    816  3701  37 13.0 104.8   40
c 
c [simplification-8] limit of 254253 conflicts hit after 254254 conflicts
c [ternres-6] limit 11062995 with penalty 0 = 0 + 0
c [ternres-6] all 3166 free variables schedulable
c [ternres-6] 421 ternary resolvents (25 bin, 396 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 553149 penalty 2 = 2 + 0
c [gauss-3] extracted 5750 xors of average arity 3.3
c [gauss-3] connected 18988 occurrences of 1562 variables (average 12.2)
c [gauss-3] limit 553149 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 4 variables
c [cgrclsr-3] limit 276574 penalty 2 = 2 + 0
c [cgrclsr-3] all 3162 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-3] limit of 2500000 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 67 transitive binary clauses
c [cce-4] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 3750000 steps for small clauses
c [cce-4] scheduling 4318 clauses = 3462 binary + 856 ternary
c [cce-4] tried to eliminate 76 small clauses 2%
c [cce-4] eliminated 8 small clauses 0%
c [cce-4] eliminated 4 binary clauses 0%
c [cce-4] eliminated 4 ternary clauses 0%
c [cce-4-1] eliminated 8 small clauses in 7500001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 8 covered clauses in round 1
c [cce-4] eliminated 8 covered clauses in TOTAL during 1 rounds
c [cce-4] 8 < 1/1000 * 283880 = 283 considered unsuccessful
c [rephase-4] after 254254 conflicts (new increment 160000, next 414254)
c [flushphases] 0 phases reset
c [simplification-8] removed 4 variables 0.1% (3162 remain 2%)
c [simplification-8] removed 15 irredundant clauses 0.0% (283872 remain 21%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 88887
c [simplification-8] new conflict interval 177774
c [simplification-8] penalized conflict interval 177774 = 1 * 177774
c [simplification-8] new conflict limit 432028
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   85.2    3162   283684    257313   19077   1186  3915  36 13.0 103.5   41
c -   87.6    3162   283561    277021   20983   1217  3975  39 12.7 116.8   41
c -   90.2    3162   283496    295867   22275   1219  4006  37 12.6 127.9   41
c -   94.5    3162   283442    314861   23459   1221  4010  36 12.5 130.8   41
c -   97.3    3162   282692    337644   25544   1250  4030  42 12.3 129.3   56
c -  101.1    3162   282513    357563   26993   1258  4030  34 12.3 133.4   56
c -  105.6    3162   281700    378992   28472   1281  4047  24 12.2 132.5   43
c -  109.8    3162   281630    399462   29661   1281  4057  37 12.2 136.2   57
c -  113.4    3162   280753    425280   31559   1321  4077  39 12.1 136.6   57
c 
c [simplification-9] limit of 432284 conflicts hit after 432284 conflicts
c [ternres-7] limit 24144580 with penalty 0 = 0 + 0
c [ternres-7] all 3162 free variables schedulable
c [ternres-7] 127 ternary resolvents (18 bin, 109 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-16] removed 14 variables
c [lift-6] limit 7243374 with penalty 1 = 1 + 0
c [lift-6] using 67 probes 2%
c [lift-6-1] found 0 units 9 impls in round 1
c [lift-6-2] found 0 units 8 impls in round 2
c [lift-6-3] found 0 units 3 impls in round 3
c [lift-6-4] found 0 units 2 impls in round 4
c [lift-6-5] found 0 units 0 impls in round 5
c [lift-6] 0 units, 22 impls, 1 eqs in 6 rounds
c [lift-6] 1311 variables remain 42% (1836 retained)
c [lift-6] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 52 transitive binary clauses
c [block-5] 115 variables 4% will be scheduled this time
c [block-5] scheduled 115 variables 4%
c [block-5] limit of 60361450 steps penalty 2 = 2 + 0
c [block-5] incomplete 94 not tried 3%
c [block-5] transition to [ all 0 rem 1 ] state
c [block-5] eliminated 0 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 3147 variables 100%
c [elim-8] limit of 241445800 steps penalty 1 = 1 + 0
c [elim-8] incomplete 720 not tried 23% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 27 = 1% variables out of 3147
c [rephase-5] after 432284 conflicts (new increment 320000, next 752284)
c [flushphases] 0 phases reset
c [simplification-9] removed 42 variables 1.3% (3120 remain 2%)
c [simplification-9] removed 688 irredundant clauses 0.2% (279973 remain 21%)
c [simplification-9] maximum reduction of 1% = max (1%, 0%)
c [simplification-9] geometric conflict interval increment 88887 = 177774 / 2
c [simplification-9] new conflict interval 266661
c [simplification-9] penalized conflict interval 266661 = 1 * 266661
c [simplification-9] new conflict limit 698945
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  122.9    3120   279563    456705   32887   1099  3967  36 11.8 138.9   42
c -  126.1    3120   279468    482858   33791   1102  3976  35 12.0 138.6   43
c -  129.2    3120   279408    513102   34574   1103  3980  39 12.0 138.1   42
c -  132.6    3120   279385    545573   35340   1108  3987  32 12.1 137.6   42
c -  135.4    3120   279351    576480   36102   1117  3990  36 12.1 137.1   42
c -  137.2    3120   279347    602132   36803   1123  3990  34 12.2 137.0   42
c -  140.2    3120   279145    629712   38024   1130  3998  38 12.4 137.8   56
c i  142.6    3119   278832    659959   59301   1210  4032  37 12.3 138.8   60
c -  142.9    3113   278787    663260   39959   1220  4041  38 12.3 139.5   56
c -  147.8    3113   278263    691936   42072   1240  4103  37 12.3 145.0   56
c 
c [simplification-10] limit of 699235 conflicts hit after 699235 conflicts
c [ternres-8] limit 38393859 with penalty 0 = 0 + 0
c [ternres-8] all 3113 free variables schedulable
c [ternres-8] 224 ternary resolvents (15 bin, 209 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2399616 penalty 3 = 3 + 0
c [card-4] found 53 at-most-one constraints of average size 5.0
c [card-4] found 59 at-most-two constraints of average size 4.0
c [card-4] using previous limit 2399616 for elimination
c [card-4] 111 out of 112 constraints (99%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-17] removed 22 variables
c [treelook-3] limit 479923 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1950 literals 31%
c [treelook-3] scheduling used 480019 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 479923 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 562750 steps
c [treelook-3] 1939 literals remain 31%
c [treelook-3] 679 variables remain to probed next time 22%
c [treelook-3] removed 0 variables, found 125 hbrs
c [lift-7] limit 20000000 with penalty 0 = 0 + 0
c [lift-7] using 49 probes 2%
c [lift-7-1] found 0 units 8 impls in round 1
c [lift-7-2] found 0 units 1 impls in round 2
c [lift-7-3] found 0 units 1 impls in round 3
c [lift-7-4] found 0 units 2 impls in round 4
c [lift-7-5] found 0 units 1 impls in round 5
c [lift-7] 0 units, 13 impls, 0 eqs in 6 rounds
c [lift-7] 1256 variables remain 41% (1842 retained)
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 49 transitive binary clauses
c [elim-9] 694 variables 22% will be scheduled this time
c [elim-9] scheduled 694 variables 22%
c [elim-9] limit of 767877189 steps penalty 0 = 0 + 0
c [elim-9] incomplete 627 not tried 20% in round 1
c [elim-9] transition to [ all 0 rem 1 ] state
c [elim-9] eliminated 60 = 2% variables out of 3098
c [bca-6] limit of 10000000 steps
c [bca-6] 2848 out of 6078 literals actually usable 47%
c [bca-6] added 1 blocked clauses in 49395 steps
c [simplification-10] removed 75 variables 2.4% (3038 remain 2%)
c [simplification-10] removed 6285 irredundant clauses 2.3% (271876 remain 20%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 88887 = 266661 / 3
c [simplification-10] new conflict interval 355548
c [simplification-10] penalized conflict interval 355548 = 1 * 355548
c [simplification-10] new conflict limit 1054783
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  162.3    3038   271595    729783   40414   1303  4133  36 12.2 154.0   42
c -  171.1    3038   271491    757701   41151   1308  4133  36 12.5 158.9   56
c -  180.6    3038   271440    785854   41889   1308  4136  35 12.8 163.7   56
c -  188.4    3038   271414    814242   42638   1311  4138  34 13.0 168.3   56
c -  199.1    3038   271359    842662   43425   1311  4139  36 13.3 172.6   56
c -  209.7    3038   271267    872034   44227   1312  4139  35 13.5 176.7   56
c -  221.1    3038   271248    901506   44927   1314  4139  34 13.7 180.4   56
c -  234.0    3038   271221    931682   45781   1314  4139  36 13.9 183.9   56
c -  247.5    3038   271212    962132   46460   1314  4139  33 14.2 187.2   57
c -  256.6    3038   271095    995300   48164   1348  4201  40 14.3 191.0   57
c -  262.0    3038   270854   1029423   50375   1383  4248  41 14.2 195.2   56
c 
c [simplification-11] limit of 1055021 conflicts hit after 1055022 conflicts
c [ternres-9] limit 93840633 with penalty 0 = 0 + 0
c [ternres-9] all 3038 free variables schedulable
c [ternres-9] 68 ternary resolvents (10 bin, 58 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-19] removed 2 variables
c [unhide-5] limit 2346015 with penalty 3 = 3 + 0
c [unhide-5-6] 0 units, 0 failed, 677 tauts, 0 hbrs, 6634 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 63 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3036 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] incomplete 599 not tried 20% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 56 = 2% variables out of 3036
c [rephase-6] after 1055022 conflicts (new increment 640000, next 1695022)
c [flushphases] 0 phases reset
c [simplification-11] removed 58 variables 1.9% (2980 remain 2%)
c [simplification-11] removed 2973 irredundant clauses 1.1% (267667 remain 20%)
c [simplification-11] maximum reduction of 2% = max (2%, 1%)
c [simplification-11] geometric conflict interval increment 118516 = 355548 / 3
c [simplification-11] new conflict interval 474064
c [simplification-11] penalized conflict interval 474064 = 1 * 474064
c [simplification-11] new conflict limit 1529086
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  278.1    2980   267636   1075892   51705   1111  4076  36 14.2 196.3   44
c -  284.0    2980   267618   1114369   52638   1114  4079  39 14.3 193.4   44
c -  289.9    2980   267582   1160108   54347   1149  4084  39 14.3 189.9   44
c i  290.3    2979   267571   1166415   56749   1185  4101  39 14.2 189.4   45
c -  295.6    2979   267149   1206408   57313   1280  4189  38 14.1 190.8   59
c -  304.7    2979   266890   1242147   58604   1281  4194  34 14.1 191.0   59
c -  314.8    2979   266763   1278344   59723   1286  4204  31 14.1 190.4   59
c -  321.9    2979   266595   1314913   60572   1288  4207  36 14.2 189.8   59
c -  328.4    2979   266486   1351402   61502   1291  4214  36 14.2 189.1   59
c -  337.5    2979   266380   1389336   62392   1295  4216  35 14.2 188.5   59
c -  346.0    2979   266291   1426951   63240   1296  4220  32 14.3 188.0   59
c -  353.0    2979   266244   1464614   64069   1297  4220  38 14.3 187.5   59
c -  359.3    2979   266196   1501618   64740   1298  4220  38 14.4 186.9   59
c 
c [simplification-12] limit of 1529310 conflicts hit after 1529312 conflicts
c [ternres-10] limit 140191643 with penalty 0 = 0 + 0
c [ternres-10] all 2979 free variables schedulable
c [ternres-10] 214 ternary resolvents (18 bin, 196 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3504791 penalty 3 = 3 + 0
c [gauss-4] extracted 5275 xors of average arity 3.3
c [gauss-4] connected 17377 occurrences of 1423 variables (average 12.2)
c [gauss-4] limit 3504791 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-20] removed 18 variables
c [basicprobe-3] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 200 sched 7%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-3-1] 616 sched 21%, 0 failed, 0 lifted, 273 hbrs
c [basicprobe-3-2] 606 sched 20%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-3-3] 606 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-4] 606 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-5] 606 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-5] fully completed probing
c [basicprobe-3-5] removed 0 variables, found 310 hbrs
c [bate-2] eliminated 5 asymmetric tautologies during probing
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 2961 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-8] limit 10000000 with penalty 1 = 1 + 0
c [lift-8] using 71 probes 2%
c [lift-8-1] found 0 units 6 impls in round 1
c [lift-8-2] found 0 units 5 impls in round 2
c [lift-8-3] found 0 units 4 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, 20 impls, 2 eqs in 6 rounds
c [lift-8] 1147 variables remain 39% (1812 retained)
c [lift-8] removed 2 variables
c [cliff-4] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-4] failed 0, lifted 0
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 101 transitive binary clauses
c [cce-5] limit of 35047910 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 24 clauses out of 111828 (0%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 24 large clauses in 35047911 steps
c [cce-5-1] allowing another 17523955 steps for small clauses
c [cce-5] scheduling 4425 clauses = 3492 binary + 933 ternary
c [cce-5] tried to eliminate 879 small clauses 20%
c [cce-5] eliminated 140 small clauses 3%
c [cce-5] eliminated 117 binary clauses 3%
c [cce-5] eliminated 23 ternary clauses 2%
c [cce-5-1] eliminated 140 small clauses in 35047911 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 164 covered clauses in round 1
c [cce-5] eliminated 164 covered clauses in TOTAL during 1 rounds
c [cce-5] 164 < 1/1000 * 266041 = 266 considered unsuccessful
c [elim-11] 560 variables 19% will be scheduled this time
c [elim-11] scheduled 560 variables 19%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] incomplete 521 not tried 18% in round 1
c [elim-11] transition to [ all 0 rem 1 ] state
c [elim-11] eliminated 1 = 0% variables out of 2959
c [elim-11] 1 < 1/1000 * 2959 = 2 considered unsuccessful
c [bca-7] limit of 10000000 steps
c [bca-7] 1997 out of 5918 literals actually usable 34%
c [bca-7] added 0 blocked clauses in 96686 steps
c [simplification-12] removed 21 variables 0.7% (2958 remain 2%)
c [simplification-12] removed 1336 irredundant clauses 0.5% (264834 remain 20%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 237032 = 474064 / 2
c [simplification-12] new conflict interval 711096
c [simplification-12] penalized conflict interval 711096 = 1 * 711096
c [simplification-12] new conflict limit 2240408
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  376.2    2957   264790   1530734   88976   1378  4503  39 14.4 186.4   54
c i  378.2    2951   264681   1550334   98970   1439  4528  39 14.3 185.1   54
c -  378.3    2951   264637   1551170   65240   1439  4528  38 14.3 185.1   46
c -  386.5    2951   263533   1604071   67933   1490  4592  34 14.2 182.5   60
c -  393.7    2951   262689   1656887   71149   1535  4667  40 14.0 181.1   61
c i  400.1    2950   261541   1701322  104233   1636  4777  39 13.9 181.9   66
c -  400.8    2944   261536   1707951   74401   1638  4777  41 13.9 181.8   61
c -  406.8    2944   261432   1750138   75679   1655  4792  41 13.9 180.8   61
c -  410.3    2944   261372   1795996   77040   1671  4805  34 13.8 179.7   61
c -  414.0    2944   261344   1845081   78384   1692  4815  32 13.7 178.4   61
c -  421.1    2944   259808   1891425   80397   1705  4879  35 13.6 173.8   62
c -  425.6    2944   259540   1935067   81209   1708  4912  35 13.6 173.7   44
c -  429.2    2944   259381   1978797   82013   1719  4955  37 13.6 174.2   44
c -  433.1    2944   259269   2021797   82801   1720  4965  31 13.6 174.6   44
c -  436.5    2944   259225   2065596   83397   1720  4968  32 13.6 175.0   46
c -  444.2    2944   258277   2114727   85665   1746  5015  34 13.5 176.5   59
c -  455.0    2944   257626   2170571   88258   1787  5066  32 13.5 179.0   60
c -  464.6    2944   256545   2227374   91031   1818  5116  39 13.6 178.1   46
c 
c [simplification-13] limit of 2241374 conflicts hit after 2241375 conflicts
c [ternres-11] limit 184042370 with penalty 0 = 0 + 0
c [ternres-11] all 2944 free variables schedulable
c [ternres-11] 186 ternary resolvents (39 bin, 147 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-26] removed 86 variables
c [lift-9] limit 20000000 with penalty 0 = 0 + 0
c [lift-9] using 115 probes 4%
c [lift-9-1] found 0 units 12 impls in round 1
c [lift-9-2] found 0 units 2 impls in round 2
c [lift-9-3] found 0 units 2 impls in round 3
c [lift-9-4] found 0 units 3 impls in round 4
c [lift-9-5] found 0 units 2 impls in round 5
c [lift-9] 0 units, 21 impls, 8 eqs in 6 rounds
c [lift-9] 1000 variables remain 35% (1864 retained)
c [lift-9] removed 8 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 45 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 2864 variables 100%
c [block-6] limit of 100000000 steps penalty 3 = 3 + 0
c [block-6] incomplete 86 not tried 3%
c [block-6] transition to [ all 1 rem 1 ] state
c [block-6] eliminated 8451 blocked clauses
c [rephase-7] after 2241375 conflicts (new increment 1280000, next 3521375)
c [flushphases] 0 phases reset
c [simplification-13] removed 173 variables 5.9% (2771 remain 2%)
c [simplification-13] removed 9740 irredundant clauses 3.8% (246770 remain 19%)
c [simplification-13] maximum reduction of 6% = max (6%, 4%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] new conflict interval 22413 = min (2241375/100, 711096)
c [simplification-13] penalized conflict interval 22413 = 1 * 22413
c [simplification-13] new conflict limit 2263788
c 
c [simplification-14] limit of 2263802 conflicts hit after 2263802 conflicts
c [ternres-12] limit 185950549 with penalty 0 = 0 + 0
c [ternres-12] all 2771 free variables schedulable
c [ternres-12] 74 ternary resolvents (18 bin, 56 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 9297527 penalty 2 = 2 + 0
c [gauss-5] extracted 5160 xors of average arity 3.3
c [gauss-5] connected 16948 occurrences of 1300 variables (average 13.0)
c [gauss-5] limit 9297527 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 1 variables
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 3 probes 0%
c [lift-10-1] found 0 units 0 impls in round 1
c [lift-10-2] found 0 units 0 impls in round 2
c [lift-10-3] found 0 units 0 impls in round 3
c [lift-10-4] found 0 units 0 impls in round 4
c [lift-10-5] found 0 units 0 impls in round 5
c [lift-10] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-10] 956 variables remain 35% (1814 retained)
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 15 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 2770 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] incomplete 581 not tried 21% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 44 = 2% variables out of 2770
c [simplification-14] removed 45 variables 1.6% (2726 remain 2%)
c [simplification-14] removed 1244 irredundant clauses 0.5% (245068 remain 18%)
c [simplification-14] maximum reduction of 2% = max (2%, 1%)
c [simplification-14] geometric conflict interval increment 237032 = 711096 / 3
c [simplification-14] new conflict interval 948128
c [simplification-14] penalized conflict interval 948128 = 1 * 948128
c [simplification-14] new conflict limit 3211930
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  483.1    2726   244866   2297201   82545   1522  4702  36 13.5 176.8   46
c -  487.5    2726   244801   2344662   83426   1525  4710  32 13.5 174.3   47
c -  491.6    2726   244684   2392843   84354   1535  4715  34 13.5 171.8   47
c -  501.2    2726   244252   2443091   86318   1547  4741  35 13.4 171.0   62
c -  516.7    2726   243402   2502742   89096   1585  4800  40 13.4 171.7   61
c i  520.2    2725   243251   2549296  120913   1650  4822  35 13.3 173.1   66
c -  521.6    2719   243088   2566473   91673   1681  4854  38 13.3 173.8   60
c i  523.1    2718   242968   2581767  104981   1706  4863  36 13.3 174.3   50
c i  524.1    2717   242892   2594777  114565   1756  4876  35 13.3 173.8   50
c -  528.0    2711   242312   2621845   93488   1758  4880  36 13.3 174.2   61
c i  533.9    2710   241792   2664975  122015   1904  5032  39 13.2 173.9   66
c -  539.0    2704   240531   2703061   98719   1981  5082  40 13.2 175.5   61
c i  539.5    2703   240491   2714436  104782   2026  5100  40 13.1 176.0   64
c -  547.7    2697   240098   2764285  102111   2044  5138  36 13.1 176.7   61
c -  554.8    2697   240050   2816547  103121   2045  5138  35 13.1 178.1   61
c -  560.7    2697   240021   2868412  103748   2045  5138  35 13.1 179.2   61
c -  566.5    2697   239866   2923915  104998   2054  5140  36 13.1 178.5   61
c -  575.5    2697   239624   2984067  106042   2056  5146  43 13.2 177.3   61
c -  583.3    2697   239573   3044066  107015   2061  5151  38 13.2 176.1   62
c -  589.1    2697   239511   3103766  108075   2072  5160  36 13.2 174.8   62
c -  594.2    2697   239337   3161570  109197   2077  5175  38 13.2 174.5   62
c 
c [simplification-15] limit of 3212824 conflicts hit after 3212825 conflicts
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 2697 free variables schedulable
c [ternres-13] 183 ternary resolvents (28 bin, 155 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 7689991 penalty 4 = 4 + 0
c [card-5] found 45 at-most-one constraints of average size 4.6
c [card-5] found 66 at-most-two constraints of average size 4.0
c [card-5] using previous limit 7689991 for elimination
c [card-5] 109 out of 111 constraints (98%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-28] removed 81 variables
c [simpleprobe-4] 1590 schedulable variables 60%
c [simpleprobe-4] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-4] 1343 variables remain 51% (1302 retained)
c [simpleprobe-4] removed 0 variables, found 303 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 174 transitive binary clauses
c [block-7] 67 variables 3% will be scheduled this time
c [block-7] scheduled 67 variables 3%
c [block-7] limit of 200000000 steps penalty 2 = 2 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 0 blocked clauses
c [elim-13] 440 variables 17% will be scheduled this time
c [elim-13] scheduled 440 variables 17%
c [elim-13] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-13] incomplete 399 not tried 15% in round 1
c [elim-13] transition to [ all 0 rem 1 ] state
c [elim-13] eliminated 179 = 7% variables out of 2645
c [bca-8] limit of 10000000 steps
c [bca-8] 829 out of 4934 literals actually usable 17%
c [bca-8] added 0 blocked clauses in 132760 steps
c [simplification-15] removed 231 variables 8.6% (2466 remain 2%)
c [simplification-15] removed 16563 irredundant clauses 6.9% (222492 remain 17%)
c [simplification-15] maximum reduction of 9% = max (9%, 7%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] new conflict interval 32128 = min (3212825/100, 948128)
c [simplification-15] penalized conflict interval 32128 = 1 * 32128
c [simplification-15] new conflict limit 3244953
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  617.6    2466   222387   3234122   99103   1706  4582  40 13.2 175.4   48
c 
c [simplification-16] limit of 3244959 conflicts hit after 3244959 conflicts
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] all 2466 free variables schedulable
c [ternres-14] 92 ternary resolvents (12 bin, 80 trn)
c [ternres-14] fully completed ternary resolution
c [lift-11] limit 10000000 with penalty 1 = 1 + 0
c [lift-11] using 70 probes 3%
c [lift-11-1] found 0 units 6 impls in round 1
c [lift-11-2] found 0 units 1 impls in round 2
c [lift-11-3] found 0 units 2 impls in round 3
c [lift-11-4] found 0 units 0 impls in round 4
c [lift-11-5] found 0 units 1 impls in round 5
c [lift-11] 0 units, 10 impls, 1 eqs in 6 rounds
c [lift-11] 778 variables remain 32% (1687 retained)
c [lift-11] removed 1 variables
c [unhide-6] limit 1250000 with penalty 4 = 4 + 0
c [unhide-6-7] 0 units, 0 failed, 1224 tauts, 0 hbrs, 6261 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 88 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2465 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] incomplete 393 not tried 16% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 187 = 8% variables out of 2465
c [simplification-16] removed 188 variables 7.6% (2278 remain 1%)
c [simplification-16] removed 12902 irredundant clauses 5.8% (209466 remain 16%)
c [simplification-16] maximum reduction of 8% = max (8%, 6%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] new conflict interval 32449 = min (3244959/100, 948128)
c [simplification-16] penalized conflict interval 32449 = 1 * 32449
c [simplification-16] new conflict limit 3277408
c 
c [simplification-17] limit of 3277424 conflicts hit after 3277424 conflicts
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 2278 free variables schedulable
c [ternres-15] 246 ternary resolvents (22 bin, 224 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-6] limit 6250000 penalty 3 = 3 + 0
c [gauss-6] extracted 3498 xors of average arity 3.3
c [gauss-6] connected 11430 occurrences of 910 variables (average 12.6)
c [gauss-6] limit 6250000 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-5] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-5] all 2278 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 7 probes 0%
c [lift-12-1] found 0 units 2 impls in round 1
c [lift-12-2] found 0 units 0 impls in round 2
c [lift-12-3] found 0 units 0 impls in round 3
c [lift-12-4] found 0 units 1 impls in round 4
c [lift-12-5] found 0 units 0 impls in round 5
c [lift-12] 0 units, 3 impls, 0 eqs in 6 rounds
c [lift-12] 708 variables remain 31% (1570 retained)
c [cliff-5] limit of 6250000 steps penalty 4 = 4 + 0
c [cliff-5] failed 0, lifted 0
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 64 transitive binary clauses
c [cce-6] limit of 31529642 steps penalty 4 = 4 + 0
c [cce-6-1] eliminated 19 clauses out of 19 (100%) of length 15
c [cce-6-1] eliminated 91 clauses out of 91 (100%) of length 14
c [cce-6-1] eliminated 9 clauses out of 9 (100%) of length 13
c [cce-6-1] eliminated 22 clauses out of 22 (100%) of length 12
c [cce-6-1] eliminated 3 clauses out of 35 (9%) of length 11
c [cce-6-1] eliminated 139 clauses out of 70621 (0%) of length 9
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 283 large clauses in 31529643 steps
c [cce-6-1] allowing another 15764821 steps for small clauses
c [cce-6] scheduling 5134 clauses = 3366 binary + 1768 ternary
c [cce-6] tried to eliminate 1178 small clauses 23%
c [cce-6] eliminated 197 small clauses 4%
c [cce-6] eliminated 154 binary clauses 5%
c [cce-6] eliminated 43 ternary clauses 2%
c [cce-6-1] eliminated 197 small clauses in 31529643 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 480 covered clauses in round 1
c [cce-6] eliminated 480 covered clauses in TOTAL during 1 rounds
c [elim-15] 315 variables 14% will be scheduled this time
c [elim-15] scheduled 315 variables 14%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] incomplete 282 not tried 12% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 3 = 0% variables out of 2278
c [simplification-17] removed 3 variables 0.1% (2275 remain 1%)
c [simplification-17] removed 1292 irredundant clauses 0.6% (208075 remain 16%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 474064 = 948128 / 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 4277424
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  649.7    2275   207844   3305225   95143   1626  4593  43 13.1 174.5   47
c -  661.4    2275   207789   3367398   96317   1628  4596  40 13.2 172.0   47
c -  669.1    2275   207429   3441310   98577   1699  4626  38 13.2 169.9   61
c -  676.8    2275   206764   3503464  100783   1744  4698  42 13.2 168.2   61
c -  681.1    2275   206691   3560756  101639   1744  4700  37 13.2 167.9   47
c -  685.4    2275   206668   3616995  102606   1745  4701  41 13.2 167.5   47
c -  689.5    2275   206647   3674107  103468   1745  4701  44 13.1 167.1   47
c -  694.6    2275   206617   3732550  104464   1746  4701  39 13.1 166.7   47
c -  699.7    2275   206585   3790740  105719   1747  4702  42 13.1 166.4   47
c i  699.7    2274   206585   3791158  105921   1747  4703  43 13.1 166.3   48
c i  704.2    2273   206397   3840522  137129   1839  4730  34 13.0 166.0   67
c i  704.2    2266   206394   3840617  137171   1847  4734  33 13.0 166.0   67
c i  709.0    2259   205542   3877172  162946   2008  4857  39 13.0 165.7   68
c -  709.4    2253   205407   3880765  111008   2008  4858  38 13.0 165.7   62
c -  714.7    2253   205066   3943347  112481   2022  4867  41 13.0 165.5   61
c -  721.1    2253   204968   4004918  113310   2024  4872  35 13.0 165.2   61
c -  727.8    2253   204909   4066598  114108   2025  4873  41 13.0 165.0   61
c -  734.6    2253   204794   4129048  115155   2028  4877  43 13.0 164.7   61
c -  741.4    2253   204766   4191850  116050   2032  4877  35 13.0 164.4   61
c -  749.3    2253   204714   4256385  116913   2031  4880  36 13.0 164.1   61
c 
c [simplification-18] limit of 4277888 conflicts hit after 4277889 conflicts
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 2253 free variables schedulable
c [ternres-16] 114 ternary resolvents (28 bin, 86 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-32] removed 68 variables
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 37 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 2207 variables 100%
c [block-8] limit of 100000000 steps penalty 3 = 3 + 0
c [block-8] incomplete 49 not tried 2%
c [block-8] transition to [ all 1 rem 1 ] state
c [block-8] eliminated 13115 blocked clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2054 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] incomplete 321 not tried 16% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 87 = 4% variables out of 2054
c [rephase-8] after 4277889 conflicts (new increment 2560000, next 6837889)
c [flushphases] 0 phases reset
c [simplification-18] removed 286 variables 12.7% (1967 remain 1%)
c [simplification-18] removed 16279 irredundant clauses 8.0% (188359 remain 14%)
c [simplification-18] maximum reduction of 13% = max (13%, 8%)
c [simplification-18] large reduction 13% >= 5% limit
c [simplification-18] new conflict interval 42778 = min (4277889/100, 1000000)
c [simplification-18] penalized conflict interval 42778 = 1 * 42778
c [simplification-18] new conflict limit 4320667
c [tabula-rasa-2] number clauses 188359 drops below limit 194214
c [flush-cache] 0 binary, 0 ternary, 104693 large
c [flushphases] 1967 phases reset fully
c [phase-5] phase bias: 293 positive 59%, 205 negative 41%
c [tabula-rasa-2] new conflict interval 20000
c [tabula-rasa-2] new conflict limit 4297889
c [tabula-rasa-2] new variable limit 491 and clause limit 94179
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  764.2    1967   188134   4285157    2525   1595  3738  44 13.0 163.9   37
c -  764.6    1967   188107   4289605    3592   1597  3740  38 13.0 163.8   37
c -  765.3    1967   188086   4294392    4316   1603  3745  32 13.0 163.8   37
c 
c [simplification-19] limit of 4297907 conflicts hit after 4297908 conflicts
c [ternres-17] limit 200000000 with penalty 0 = 0 + 0
c [ternres-17] all 1967 free variables schedulable
c [ternres-17] 111 ternary resolvents (11 bin, 100 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-33] removed 4 variables
c [treelook-4] limit 1964238 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 2028 literals 52%
c [treelook-4] scheduling used 396098 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1964238 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 2067757 steps
c [treelook-4] 1945 literals remain 50%
c [treelook-4] 504 variables remain to probed next time 26%
c [treelook-4] removed 0 variables, found 439 hbrs
c [lift-13] limit 10000000 with penalty 1 = 1 + 0
c [lift-13] using 67 probes 3%
c [lift-13-1] found 0 units 1 impls in round 1
c [lift-13-2] found 0 units 0 impls in round 2
c [lift-13-3] found 0 units 3 impls in round 3
c [lift-13-4] found 0 units 0 impls in round 4
c [lift-13-5] found 0 units 0 impls in round 5
c [lift-13] 0 units, 4 impls, 1 eqs in 6 rounds
c [lift-13] 519 variables remain 26% (1443 retained)
c [lift-13] removed 1 variables
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 39 transitive binary clauses
c [elim-17] 225 variables 11% will be scheduled this time
c [elim-17] scheduled 225 variables 11%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] incomplete 194 not tried 10% in round 1
c [elim-17] transition to [ all 0 rem 1 ] state
c [elim-17] eliminated 0 = 0% variables out of 1962
c [bca-9] limit of 10000000 steps
c [bca-9] 3360 out of 3926 literals actually usable 86%
c [bca-9] added 0 blocked clauses in 19683 steps
c [rephase-9] after 4297908 conflicts (new increment 20000, next 4317908)
c [flushphases] 706 phases reset
c [phase-6] phase bias: 4 positive 36%, 7 negative 64%
c [simplification-19] removed 5 variables 0.3% (1962 remain 1%)
c [simplification-19] removed 954 irredundant clauses 0.5% (187126 remain 14%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-19] new conflict interval 30000
c [simplification-19] penalized conflict interval 30000 = 1 * 30000
c [simplification-19] new conflict limit 4327908
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  773.8    1962   187122   4299565    4973   1701  4165  36 13.0 163.8   33
c -  774.3    1962   187076   4304983    5763   1702  4165  37 13.0 163.8   33
c -  775.0    1962   187066   4310835    6425   1703  4165  34 13.0 163.9   33
c -  775.9    1962   187059   4317562    7155   1703  4166  35 13.0 163.9   33
c -  777.0    1962   186943   4325303    7936   1704  4168  38 13.0 164.0   33
c 
c [simplification-20] limit of 4327920 conflicts hit after 4327922 conflicts
c [ternres-18] limit 200000000 with penalty 0 = 0 + 0
c [ternres-18] all 1962 free variables schedulable
c [ternres-18] 22 ternary resolvents (11 bin, 11 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-35] removed 2 variables
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 3 probes 0%
c [lift-14-1] found 0 units 0 impls in round 1
c [lift-14-2] found 0 units 0 impls in round 2
c [lift-14-3] found 0 units 0 impls in round 3
c [lift-14-4] found 0 units 0 impls in round 4
c [lift-14-5] found 0 units 0 impls in round 5
c [lift-14] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-14] 516 variables remain 26% (1444 retained)
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 23 transitive binary clauses
c [block-9] 49 variables 2% will be scheduled this time
c [block-9] scheduled 49 variables 2%
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 0 blocked clauses
c [cce-7] limit of 78964747 steps penalty 3 = 3 + 0
c [cce-7-1] eliminated 12 clauses out of 12 (100%) of length 14
c [cce-7-1] eliminated 29 clauses out of 29 (100%) of length 13
c [cce-7-1] eliminated 11 clauses out of 19 (58%) of length 12
c [cce-7-1] eliminated 2 clauses out of 22 (9%) of length 11
c [cce-7-1] eliminated 588 clauses out of 58064 (1%) of length 9
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 642 large clauses in 78964748 steps
c [cce-7-1] allowing another 39482374 steps for small clauses
c [cce-7] scheduling 4353 clauses = 2839 binary + 1514 ternary
c [cce-7] tried to eliminate 2946 small clauses 68%
c [cce-7] eliminated 506 small clauses 12%
c [cce-7] eliminated 429 binary clauses 15%
c [cce-7] eliminated 77 ternary clauses 5%
c [cce-7-1] eliminated 506 small clauses in 78964748 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1148 covered clauses in round 1
c [cce-7] eliminated 1148 covered clauses in TOTAL during 1 rounds
c [rephase-10] after 4327922 conflicts (new increment 40000, next 4367922)
c [flushphases] 342 phases reset
c [phase-7] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-20] removed 2 variables 0.1% (1960 remain 1%)
c [simplification-20] removed 1148 irredundant clauses 0.6% (185636 remain 14%)
c [simplification-20] maximum reduction of 1% = max (0%, 1%)
c [simplification-20] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-20] new conflict interval 45000
c [simplification-20] penalized conflict interval 45000 = 1 * 45000
c [simplification-20] new conflict limit 4372922
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  784.6    1960   185502   4334259    9313   1790  4583  41 13.0 164.0   33
c -  786.1    1960   185454   4342393   10037   1789  4584  38 13.0 164.0   33
c -  787.6    1960   185322   4352397   10931   1798  4587  42 13.0 164.0   33
c -  788.7    1960   185283   4361571   11760   1803  4588  41 13.0 164.0   33
c -  789.7    1960   185257   4371353   12579   1805  4588  43 13.0 164.0   33
c 
c [simplification-21] limit of 4372922 conflicts hit after 4372923 conflicts
c [ternres-19] limit 200000000 with penalty 0 = 0 + 0
c [ternres-19] all 1960 free variables schedulable
c [ternres-19] 45 ternary resolvents (11 bin, 34 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 9963332 penalty 4 = 4 + 0
c [card-6] found 26 at-most-one constraints of average size 3.8
c [card-6] found 56 at-most-two constraints of average size 4.0
c [card-6] using previous limit 9963332 for elimination
c [card-6] 81 out of 82 constraints (99%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] extracted 2738 xors of average arity 3.2
c [gauss-7] connected 8850 occurrences of 696 variables (average 12.7)
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 1 variables
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 30 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 1959 variables 100%
c [elim-18] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-18] incomplete 275 not tried 14% in round 1
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 145 = 7% variables out of 1959
c [rephase-11] after 4372923 conflicts (new increment 80000, next 4452923)
c [flushphases] 283 phases reset
c [phase-8] phase bias: 38 positive 61%, 24 negative 39%
c [simplification-21] removed 146 variables 7.4% (1814 remain 1%)
c [simplification-21] removed 1255 irredundant clauses 0.7% (184000 remain 14%)
c [simplification-21] maximum reduction of 7% = max (7%, 1%)
c [simplification-21] large reduction 7% >= 5% limit
c [simplification-21] new conflict interval 43729 = min (4372923/100, 45000)
c [simplification-21] penalized conflict interval 43729 = 1 * 43729
c [simplification-21] new conflict limit 4416652
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  794.8    1814   183931   4382128   13179   1586  1813  41 13.0 163.8   33
c i  794.9    1813   183919   4385162   15415   1588  1815  40 13.0 163.7   34
c -  796.5    1813   183677   4394506   14363   1591  1818  43 13.0 163.5   33
c -  799.0    1813   183380   4410028   15767   1613  1829  44 13.0 163.1   33
c 
c [simplification-22] limit of 4416706 conflicts hit after 4416706 conflicts
c [ternres-20] limit 200000000 with penalty 0 = 0 + 0
c [ternres-20] all 1813 free variables schedulable
c [ternres-20] 112 ternary resolvents (14 bin, 98 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-37] removed 8 variables
c [basicprobe-4] limit 25000000 penalty 2 = 2 + 0
c [basicprobe-4-0] 638 sched 35%, 0 failed, 0 lifted, 80 hbrs
c [basicprobe-4-1] 629 sched 35%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-1] fully completed probing
c [basicprobe-4-1] removed 0 variables, found 80 hbrs
c [bate-3] eliminated 2 asymmetric tautologies during probing
c [lift-15] limit 10000000 with penalty 1 = 1 + 0
c [lift-15] using 21 probes 1%
c [lift-15-1] found 0 units 3 impls in round 1
c [lift-15-2] found 0 units 0 impls in round 2
c [lift-15-3] found 0 units 0 impls in round 3
c [lift-15-4] found 0 units 1 impls in round 4
c [lift-15-5] found 0 units 1 impls in round 5
c [lift-15] 0 units, 5 impls, 1 eqs in 6 rounds
c [lift-15] 392 variables remain 22% (1413 retained)
c [lift-15] removed 1 variables
c [unhide-7] limit 1250000 with penalty 4 = 4 + 0
c [unhide-7-9] 0 units, 0 failed, 1052 tauts, 0 hbrs, 3432 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 13 transitive binary clauses
c [cce-8] limit of 160761246 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 2916 clauses out of 55794 (5%) of length 9
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 2916 large clauses in 160761247 steps
c [cce-8-1] allowing another 80380623 steps for small clauses
c [cce-8] scheduling 2516 clauses = 1174 binary + 1342 ternary
c [cce-8] tried to eliminate 2516 small clauses 100%
c [cce-8] eliminated 131 small clauses 5%
c [cce-8] eliminated 59 binary clauses 5%
c [cce-8] eliminated 72 ternary clauses 5%
c [cce-8-1] eliminated 131 small clauses in 97684595 steps
c [cce-8-1] completed small round (ACCE)
c [cce-8-1] eliminated 3047 covered clauses in round 1
c [cce-8-2] eliminated 1931 clauses out of 102086 (2%) of length 8
c [cce-8-2] incomplete large round (ACCE)
c [cce-8-2] eliminated 1931 large clauses in 63076652 steps
c [cce-8-2] allowing another 31538326 steps for small clauses
c [cce-8] scheduling 2385 clauses = 1115 binary + 1270 ternary
c [cce-8] tried to eliminate 2385 small clauses 100%
c [cce-8] eliminated 1 small clauses 0%
c [cce-8] eliminated 1 binary clauses 0%
c [cce-8-2] eliminated 1 small clauses in 47190503 steps
c [cce-8-2] completed small round (ACCE)
c [cce-8-2] eliminated 1932 covered clauses in round 2
c [cce-8-3] eliminated 447 clauses out of 19098 (2%) of length 7
c [cce-8-3] incomplete large round (ACCE)
c [cce-8-3] eliminated 447 large clauses in 15886149 steps
c [cce-8-3] allowing another 7943074 steps for small clauses
c [cce-8] scheduling 2384 clauses = 1114 binary + 1270 ternary
c [cce-8] tried to eliminate 1203 small clauses 50%
c [cce-8-3] incomplete small round (ACCE)
c [cce-8-3] eliminated 447 covered clauses in round 3
c [cce-8] eliminated 5426 covered clauses in TOTAL during 3 rounds
c [elim-19] 178 variables 10% will be scheduled this time
c [elim-19] scheduled 178 variables 10%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] incomplete 152 not tried 8% in round 1
c [elim-19] transition to [ all 0 rem 1 ] state
c [elim-19] eliminated 0 = 0% variables out of 1805
c [phase-9] phase bias: 3 positive 30%, 7 negative 70%
c [simplification-22] removed 8 variables 0.4% (1805 remain 1%)
c [simplification-22] removed 6925 irredundant clauses 3.8% (176189 remain 13%)
c [simplification-22] maximum reduction of 4% = max (0%, 4%)
c [simplification-22] geometric conflict interval increment 9000 = 45000 / 5
c [simplification-22] new conflict interval 54000
c [simplification-22] penalized conflict interval 54000 = 1 * 54000
c [simplification-22] new conflict limit 4470706
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  815.9    1805   175792   4427253   16712   1449  1907  38 12.9 162.9   33
c -  818.0    1805   175242   4443841   18567   1488  1926  38 12.9 162.7   41
c -  820.2    1805   174989   4461324   19854   1500  1937  38 13.0 162.4   41
c 
c [simplification-23] limit of 4470732 conflicts hit after 4470732 conflicts
c [ternres-21] limit 200000000 with penalty 0 = 0 + 0
c [ternres-21] all 1805 free variables schedulable
c [ternres-21] 81 ternary resolvents (9 bin, 72 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-39] removed 12 variables
c [cgrclsr-6] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-6] all 1793 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 21 probes 1%
c [lift-16-1] found 0 units 0 impls in round 1
c [lift-16-2] found 0 units 0 impls in round 2
c [lift-16-3] found 0 units 1 impls in round 3
c [lift-16-4] found 0 units 0 impls in round 4
c [lift-16-5] found 0 units 0 impls in round 5
c [lift-16] 0 units, 1 impls, 1 eqs in 6 rounds
c [lift-16] 366 variables remain 20% (1426 retained)
c [lift-16] removed 1 variables
c [cliff-6] limit of 6250000 steps penalty 4 = 4 + 0
c [cliff-6] failed 0, lifted 0
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 19 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 1792 variables 100%
c [block-10] limit of 100000000 steps penalty 3 = 3 + 0
c [block-10] incomplete 58 not tried 3%
c [block-10] transition to [ all 1 rem 1 ] state
c [block-10] eliminated 7 blocked clauses
c [block-10] 7 < 1/1000 * 174823 = 174 considered unsuccessful
c [cce-9] limit of 324529401 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 2783 clauses out of 49394 (6%) of length 9
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 2783 large clauses in 324529402 steps
c [cce-9-1] allowing another 162264701 steps for small clauses
c [cce-9] scheduling 1964 clauses = 1113 binary + 851 ternary
c [cce-9] tried to eliminate 1964 small clauses 100%
c [cce-9] eliminated 171 small clauses 9%
c [cce-9] eliminated 67 binary clauses 6%
c [cce-9] eliminated 104 ternary clauses 12%
c [cce-9-1] eliminated 171 small clauses in 174576626 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 2954 covered clauses in round 1
c [cce-9-2] eliminated 1806 clauses out of 98568 (2%) of length 8
c [cce-9-2] incomplete large round (ACCE)
c [cce-9-2] eliminated 1806 large clauses in 149952776 steps
c [cce-9-2] allowing another 74976388 steps for small clauses
c [cce-9] scheduling 1793 clauses = 1046 binary + 747 ternary
c [cce-9] tried to eliminate 1793 small clauses 100%
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 1806 covered clauses in round 2
c [cce-9-3] eliminated 769 clauses out of 20819 (4%) of length 7
c [cce-9-3] incomplete large round (ACCE)
c [cce-9-3] eliminated 769 large clauses in 64207727 steps
c [cce-9-3] allowing another 32103863 steps for small clauses
c [cce-9] scheduling 1793 clauses = 1046 binary + 747 ternary
c [cce-9] tried to eliminate 1793 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 769 covered clauses in round 3
c [cce-9-4] eliminated 176 clauses out of 641 (27%) of length 6
c [cce-9-4] eliminated 75 clauses out of 211 (36%) of length 5
c [cce-9-4] eliminated 159 clauses out of 1806 (9%) of length 4
c [cce-9-4] completed large round (ACCE)
c [cce-9-4] eliminated 410 large clauses in 13012585 steps
c [cce-9-4] allowing another 6506292 steps for small clauses
c [cce-9] scheduling 1793 clauses = 1046 binary + 747 ternary
c [cce-9] tried to eliminate 1793 small clauses 100%
c [cce-9] eliminated 2 small clauses 0%
c [cce-9] eliminated 2 ternary clauses 0%
c [cce-9-4] eliminated 2 small clauses in 17202676 steps
c [cce-9-4] completed small round (ACCE)
c [cce-9-4] completed small and large (ACCE)
c [cce-9-4] eliminated 412 covered clauses in round 4
c [cce-9-5] completed large round (ACCE)
c [cce-9-5] allowing another 0 steps for small clauses
c [cce-9] scheduling 1791 clauses = 1046 binary + 745 ternary
c [cce-9] tried to eliminate 807 small clauses 45%
c [cce-9-5] incomplete small round (ACCE)
c [cce-9-5] eliminated 0 covered clauses in round 5
c [cce-9] eliminated 5941 covered clauses in TOTAL during 5 rounds
c [rephase-12] after 4470732 conflicts (new increment 160000, next 4630732)
c [flushphases] 283 phases reset
c [phase-10] phase bias: 5 positive 62%, 3 negative 38%
c [simplification-23] removed 13 variables 0.7% (1792 remain 1%)
c [simplification-23] removed 5949 irredundant clauses 3.4% (168875 remain 13%)
c [simplification-23] maximum reduction of 3% = max (1%, 3%)
c [simplification-23] geometric conflict interval increment 13500 = 54000 / 4
c [simplification-23] new conflict interval 67500
c [simplification-23] penalized conflict interval 67500 = 1 * 67500
c [simplification-23] new conflict limit 4538232
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  840.4    1792   168509   4482156   20833   1698  1992  45 12.9 162.3   33
c -  843.0    1792   168175   4506518   23058   1749  2019  43 12.9 162.2   33
c i  844.6    1791   168146   4529643   35577   1806  2032  39 12.9 162.1   43
c -  844.6    1785   168146   4530754   24134   1806  2032  39 12.9 162.1   42
c 
c [simplification-24] limit of 4538290 conflicts hit after 4538291 conflicts
c [ternres-22] limit 200000000 with penalty 0 = 0 + 0
c [ternres-22] all 1785 free variables schedulable
c [ternres-22] 40 ternary resolvents (9 bin, 31 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-40] removed 25 variables
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 16 probes 1%
c [lift-17-1] found 0 units 0 impls in round 1
c [lift-17-2] found 0 units 0 impls in round 2
c [lift-17-3] found 0 units 0 impls in round 3
c [lift-17-4] found 0 units 1 impls in round 4
c [lift-17-5] found 0 units 0 impls in round 5
c [lift-17] 0 units, 1 impls, 1 eqs in 6 rounds
c [lift-17] 340 variables remain 19% (1426 retained)
c [lift-17] removed 1 variables
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 13 transitive binary clauses
c [cce-10] limit of 654635361 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 8353 clauses out of 44855 (19%) of length 9
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 8353 large clauses in 654635362 steps
c [cce-10-1] allowing another 327317681 steps for small clauses
c [cce-10] scheduling 1801 clauses = 1039 binary + 762 ternary
c [cce-10] tried to eliminate 1801 small clauses 100%
c [cce-10] eliminated 1 small clauses 0%
c [cce-10] eliminated 1 binary clauses 0%
c [cce-10-1] eliminated 1 small clauses in 337880399 steps
c [cce-10-1] completed small round (ACCE)
c [cce-10-1] eliminated 8354 covered clauses in round 1
c [cce-10-2] eliminated 4410 clauses out of 96953 (5%) of length 8
c [cce-10-2] incomplete large round (ACCE)
c [cce-10-2] eliminated 4410 large clauses in 316754963 steps
c [cce-10-2] allowing another 158377481 steps for small clauses
c [cce-10] scheduling 1800 clauses = 1038 binary + 762 ternary
c [cce-10] tried to eliminate 1800 small clauses 100%
c [cce-10-2] completed small round (ACCE)
c [cce-10-2] eliminated 4410 covered clauses in round 2
c [cce-10-3] eliminated 1434 clauses out of 20232 (7%) of length 7
c [cce-10-3] incomplete large round (ACCE)
c [cce-10-3] eliminated 1434 large clauses in 147912474 steps
c [cce-10-3] allowing another 73956237 steps for small clauses
c [cce-10] scheduling 1800 clauses = 1038 binary + 762 ternary
c [cce-10] tried to eliminate 1800 small clauses 100%
c [cce-10-3] completed small round (ACCE)
c [cce-10-3] eliminated 1434 covered clauses in round 3
c [cce-10-4] eliminated 15 clauses out of 479 (3%) of length 6
c [cce-10-4] eliminated 7 clauses out of 1641 (0%) of length 4
c [cce-10-4] completed large round (ACCE)
c [cce-10-4] eliminated 22 large clauses in 10139309 steps
c [cce-10-4] allowing another 5069654 steps for small clauses
c [cce-10] scheduling 1800 clauses = 1038 binary + 762 ternary
c [cce-10] tried to eliminate 1800 small clauses 100%
c [cce-10] eliminated 1 small clauses 0%
c [cce-10] eliminated 1 ternary clauses 0%
c [cce-10-4] eliminated 1 small clauses in 15474502 steps
c [cce-10-4] completed small round (ACCE)
c [cce-10-4] eliminated 23 covered clauses in round 4
c [cce-10-5] completed large round (ACCE)
c [cce-10-5] allowing another 0 steps for small clauses
c [cce-10] scheduling 1799 clauses = 1038 binary + 761 ternary
c [cce-10] tried to eliminate 1799 small clauses 100%
c [cce-10-5] completed small round (ACCE)
c [cce-10-5] eliminated 0 covered clauses in round 5
c [cce-10] eliminated 14221 covered clauses in TOTAL during 5 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 1766 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] incomplete 250 not tried 14% in round 1
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 147 = 8% variables out of 1766
c [bca-10] limit of 10000000 steps
c [bca-10] 1817 out of 3240 literals actually usable 56%
c [bca-10] added 11 blocked clauses in 25771 steps
c [phase-11] phase bias: 8 positive 44%, 10 negative 56%
c [simplification-24] removed 166 variables 9.3% (1619 remain 1%)
c [simplification-24] removed 21632 irredundant clauses 12.9% (146495 remain 11%)
c [simplification-24] maximum reduction of 13% = max (9%, 13%)
c [simplification-24] large reduction 13% >= 5% limit
c [simplification-24] new conflict interval 45382 = min (4538291/100, 67500)
c [simplification-24] penalized conflict interval 45382 = 1 * 45382
c [simplification-24] new conflict limit 4583673
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  877.2    1619   146210   4561115   22890   1506  1699  36 12.9 162.0   31
c -  878.5    1619   146052   4580435   24386   1539  1728  41 12.9 161.8   39
c 
c [simplification-25] limit of 4583703 conflicts hit after 4583704 conflicts
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 1619 free variables schedulable
c [ternres-23] 62 ternary resolvents (5 bin, 57 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-41] removed 6 variables
c [lift-18] limit 20000000 with penalty 0 = 0 + 0
c [lift-18] using 9 probes 1%
c [lift-18-1] found 1 units 0 impls in round 1
c [lift-18-2] found 0 units 0 impls in round 2
c [lift-18-3] found 0 units 1 impls in round 3
c [lift-18-4] found 0 units 1 impls in round 4
c [lift-18-5] found 0 units 0 impls in round 5
c [lift-18] 1 units, 2 impls, 0 eqs in 6 rounds
c [lift-18] 308 variables remain 19% (1304 retained)
c [lift-18] removed 1 variables
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 10 transitive binary clauses
c [transred-23] found 1 units
c [cce-11] limit of 657470233 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 7 clauses out of 7 (100%) of length 14
c [cce-11-1] eliminated 64 clauses out of 163 (39%) of length 10
c [cce-11-1] eliminated 5842 clauses out of 34548 (17%) of length 9
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 5913 large clauses in 657470234 steps
c [cce-11-1] allowing another 328735117 steps for small clauses
c [cce-11] scheduling 1670 clauses = 967 binary + 703 ternary
c [cce-11] tried to eliminate 1670 small clauses 100%
c [cce-11] eliminated 7 small clauses 0%
c [cce-11] eliminated 5 binary clauses 1%
c [cce-11] eliminated 2 ternary clauses 0%
c [cce-11-1] eliminated 62 small clauses in 337359923 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 5975 covered clauses in round 1
c [cce-11-2] eliminated 1705 clauses out of 88689 (2%) of length 8
c [cce-11-2] incomplete large round (ACCE)
c [cce-11-2] eliminated 1705 large clauses in 320110311 steps
c [cce-11-2] allowing another 160055155 steps for small clauses
c [cce-11] scheduling 1663 clauses = 962 binary + 701 ternary
c [cce-11] tried to eliminate 1663 small clauses 100%
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 1705 covered clauses in round 2
c [cce-11-3] eliminated 816 clauses out of 17524 (5%) of length 7
c [cce-11-3] incomplete large round (ACCE)
c [cce-11-3] eliminated 816 large clauses in 151500084 steps
c [cce-11-3] allowing another 75750042 steps for small clauses
c [cce-11] scheduling 1663 clauses = 962 binary + 701 ternary
c [cce-11] tried to eliminate 1663 small clauses 100%
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 816 covered clauses in round 3
c [cce-11-4] eliminated 19 clauses out of 488 (4%) of length 6
c [cce-11-4] eliminated 4 clauses out of 1551 (0%) of length 4
c [cce-11-4] completed large round (ACCE)
c [cce-11-4] eliminated 23 large clauses in 9703461 steps
c [cce-11-4] allowing another 4851730 steps for small clauses
c [cce-11] scheduling 1663 clauses = 962 binary + 701 ternary
c [cce-11] tried to eliminate 1663 small clauses 100%
c [cce-11-4] completed small round (ACCE)
c [cce-11-4] eliminated 23 covered clauses in round 4
c [cce-11-5] completed large round (ACCE)
c [cce-11-5] allowing another 0 steps for small clauses
c [cce-11] scheduling 1663 clauses = 962 binary + 701 ternary
c [cce-11] tried to eliminate 1663 small clauses 100%
c [cce-11-5] completed small round (ACCE)
c [cce-11-5] eliminated 0 covered clauses in round 5
c [cce-11] eliminated 8519 covered clauses in TOTAL during 5 rounds
c [elim-21] 143 variables 9% will be scheduled this time
c [elim-21] scheduled 143 variables 9%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] incomplete 141 not tried 9% in round 1
c [elim-21] transition to [ all 0 rem 1 ] state
c [elim-21] eliminated 0 = 0% variables out of 1611
c [phase-12] phase bias: 8 positive 47%, 9 negative 53%
c [simplification-25] removed 8 variables 0.5% (1611 remain 1%)
c [simplification-25] removed 9898 irredundant clauses 6.8% (136141 remain 10%)
c [simplification-25] maximum reduction of 7% = max (0%, 7%)
c [simplification-25] large reduction 7% >= 5% limit
c [simplification-25] new conflict interval 45837 = min (4583704/100, 67500)
c [simplification-25] penalized conflict interval 45837 = 1 * 45837
c [simplification-25] new conflict limit 4629541
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  915.5    1611   135916   4606146   26283   1627  1694  44 12.8 161.4   31
c i  915.7    1610   135910   4610883   28556   1675  1704  40 12.8 161.3   31
c -  917.1    1604   135813   4628991   27596   1684  1709  39 12.8 161.1   38
c 
c [simplification-26] limit of 4629583 conflicts hit after 4629585 conflicts
c [ternres-24] limit 200000000 with penalty 0 = 0 + 0
c [ternres-24] all 1604 free variables schedulable
c [ternres-24] 23 ternary resolvents (15 bin, 8 trn)
c [ternres-24] fully completed ternary resolution
c [gauss-8] limit 3125000 penalty 4 = 4 + 0
c [gauss-8] extracted 2225 xors of average arity 3.2
c [gauss-8] connected 7159 occurrences of 548 variables (average 13.1)
c [gauss-8] limit 3125000 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-42] removed 17 variables
c [simpleprobe-5] 829 schedulable variables 52%
c [simpleprobe-5] limit 25000000 penalty 3 = 3 + 0
c [simpleprobe-5] 792 variables remain 50% (795 retained)
c [simpleprobe-5] removed 0 variables, found 40 hbrs, 0 units
c [lift-19] limit 20000000 with penalty 0 = 0 + 0
c [lift-19] using 7 probes 0%
c [lift-19-1] found 0 units 0 impls in round 1
c [lift-19-2] found 0 units 0 impls in round 2
c [lift-19-3] found 0 units 0 impls in round 3
c [lift-19-4] found 0 units 0 impls in round 4
c [lift-19-5] found 0 units 0 impls in round 5
c [lift-19] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-19] 294 variables remain 19% (1293 retained)
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 37 transitive binary clauses
c [cce-12] limit of 660804381 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 5464 clauses out of 26620 (21%) of length 9
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 5464 large clauses in 660804382 steps
c [cce-12-1] allowing another 330402191 steps for small clauses
c [cce-12] scheduling 1975 clauses = 962 binary + 1013 ternary
c [cce-12] tried to eliminate 1975 small clauses 100%
c [cce-12] eliminated 4 small clauses 0%
c [cce-12] eliminated 2 binary clauses 0%
c [cce-12] eliminated 2 ternary clauses 0%
c [cce-12-1] eliminated 4 small clauses in 339552290 steps
c [cce-12-1] completed small round (ACCE)
c [cce-12-1] eliminated 5468 covered clauses in round 1
c [cce-12-2] eliminated 1698 clauses out of 85596 (2%) of length 8
c [cce-12-2] incomplete large round (ACCE)
c [cce-12-2] eliminated 1698 large clauses in 321252092 steps
c [cce-12-2] allowing another 160626046 steps for small clauses
c [cce-12] scheduling 1971 clauses = 960 binary + 1011 ternary
c [cce-12] tried to eliminate 1971 small clauses 100%
c [cce-12-2] completed small round (ACCE)
c [cce-12-2] eliminated 1698 covered clauses in round 2
c [cce-12-3] eliminated 1146 clauses out of 17959 (6%) of length 7
c [cce-12-3] incomplete large round (ACCE)
c [cce-12-3] eliminated 1146 large clauses in 151609070 steps
c [cce-12-3] allowing another 75804535 steps for small clauses
c [cce-12] scheduling 1971 clauses = 960 binary + 1011 ternary
c [cce-12] tried to eliminate 1971 small clauses 100%
c [cce-12-3] completed small round (ACCE)
c [cce-12-3] eliminated 1146 covered clauses in round 3
c [cce-12-4] eliminated 25 clauses out of 530 (5%) of length 6
c [cce-12-4] completed large round (ACCE)
c [cce-12-4] eliminated 25 large clauses in 9572217 steps
c [cce-12-4] allowing another 4786108 steps for small clauses
c [cce-12] scheduling 1971 clauses = 960 binary + 1011 ternary
c [cce-12] tried to eliminate 1971 small clauses 100%
c [cce-12-4] completed small round (ACCE)
c [cce-12-4] eliminated 25 covered clauses in round 4
c [cce-12-5] completed large round (ACCE)
c [cce-12-5] allowing another 0 steps for small clauses
c [cce-12] scheduling 1971 clauses = 960 binary + 1011 ternary
c [cce-12] tried to eliminate 1971 small clauses 100%
c [cce-12-5] completed small round (ACCE)
c [cce-12-5] eliminated 0 covered clauses in round 5
c [cce-12] eliminated 8337 covered clauses in TOTAL during 5 rounds
c [phase-13] phase bias: 5 positive 62%, 3 negative 38%
c [simplification-26] removed 17 variables 1.1% (1587 remain 1%)
c [simplification-26] removed 8967 irredundant clauses 6.6% (126846 remain 10%)
c [simplification-26] maximum reduction of 7% = max (1%, 7%)
c [simplification-26] large reduction 7% >= 5% limit
c [simplification-26] new conflict interval 46295 = min (4629585/100, 67500)
c [simplification-26] penalized conflict interval 46295 = 1 * 46295
c [simplification-26] new conflict limit 4675880
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  947.5    1587   126644   4656032   29233   1646  1690  44 12.8 160.7   37
c i  948.6    1586   126623   4671214   36447   1705  1708  38 12.8 160.4   38
c 
c [simplification-27] limit of 4675948 conflicts hit after 4675948 conflicts
c [ternres-25] limit 200000000 with penalty 0 = 0 + 0
c [ternres-25] all 1580 free variables schedulable
c [ternres-25] 26 ternary resolvents (6 bin, 20 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-44] removed 21 variables
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 18 transitive binary clauses
c [block-11] 58 variables 4% will be scheduled this time
c [block-11] scheduled 58 variables 4%
c [block-11] limit of 50000000 steps penalty 4 = 4 + 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-13] limit of 664716006 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 2984 clauses out of 20320 (15%) of length 9
c [cce-13-1] incomplete large round (ACCE)
c [cce-13-1] eliminated 2984 large clauses in 664716007 steps
c [cce-13-1] allowing another 332358003 steps for small clauses
c [cce-13] scheduling 1687 clauses = 960 binary + 727 ternary
c [cce-13] tried to eliminate 1687 small clauses 100%
c [cce-13] eliminated 2 small clauses 0%
c [cce-13] eliminated 2 binary clauses 0%
c [cce-13-1] eliminated 2 small clauses in 341339192 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 2986 covered clauses in round 1
c [cce-13-2] eliminated 1309 clauses out of 83722 (2%) of length 8
c [cce-13-2] incomplete large round (ACCE)
c [cce-13-2] eliminated 1309 large clauses in 323376815 steps
c [cce-13-2] allowing another 161688407 steps for small clauses
c [cce-13] scheduling 1685 clauses = 958 binary + 727 ternary
c [cce-13] tried to eliminate 1685 small clauses 100%
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 1309 covered clauses in round 2
c [cce-13-3] eliminated 1444 clauses out of 16887 (9%) of length 7
c [cce-13-3] incomplete large round (ACCE)
c [cce-13-3] eliminated 1444 large clauses in 152819465 steps
c [cce-13-3] allowing another 76409732 steps for small clauses
c [cce-13] scheduling 1685 clauses = 958 binary + 727 ternary
c [cce-13] tried to eliminate 1685 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 1444 covered clauses in round 3
c [cce-13-4] eliminated 21 clauses out of 510 (4%) of length 6
c [cce-13-4] eliminated 4 clauses out of 1544 (0%) of length 4
c [cce-13-4] completed large round (ACCE)
c [cce-13-4] eliminated 25 large clauses in 8815215 steps
c [cce-13-4] allowing another 4407607 steps for small clauses
c [cce-13] scheduling 1685 clauses = 958 binary + 727 ternary
c [cce-13] tried to eliminate 1685 small clauses 100%
c [cce-13-4] completed small round (ACCE)
c [cce-13-4] eliminated 25 covered clauses in round 4
c [cce-13-5] completed large round (ACCE)
c [cce-13-5] allowing another 0 steps for small clauses
c [cce-13] scheduling 1685 clauses = 958 binary + 727 ternary
c [cce-13] tried to eliminate 1685 small clauses 100%
c [cce-13-5] completed small round (ACCE)
c [cce-13-5] eliminated 0 covered clauses in round 5
c [cce-13] eliminated 5764 covered clauses in TOTAL during 5 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 1566 variables 100%
c [elim-22] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-22] incomplete 230 not tried 15% in round 1
c [elim-22] transition to [ all 1 rem 1 ] state
c [elim-22] eliminated 127 = 8% variables out of 1566
c [bca-11] limit of 10000000 steps
c [bca-11] 1522 out of 2880 literals actually usable 53%
c [bca-11] added 0 blocked clauses in 31641 steps
c [rephase-13] after 4675948 conflicts (new increment 320000, next 4995948)
c [flushphases] 260 phases reset
c [phase-14] phase bias: 5 positive 56%, 4 negative 44%
c [simplification-27] removed 141 variables 8.9% (1439 remain 1%)
c [simplification-27] removed 13103 irredundant clauses 10.4% (113441 remain 9%)
c [simplification-27] maximum reduction of 10% = max (9%, 10%)
c [simplification-27] large reduction 10% >= 5% limit
c [simplification-27] new conflict interval 46759 = min (4675948/100, 67500)
c [simplification-27] penalized conflict interval 46759 = 1 * 46759
c [simplification-27] new conflict limit 4722707
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  982.0    1439   113423   4696908   26993   1527  1408  37 12.8 159.6   29
c -  983.2    1439   113416   4719448   27681   1528  1408  35 12.8 158.9   29
c 
c [simplification-28] limit of 4722707 conflicts hit after 4722707 conflicts
c [ternres-26] limit 200000000 with penalty 0 = 0 + 0
c [ternres-26] all 1439 free variables schedulable
c [ternres-26] 14 ternary resolvents (8 bin, 6 trn)
c [ternres-26] fully completed ternary resolution
c [card-7] limit 10423333 penalty 4 = 4 + 0
c [card-7] found 11 at-most-one constraints of average size 3.7
c [card-7] found 38 at-most-two constraints of average size 4.0
c [card-7] using previous limit 10423333 for elimination
c [card-7] 47 out of 49 constraints (96%) meet size limits
c [card-7] no units found
c [card-7] no at-most-one constraints generated
c [decomp-45] removed 4 variables
c [lift-20] limit 10000000 with penalty 1 = 1 + 0
c [lift-20] using 8 probes 1%
c [lift-20-1] found 0 units 0 impls in round 1
c [lift-20-2] found 0 units 0 impls in round 2
c [lift-20-3] found 0 units 0 impls in round 3
c [lift-20-4] found 0 units 0 impls in round 4
c [lift-20-5] found 0 units 0 impls in round 5
c [lift-20] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-20] 231 variables remain 16% (1204 retained)
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 8 transitive binary clauses
c [cce-14] limit of 667093346 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-14-1] eliminated 14 clauses out of 14 (100%) of length 12
c [cce-14-1] eliminated 15 clauses out of 23 (65%) of length 11
c [cce-14-1] eliminated 1 clauses out of 71 (1%) of length 10
c [cce-14-1] eliminated 263 clauses out of 16136 (2%) of length 9
c [cce-14-1] eliminated 119 clauses out of 77902 (0%) of length 8
c [cce-14-1] incomplete large round (ACCE)
c [cce-14-1] eliminated 413 large clauses in 667093347 steps
c [cce-14-1] allowing another 333546673 steps for small clauses
c [cce-14] scheduling 1577 clauses = 886 binary + 691 ternary
c [cce-14] tried to eliminate 1577 small clauses 100%
c [cce-14] eliminated 6 small clauses 0%
c [cce-14] eliminated 2 binary clauses 0%
c [cce-14] eliminated 4 ternary clauses 1%
c [cce-14-1] eliminated 6 small clauses in 340081454 steps
c [cce-14-1] completed small round (ACCE)
c [cce-14-1] eliminated 419 covered clauses in round 1
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 13 basic ate = 6 trn 46% + 7 lrg 54% in 3 updates
c bcas: 11 count, 322 added (0 skipped), 498918 steps
c bkwd: tried 174997 clauses, 204709 lits, 1.17 lits/clause
c bkwd: checked 37322057 occs, 213.27 occs/clause, 182.32 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 7 large
c bkwd: strengthened 2 binary, 0 ternary (0% self), 145840 large (100% self)
c blkd: 11 bces, 35455 removed, 1085888443 resolutions, 1140563346 steps
c blkd: 1291 blocking literals 0%, 333 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 7 count, 0 units, 0 am1, 34296742 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 7280 subsumed
c card: 265 at-most-one constraints found, average size 4.52
c card: 265 at-most-one constraints used 100%, average size 4.52
c card: 297 at-most-two constraints found, average size 4.01
c card: 291 at-most-two constraints used 98%, average size 4.01
c cces: 14 cces, 109548 eliminated, 107469 ate 98%, 2079 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 6 count, 2631926 esteps, 8462 csteps
c cgrs: 0 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 205 extracted (36 ands 18%, 161 xors 79%, 8 ites 4%)
c clff: 6 cliffs, 0 lifted, 0 failed
c clff: 178957 decisions, 42508752 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 5816471 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 144 gcs, 0 rescored clauses, 2373 rescored vars
c dcps: 45 decompositions, 33920 equivalent 13%
c deco: 1181 decision-only clauses 0%, 47% reduction
c decs: 6122506 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 23862 flipped 0.390% (in 200 phases)
c elms: 22 elims, 104342 eliminated 39%
c elms: 24 rounds, 1.1 rounds/bve
c elms: 68144 small 65%, 35865 large 34%
c elms: 78522 tried small, 68145 succeeded 87%, 10377 failed 13%
c elms: 20133 subsumed, 27109 strengthened, 1778 blocked
c elms: 16456946 copies, 251590759 resolutions, 1452719 ipos
c elms: 3575303 subchks, 3109701 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 8 extractions, 39363 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 0 binary and 3 ternary equations
c gaus: 2 gc, 57718136 steps, 28859068 extr 50%, 2918048 elim 5%
c glue: 12.8 orig avg, 12.8 real avg, 3.3 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 20761 = 15119 simple + 5170 trn 73% + 472 lrg 25%, 404 sub 2%
c hght: 159 average, 12.41 height/glue
c ints: 122550 luby (37058615 steps), 0 inout (0 steps)
c lift: 20 phases, 31116 probed (10436 level1 34%, 20680 level2 66%)
c lift: 6 units, 29 equivalences, 235 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4510978 clauses, 27.4 length
c lrnd: 380101 uips 8%, 3895602 flips 86%
c mega: 0 count, 0 failed, 0 rounds
c mins: 123545527 learned lits, 9% minimized
c mins: 4478080 mins 99%, 1652 bin 0%, 30065 size 1%, 1181 deco 0%
c move: moved 4510978, 1722 bin 0%, 1727 trn 0%, 0 lrg 0%
c otfs: str 977928 dyn (926033 red, 51895 irr) 211729 drv 22%, 766199 rst 78%
c otfs: sub 65781 dyn (30198 red, 35583 irr)
c phas: 14 computed, 4918 set, 1609 pos (33%), 3309 neg (67%)
c prbs: 4 basic, 12766 probed, 14 failed, 0 lifted
c prbs: 5 simple, 178887 probed, 30 failed, 1168 eqs
c prbs: 4 treelook, 108 probed, 0 failed, 0 lifted
c prps: 235467294 props, 38 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 115690164 searches, 18584026 hits, 16% 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: 142 count, 0 reset, 21 acts 15%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 142 arith 100%, 0 double 0%
c rmbd: 1635 removed, 723 red 44%
c rphs: 13 recomputed phases
c rsts: 2445 restarts 2%, 120105 skipped 98%
c rsts: 0 saturating 0%, 120057 agile 100%, 48 reuse 0%
c rsts: 1899.0 avg interval, 1899.0 scaled, 1.0 factor
c rsts: 333 kept 13.6% average 31.2%
c simp: 28 count (28 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 4510978 count (3196205 tried 0.7), 531941 sub out of 4507223 (11.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 2 count
c tops: 126502 fixed 48%, 19 its, 248563.53 confs/it
c trvs: 62184335453 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 265.0 search traversals per propagation, 13153.8 per conflict
c trvs: 1.9 search traversals per search visit
c trds: 26 transitive reductions, 1596 removed, 1 failed
c trds: 123204 nodes, 154833 edges, 5953529 steps
c trim: 3563490 words, 13.6 MB
c trnr: 26 count, 397 bin, 3233 trn, 37677698 steps
c unhd: 7 count, 9 rounds, 15954711 steps
c unhd: 838 non-trivial sccs of average size 2.2
c unhd: 31 units, 2 bin, 29 trn, 0 lrg
c unhd: 235 failed, 232 stamp, 0 lits, 1 bin, 2 trn, 0 lrg
c unhd: 5329 tauts, 39 bin 1%, 2029 trn 38%, 2137 lrg 40%
c unhd: 5329 tauts, 1124 stamp 21%, 4150 red 78%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 19245 str, 2 bin 0%, 1629 trn 8%, 17614 lrg 92%, 15871 red 82%
c vars: 1435 remaining 1% and 264764 removed 99% out of 266199
c vars: 126502 fixed 48%, 104342 eliminated 39%, 33920 equivalent 13%
c vsts: 33417475097 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 142.3 search visits per propagation, 7062.6 per conflict
c wchs: 16277068124 pushed, 9903147 enlarged, 251 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   4507223 100   3646358 100  39924700 100  31629497 100   2918789 100
c 
c  0     131020   3         0   0  11171673  28   4819677  15    309046  11 
c  1     196520   4     75562   2   9539471  24   5270821  17    362336  12 
c  2     904692  20    772233  21  10392087  26<  8851866  28<   793401  27<
c  3    1246250  28<  1082997  30<  4975376  12   6332343  20    782418  27 
c  4    1245801  28   1053140  29   2569706   6   4152646  13    458713  16 
c  5     649233  14    543604  15   1050392   3   1747040   6    133162   5 
c  6     126291   3    112570   3    212331   1    426344   1     73231   3 
c  7       7210   0      6052   0     13382   0     28183   0      6407   0 
c  8        202   0       200   0       277   0       570   0        75   0 
c  9          4   0         0   0         5   0         7   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.3           3.4           1.6           2.2           2.5
c std             1.3           1.1           1.4           1.5           1.4
c 
c  159.429  16% cce
c  110.381  11% elim
c   47.671   5% block
c   38.360   4% analysis
c   11.251   1% mincls
c    9.530   1% gc
c    6.560   1% decomp
c    5.744   1% bump
c    5.591   1% backward
c    5.155   1% probe
c    4.731   0% decide
c    3.801   0% defrag
c    2.262   0% lift
c    2.180   0% cliff
c    1.762   0% gauss
c    1.422   0% bca
c    1.417   0% reduce
c    1.392   0% unhide
c    1.094   0% transred
c    1.021   0% cgrclsr
c    0.931   0% card
c    0.547   0% phase
c    0.255   0% restart
c    0.211   0% ternres
c    0.104   0% tabularasa
c    0.022   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c    2.688   0% probe simple     52%
c    1.395   0% probe basic      27%
c    1.072   0% probe tree-look  21%
c ==================================
c   12.875   1% preprocessing     4%
c  328.462  33% inprocessing     96%
c ==================================
c  341.337  34% simplifying
c  657.801  66% search
c ==================================
c  999.142 100% all
c 
c 6122506 decisions, 6127.8 decisions/sec
c 4722707 conflicts, 4726.8 conflicts/sec
c 235467294 propagations, 0.2 megaprops/sec
c 999.1 seconds, 196.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
