c launch: /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2
c host: atom17
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/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.025-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 95456 483561' header
c read 95456 variables, 483561 clauses, 1149911 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 67515 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   67515   276407         0       0      0     0  24  0.0   0.0   14
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 28242 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 28242 out of 28242 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 29475 variables
c [simpleprobe-1] all 65981 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 910 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 910 variables, found 1430 hbrs, 62 units
c [unhide-1] limit 106953 based on 213907 irredundant clauses
c [unhide-1-1] 0 units, 6 failed, 5772 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 65049 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 36692 variables 56% in round 1 in 7334031 steps
c [elim-1-1] backward subsumption/strengthening limit 14668062
c [elim-1-1] subsumed 24 and strengthened 1733 clauses in 14668146 steps
c [elim-1-1] rescheduled 1792 variables 3% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 375724 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 36692 = 56% variables out of 65049
c [phase-1] phase bias: 4302 positive 15%, 24055 negative 85%
c [simplification-1] removed 38408 variables 57.5% (28357 remain 42%)
c [simplification-1] removed 103500 irredundant clauses 37.4% (172907 remain 63%)
c [simplification-1] maximum reduction of 58% = max (58%, 37%)
c [simplification-1] large reduction 58% >= 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] 10820, max 23650, min4 5540 at 26%, min10 3690 at 11%
c [cut-width] cut-width based bias -1
c [decision-order] bias -1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    1.4   28357   172907        66      59      0  1276  29 15.7 846.4    9
c R    1.4   28357   172907       173     155      0  1278   8 16.8 510.5    9
c R    1.5   28357   172907       423     373      0  1278   5 21.4 354.4   10
c R    1.6   28357   172907      1006     853      8  1284   4 33.0 318.7   10
c 
c [simplification-2] limit of 1012 conflicts hit after 1012 conflicts
c [simpleprobe-2] all 28357 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 116 variables
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 116 variables, found 1556 hbrs, 17 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 46475 literals 82%
c [treelook-1] scheduling used 300005 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 342432 steps
c [treelook-1] 46471 literals remain 82%
c [treelook-1] 28134 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 173 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 17005 probes remain 60% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 0 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 2 failed, 196 tauts, 0 hbrs, 11697 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 28239 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 48 blocked clauses
c [block-1] 48 < 1/1000 * 171940 = 171 considered unsuccessful
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 268 clauses out of 429 (62%) of length 63
c [cce-1-1] eliminated 208 clauses out of 404 (51%) of length 62
c [cce-1-1] eliminated 11 clauses out of 19 (58%) of length 61
c [cce-1-1] eliminated 11 clauses out of 18 (61%) of length 60
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 58
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 46
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 44
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 42
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 38
c [cce-1-1] eliminated 1 clauses out of 19 (5%) of length 37
c [cce-1-1] eliminated 2 clauses out of 84 (2%) of length 35
c [cce-1-1] eliminated 2 clauses out of 37 (5%) of length 34
c [cce-1-1] eliminated 48 clauses out of 101 (48%) of length 33
c [cce-1-1] eliminated 68 clauses out of 139 (49%) of length 32
c [cce-1-1] eliminated 4 clauses out of 20 (20%) of length 31
c [cce-1-1] eliminated 3 clauses out of 10 (30%) of length 30
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 27
c [cce-1-1] eliminated 31 clauses out of 61 (51%) of length 25
c [cce-1-1] eliminated 31 clauses out of 91 (34%) of length 24
c [cce-1-1] eliminated 90 clauses out of 150 (60%) of length 23
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 22
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 21
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 20
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 19
c [cce-1-1] eliminated 61 clauses out of 122 (50%) of length 18
c [cce-1-1] eliminated 59 clauses out of 119 (50%) of length 17
c [cce-1-1] eliminated 61 clauses out of 122 (50%) of length 16
c [cce-1-1] eliminated 60 clauses out of 121 (50%) of length 15
c [cce-1-1] eliminated 61 clauses out of 122 (50%) of length 14
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 13
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 12
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 11
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 10
c [cce-1-1] eliminated 60 clauses out of 120 (50%) of length 9
c [cce-1-1] eliminated 61 clauses out of 119 (51%) of length 8
c [cce-1-1] eliminated 70 clauses out of 111 (63%) of length 7
c [cce-1-1] eliminated 44 clauses out of 135 (33%) of length 6
c [cce-1-1] eliminated 10 clauses out of 51 (20%) of length 5
c [cce-1-1] eliminated 16 clauses out of 95 (17%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1833 large clauses in 87394227 steps
c [cce-1-1] allowing another 43697113 steps for small clauses
c [cce-1] scheduling 167548 clauses = 166463 binary + 1085 ternary
c [cce-1] tried to eliminate 8426 small clauses 5%
c [cce-1] eliminated 2773 small clauses 2%
c [cce-1] eliminated 2773 binary clauses 2%
c [cce-1-1] eliminated 2773 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4606 covered clauses in round 1
c [cce-1] eliminated 4606 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 28233 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 7810 not tried 28% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 316 = 1% variables out of 28233
c [bca-1] limit of 10000000 steps
c [bca-1] 47244 out of 55836 literals actually usable 85%
c [bca-1] added 4608 blocked clauses in 129139 steps
c [phase-2] phase bias: 31 positive 79%, 8 negative 21%
c [simplification-2] removed 440 variables 1.6% (27917 remain 41%)
c [simplification-2] removed 6196 irredundant clauses 3.6% (166711 remain 60%)
c [simplification-2] maximum reduction of 4% = max (2%, 4%)
c [simplification-2] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-2] new conflict interval 4000
c [simplification-2] penalized conflict interval 4000 = 1 * 4000
c [simplification-2] new conflict limit 5012
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   12.3   27916   166711      1735    1070     11  9922   1 47.8 270.9   10
c R   12.4   27916   166711      2361    1491     12  9923   2 95.7 280.6   12
c i   12.5   27915   166711      2750    1821     15  9925   3 91.3 267.3   12
c i   12.5   27908   166711      2754    1821     16  9927   2 91.1 267.0   12
c i   12.7   27895   166711      3432    2350     19  9930   2 95.4 273.2   13
c 
c [simplification-3] limit of 5116 conflicts hit after 5117 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 27818 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 17186 at-most-one constraints of average size 3.5
c [card-2] found 2 at-most-two constraints of average size 5.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 17188 out of 17188 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 2 xors of average arity 3.0
c [gauss-1] connected 6 occurrences of 3 variables (average 2.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 27818 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 11102 probes 40%
c [lift-1] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-1] 27723 variables remain 100% (95 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 78, lifted 103
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 0 failed, 2922 tauts, 0 hbrs, 24135 literals
c [transred-1] limit 338198 with penalty 0 = 0 + 0
c [transred-1] removed 8 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 5 clauses out of 6 (83%) of length 50
c [cce-2-1] eliminated 11 clauses out of 22 (50%) of length 48
c [cce-2-1] eliminated 12 clauses out of 22 (55%) of length 46
c [cce-2-1] eliminated 5 clauses out of 13 (38%) of length 44
c [cce-2-1] eliminated 1 clauses out of 12 (8%) of length 40
c [cce-2-1] eliminated 2 clauses out of 54 (4%) of length 34
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 36 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 156307 clauses = 155903 binary + 404 ternary
c [cce-2] tried to eliminate 375 small clauses 0%
c [cce-2] eliminated 124 small clauses 0%
c [cce-2] eliminated 124 binary clauses 0%
c [cce-2-1] eliminated 132 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 168 covered clauses in round 1
c [cce-2] eliminated 168 covered clauses in TOTAL during 1 rounds
c [elim-3] 7503 variables 27% will be scheduled this time
c [elim-3] scheduled 7503 variables 27%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 283 not tried 1% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 181 = 1% variables out of 27585
c [bca-2] limit of 10000000 steps
c [bca-2] 39314 out of 54810 literals actually usable 72%
c [bca-2] added 4085 blocked clauses in 107913 steps
c [phase-3] phase bias: 4 positive 33%, 8 negative 67%
c [simplification-3] removed 414 variables 1.5% (27404 remain 41%)
c [simplification-3] removed 7712 irredundant clauses 4.6% (158999 remain 58%)
c [simplification-3] maximum reduction of 5% = max (1%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] new conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] new conflict limit 7117
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   16.3   27404   158999      5336    2271     22 10900   3 139.9 289.9   12
c i   16.3   27403   158999      5381    2307     23 10900   2 139.3 287.6   12
c 
c [simplification-4] limit of 7173 conflicts hit after 7173 conflicts
c [decomp-7] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 26536 literals 48%
c [treelook-2] scheduling used 150038 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 239928 steps
c [treelook-2] 26532 literals remain 48%
c [treelook-2] 23792 variables remain to probed next time 87%
c [treelook-2] removed 2 variables, found 231 hbrs
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 77, lifted 4
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 6 units, 0 failed, 407 tauts, 0 hbrs, 23772 literals
c [transred-2] limit 469661 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 27296 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 88 blocked clauses
c [block-2] 88 < 1/1000 * 157990 = 157 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 104 clauses out of 104 (100%) of length 61
c [cce-3-1] eliminated 99 clauses out of 99 (100%) of length 60
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 52
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 50
c [cce-3-1] eliminated 14 clauses out of 20 (70%) of length 48
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 47
c [cce-3-1] eliminated 12 clauses out of 12 (100%) of length 46
c [cce-3-1] eliminated 26 clauses out of 26 (100%) of length 44
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-3-1] eliminated 16 clauses out of 407 (4%) of length 33
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 279 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 153805 clauses = 153349 binary + 456 ternary
c [cce-3] tried to eliminate 806 small clauses 1%
c [cce-3] eliminated 375 small clauses 0%
c [cce-3] eliminated 374 binary clauses 0%
c [cce-3] eliminated 1 ternary clauses 0%
c [cce-3-1] eliminated 375 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 654 covered clauses in round 1
c [cce-3] eliminated 654 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 27245 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 72 not tried 0% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 666 = 2% variables out of 27245
c [bca-3] limit of 10000000 steps
c [bca-3] 41603 out of 53160 literals actually usable 78%
c [bca-3] added 48662 blocked clauses in 213473 steps
c [phase-4] phase bias: 3 positive 100%, 0 negative 0%
c [simplification-4] removed 819 variables 3.0% (26579 remain 39%)
c [simplification-4] removed 8680 irredundant clauses 5.5% (150319 remain 54%)
c [simplification-4] maximum reduction of 5% = max (3%, 5%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] new conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] new conflict limit 9173
c 
c [simplification-5] limit of 9239 conflicts hit after 9239 conflicts
c [ternres-2] limit 2000000 with penalty 1 = 1 + 0
c [ternres-2] all 26579 free variables schedulable
c [ternres-2] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5 xors of average arity 3.0
c [gauss-2] connected 15 occurrences of 12 variables (average 1.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 15815 probes remain 60% after last round
c [basicprobe-2-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1 variables, found 208 hbrs
c [cgrclsr-2] limit 100000 penalty 1 = 1 + 0
c [cgrclsr-2] all 26578 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 250000 with penalty 1 = 1 + 0
c [lift-2] using 10638 probes 40%
c [lift-2] 0 units, 1 impls, 0 eqs in 1 rounds
c [lift-2] 26397 variables remain 99% (181 retained)
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 5
c [unhide-5] limit 117722 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 1 failed, 3296 tauts, 0 hbrs, 13866 literals
c [transred-3] limit 588614 with penalty 0 = 0 + 0
c [transred-3] removed 41 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 7 (14%) of length 48
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-4-1] eliminated 15 clauses out of 393 (4%) of length 33
c [cce-4-1] eliminated 5 clauses out of 20 (25%) of length 32
c [cce-4-1] eliminated 33 clauses out of 36 (92%) of length 31
c [cce-4-1] eliminated 43 clauses out of 50 (86%) of length 30
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 98 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 142324 clauses = 140933 binary + 1391 ternary
c [cce-4] tried to eliminate 492 small clauses 0%
c [cce-4] eliminated 255 small clauses 0%
c [cce-4] eliminated 255 binary clauses 0%
c [cce-4-1] eliminated 260 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 358 covered clauses in round 1
c [cce-4] eliminated 358 covered clauses in TOTAL during 1 rounds
c [elim-5] 72 variables 0% will be scheduled this time
c [elim-5] scheduled 72 variables 0%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5-1] no variable eliminated in round 1 in 3004052 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 26572
c [bca-4] limit of 10000000 steps
c [bca-4] 40137 out of 53146 literals actually usable 76%
c [bca-4] added 14429 blocked clauses in 231526 steps
c [phase-5] phase bias: 0 positive 0%, 18 negative 100%
c [simplification-5] removed 7 variables 0.0% (26572 remain 39%)
c [simplification-5] removed 3636 irredundant clauses 2.4% (146683 remain 53%)
c [simplification-5] maximum reduction of 2% = max (0%, 2%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 10666
c [simplification-5] penalized conflict interval 10666 = 1 * 10666
c [simplification-5] new conflict limit 19905
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   21.9   26572   146683     10720    2516    101 73088   4 116.7 260.7   12
c R   22.1   26572   146683     11940    2992    101 73092   3 121.9 260.5   14
c -   22.8   26572   146683     15272    3196    132 73117   4 111.0 250.2   12
c i   23.6   26571   146683     18758    5904    160 73155   1 116.7 253.0   18
c 
c [simplification-6] limit of 20065 conflicts hit after 20066 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 26525 free variables schedulable
c [ternres-3] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 13431 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 13431 out of 13431 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 47 variables
c [simpleprobe-3] all 26525 free variables schedulable
c [simpleprobe-3] limit 4658597 penalty 0 = 0 + 0
c [decomp-11] removed 13 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 13 variables, found 2832 hbrs, 6 units
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 0, lifted 9
c [unhide-6] limit 232929 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 1 failed, 2020 tauts, 0 hbrs, 29755 literals
c [transred-4] limit 1164649 with penalty 0 = 0 + 0
c [transred-4] removed 92 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 378 (0%) of length 33
c [cce-5-1] eliminated 1 clauses out of 15 (7%) of length 32
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-5-1] eliminated 1 clauses out of 7 (14%) of length 30
c [cce-5-1] eliminated 8 clauses out of 8 (100%) of length 29
c [cce-5-1] eliminated 8 clauses out of 15 (53%) of length 28
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 26
c [cce-5-1] eliminated 76 clauses out of 278 (27%) of length 25
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 100 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 141465 clauses = 140096 binary + 1369 ternary
c [cce-5] tried to eliminate 496 small clauses 0%
c [cce-5] eliminated 210 small clauses 0%
c [cce-5] eliminated 210 binary clauses 0%
c [cce-5-1] eliminated 226 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 326 covered clauses in round 1
c [cce-5] eliminated 326 covered clauses in TOTAL during 1 rounds
c [bca-5] limit of 10000000 steps
c [bca-5] 38896 out of 53000 literals actually usable 73%
c [bca-5] added 5581 blocked clauses in 218107 steps
c [rephase-1] after 20066 conflicts (new increment 20000, next 40066)
c [flushphases] 995 phases reset
c [phase-6] phase bias: 5 positive 83%, 1 negative 17%
c [simplification-6] removed 26 variables 0.1% (26499 remain 39%)
c [simplification-6] removed 978 irredundant clauses 0.7% (145705 remain 53%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 20666
c [simplification-6] penalized conflict interval 20666 = 1 * 20666
c [simplification-6] new conflict limit 40732
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   26.3   26499   145705     20278    3912    170 79725   2 117.1 251.7   12
c R   27.1   26499   145705     26395    7210    183 79747   6 113.5 246.9   19
c -   27.5   26499   145705     27512    4565    182 79750   2 113.6 247.6   13
c -   28.9   26499   145705     34037    5268    219 79819   4 113.2 247.3   13
c 
c [simplification-7] limit of 40914 conflicts hit after 40915 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 26499 free variables schedulable
c [ternres-4] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-4] fully completed ternary resolution
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 40588 literals 77%
c [treelook-3] scheduling used 300004 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 370516 steps
c [treelook-3] 40583 literals remain 77%
c [treelook-3] 22959 variables remain to probed next time 87%
c [treelook-3] removed 0 variables, found 194 hbrs
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 0, lifted 18
c [unhide-7] limit 459877 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 1736 tauts, 0 hbrs, 56851 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 128 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 26481 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 2844 blocked clauses
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-6-1] eliminated 103 clauses out of 200 (52%) of length 25
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 108 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 136659 clauses = 135295 binary + 1364 ternary
c [cce-6] tried to eliminate 328 small clauses 0%
c [cce-6] eliminated 132 small clauses 0%
c [cce-6] eliminated 132 binary clauses 0%
c [cce-6-1] eliminated 132 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 240 covered clauses in round 1
c [cce-6] eliminated 240 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 26474 variables 100%
c [elim-6] limit of 22993886 steps penalty 1 = 1 + 0
c [elim-6-1] eliminated 155 variables 1% in round 1 in 16477367 steps
c [elim-6-1] backward subsumption/strengthening limit 6516519
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 6516630 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 155 = 1% variables out of 26474
c [bca-6] limit of 10000000 steps
c [bca-6] 39802 out of 52640 literals actually usable 76%
c [bca-6] added 2973 blocked clauses in 250177 steps
c [rephase-2] after 40915 conflicts (new increment 40000, next 80915)
c [flushphases] 951 phases reset
c [phase-7] phase bias: 13 positive 93%, 1 negative 7%
c [simplification-7] removed 180 variables 0.7% (26319 remain 39%)
c [simplification-7] removed 5159 irredundant clauses 3.5% (140546 remain 51%)
c [simplification-7] maximum reduction of 4% = max (1%, 4%)
c [simplification-7] geometric conflict interval increment 4133 = 20666 / 5
c [simplification-7] new conflict interval 24799
c [simplification-7] penalized conflict interval 24799 = 1 * 24799
c [simplification-7] new conflict limit 65714
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   33.7   26318   140546     42099    7300    254 84573   2 122.3 247.4   15
c -   34.7   26285   140546     46519    6009    275 84592   2 119.5 245.2   13
c -   36.0   26285   140546     54695    6676    284 84598   8 131.6 247.1   13
c i   36.0   26284   140546     54860    6807    285 84598   8 131.9 247.3   14
c R   36.5   26276   140546     57919    8631    291 84600   2 132.7 247.6   22
c -   37.8   26276   140546     63540    7316    311 84625   3 130.3 244.0   13
c 
c [simplification-8] limit of 65908 conflicts hit after 65908 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 26276 free variables schedulable
c [ternres-5] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 3553510 penalty 0 = 0 + 0
c [basicprobe-3-0] 15512 probes remain 59% after last round
c [basicprobe-3-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1 variables, found 192 hbrs
c [cgrclsr-3] limit 88837 penalty 2 = 2 + 0
c [cgrclsr-3] all 26275 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 533026 with penalty 2 = 2 + 0
c [lift-3] using 10514 probes 40%
c [lift-3] 29 units, 2 impls, 0 eqs in 1 rounds
c [lift-3] 26010 variables remain 99% (236 retained)
c [lift-3] removed 29 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 0, lifted 16
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 130 transitive binary clauses
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 48
c [cce-7-1] eliminated 12 clauses out of 14 (86%) of length 44
c [cce-7-1] eliminated 2 clauses out of 15 (13%) of length 32
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-7-1] eliminated 7 clauses out of 244 (3%) of length 25
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 24 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 134436 clauses = 133862 binary + 574 ternary
c [cce-7] tried to eliminate 380 small clauses 0%
c [cce-7] eliminated 112 small clauses 0%
c [cce-7] eliminated 112 binary clauses 0%
c [cce-7-1] eliminated 241 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 265 covered clauses in round 1
c [cce-7] eliminated 265 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 26230 variables 100%
c [elim-7] limit of 71070214 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 93 variables 0% in round 1 in 15971659 steps
c [elim-7-1] backward subsumption/strengthening limit 31943318
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 7846318 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 93 = 0% variables out of 26230
c [bca-7] limit of 10000000 steps
c [bca-7] 38382 out of 52276 literals actually usable 73%
c [bca-7] added 628 blocked clauses in 234739 steps
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 139 variables 0.5% (26137 remain 39%)
c [simplification-8] removed 1066 irredundant clauses 0.8% (139480 remain 50%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 12399 = 24799 / 2
c [simplification-8] new conflict interval 37198
c [simplification-8] penalized conflict interval 37198 = 1 * 37198
c [simplification-8] new conflict limit 103106
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   41.5   26136   139480     70574   11505    312 84101   2 126.1 240.8   20
c i   41.6   26135   139480     70904   11703    312 84101   2 126.0 240.5   21
c -   42.4   26132   139480     73876    8092    327 84105   2 125.3 241.0   13
c -   44.4   26132   139480     84342    8774    356 84127   1 131.7 242.5   13
c -   46.8   26132   139480     94149    9571    389 84148   5 128.5 239.6   13
c 
c [simplification-9] limit of 103290 conflicts hit after 103291 conflicts
c [ternres-6] limit 5656260 with penalty 0 = 0 + 0
c [ternres-6] all 26132 free variables schedulable
c [ternres-6] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-15] removed 5 variables
c [simpleprobe-4] all 26132 free variables schedulable
c [simpleprobe-4] limit 22625041 penalty 0 = 0 + 0
c [decomp-16] removed 51 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 51 variables, found 734 hbrs, 28 units
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 0, lifted 0
c [unhide-8] limit 565626 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 0 failed, 3206 tauts, 0 hbrs, 57959 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 130 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 26081 variables 100%
c [block-4] limit of 28281301 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16 blocked clauses
c [block-4] 16 < 1/1000 * 138956 = 138 considered unsuccessful
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 16 clauses out of 18 (89%) of length 42
c [cce-8-1] eliminated 1 clauses out of 246 (0%) of length 25
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 17 large clauses in 30000001 steps
c [cce-8-1] allowing another 15000000 steps for small clauses
c [cce-8] scheduling 133603 clauses = 133008 binary + 595 ternary
c [cce-8] tried to eliminate 434 small clauses 0%
c [cce-8] eliminated 193 small clauses 0%
c [cce-8] eliminated 193 binary clauses 0%
c [cce-8-1] eliminated 193 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 210 covered clauses in round 1
c [cce-8] eliminated 210 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 26079 variables 100%
c [elim-8] limit of 113125205 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 50 variables 0% in round 1 in 15388232 steps
c [elim-8-1] backward subsumption/strengthening limit 30776464
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 7760456 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 50 = 0% variables out of 26079
c [bca-8] limit of 10000000 steps
c [bca-8] 35721 out of 52060 literals actually usable 69%
c [bca-8] added 1943 blocked clauses in 211378 steps
c [rephase-3] after 103291 conflicts (new increment 80000, next 183291)
c [flushphases] 921 phases reset
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 103 variables 0.4% (26029 remain 39%)
c [simplification-9] removed 914 irredundant clauses 0.7% (138566 remain 50%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 18599 = 37198 / 2
c [simplification-9] new conflict interval 55797
c [simplification-9] penalized conflict interval 55797 = 1 * 55797
c [simplification-9] new conflict limit 159088
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   52.8   26029   138566    106781   10189    432 83580   8 128.2 239.4   14
c -   54.9   26029   138566    119628   10770    449 83588   3 137.4 242.0   14
c R   56.0   26029   138566    125983   15450    452 83589   5 131.8 240.8   33
c -   57.6   26029   138566    132154   11436    472 83622   2 130.5 239.5   14
c i   60.2   26028   138566    143652   19683    499 83638   2 128.5 237.7   34
c -   60.9   26028   138566    145710   12201    501 83650   2 129.0 237.9   14
c 
c [simplification-10] limit of 159274 conflicts hit after 159277 conflicts
c [ternres-7] limit 8530263 with penalty 0 = 0 + 0
c [ternres-7] all 26028 free variables schedulable
c [ternres-7] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 533141 penalty 3 = 3 + 0
c [card-4] found 14757 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 533141 for elimination
c [card-4] 14757 out of 14757 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-17] removed 4 variables
c [lift-4] limit 2559078 with penalty 1 = 1 + 0
c [lift-4] using 10400 probes 40%
c [lift-4] 269 units, 14 impls, 0 eqs in 1 rounds
c [lift-4] 25236 variables remain 98% (515 retained)
c [lift-4] removed 274 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 137 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] allowing another 15000000 steps for small clauses
c [cce-9] scheduling 131314 clauses = 130715 binary + 599 ternary
c [cce-9] tried to eliminate 437 small clauses 0%
c [cce-9] eliminated 107 small clauses 0%
c [cce-9] eliminated 106 binary clauses 0%
c [cce-9] eliminated 1 ternary clauses 0%
c [cce-9-1] eliminated 107 small clauses in 30000001 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 107 covered clauses in round 1
c [cce-9] eliminated 107 covered clauses in TOTAL during 1 rounds
c [cce-9] 107 < 1/1000 * 136440 = 136 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 25751 variables 100%
c [elim-9] limit of 170605261 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 131 variables 1% in round 1 in 15140280 steps
c [elim-9-1] backward subsumption/strengthening limit 30280560
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 7609512 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 131 = 1% variables out of 25751
c [bca-9] limit of 10000000 steps
c [bca-9] 34300 out of 51242 literals actually usable 67%
c [bca-9] added 484 blocked clauses in 205103 steps
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 408 variables 1.6% (25620 remain 38%)
c [simplification-10] removed 2371 irredundant clauses 1.7% (136195 remain 49%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 18599 = 55797 / 3
c [simplification-10] new conflict interval 74396
c [simplification-10] penalized conflict interval 74396 = 1 * 74396
c [simplification-10] new conflict limit 233673
c [tabula-rasa-1] number clauses 136195 drops below limit 138203
c [flush-cache] 0 binary, 0 ternary, 20774 large
c [flushphases] 25620 phases reset fully
c [phase-11] phase bias: 321 positive 36%, 565 negative 64%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] new conflict limit 179277
c [tabula-rasa-1] new variable limit 6405 and clause limit 68097
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   67.1   25620   136195    164999    2329    554 81055   2 129.8 237.2   13
c -   68.0   25620   136195    169238    3054    565 81067   2 128.9 236.6   13
c -   69.1   25620   136195    173872    3733    582 81089   3 128.3 236.6   13
c 
c [simplification-11] limit of 179341 conflicts hit after 179344 conflicts
c [ternres-8] limit 9517010 with penalty 0 = 0 + 0
c [ternres-8] all 25620 free variables schedulable
c [ternres-8] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-8] fully completed ternary resolution
c [treelook-4] limit 237925 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 36040 literals 70%
c [treelook-4] scheduling used 237955 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 237925 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 280114 steps
c [treelook-4] 36033 literals remain 70%
c [treelook-4] 22073 variables remain to probed next time 86%
c [treelook-4] removed 0 variables, found 452 hbrs
c [lift-5] limit 5710206 with penalty 0 = 0 + 0
c [lift-5] using 9994 probes 39%
c [lift-5] 201 units, 8 impls, 0 eqs in 1 rounds
c [lift-5] 24178 variables remain 95% (1241 retained)
c [lift-5] removed 201 variables
c [cliff-8] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-8] failed 0, lifted 0
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 143 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 25419 variables 100%
c [elim-10] limit of 190340216 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 95 variables 0% in round 1 in 14931074 steps
c [elim-10-1] backward subsumption/strengthening limit 29862148
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 7508470 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 95 = 0% variables out of 25419
c [bca-10] limit of 10000000 steps
c [bca-10] 38080 out of 50650 literals actually usable 75%
c [bca-10] added 1221 blocked clauses in 216573 steps
c [rephase-4] after 179344 conflicts (new increment 20000, next 199344)
c [flushphases] 2896 phases reset
c [phase-12] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-11] removed 296 variables 1.2% (25324 remain 38%)
c [simplification-11] removed 1719 irredundant clauses 1.3% (134476 remain 49%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-11] new conflict interval 30000
c [simplification-11] penalized conflict interval 30000 = 1 * 30000
c [simplification-11] new conflict limit 209344
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   71.3   25324   134476    182022    4324    549 80735   2 130.3 237.0   13
c -   72.6   25324   134476    188921    5066    572 80755   3 128.0 235.9   13
c -   74.1   25324   134476    196161    5680    581 80767   2 129.4 236.4   13
c -   76.0   25324   134476    203961    6492    599 80781   3 129.0 237.7   14
c 
c [simplification-12] limit of 209420 conflicts hit after 209421 conflicts
c [ternres-9] limit 11108995 with penalty 0 = 0 + 0
c [ternres-9] all 25324 free variables schedulable
c [ternres-9] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 277724 penalty 3 = 3 + 0
c [gauss-4] extracted 1 xors of average arity 3.0
c [gauss-4] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-4] limit 277724 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-4] limit 11108995 penalty 0 = 0 + 0
c [basicprobe-4-0] 14544 probes remain 57% after last round
c [basicprobe-4-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 2 variables, found 203 hbrs
c [cgrclsr-4] limit 138862 penalty 3 = 3 + 0
c [cgrclsr-4] all 25322 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-6] limit 6665397 with penalty 0 = 0 + 0
c [lift-6] using 9165 probes 36%
c [lift-6] 198 units, 12 impls, 1 eqs in 1 rounds
c [lift-6] 23144 variables remain 92% (1962 retained)
c [lift-6] removed 216 variables
c [unhide-9] limit 555449 with penalty 2 = 2 + 0
c [unhide-9-9] 0 units, 1 failed, 786 tauts, 0 hbrs, 19683 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 141 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 25105 variables 100%
c [block-5] limit of 27772488 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 125 blocked clauses
c [block-5] 125 < 1/1000 * 132067 = 132 considered unsuccessful
c [cce-10] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 5 clauses out of 7 (71%) of length 38
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 5 large clauses in 15000001 steps
c [cce-10-1] allowing another 7500000 steps for small clauses
c [cce-10] scheduling 126885 clauses = 126285 binary + 600 ternary
c [cce-10] tried to eliminate 132 small clauses 0%
c [cce-10] eliminated 56 small clauses 0%
c [cce-10] eliminated 55 binary clauses 0%
c [cce-10] eliminated 1 ternary clauses 0%
c [cce-10-1] eliminated 56 small clauses in 15000001 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 61 covered clauses in round 1
c [cce-10] eliminated 61 covered clauses in TOTAL during 1 rounds
c [cce-10] 61 < 1/1000 * 131934 = 131 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 25020 variables 100%
c [elim-11] limit of 222179904 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 22 variables 0% in round 1 in 14415603 steps
c [elim-11-1] backward subsumption/strengthening limit 28831206
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 7313331 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 22 = 0% variables out of 25020
c [elim-11] 22 < 1/1000 * 25020 = 25 considered unsuccessful
c [bca-11] limit of 10000000 steps
c [bca-11] 36447 out of 49998 literals actually usable 73%
c [bca-11] added 369 blocked clauses in 207464 steps
c [rephase-5] after 209421 conflicts (new increment 40000, next 249421)
c [flushphases] 2331 phases reset
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-12] removed 326 variables 1.3% (24998 remain 37%)
c [simplification-12] removed 2613 irredundant clauses 1.9% (131863 remain 48%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 10000 = 30000 / 3
c [simplification-12] new conflict interval 40000
c [simplification-12] penalized conflict interval 40000 = 1 * 40000
c [simplification-12] new conflict limit 249421
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   79.5   24997   131863    210629   10304    550 77605   2 128.8 237.6   22
c -   80.3   24997   131863    213696    7138    563 77609   3 128.5 237.4   14
c i   82.1   24996   131863    222589   13511    585 77617   2 129.9 238.9   32
c -   82.3   24976   131863    223015    7833    587 77618   2 129.8 238.9   14
c -   84.6   24976   131863    233332    8677    605 77637   4 130.0 239.3   14
c 
c [simplification-13] limit of 249523 conflicts hit after 249523 conflicts
c [ternres-10] limit 12981442 with penalty 0 = 0 + 0
c [ternres-10] all 24976 free variables schedulable
c [ternres-10] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-21] removed 23 variables
c [simpleprobe-5] all 24975 free variables schedulable
c [simpleprobe-5] limit 51925770 penalty 0 = 0 + 0
c [decomp-22] removed 8 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 8 variables, found 661 hbrs, 7 units
c [lift-7] limit 7788865 with penalty 0 = 0 + 0
c [lift-7] using 8336 probes 33%
c [lift-7] 12 units, 16 impls, 1 eqs in 1 rounds
c [lift-7] 22085 variables remain 89% (2863 retained)
c [lift-7] removed 19 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 139 transitive binary clauses
c [bca-12] limit of 10000000 steps
c [bca-12] 35975 out of 49898 literals actually usable 72%
c [bca-12] added 111 blocked clauses in 210923 steps
c [rephase-6] after 249523 conflicts (new increment 80000, next 329523)
c [flushphases] 2122 phases reset
c [phase-14] phase bias: 2 positive 100%, 0 negative 0%
c [simplification-13] removed 28 variables 0.1% (24948 remain 37%)
c [simplification-13] removed 432 irredundant clauses 0.3% (131431 remain 48%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 40000
c [simplification-13] new conflict interval 80000
c [simplification-13] penalized conflict interval 80000 = 1 * 80000
c [simplification-13] new conflict limit 329523
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   88.5   24948   131431    249963    9171    586 78288   3 152.1 243.8   16
c -   91.8   24948   131431    268732    9927    590 78289   3 147.0 242.5   16
c -   95.2   24948   131431    288175   10452    604 78293   2 141.5 241.6   17
c -   98.4   24948   131431    309251   11158    613 78311   5 149.0 243.2   21
c 
c [simplification-14] limit of 329561 conflicts hit after 329564 conflicts
c [ternres-11] limit 16353187 with penalty 0 = 0 + 0
c [ternres-11] all 24948 free variables schedulable
c [ternres-11] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-11] fully completed ternary resolution
c [lift-8] limit 9811912 with penalty 0 = 0 + 0
c [lift-8] using 7403 probes 30%
c [lift-8] 79 units, 21 impls, 0 eqs in 1 rounds
c [lift-8] 20937 variables remain 84% (3920 retained)
c [lift-8] removed 91 variables
c [cliff-9] limit of 3270637 steps penalty 2 = 2 + 0
c [cliff-9] failed 0, lifted 0
c [unhide-10] limit 1635318 with penalty 1 = 1 + 0
c [unhide-10-11] 0 units, 0 failed, 3227 tauts, 0 hbrs, 102844 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 114 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 24857 variables 100%
c [elim-12] limit of 163531879 steps penalty 1 = 1 + 0
c [elim-12-1] eliminated 73 variables 0% in round 1 in 14001506 steps
c [elim-12-1] backward subsumption/strengthening limit 28003012
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 7135214 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 73 = 0% variables out of 24857
c [bca-13] limit of 10000000 steps
c [bca-13] 36211 out of 49570 literals actually usable 73%
c [bca-13] added 1290 blocked clauses in 214596 steps
c [rephase-7] after 329564 conflicts (new increment 160000, next 489564)
c [flushphases] 1982 phases reset
c [phase-15] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-14] removed 164 variables 0.7% (24784 remain 37%)
c [simplification-14] removed 1754 irredundant clauses 1.3% (129677 remain 47%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 40000 = 80000 / 2
c [simplification-14] new conflict interval 120000
c [simplification-14] penalized conflict interval 120000 = 1 * 120000
c [simplification-14] new conflict limit 449564
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  106.3   24784   129677    349589   11542    612 75798   5 168.7 245.8   21
c -  111.8   24784   129677    388705   12003    614 75799   6 182.4 247.7   26
c -  114.9   24784   129677    410561   12817    618 75799   6 191.0 251.5   26
c -  118.9   24784   129677    442772   13434    619 75801   4 202.5 254.3   26
c 
c [simplification-15] limit of 449574 conflicts hit after 449574 conflicts
c [ternres-12] limit 20584336 with penalty 0 = 0 + 0
c [ternres-12] all 24784 free variables schedulable
c [ternres-12] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 643260 penalty 4 = 4 + 0
c [card-5] found 14648 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 643260 for elimination
c [card-5] 14648 out of 14648 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [lift-9] limit 12350601 with penalty 0 = 0 + 0
c [lift-9] using 6289 probes 25%
c [lift-9] 0 units, 26 impls, 0 eqs in 1 rounds
c [lift-9] 19338 variables remain 78% (5446 retained)
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 140 transitive binary clauses
c [cce-11] limit of 10292168 steps penalty 2 = 2 + 0
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] allowing another 5146084 steps for small clauses
c [cce-11] scheduling 125388 clauses = 124119 binary + 1269 ternary
c [cce-11] tried to eliminate 207 small clauses 0%
c [cce-11] eliminated 80 small clauses 0%
c [cce-11] eliminated 80 binary clauses 0%
c [cce-11-1] eliminated 80 small clauses in 10292169 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 80 covered clauses in round 1
c [cce-11] eliminated 80 covered clauses in TOTAL during 1 rounds
c [cce-11] 80 < 1/1000 * 129668 = 129 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 24784 variables 100%
c [elim-13] limit of 411686725 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 1 variables 0% in round 1 in 13939073 steps
c [elim-13-1] backward subsumption/strengthening limit 27878146
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 7130856 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 1 = 0% variables out of 24784
c [elim-13] 1 < 1/1000 * 24784 = 24 considered unsuccessful
c [bca-14] limit of 10000000 steps
c [bca-14] 36046 out of 49568 literals actually usable 73%
c [bca-14] added 92 blocked clauses in 217388 steps
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-15] removed 1 variables 0.0% (24783 remain 37%)
c [simplification-15] removed 91 irredundant clauses 0.1% (129586 remain 47%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 120000
c [simplification-15] new conflict interval 240000
c [simplification-15] penalized conflict interval 240000 = 1 * 240000
c [simplification-15] new conflict limit 689574
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  121.4   24782   129586    449773   16835    602 76052   2 204.0 255.0   29
c -  125.1   24782   129586    474137   14021    605 76052   2 208.2 256.2   22
c -  131.3   24782   129586    517650   14553    605 76052   2 216.1 258.0   21
c i  134.1   24781   129586    538635   21988    605 76052   4 218.4 258.8   53
c -  135.3   24781   129586    546216   15092    607 76053   6 215.8 258.3   22
c -  138.1   24781   129586    564031   15745    611 76055   5 209.8 256.9   26
c -  141.3   24781   129586    582798   16341    614 76055   5 203.8 255.5   26
c -  145.5   24781   129586    608613   16884    616 76056   4 196.7 253.8   26
c -  149.2   24781   129586    628821   17427    617 76056   4 191.2 252.4   23
c -  153.7   24781   129586    660211   18144    618 76056   8 184.5 250.3   23
c 
c [simplification-16] limit of 689622 conflicts hit after 689625 conflicts
c [ternres-13] limit 31008246 with penalty 0 = 0 + 0
c [ternres-13] all 24781 free variables schedulable
c [ternres-13] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-25] removed 2 variables
c [treelook-5] limit 387603 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 42303 literals 85%
c [treelook-5] scheduling used 387607 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 387603 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 394266 steps
c [treelook-5] 42267 literals remain 85%
c [treelook-5] 21325 variables remain to probed next time 86%
c [treelook-5] removed 0 variables, found 302 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 136 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 24781 variables 100%
c [block-6] limit of 38760308 steps penalty 3 = 3 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [bca-15] limit of 10000000 steps
c [bca-15] 35966 out of 49564 literals actually usable 73%
c [bca-15] added 94 blocked clauses in 227196 steps
c [rephase-8] after 689625 conflicts (new increment 320000, next 1009625)
c [flushphases] 1943 phases reset
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-16] removed 0 variables 0.0% (24781 remain 37%)
c [simplification-16] removed 26 irredundant clauses 0.0% (129560 remain 47%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 240000
c [simplification-16] new conflict interval 480000
c [simplification-16] penalized conflict interval 480000 = 1 * 480000
c [simplification-16] new conflict limit 1169625
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  159.1   24781   129560    693017   18719    625 76327   5 178.3 248.4   19
c -  162.7   24781   129560    718704   19457    631 76328   5 175.6 248.1   19
c -  167.2   24781   129560    756002   20151    642 76329   6 173.8 247.7   19
c -  172.7   24781   129560    799351   20848    650 76331   1 173.7 247.6   19
c -  180.9   24781   129560    860723   21423    654 76334   5 176.1 247.8   25
c -  190.7   24781   129560    929638   21987    658 76336   3 179.1 248.1   25
c -  200.2   24781   129560    998486   22718    659 76338   5 182.8 249.0   25
c -  208.3   24781   129560   1060226   23282    661 76338   5 184.3 249.3   25
c -  216.0   24781   129560   1117635   23804    665 76340   4 184.0 249.1   25
c 
c [simplification-17] limit of 1169663 conflicts hit after 1169664 conflicts
c [ternres-14] limit 51265331 with penalty 0 = 0 + 0
c [ternres-14] all 24781 free variables schedulable
c [ternres-14] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 640816 penalty 4 = 4 + 0
c [gauss-5] extracted 3 xors of average arity 3.0
c [gauss-5] connected 9 occurrences of 9 variables (average 1.0)
c [gauss-5] limit 640816 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-5] limit 51265331 penalty 0 = 0 + 0
c [basicprobe-5-0] 12541 probes remain 51% after last round
c [basicprobe-5-0] 17 units = 17 failed (100%) + 0 lifted (0%)
c [basicprobe-5-0] removed 17 variables, found 461 hbrs
c [cgrclsr-5] limit 320408 penalty 4 = 4 + 0
c [cgrclsr-5] all 24764 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-10] limit 10000000 with penalty 1 = 1 + 0
c [lift-10] using 4753 probes 19%
c [lift-10] 4 units, 23 impls, 1 eqs in 1 rounds
c [lift-10] 18140 variables remain 73% (6619 retained)
c [lift-10] removed 5 variables
c [unhide-11] limit 2563266 with penalty 2 = 2 + 0
c [unhide-11-14] 0 units, 0 failed, 3354 tauts, 0 hbrs, 432302 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 145 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 24759 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14-1] eliminated 19 variables 0% in round 1 in 13477432 steps
c [elim-14-1] backward subsumption/strengthening limit 26954864
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 6968002 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 19 = 0% variables out of 24759
c [elim-14] 19 < 1/1000 * 24759 = 24 considered unsuccessful
c [bca-16] limit of 10000000 steps
c [bca-16] 36237 out of 49482 literals actually usable 73%
c [bca-16] added 1425 blocked clauses in 245510 steps
c [rephase-9] after 1169664 conflicts (new increment 640000, next 1809664)
c [flushphases] 1928 phases reset
c [phase-18] phase bias: 3 positive 100%, 0 negative 0%
c [simplification-17] removed 41 variables 0.2% (24740 remain 37%)
c [simplification-17] removed 1584 irredundant clauses 1.2% (127976 remain 46%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 240000 = 480000 / 2
c [simplification-17] new conflict interval 720000
c [simplification-17] penalized conflict interval 720000 = 1 * 720000
c [simplification-17] new conflict limit 1889664
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  231.1   24740   127976   1174537   24547    648 76170   6 188.6 251.6   20
c -  244.4   24740   127976   1272816   25082    657 76172   2 193.0 252.4   32
c -  258.6   24740   127976   1354960   25599    657 76176   1 195.1 253.1   32
c -  269.8   24740   127976   1433241   26187    662 76180   1 196.4 253.3   32
c -  280.1   24740   127976   1500960   26753    663 76181   2 199.5 255.8   32
c -  292.4   24740   127976   1567041   27254    664 76181   3 207.2 260.8   44
c -  305.6   24740   127976   1634247   27821    665 76181   1 213.3 266.5   44
c -  317.8   24740   127976   1714872   28437    669 76184   3 214.4 267.8   44
c -  331.0   24740   127976   1794867   28944    673 76185   4 217.7 270.8   45
c -  344.6   24740   127976   1874798   29441    674 76186   1 221.1 274.1   45
c 
c [simplification-18] limit of 1889692 conflicts hit after 1889693 conflicts
c [ternres-15] limit 87330504 with penalty 0 = 0 + 0
c [ternres-15] all 24740 free variables schedulable
c [ternres-15] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-15] fully completed ternary resolution
c [simpleprobe-6] all 24740 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-29] removed 2 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 2 variables, found 1105 hbrs, 0 units
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 3585 probes 14%
c [lift-11] 11 units, 36 impls, 1 eqs in 1 rounds
c [lift-11] 16006 variables remain 65% (8720 retained)
c [lift-11] removed 12 variables
c [cliff-10] limit of 8733050 steps penalty 3 = 3 + 0
c [cliff-10] failed 0, lifted 0
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 141 transitive binary clauses
c [bca-17] limit of 10000000 steps
c [bca-17] 36335 out of 49454 literals actually usable 73%
c [bca-17] added 159 blocked clauses in 240949 steps
c [rephase-10] after 1889693 conflicts (new increment 1280000, next 3169693)
c [flushphases] 1874 phases reset
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-18] removed 14 variables 0.1% (24726 remain 37%)
c [simplification-18] removed 109 irredundant clauses 0.1% (127867 remain 46%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 720000
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] new conflict limit 2889693
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  357.8   24726   127867   1958850   29929    644 77759   5 223.9 275.7   33
c -  371.8   24726   127867   2053943   30492    644 77759  10 227.6 277.6   33
c -  386.9   24726   127867   2155403   31964    645 77760   9 232.6 280.1   33
c -  402.9   24726   127867   2261714   32806    646 77761   6 235.8 281.8   33
c -  418.0   24726   127867   2365103   33426    647 77761   5 239.4 283.8   44
c -  432.6   24726   127867   2466622   34287    647 77761   8 241.6 285.4   44
c -  448.4   24726   127867   2577707   34913    647 77762   8 243.7 286.6   44
c -  462.5   24726   127867   2678065   35528    648 77762   6 245.9 288.3   44
c -  478.3   24726   127867   2788975   36756    648 77762   5 247.9 289.7   46
c -  490.9   24726   127867   2878843   37923    649 77763   6 248.2 290.5   46
c 
c [simplification-19] limit of 2889701 conflicts hit after 2889703 conflicts
c [ternres-16] limit 132737118 with penalty 0 = 0 + 0
c [ternres-16] all 24726 free variables schedulable
c [ternres-16] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-16] fully completed ternary resolution
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 1469 probes 6%
c [lift-12-1] found 0 units 25 impls in round 1
c [lift-12] 0 units, 35 impls, 2 eqs in 2 rounds
c [lift-12] 14537 variables remain 59% (10187 retained)
c [lift-12] removed 2 variables
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 131 transitive binary clauses
c [cce-12] limit of 33184279 steps penalty 3 = 3 + 0
c [cce-12-1] eliminated 1 clauses out of 15 (7%) of length 32
c [cce-12-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-12-1] eliminated 5 clauses out of 258 (2%) of length 24
c [cce-12-1] eliminated 1 clauses out of 130 (1%) of length 23
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 9 large clauses in 33184280 steps
c [cce-12-1] allowing another 16592140 steps for small clauses
c [cce-12] scheduling 123594 clauses = 122343 binary + 1251 ternary
c [cce-12] tried to eliminate 529 small clauses 0%
c [cce-12] eliminated 150 small clauses 0%
c [cce-12] eliminated 149 binary clauses 0%
c [cce-12] eliminated 1 ternary clauses 0%
c [cce-12-1] eliminated 150 small clauses in 33184280 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 159 covered clauses in round 1
c [cce-12] eliminated 159 covered clauses in TOTAL during 1 rounds
c [bca-18] limit of 10000000 steps
c [bca-18] 36149 out of 49450 literals actually usable 73%
c [bca-18] added 92 blocked clauses in 244931 steps
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-19] removed 2 variables 0.0% (24724 remain 37%)
c [simplification-19] removed 164 irredundant clauses 0.1% (127703 remain 46%)
c [simplification-19] maximum reduction of 0% = max (0%, 0%)
c [simplification-19] full geometric conflict interval increment 1000000
c [simplification-19] conflict interval soft limit 1000000 reached
c [simplification-19] new conflict interval 1000000
c [simplification-19] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-19] new conflict limit 3889703
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  515.0   24724   127703   3009826   38923    645 78027   5 249.2 291.0   40
c -  539.9   24724   127703   3169009   40975    646 78027   5 250.1 291.2   40
c -  564.8   24724   127703   3321743   43333    646 78028   5 250.9 291.5   52
c -  588.7   24724   127703   3463942   45508    646 78028   4 252.4 292.5   53
c -  617.5   24724   127703   3633420   47346    646 78028   4 253.9 293.2   57
c -  650.9   24724   127703   3799589   49469    647 78028   5 255.2 293.8   57
c 
c [simplification-20] limit of 3889719 conflicts hit after 3889720 conflicts
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 1 probes 0%
c [lift-13-1] found 0 units 0 impls in round 1
c [lift-13-2] found 0 units 0 impls in round 2
c [lift-13-3] found 0 units 0 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, 0 impls, 0 eqs in 6 rounds
c [lift-13] 14536 variables remain 59% (10188 retained)
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 149 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 24724 variables 100%
c [elim-15] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-15-1] eliminated 7 variables 0% in round 1 in 13433988 steps
c [elim-15-1] backward subsumption/strengthening limit 26867976
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 6947914 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 7 = 0% variables out of 24724
c [elim-15] 7 < 1/1000 * 24724 = 24 considered unsuccessful
c [bca-19] limit of 10000000 steps
c [bca-19] 35888 out of 49436 literals actually usable 73%
c [bca-19] added 86 blocked clauses in 268392 steps
c [rephase-11] after 3889720 conflicts (new increment 2560000, next 6449720)
c [flushphases] 1872 phases reset
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-20] removed 7 variables 0.0% (24717 remain 37%)
c [simplification-20] removed 21 irredundant clauses 0.0% (127682 remain 46%)
c [simplification-20] maximum reduction of 0% = max (0%, 0%)
c [simplification-20] full geometric conflict interval increment 1000000
c [simplification-20] conflict interval soft limit 1000000 reached
c [simplification-20] new conflict interval 1000000
c [simplification-20] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-20] new conflict limit 4889720
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  671.5   24717   127682   3928570   51245    661 77977   7 254.8 293.8   50
c -  684.2   24717   127682   4020463   52045    693 77993   3 254.8 294.4   49
c -  700.5   24717   127682   4127056   52859    724 78020   4 255.2 295.1   63
c -  717.7   24717   127682   4241597   53544    748 78033   4 255.9 295.9   56
c -  733.3   24717   127682   4341750   54412    766 78044   3 256.2 296.6   56
c -  750.2   24717   127682   4448130   55004    775 78052   4 256.4 297.2   56
c -  768.3   24717   127682   4559106   55938    781 78062   5 257.5 298.5   56
c -  786.7   24717   127682   4675872   56465    791 78063   4 258.6 299.7   56
c -  804.5   24717   127682   4794315   57306    798 78065   6 259.5 300.9   55
c 
c [simplification-21] limit of 4889898 conflicts hit after 4889899 conflicts
c [ternres-17] limit 100000000 with penalty 1 = 1 + 0
c [ternres-17] all 24717 free variables schedulable
c [ternres-17] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 7582959 penalty 4 = 4 + 0
c [card-6] found 14799 at-most-one constraints of average size 4.0
c [card-6] found 12 at-most-two constraints of average size 7.2
c [card-6] using previous limit 7582959 for elimination
c [card-6] 14811 out of 14811 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 397 at-most-one constraints, 397 used 100%
c [card-6] exported 12232 binary clauses, 30.8 per/constraint
c [unhide-12] limit 2500000 with penalty 3 = 3 + 0
c [unhide-12-16] 0 units, 0 failed, 7769 tauts, 0 hbrs, 539760 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 149 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 24717 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 0 blocked clauses
c [cce-13] limit of 121327352 steps penalty 2 = 2 + 0
c [cce-13-1] eliminated 1 clauses out of 378 (0%) of length 33
c [cce-13-1] eliminated 1 clauses out of 15 (7%) of length 32
c [cce-13-1] eliminated 1 clauses out of 129 (1%) of length 23
c [cce-13-1] eliminated 10 clauses out of 192 (5%) of length 22
c [cce-13-1] eliminated 12 clauses out of 210 (6%) of length 21
c [cce-13-1] eliminated 38 clauses out of 206 (18%) of length 20
c [cce-13-1] eliminated 12 clauses out of 119 (10%) of length 19
c [cce-13-1] eliminated 24 clauses out of 172 (14%) of length 18
c [cce-13-1] eliminated 16 clauses out of 164 (10%) of length 17
c [cce-13-1] eliminated 9 clauses out of 169 (5%) of length 16
c [cce-13-1] eliminated 11 clauses out of 166 (7%) of length 15
c [cce-13-1] eliminated 17 clauses out of 175 (10%) of length 14
c [cce-13-1] eliminated 2 clauses out of 163 (1%) of length 13
c [cce-13-1] eliminated 13 clauses out of 171 (8%) of length 12
c [cce-13-1] eliminated 52 clauses out of 211 (25%) of length 11
c [cce-13-1] eliminated 9 clauses out of 90 (10%) of length 10
c [cce-13-1] eliminated 12 clauses out of 109 (11%) of length 9
c [cce-13-1] eliminated 18 clauses out of 105 (17%) of length 8
c [cce-13-1] eliminated 13 clauses out of 87 (15%) of length 7
c [cce-13-1] eliminated 8 clauses out of 92 (9%) of length 6
c [cce-13-1] eliminated 6 clauses out of 77 (8%) of length 5
c [cce-13-1] eliminated 58 clauses out of 190 (31%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 343 large clauses in 96499530 steps
c [cce-13-1] allowing another 48249765 steps for small clauses
c [cce-13] scheduling 122261 clauses = 121666 binary + 595 ternary
c [cce-13] tried to eliminate 2482 small clauses 2%
c [cce-13] eliminated 617 small clauses 1%
c [cce-13] eliminated 616 binary clauses 1%
c [cce-13] eliminated 1 ternary clauses 0%
c [cce-13-1] eliminated 617 small clauses in 121327353 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 960 covered clauses in round 1
c [cce-13] eliminated 960 covered clauses in TOTAL during 1 rounds
c [bca-20] limit of 10000000 steps
c [bca-20] 35806 out of 49436 literals actually usable 72%
c [bca-20] added 1259 blocked clauses in 277838 steps
c [phase-22] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-21] removed 0 variables 0.0% (24717 remain 37%)
c [simplification-21] removed 1469 irredundant clauses 1.2% (126213 remain 46%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-21] conflict interval soft limit 1000000 reached
c [simplification-21] new conflict interval 1000000
c [simplification-21] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-21] new conflict limit 5889899
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  832.3   24717   126213   4910896   57969    943 84964   1 260.3 301.9   43
c -  859.7   24717   126213   5055666   58508    948 84970   4 261.0 302.8   60
c -  888.5   24717   126213   5185127   59005    954 84977   2 263.0 305.2   60
c -  913.4   24717   126213   5299640   59550    960 84979   6 264.4 307.3   93
c -  937.4   24717   126213   5422459   60070    961 84979   4 265.9 309.5   93
c -  966.0   24717   126213   5554671   60638    962 84980   2 267.8 312.4   94
c -  992.7   24717   126213   5676077   61225    965 84981   2 269.7 315.1   94
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 20 count, 89591 added (2393 skipped), 4373315 steps
c bkwd: tried 1427108 clauses, 2854097 lits, 2.00 lits/clause
c bkwd: checked 78286477 occs, 54.86 occs/clause, 27.43 occs/lit
c bkwd: subsumed 1 binary, 2 ternary, 21 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1733 large (0% self)
c blkd: 7 bces, 3121 removed, 2901959 resolutions, 8855956 steps
c blkd: 13936 blocking literals 7%, 151 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 12232 am1, 17039473 steps
c card: 46 rescheduled, 420 eliminated, 420 resolved, 146828 subsumed
c card: 103063 at-most-one constraints found, average size 3.66
c card: 103063 at-most-one constraints used 100%, average size 3.66
c card: 14 at-most-two constraints found, average size 6.93
c card: 14 at-most-two constraints used 100%, average size 6.93
c cces: 13 cces, 8036 eliminated, 6954 ate 87%, 1082 abce 13%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 5 count, 848117 esteps, 143790 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: 296 extracted (287 ands 97%, 3 xors 1%, 6 ites 2%)
c clff: 10 cliffs, 155 lifted, 155 failed
c clff: 10120 decisions, 87723467 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1633472 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 127 gcs, 0 rescored clauses, 2974 rescored vars
c dcps: 32 decompositions, 946 equivalent 1%
c deco: 3737366 decision-only clauses 66%, 67% reduction
c decs: 12688149 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 107899 flipped 0.850% (in 680 phases)
c elms: 15 elims, 38652 eliminated 40%
c elms: 26 rounds, 1.7 rounds/bve
c elms: 8745 small 23%, 29756 large 77%
c elms: 104943 tried small, 8745 succeeded 8%, 96198 failed 92%
c elms: 1661 subsumed, 42525 strengthened, 7202 blocked
c elms: 7087059 copies, 8178634 resolutions, 1334655 ipos
c elms: 10017640 subchks, 12022051 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 11 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8844174 steps, 4422087 extr 50%, 52 elim 0%
c glue: 270.9 orig avg, 218.8 real avg, 10.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 13659 = 8318 simple + 4266 trn 61% + 1075 lrg 31%, 425 sub 8%
c hght: 317 average, 1.17 height/glue
c ints: 131709 luby (40616594 steps), 0 inout (0 steps)
c lift: 13 phases, 66114 probed (22102 level1 33%, 44012 level2 67%)
c lift: 803 units, 6 equivalences, 194 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5654953 clauses, 340.7 length
c lrnd: 1527158 uips 27%, 3817155 flips 68%
c mega: 0 count, 0 failed, 0 rounds
c mins: 1926679091 learned lits, 57% minimized
c mins: 1894325 mins 33%, 710 bin 0%, 22552 size 0%, 3737366 deco 66%
c move: moved 5654953, 8117 bin 0%, 8 trn 0%, 0 lrg 0%
c otfs: str 287856 dyn (286920 red, 936 irr) 57184 drv 20%, 230672 rst 80%
c otfs: sub 7543 dyn (7543 red, 0 irr)
c phas: 22 computed, 29343 set, 4686 pos (16%), 24657 neg (84%)
c prbs: 5 basic, 4423 probed, 22 failed, 0 lifted
c prbs: 6 simple, 400369 probed, 120 failed, 365 eqs
c prbs: 5 treelook, 56 probed, 2 failed, 0 lifted
c prps: 2401392533 props, 184 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c psns: 335311836 searches, 137685193 hits, 41% 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: 92 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 92 arith 100%, 0 double 0%
c rmbd: 4589 removed, 1257 red 27%
c rphs: 11 recomputed phases
c rsts: 8572 restarts 7%, 123137 skipped 93%
c rsts: 123007 saturating 100%, 6 agile 0%, 124 reuse 0%
c rsts: 651.5 avg interval, 651.5 scaled, 1.0 factor
c rsts: 1237 kept 14.4% average 26.7%
c simp: 21 count (21 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 5654953 count (7173741 tried 1.3), 3836646 sub out of 5653086 (67.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 1 count
c tops: 31141 fixed 33%, 15 its, 380809.20 confs/it
c trvs: 70308727110 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 30.0 search traversals per propagation, 12264.4 per conflict
c trvs: 2.3 search traversals per search visit
c trds: 19 transitive reductions, 2198 removed, 0 failed
c trds: 9450 nodes, 32450 edges, 32583911 steps
c trim: 398187315 words, 1519.0 MB
c trnr: 17 count, 0 bin, 71 trn, 12091434 steps
c unhd: 12 count, 16 rounds, 17026656 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 7 units, 7 bin, 0 trn, 0 lrg
c unhd: 11 failed, 9 stamp, 0 lits, 2 bin, 0 trn, 0 lrg
c unhd: 34691 tauts, 805 bin 2%, 58 trn 0%, 330 lrg 1%
c unhd: 34691 tauts, 33498 stamp 97%, 17740 red 51%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1312624 str, 7 bin 0%, 116 trn 0%, 1312501 lrg 100%, 1303085 red 99%
c vars: 24717 remaining 26% and 70739 removed 74% out of 95456
c vars: 31141 fixed 33%, 38652 eliminated 40%, 946 equivalent 1%
c vsts: 30432451025 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 12.9 search visits per propagation, 5283.4 per conflict
c wchs: 6642532280 pushed, 140583466 enlarged, 198 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   5653086 100   1697324 100 135331368 100  46354267 100   4025845 100
c 
c  0      25508   0         0   0  20791404  15   2225509   5    190489   5 
c  1      12516   0         0   0  18617435  14   2150698   5    122883   3 
c  2      57911   1     16748   1  31080832  23   6126385  13    358538   9 
c  3     121038   2    116116   7  10982805   8   3642707   8    254737   6 
c  4     174195   3    166939  10  10292008   8<  3893183   8    289206   7 
c  5     249115   4    240590  14   8803900   7   4098527   9    414490  10 
c  6     271348   5    162761  10   6677649   5   3453793   7<   388282  10 
c  7     265626   5    115195   7   5148508   4   2796006   6    302437   8<
c  8     246561   4     87224   5<  3848863   3   2224903   5    252142   6 
c  9     210520   4     62441   4   2740774   2   1627078   4    184366   5 
c 10     413491   7<   141642   8   6140767   5   3440378   7    342761   9 
c 11     690824  12    136067   8   4218518   3   3134250   7    304430   8 
c 12    2827540  50    434807  26   5818175   4   7311726  16    595170  15 
c 13      86893   2     16794   1    169730   0    229124   0     25914   1 
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            10.0           8.0           3.8           6.3           6.8
c std             2.9           3.3           3.5           3.9           3.7
c 
c  270.755  27% analysis
c   74.768   7% bump
c   23.413   2% cce
c   14.593   1% mincls
c   14.223   1% decide
c   10.312   1% unhide
c   10.083   1% elim
c    5.222   1% gc
c    3.985   0% lift
c    3.687   0% probe
c    3.451   0% decomp
c    2.817   0% reduce
c    2.190   0% restart
c    1.948   0% cliff
c    1.692   0% bca
c    1.556   0% backward
c    1.355   0% phase
c    1.148   0% block
c    1.003   0% transred
c    0.707   0% defrag
c    0.619   0% cgrclsr
c    0.570   0% card
c    0.375   0% gauss
c    0.091   0% ternres
c    0.019   0% tabularasa
c    0.005   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c    1.384   0% probe simple     38%
c    1.512   0% probe basic      41%
c    0.791   0% probe tree-look  21%
c ==================================
c    1.364   0% preprocessing     2%
c   62.306   6% inprocessing     98%
c ==================================
c   63.670   6% simplifying
c  936.182  94% search
c ==================================
c  999.853 100% all
c 
c 12688149 decisions, 12690.0 decisions/sec
c 5712138 conflicts, 5713.0 conflicts/sec
c 2401392533 propagations, 2.4 megaprops/sec
c 999.9 seconds, 363.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
