c launch: /data/cnf/sc2014/app/velev-vliw-uns-4.0-9.cnf.bz2
c host: atom09
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/velev-vliw-uns-4.0-9.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/velev-vliw-uns-4.0-9.cnf.bz2
c no embedded options
c found 'p cnf 96177 1814189' header
c read 96177 variables, 1814189 clauses, 5280501 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 96176 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   96176  1814188         0       0      0     0   0  0.0   0.0   78
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 5977 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] 5977 out of 5977 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 3 variables
c [simpleprobe-1] all 96174 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 90925 variables remain 95% (5249 retained)
c [simpleprobe-1] removed 0 variables, found 4031 hbrs, 0 units
c [unhide-1] limit 907080 based on 1814161 irredundant clauses
c [unhide-1-1] 0 units, 3 failed, 478 tauts, 0 hbrs, 12333 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 96171 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 13493 variables 14% in round 1 in 157348809 steps
c [elim-1-1] backward subsumption/strengthening limit 314697618
c [elim-1-1] subsumed 88 and strengthened 19 clauses in 314698053 steps
c [elim-1-1] rescheduled 154 variables 0% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 2822 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 13493 = 14% variables out of 96171
c [phase-1] phase bias: 5859 positive 7%, 76819 negative 93%
c [simplification-1] removed 13496 variables 14.0% (82678 remain 86%)
c [simplification-1] removed 29919 irredundant clauses 1.6% (1784269 remain 98%)
c [simplification-1] maximum reduction of 14% = max (14%, 2%)
c [simplification-1] large reduction 14% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 2000 = 2 * 1000
c [simplification-1] new conflict limit 2000
c [cut-width] 1322455, max 1693816, min4 1106520 at 75%, min10 871732 at 90%
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   18.8   82678  1784269         5       5      0  2753  29  2.8 1431.0   86
c R   18.8   82678  1784269        20      12      4  2757  20 11.8 1386.3   86
c R   18.9   82678  1784263        62      49      8  2758   2  8.1 1273.7   86
c R   19.0   82678  1784263       167     136     13  2759   1  9.7 1208.6   86
c R   19.2   82678  1784262       416     339     26  2761   1 10.4 997.2   86
c R   21.0   82678  1784262      1016     887     48  2768   1 13.5 2569.3   87
c 
c [simplification-2] limit of 2098 conflicts hit after 2102 conflicts
c [decomp-3] removed 3 variables
c [treelook-1] limit 446054 based on 1784216 irredundant clauses
c [treelook-1] scheduled 53736 literals 32%
c [treelook-1] scheduling used 446098 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 446054 based on 1784216 irredundant clauses
c [treelook-1] used 1801868 steps
c [treelook-1] 53734 literals remain 32%
c [treelook-1] 53297 variables remain to probed next time 64%
c [treelook-1] removed 0 variables, found 256 hbrs
c [basicprobe-1] limit 3568432 based on 1784216 irredundant clauses
c [basicprobe-1-0] 78425 probes remain 95% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 9 variables, found 853 hbrs
c [unhide-2] limit 892108 based on 1784216 irredundant clauses
c [unhide-2-2] 302 units, 2 failed, 26 tauts, 0 hbrs, 38343 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 82362 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 81282 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 164
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 163
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 162
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 126
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 109
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 97
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 95
c [cce-1-1] eliminated 3 clauses out of 8 (38%) of length 90
c [cce-1-1] eliminated 5 clauses out of 21 (24%) of length 84
c [cce-1-1] eliminated 5 clauses out of 52 (10%) of length 83
c [cce-1-1] eliminated 5 clauses out of 24 (21%) of length 82
c [cce-1-1] eliminated 5 clauses out of 41 (12%) of length 81
c [cce-1-1] eliminated 5 clauses out of 46 (11%) of length 80
c [cce-1-1] eliminated 4 clauses out of 44 (9%) of length 79
c [cce-1-1] eliminated 2 clauses out of 51 (4%) of length 69
c [cce-1-1] eliminated 4 clauses out of 49 (8%) of length 63
c [cce-1-1] eliminated 12 clauses out of 66 (18%) of length 61
c [cce-1-1] eliminated 4 clauses out of 106 (4%) of length 59
c [cce-1-1] eliminated 4 clauses out of 153 (3%) of length 54
c [cce-1-1] eliminated 7 clauses out of 119 (6%) of length 52
c [cce-1-1] eliminated 9 clauses out of 143 (6%) of length 51
c [cce-1-1] eliminated 25 clauses out of 309 (8%) of length 50
c [cce-1-1] eliminated 2 clauses out of 113 (2%) of length 49
c [cce-1-1] eliminated 17 clauses out of 181 (9%) of length 48
c [cce-1-1] eliminated 2 clauses out of 144 (1%) of length 47
c [cce-1-1] eliminated 6 clauses out of 167 (4%) of length 46
c [cce-1-1] eliminated 5 clauses out of 157 (3%) of length 45
c [cce-1-1] eliminated 30 clauses out of 190 (16%) of length 44
c [cce-1-1] eliminated 16 clauses out of 208 (8%) of length 43
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 190 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 1573595 clauses = 1014429 binary + 559166 ternary
c [cce-1] tried to eliminate 3359 small clauses 0%
c [cce-1] eliminated 302 small clauses 0%
c [cce-1] eliminated 158 binary clauses 0%
c [cce-1] eliminated 144 ternary clauses 0%
c [cce-1-1] eliminated 302 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 492 covered clauses in round 1
c [cce-1] eliminated 492 covered clauses in TOTAL during 1 rounds
c [cce-1] 492 < 1/1000 * 1699757 = 1699 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 82362 variables 100%
c [elim-2] limit of 22792681 steps penalty 0 = 0 + 0
c [elim-2] incomplete 80237 not tried 97% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 2126 = 3% variables out of 82362
c [bca-1] limit of 10000000 steps
c [bca-1] 154353 out of 160474 literals actually usable 96%
c [bca-1] added 4951 blocked clauses in 472344 steps
c [simplification-2] removed 2442 variables 3.0% (80236 remain 83%)
c [simplification-2] removed 87117 irredundant clauses 4.9% (1697139 remain 94%)
c [simplification-2] maximum reduction of 5% = max (3%, 5%)
c [simplification-2] large reduction 5% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 4000 = 2 * 2000
c [simplification-2] new conflict limit 6102
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   64.8   80236  1697139      2349    1921    586 54796   1 13.8 2352.1   86
c -   67.3   80236  1697139      5155    2533    647 54827   2 17.1 2007.7   87
c R   67.3   80236  1697139      5373    2737    652 54827   1 17.5 1997.6   87
c 
c [simplification-3] limit of 6202 conflicts hit after 6202 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 80236 free variables schedulable
c [ternres-1] 7370 ternary resolvents (0 bin, 7370 trn)
c [ternres-1] 69885 variables remain 87% (10351 retained)
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 9317 at-most-one constraints of average size 3.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 9317 out of 9317 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 1 xors of average arity 2.0
c [gauss-1] connected 2 occurrences of 2 variables (average 1.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 [decomp-5] removed 9 variables
c [simpleprobe-2] 75854 schedulable variables 95%
c [simpleprobe-2] limit 5243621 penalty 1 = 1 + 0
c [decomp-6] removed 778 variables
c [simpleprobe-2] 73147 variables remain 92% (6302 retained)
c [simpleprobe-2] removed 778 variables, found 9 hbrs, 778 units
c [cgrclsr-1] limit 840752 based on 1681504 irredundant clauses
c [cgrclsr-1] all 79449 free variables schedulable
c [cgrclsr-1] 18031 variables remain 23% (61417 retained)
c [cgrclsr-1] removed 1 variables
c [lift-1] limit 1573086 with penalty 0 = 0 + 0
c [lift-1] using 21933 probes 28%
c [lift-1] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-1] 79234 variables remain 100% (214 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 3604
c [unhide-3] limit 840743 based on 1681487 irredundant clauses
c [unhide-3-3] 126 units, 5 failed, 6619 tauts, 0 hbrs, 4582 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 75713 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1443 blocked clauses
c [block-2] 1443 < 1/1000 * 1615208 = 1615 considered unsuccessful
c [elim-3] 75713 variables 100% will be scheduled this time
c [elim-3] scheduled 75713 variables 100%
c [elim-3] limit of 52436213 steps penalty 0 = 0 + 0
c [elim-3] incomplete 40790 not tried 54% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 3495 = 5% variables out of 75713
c [bca-2] limit of 10000000 steps
c [bca-2] 135405 out of 144438 literals actually usable 94%
c [bca-2] added 20850 blocked clauses in 435564 steps
c [simplification-3] removed 8018 variables 10.0% (72218 remain 75%)
c [simplification-3] removed 90442 irredundant clauses 5.3% (1606691 remain 89%)
c [simplification-3] maximum reduction of 10% = max (10%, 5%)
c [simplification-3] large reduction 10% >= 5% limit
c [simplification-3] new conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 4000 = 2 * 2000
c [simplification-3] new conflict limit 10202
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   83.1   72217  1606691      6566    3567   7672 31723   0 16.9 1860.1   85
c -   84.2   72217  1606691      8822    3111   7715 31742   0 16.6 1723.0   86
c 
c [simplification-4] limit of 10274 conflicts hit after 10277 conflicts
c [ternres-2] limit 6426764 based on 1606691 irredundant clauses
c [ternres-2] 62912 schedulable variables 87%
c [ternres-2] 1123 ternary resolvents (0 bin, 1123 trn)
c [ternres-2] 62691 variables remain 87% (9526 retained)
c [decomp-7] removed 7 variables
c [cgrclsr-2] limit 803305 based on 1606610 irredundant clauses
c [cgrclsr-2] 16383 schedulable variables 23%
c [cgrclsr-2] fully completed congruence closure
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 0, lifted 1134
c [unhide-4] limit 803305 based on 1606610 irredundant clauses
c [unhide-4-4] 120 units, 5 failed, 126 tauts, 0 hbrs, 39459 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 9 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 1162
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 921
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 740
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 737
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 689
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 605
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 601
c [cce-2-1] eliminated 3 clauses out of 6 (50%) of length 469
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 324
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 323
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 293
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 270
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 269
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 268
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 257
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 241
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 239
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 216
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 214
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 210
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 193
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 192
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 189
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 188
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 161
c [cce-2-1] eliminated 5 clauses out of 6 (83%) of length 157
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 156
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 149
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 143
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 47 large clauses in 15000001 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2] scheduling 1456985 clauses = 897717 binary + 559268 ternary
c [cce-2] tried to eliminate 276 small clauses 0%
c [cce-2] eliminated 13 small clauses 0%
c [cce-2] eliminated 13 binary clauses 0%
c [cce-2-1] eliminated 2579 small clauses in 15000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 2626 covered clauses in round 1
c [cce-2] eliminated 2626 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 70954 variables 100%
c [elim-4] limit of 71084145 steps penalty 0 = 0 + 0
c [elim-4] incomplete 21006 not tried 30% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 357 = 1% variables out of 70954
c [bca-3] limit of 10000000 steps
c [bca-3] 133912 out of 141196 literals actually usable 95%
c [bca-3] added 213 blocked clauses in 418385 steps
c [rephase-1] after 10277 conflicts (new increment 20000, next 30277)
c [flushphases] 0 phases reset
c [simplification-4] removed 1620 variables 2.2% (70597 remain 73%)
c [simplification-4] removed 25399 irredundant clauses 1.6% (1581292 remain 87%)
c [simplification-4] maximum reduction of 2% = max (2%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 13332 = 2 * 6666
c [simplification-4] new conflict limit 23609
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   99.3   70597  1581292     12004    5857   8577 19329   3 16.7 1612.9   85
c -  100.0   70597  1581292     12987    3743   8615 19337   2 16.5 1544.1   84
c -  102.1   70597  1581292     17539    4445   8691 19350   1 16.1 1379.5   84
c -  104.6   70597  1581292     22932    5247   8778 19371   2 16.3 1235.8   84
c 
c [simplification-5] limit of 23687 conflicts hit after 23688 conflicts
c [ternres-3] limit 6325168 based on 1581292 irredundant clauses
c [ternres-3] 61296 schedulable variables 87%
c [ternres-3] 1689 ternary resolvents (0 bin, 1689 trn)
c [ternres-3] 58493 variables remain 83% (12104 retained)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 5 variables
c [treelook-2] limit 395319 based on 1581279 irredundant clauses
c [treelook-2] scheduled 47493 literals 34%
c [treelook-2] scheduling used 396414 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 395319 based on 1581279 irredundant clauses
c [treelook-2] used 1953271 steps
c [treelook-2] 47490 literals remain 34%
c [treelook-2] 39592 variables remain to probed next time 56%
c [treelook-2] removed 0 variables, found 245 hbrs
c [lift-2] limit 1820268 with penalty 1 = 1 + 0
c [lift-2] using 21784 probes 31%
c [lift-2] 1322 units, 0 impls, 3 eqs in 1 rounds
c [lift-2] 69031 variables remain 100% (236 retained)
c [lift-2] removed 1325 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 0, lifted 0
c [unhide-5] limit 1213512 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 4 failed, 1735 tauts, 0 hbrs, 3538 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 69264 variables 100%
c [block-3] limit of 30337812 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 609 blocked clauses
c [block-3] 609 < 1/1000 * 1553929 = 1553 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 1404
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 1394
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 1119
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 1105
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 1096
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 1084
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 1002
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 858
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 806
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 775
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 728
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 725
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 620
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 590
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 587
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 558
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 557
c [cce-3-1] eliminated 2 clauses out of 6 (33%) of length 515
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 492
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 457
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 454
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 312
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 307
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 264
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 259
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 258
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 255
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 218
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 212
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 210
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 209
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 197
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 196
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 173
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 169
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 167
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 163
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 161
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 143
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 135
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 133
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 125
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 119
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 100
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 99
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 85 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 902790 clauses = 868591 binary + 34199 ternary
c [cce-3] tried to eliminate 152 small clauses 0%
c [cce-3] eliminated 27 small clauses 0%
c [cce-3] eliminated 27 binary clauses 0%
c [cce-3-1] eliminated 27 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 112 covered clauses in round 1
c [cce-3] eliminated 112 covered clauses in TOTAL during 1 rounds
c [cce-3] 112 < 1/1000 * 1553260 = 1553 considered unsuccessful
c [elim-5] 20952 variables 30% will be scheduled this time
c [elim-5] scheduled 20952 variables 30%
c [elim-5] limit of 121351249 steps penalty 0 = 0 + 0
c [elim-5] incomplete 10712 not tried 15% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 102 = 0% variables out of 69262
c [bca-4] limit of 10000000 steps
c [bca-4] 129119 out of 138322 literals actually usable 93%
c [bca-4] added 357 blocked clauses in 338220 steps
c [simplification-5] removed 1437 variables 2.0% (69160 remain 72%)
c [simplification-5] removed 30588 irredundant clauses 1.9% (1550704 remain 85%)
c [simplification-5] maximum reduction of 2% = max (2%, 2%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 13332
c [simplification-5] penalized conflict interval 26664 = 2 * 13332
c [simplification-5] new conflict limit 50352
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  123.1   69160  1550704     26538    8561   9754 20045   3 17.0 1205.7   85
c -  124.2   69160  1550704     28344    5683   9793 20047   1 17.0 1157.0   84
c -  127.2   69160  1550704     34628    6359   9902 20060   1 17.2 1052.1   84
c -  130.0   69160  1550704     41449    6998   9976 20098   1 18.1 981.8   84
c -  133.5   69160  1550704     48889    7739  10082 20117   2 18.0 909.6   84
c 
c [simplification-6] limit of 50486 conflicts hit after 50488 conflicts
c [ternres-4] limit 10870557 with penalty 0 = 0 + 0
c [ternres-4] 57296 schedulable variables 83%
c [ternres-4] 3032 ternary resolvents (0 bin, 3032 trn)
c [ternres-4] 52731 variables remain 76% (16429 retained)
c [card-3] limit 1358819 penalty 2 = 2 + 0
c [card-3] found 10372 at-most-one constraints of average size 3.7
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1358819 for elimination
c [card-3] 10372 out of 10372 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 3 variables
c [basicprobe-2] limit 10870557 penalty 0 = 0 + 0
c [basicprobe-2-0] 61516 probes remain 89% after last round
c [basicprobe-2-0] 41 units = 41 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 41 variables, found 4657 hbrs
c [cgrclsr-3] limit 775034 based on 1550068 irredundant clauses
c [cgrclsr-3] all 69116 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 6522334 with penalty 0 = 0 + 0
c [lift-3] using 22046 probes 32%
c [lift-3] 899 units, 6 impls, 24 eqs in 1 rounds
c [lift-3] 67849 variables remain 99% (344 retained)
c [lift-3] removed 923 variables
c [unhide-6] limit 2174111 with penalty 0 = 0 + 0
c [unhide-6-6] 38 units, 1 failed, 276 tauts, 0 hbrs, 26734 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 2 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 68154 variables 100%
c [elim-6] limit of 217411149 steps penalty 0 = 0 + 0
c [elim-6] incomplete 14117 not tried 21% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 9333 = 14% variables out of 68154
c [bca-5] limit of 10000000 steps
c [bca-5] 106638 out of 117644 literals actually usable 91%
c [bca-5] added 637 blocked clauses in 330365 steps
c [rephase-2] after 50488 conflicts (new increment 40000, next 90488)
c [flushphases] 0 phases reset
c [simplification-6] removed 10339 variables 14.9% (58821 remain 61%)
c [simplification-6] removed 140171 irredundant clauses 9.0% (1410533 remain 78%)
c [simplification-6] maximum reduction of 15% = max (15%, 9%)
c [simplification-6] large reduction 15% >= 5% limit
c [simplification-6] new conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 4000 = 2 * 2000
c [simplification-6] new conflict limit 54488
c 
c [simplification-7] limit of 54488 conflicts hit after 54490 conflicts
c [ternres-5] limit 11061916 with penalty 0 = 0 + 0
c [ternres-5] 44885 schedulable variables 76%
c [ternres-5] 6243 ternary resolvents (2 bin, 6241 trn)
c [ternres-5] 40926 variables remain 70% (17895 retained)
c [decomp-11] removed 14 variables
c [simpleprobe-3] 54158 schedulable variables 92%
c [simpleprobe-3] limit 44247666 penalty 0 = 0 + 0
c [decomp-12] removed 168 variables
c [simpleprobe-3] 53047 variables remain 90% (5592 retained)
c [simpleprobe-3] removed 168 variables, found 12010 hbrs, 168 units
c [lift-4] limit 6637150 with penalty 0 = 0 + 0
c [lift-4] using 21912 probes 37%
c [lift-4] 980 units, 12 impls, 0 eqs in 1 rounds
c [lift-4] 57140 variables remain 99% (519 retained)
c [lift-4] removed 980 variables
c [cliff-4] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-4] failed 1, lifted 0
c [unhide-7] limit 2212383 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 3980 tauts, 0 hbrs, 21098 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 9 transitive binary clauses
c [cce-4] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 1120
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 1048
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 864
c [cce-4-1] eliminated 11 clauses out of 11 (100%) of length 825
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 763
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 755
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 650
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 609
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 465
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 463
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 452
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 450
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 442
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 424
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 408
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 396
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 395
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 385
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 360
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 348
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 347
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 319
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 284
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 282
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 259
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 258
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 253
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 243
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 224
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 213
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 196
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 191
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 188
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 176
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 172
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 164
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 163
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 162
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 77 large clauses in 15000001 steps
c [cce-4-1] allowing another 7500000 steps for small clauses
c [cce-4] scheduling 715983 clauses = 682709 binary + 33274 ternary
c [cce-4] tried to eliminate 20 small clauses 0%
c [cce-4] eliminated 4 small clauses 0%
c [cce-4] eliminated 4 binary clauses 0%
c [cce-4-1] eliminated 4 small clauses in 15000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 81 covered clauses in round 1
c [cce-4] eliminated 81 covered clauses in TOTAL during 1 rounds
c [cce-4] 81 < 1/1000 * 1382456 = 1382 considered unsuccessful
c [elim-7] 10016 variables 17% will be scheduled this time
c [elim-7] scheduled 10016 variables 17%
c [elim-7] limit of 221238333 steps penalty 0 = 0 + 0
c [elim-7] incomplete 6989 not tried 12% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 97 = 0% variables out of 57657
c [bca-6] limit of 10000000 steps
c [bca-6] 101179 out of 115122 literals actually usable 88%
c [bca-6] added 589 blocked clauses in 289822 steps
c [simplification-7] removed 1261 variables 2.1% (57560 remain 60%)
c [simplification-7] removed 31245 irredundant clauses 2.2% (1379288 remain 76%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 19998
c [simplification-7] penalized conflict interval 39996 = 2 * 19998
c [simplification-7] new conflict limit 94486
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  188.4   57560  1379288     56795    8099  14550 31189   2 19.4 892.7   83
c R  188.6   57560  1379288     58156    9337  14566 31191   2 19.5 889.3   84
c -  191.8   57560  1379288     65093    8639  14631 31215   1 19.4 839.0   83
c i  193.1   57559  1379288     67414   10788  14661 31219   1 19.4 825.3   84
c -  195.6   57552  1379288     73936    9280  14704 31225   1 19.9 796.2   83
c i  198.4   57551  1379288     78802   13660  14793 31256   0 19.8 778.1   84
c -  199.8   57158  1379288     83801   10316  14810 31277   2 20.3 767.7   83
c -  204.3   57158  1379288     93543   10703  14889 31298   1 20.3 732.5   83
c 
c [simplification-8] limit of 94726 conflicts hit after 94726 conflicts
c [ternres-6] limit 17715604 with penalty 0 = 0 + 0
c [ternres-6] 39781 schedulable variables 69%
c [ternres-6] 3434 ternary resolvents (4 bin, 3430 trn)
c [ternres-6] 33199 variables remain 58% (23959 retained)
c [gauss-3] limit 885780 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 [decomp-13] removed 8 variables
c [lift-5] limit 10629362 with penalty 0 = 0 + 0
c [lift-5] using 22323 probes 39%
c [lift-5] 3750 units, 12 impls, 12 eqs in 1 rounds
c [lift-5] 52589 variables remain 99% (799 retained)
c [lift-5] removed 3762 variables
c [cliff-5] limit of 14172483 steps penalty 0 = 0 + 0
c [cliff-5] failed 0, lifted 622
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 52766 variables 100%
c [block-4] limit of 44289012 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 43617 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 52756 variables 100%
c [elim-8] limit of 354312096 steps penalty 0 = 0 + 0
c [elim-8] incomplete 7199 not tried 14% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 4447 = 8% variables out of 52756
c [bca-7] limit of 10000000 steps
c [bca-7] 82305 out of 96620 literals actually usable 85%
c [bca-7] added 806 blocked clauses in 254513 steps
c [rephase-3] after 94726 conflicts (new increment 80000, next 174726)
c [flushphases] 0 phases reset
c [simplification-8] removed 8849 variables 15.5% (48309 remain 50%)
c [simplification-8] removed 144954 irredundant clauses 10.5% (1234334 remain 68%)
c [simplification-8] maximum reduction of 15% = max (15%, 11%)
c [simplification-8] large reduction 15% >= 5% limit
c [simplification-8] new conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 4000 = 2 * 2000
c [simplification-8] new conflict limit 98726
c 
c [simplification-9] limit of 98738 conflicts hit after 98740 conflicts
c [ternres-7] limit 18282702 with penalty 0 = 0 + 0
c [ternres-7] 28055 schedulable variables 58%
c [ternres-7] 3926 ternary resolvents (3 bin, 3923 trn)
c [ternres-7] 22723 variables remain 47% (25586 retained)
c [decomp-14] removed 23 variables
c [cgrclsr-4] limit 617144 based on 1234288 irredundant clauses
c [cgrclsr-4] all 48286 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-6] limit 10969621 with penalty 0 = 0 + 0
c [lift-6] using 21968 probes 45%
c [lift-6] 728 units, 10 impls, 4 eqs in 1 rounds
c [lift-6] 46428 variables remain 98% (1126 retained)
c [lift-6] removed 732 variables
c [cliff-6] limit of 14626161 steps penalty 0 = 0 + 0
c [cliff-6] failed 1, lifted 714
c [unhide-8] limit 1828270 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 0 failed, 759 tauts, 0 hbrs, 55025 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 16 transitive binary clauses
c [transred-7] found 18 units
c [elim-9] 6875 variables 15% will be scheduled this time
c [elim-9] scheduled 6875 variables 15%
c [elim-9] limit of 365654049 steps penalty 0 = 0 + 0
c [elim-9] incomplete 2337 not tried 5% in round 1
c [elim-9] transition to [ all 0 rem 1 ] state
c [elim-9] eliminated 8 = 0% variables out of 46506
c [elim-9] 8 < 1/1000 * 46506 = 46 considered unsuccessful
c [bca-8] limit of 10000000 steps
c [bca-8] 76747 out of 92998 literals actually usable 83%
c [bca-8] added 2387 blocked clauses in 241244 steps
c [simplification-9] removed 1811 variables 3.7% (46498 remain 48%)
c [simplification-9] removed 34950 irredundant clauses 2.8% (1199384 remain 66%)
c [simplification-9] maximum reduction of 4% = max (4%, 3%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 23998
c [simplification-9] penalized conflict interval 47996 = 2 * 23998
c [simplification-9] new conflict limit 146736
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  288.9   46498  1199384    105309   10877  21521 18826   1 20.3 699.1   78
c -  291.2   46498  1199384    116596   11808  21564 18830   2 22.1 693.7   78
c R  292.3   46498  1199384    126342   20600  21595 18838   3 22.7 690.1   82
c -  293.2   46498  1199384    127910   12038  21621 18850   1 22.7 686.6   78
c -  298.1   46498  1199384    140308   12730  21765 18882   2 22.8 663.6   78
c 
c [simplification-10] limit of 146938 conflicts hit after 146941 conflicts
c [ternres-8] limit 23691771 with penalty 0 = 0 + 0
c [ternres-8] 21879 schedulable variables 47%
c [ternres-8] 6739 ternary resolvents (18 bin, 6721 trn)
c [ternres-8] 14408 variables remain 31% (32090 retained)
c [card-4] limit 1480735 penalty 3 = 3 + 0
c [card-4] found 8613 at-most-one constraints of average size 3.2
c [card-4] found 79 at-most-two constraints of average size 4.2
c [card-4] using previous limit 1480735 for elimination
c [card-4] 8692 out of 8692 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-15] removed 2 variables
c [treelook-3] limit 299845 based on 1199380 irredundant clauses
c [treelook-3] scheduled 25000 literals 27%
c [treelook-3] scheduling used 299934 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 299845 based on 1199380 irredundant clauses
c [treelook-3] used 1843499 steps
c [treelook-3] 24998 literals remain 27%
c [treelook-3] 15894 variables remain to probed next time 34%
c [treelook-3] removed 0 variables, found 298 hbrs
c [lift-7] limit 14215062 with penalty 0 = 0 + 0
c [lift-7] using 21729 probes 47%
c [lift-7] 2108 units, 15 impls, 6 eqs in 1 rounds
c [lift-7] 42729 variables remain 96% (1653 retained)
c [lift-7] removed 2114 variables
c [cliff-7] limit of 18953416 steps penalty 0 = 0 + 0
c [cliff-7] failed 4, lifted 21
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 8 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 44316 variables 100%
c [block-5] limit of 118458856 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 10325 blocked clauses
c [cce-5] limit of 11845885 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 549
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 458
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 413
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 367
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 309
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 277
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 263
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 246
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 244
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 229
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 209
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 187
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 186
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 159
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 152
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 143
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 139
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 97
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 96
c [cce-5-1] eliminated 1 clauses out of 9 (11%) of length 95
c [cce-5-1] eliminated 1 clauses out of 7 (14%) of length 94
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 92
c [cce-5-1] eliminated 3 clauses out of 16 (19%) of length 84
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 38 large clauses in 11845886 steps
c [cce-5-1] allowing another 5922943 steps for small clauses
c [cce-5] scheduling 520295 clauses = 489743 binary + 30552 ternary
c [cce-5] tried to eliminate 132 small clauses 0%
c [cce-5] eliminated 33 small clauses 0%
c [cce-5] eliminated 32 binary clauses 0%
c [cce-5] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 33 small clauses in 11845886 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 71 covered clauses in round 1
c [cce-5] eliminated 71 covered clauses in TOTAL during 1 rounds
c [cce-5] 71 < 1/1000 * 1157108 = 1157 considered unsuccessful
c [bca-9] limit of 10000000 steps
c [bca-9] 66718 out of 88628 literals actually usable 75%
c [bca-9] added 129 blocked clauses in 195467 steps
c [simplification-10] removed 2185 variables 4.7% (44313 remain 46%)
c [simplification-10] removed 42347 irredundant clauses 3.5% (1157037 remain 64%)
c [simplification-10] maximum reduction of 5% = max (5%, 4%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] new conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 4000 = 2 * 2000
c [simplification-10] new conflict limit 150941
c 
c [simplification-11] limit of 150947 conflicts hit after 150949 conflicts
c [ternres-9] limit 24041403 with penalty 0 = 0 + 0
c [ternres-9] 13753 schedulable variables 31%
c [ternres-9] 4970 ternary resolvents (9 bin, 4961 trn)
c [ternres-9] 7178 variables remain 16% (37135 retained)
c [decomp-17] removed 5 variables
c [basicprobe-3] limit 24041403 penalty 0 = 0 + 0
c [basicprobe-3-0] 33249 probes remain 76% after last round
c [basicprobe-3-0] 86 units = 81 failed (94%) + 5 lifted (6%)
c [basicprobe-3-0] removed 654 variables, found 18026 hbrs
c [bate-1] eliminated 42 asymmetric tautologies during probing
c [lift-8] limit 14424842 with penalty 0 = 0 + 0
c [lift-8] using 21680 probes 50%
c [lift-8] 101 units, 22 impls, 12 eqs in 1 rounds
c [lift-8] 41306 variables remain 95% (2235 retained)
c [lift-8] removed 113 variables
c [cliff-8] limit of 19233123 steps penalty 0 = 0 + 0
c [cliff-8] failed 0, lifted 9
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 14 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 43532 variables 100%
c [block-6] limit of 240414039 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 6794 blocked clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 43524 variables 100%
c [elim-10] limit of 240414039 steps penalty 1 = 1 + 0
c [elim-10] incomplete 6706 not tried 15% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1875 = 4% variables out of 43524
c [bca-10] limit of 10000000 steps
c [bca-10] 61226 out of 83300 literals actually usable 74%
c [bca-10] added 2975 blocked clauses in 195574 steps
c [simplification-11] removed 2664 variables 6.0% (41649 remain 43%)
c [simplification-11] removed 25549 irredundant clauses 2.2% (1131488 remain 62%)
c [simplification-11] maximum reduction of 6% = max (6%, 2%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] new conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 4000 = 2 * 2000
c [simplification-11] new conflict limit 154949
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  324.7   41649  1131488    154097   13331  31375 31896   1 22.7 647.7   77
c 
c [simplification-12] limit of 154967 conflicts hit after 154968 conflicts
c [ternres-10] limit 24542341 with penalty 0 = 0 + 0
c [ternres-10] 6774 schedulable variables 16%
c [ternres-10] 7736 ternary resolvents (25 bin, 7711 trn)
c [ternres-10] 415 variables remain 1% (41234 retained)
c [gauss-4] limit 613558 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 37571 schedulable variables 90%
c [simpleprobe-4] limit 98169364 penalty 0 = 0 + 0
c [decomp-19] removed 17 variables
c [simpleprobe-4] 33315 variables remain 80% (8317 retained)
c [simpleprobe-4] removed 17 variables, found 12058 hbrs, 11 units
c [lift-9] limit 14725404 with penalty 0 = 0 + 0
c [lift-9] using 20897 probes 50%
c [lift-9] 177 units, 7 impls, 3 eqs in 1 rounds
c [lift-9] 38568 variables remain 93% (2884 retained)
c [lift-9] removed 180 variables
c [cliff-9] limit of 19633872 steps penalty 0 = 0 + 0
c [cliff-9] failed 0, lifted 2
c [unhide-9] limit 1227117 with penalty 2 = 2 + 0
c [unhide-9-9] 0 units, 0 failed, 4763 tauts, 0 hbrs, 8251 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 18 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 41450 variables 100%
c [block-7] limit of 245423410 steps penalty 0 = 0 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 283 blocked clauses
c [block-7] 283 < 1/1000 * 1125982 = 1125 considered unsuccessful
c [elim-11] 2312 variables 6% will be scheduled this time
c [elim-11] scheduled 2312 variables 6%
c [elim-11] limit of 490846821 steps penalty 0 = 0 + 0
c [elim-11] incomplete 301 not tried 1% in round 1
c [elim-11] transition to [ all 0 rem 1 ] state
c [elim-11] eliminated 23 = 0% variables out of 41448
c [elim-11] 23 < 1/1000 * 41448 = 41 considered unsuccessful
c [bca-11] limit of 10000000 steps
c [bca-11] 66740 out of 82852 literals actually usable 81%
c [bca-11] added 15599 blocked clauses in 225195 steps
c [simplification-12] removed 224 variables 0.5% (41425 remain 43%)
c [simplification-12] removed 17130 irredundant clauses 1.5% (1114358 remain 61%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 7999 = 23998 / 3
c [simplification-12] new conflict interval 31997
c [simplification-12] penalized conflict interval 63994 = 2 * 31997
c [simplification-12] new conflict limit 218962
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  342.3   41425  1114358    167612   13953  38344 57690   1 22.7 631.9   77
c -  345.9   41425  1114358    181883   14976  38417 57709   2 23.0 621.4   77
c -  350.8   41425  1114358    196316   15386  38543 57741   2 23.1 610.1   77
c -  355.4   41425  1114358    211683   16029  38638 57777   3 23.1 595.5   77
c 
c [simplification-13] limit of 219150 conflicts hit after 219150 conflicts
c [ternres-11] limit 32095927 with penalty 0 = 0 + 0
c [ternres-11] 415 schedulable variables 1%
c [ternres-11] 20160 ternary resolvents (311 bin, 19849 trn)
c [ternres-11] 4 variables remain 0% (41421 retained)
c [decomp-20] removed 2 variables
c [cgrclsr-5] limit 557176 based on 1114352 irredundant clauses
c [cgrclsr-5] all 41423 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-10] limit 19257556 with penalty 0 = 0 + 0
c [lift-10] using 20279 probes 49%
c [lift-10] 133 units, 22 impls, 4 eqs in 1 rounds
c [lift-10] 37636 variables remain 91% (3650 retained)
c [lift-10] removed 137 variables
c [cliff-10] limit of 25676742 steps penalty 0 = 0 + 0
c [cliff-10] failed 1, lifted 31
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 42 transitive binary clauses
c [bca-12] limit of 10000000 steps
c [bca-12] 61682 out of 82186 literals actually usable 75%
c [bca-12] added 28 blocked clauses in 213308 steps
c [rephase-4] after 219150 conflicts (new increment 160000, next 379150)
c [flushphases] 0 phases reset
c [simplification-13] removed 333 variables 0.8% (41092 remain 43%)
c [simplification-13] removed 5671 irredundant clauses 0.5% (1108687 remain 61%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 15998 = 31997 / 2
c [simplification-13] new conflict interval 47995
c [simplification-13] penalized conflict interval 95990 = 2 * 47995
c [simplification-13] new conflict limit 315140
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  364.4   41092  1108682    227381   16795  57538 56885   2 23.1 584.2   78
c -  368.6   41092  1108682    244200   17643  57655 56906   3 23.9 578.1   79
c -  371.1   41092  1108682    264619   18189  57712 56916   4 27.3 571.5   79
c R  372.0   41092  1108682    273064   23603  57719 56917   4 28.3 569.2   82
c -  376.3   41092  1108682    284768   18971  57807 56934   3 28.2 562.2   79
c -  382.2   41092  1108682    302787   19476  57899 56958   2 28.3 554.4   79
c 
c [simplification-14] limit of 315348 conflicts hit after 315348 conflicts
c [ternres-12] limit 41018081 with penalty 0 = 0 + 0
c [ternres-12] 4 schedulable variables 0%
c [ternres-12] 2461 ternary resolvents (21 bin, 2440 trn)
c [ternres-12] 3 variables remain 0% (41089 retained)
c [decomp-21] removed 7 variables
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 19574 probes 48%
c [lift-11] 209 units, 16 impls, 13 eqs in 1 rounds
c [lift-11] 36461 variables remain 89% (4400 retained)
c [lift-11] removed 224 variables
c [cliff-11] limit of 32814465 steps penalty 0 = 0 + 0
c [cliff-11] failed 0, lifted 161
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 75 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 40700 variables 100%
c [block-8] limit of 205090408 steps penalty 1 = 1 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 433 blocked clauses
c [block-8] 433 < 1/1000 * 1104930 = 1104 considered unsuccessful
c [cce-6] limit of 10254520 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 424
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 304
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 251
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 189
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 179
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 169
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 144
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 118
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 110
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 104
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 87
c [cce-6-1] eliminated 5 clauses out of 26 (19%) of length 82
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 23 large clauses in 10254521 steps
c [cce-6-1] allowing another 5127260 steps for small clauses
c [cce-6] scheduling 481869 clauses = 451764 binary + 30105 ternary
c [cce-6] tried to eliminate 176 small clauses 0%
c [cce-6] eliminated 64 small clauses 0%
c [cce-6] eliminated 64 binary clauses 0%
c [cce-6-1] eliminated 64 small clauses in 10254521 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 87 covered clauses in round 1
c [cce-6] eliminated 87 covered clauses in TOTAL during 1 rounds
c [cce-6] 87 < 1/1000 * 1101836 = 1101 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 40690 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] incomplete 2801 not tried 7% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 1193 = 3% variables out of 40690
c [bca-13] limit of 10000000 steps
c [bca-13] 56614 out of 78996 literals actually usable 72%
c [bca-13] added 560 blocked clauses in 200472 steps
c [simplification-14] removed 1595 variables 3.9% (39497 remain 41%)
c [simplification-14] removed 22799 irredundant clauses 2.1% (1085883 remain 60%)
c [simplification-14] maximum reduction of 4% = max (4%, 2%)
c [simplification-14] geometric conflict interval increment 9599 = 47995 / 5
c [simplification-14] new conflict interval 57594
c [simplification-14] penalized conflict interval 115188 = 2 * 57594
c [simplification-14] new conflict limit 430536
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  406.8   39497  1085883    323230   20373  57459 42799   2 28.2 548.7   79
c -  413.1   39497  1085883    343305   21088  57648 42829   1 28.3 543.0   79
c -  419.8   39497  1085883    363988   21876  57824 42851   2 28.3 536.7   79
c -  426.5   39497  1085883    385122   22928  58097 42901   2 28.0 531.7   79
c -  431.4   39497  1085883    406068   23914  58303 42951   1 27.7 530.8   79
c -  439.2   39497  1085883    428018   24872  58565 43012   2 27.5 526.7   79
c 
c [simplification-15] limit of 430958 conflicts hit after 430964 conflicts
c [ternres-13] limit 53674013 with penalty 0 = 0 + 0
c [ternres-13] 2 schedulable variables 0%
c [ternres-13] 11074 ternary resolvents (292 bin, 10782 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1677312 penalty 4 = 4 + 0
c [card-5] found 7584 at-most-one constraints of average size 3.3
c [card-5] found 197 at-most-two constraints of average size 4.1
c [card-5] using previous limit 1677312 for elimination
c [card-5] 7781 out of 7781 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-22] removed 2 variables
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 18967 probes 48%
c [lift-12] 43 units, 17 impls, 5 eqs in 1 rounds
c [lift-12] 34265 variables remain 87% (5181 retained)
c [lift-12] removed 49 variables
c [cliff-12] limit of 42939210 steps penalty 0 = 0 + 0
c [cliff-12] failed 11, lifted 8
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 46 transitive binary clauses
c [elim-13] 294 variables 1% will be scheduled this time
c [elim-13] scheduled 294 variables 1%
c [elim-13] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-13] incomplete 175 not tried 0% in round 1
c [elim-13] transition to [ all 0 rem 1 ] state
c [elim-13] eliminated 11 = 0% variables out of 39426
c [elim-13] 11 < 1/1000 * 39426 = 39 considered unsuccessful
c [bca-14] limit of 10000000 steps
c [bca-14] 55471 out of 78832 literals actually usable 70%
c [bca-14] added 149 blocked clauses in 199486 steps
c [rephase-5] after 430964 conflicts (new increment 320000, next 750964)
c [flushphases] 0 phases reset
c [simplification-15] removed 82 variables 0.2% (39415 remain 41%)
c [simplification-15] removed 8479 irredundant clauses 0.8% (1077404 remain 59%)
c [simplification-15] maximum reduction of 1% = max (0%, 1%)
c [simplification-15] geometric conflict interval increment 28797 = 57594 / 2
c [simplification-15] new conflict interval 86391
c [simplification-15] penalized conflict interval 172782 = 2 * 86391
c [simplification-15] new conflict limit 603746
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  460.8   39415  1077404    450783   25879  68393 50845   3 27.4 522.8   79
c -  469.2   39415  1077404    474272   26653  68731 50878   3 27.5 521.8   79
c -  475.6   39415  1077404    499163   27228  68825 50904   1 27.5 515.0   80
c -  481.2   39415  1077404    524814   28184  68967 50930   2 27.4 509.2   80
c -  485.4   39415  1077404    551464   28633  69016 50959   3 27.2 502.0   80
c -  489.0   39415  1077404    580411   29272  69086 50961   2 28.2 497.3   80
c R  489.8   39415  1077404    586600   33836  69094 50961   3 28.3 496.1   83
c i  492.0   39414  1077404    598129   43253  69127 50972   1 28.1 492.4   85
c i  492.6   38157  1077404    599087   44098  69157 50993   1 28.1 492.5   85
c i  493.5   38056  1077404    601244   45939  69189 51033   1 28.1 492.6   85
c i  493.8   38047  1077404    601825   46453  69195 51047   2 28.1 492.5   85
c i  493.8   38013  1077404    601826   46453  69195 51047   1 28.1 492.5   85
c i  493.8   37983  1077404    601827   46453  69195 51047   1 28.1 492.5   85
c 
c [simplification-16] limit of 604332 conflicts hit after 604332 conflicts
c [ternres-14] limit 67873018 with penalty 0 = 0 + 0
c [ternres-14] all 37954 free variables schedulable
c [ternres-14] 368 ternary resolvents (1 bin, 367 trn)
c [ternres-14] 21049 variables remain 55% (16905 retained)
c [decomp-23] removed 3934 variables
c [treelook-4] limit 424206 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 21344 literals 30%
c [treelook-4] scheduling used 424249 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 424206 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 676462 steps
c [treelook-4] 21342 literals remain 30%
c [treelook-4] 7599 variables remain to probed next time 21%
c [treelook-4] removed 0 variables, found 35 hbrs
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 17296 probes 49%
c [lift-13] 349 units, 72 impls, 100 eqs in 1 rounds
c [lift-13] 26310 variables remain 75% (8676 retained)
c [lift-13] removed 495 variables
c [cliff-13] limit of 54298414 steps penalty 0 = 0 + 0
c [cliff-13] failed 44, lifted 225
c [unhide-10] limit 1696825 with penalty 3 = 3 + 0
c [unhide-10-11] 0 units, 0 failed, 18882 tauts, 0 hbrs, 74930 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 82 transitive binary clauses
c [bca-15] limit of 10000000 steps
c [bca-15] 49186 out of 69386 literals actually usable 71%
c [bca-15] added 2155 blocked clauses in 152414 steps
c [simplification-16] removed 3262 variables 8.6% (34692 remain 36%)
c [simplification-16] removed 105353 irredundant clauses 9.8% (972051 remain 54%)
c [simplification-16] maximum reduction of 10% = max (9%, 10%)
c [simplification-16] large reduction 10% >= 5% limit
c [simplification-16] new conflict interval 6043 = min (604332/100, 86391)
c [simplification-16] penalized conflict interval 6043 = 1 * 6043
c [simplification-16] new conflict limit 610375
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  500.5   34691   972051    605005   16160  26359 55684   1 28.0 493.6   71
c i  500.6   34683   972051    605298   16394  26366 55691   1 28.0 493.5   71
c i  501.1   34675   972051    606807   17739  26382 55694   1 28.0 493.3   71
c i  501.1   34674   972051    606808   17739  26382 55694   1 28.0 493.3   71
c i  501.3   34660   972051    607365   18219  26387 55708   1 28.0 493.2   71
c 
c [simplification-17] limit of 610523 conflicts hit after 610523 conflicts
c [ternres-15] limit 68531534 with penalty 0 = 0 + 0
c [ternres-15] 19245 schedulable variables 55%
c [ternres-15] 645 ternary resolvents (0 bin, 645 trn)
c [ternres-15] 3326 variables remain 10% (31330 retained)
c [gauss-5] limit 856644 penalty 4 = 4 + 0
c [gauss-5] extracted 16 xors of average arity 2.0
c [gauss-5] connected 32 occurrences of 32 variables (average 1.0)
c [gauss-5] limit 856644 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 796 variables
c [basicprobe-4] limit 68531534 penalty 0 = 0 + 0
c [basicprobe-4-0] 20246 sched 60%, 176 failed, 0 lifted, 17816 hbrs
c [decomp-26] removed 283 variables
c [basicprobe-4-1] 20037 probes remain 60% after last round
c [basicprobe-4-1] 176 units = 176 failed (100%) + 0 lifted (0%)
c [basicprobe-4-1] removed 283 variables, found 17854 hbrs
c [bate-2] eliminated 239 asymmetric tautologies during probing
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 12306 probes 37%
c [lift-14] 31 units, 39 impls, 64 eqs in 1 rounds
c [lift-14] 20708 variables remain 62% (12769 retained)
c [lift-14] removed 100 variables
c [cliff-14] limit of 54825227 steps penalty 0 = 0 + 0
c [cliff-14] failed 2, lifted 1
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 216 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 33474 variables 100%
c [block-9] limit of 171328835 steps penalty 2 = 2 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 38527 blocked clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 32148 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] incomplete 3135 not tried 10% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 4156 = 13% variables out of 32148
c [bca-16] limit of 10000000 steps
c [bca-16] 37808 out of 55986 literals actually usable 68%
c [bca-16] added 3165 blocked clauses in 122536 steps
c [simplification-17] removed 6664 variables 19.2% (27992 remain 29%)
c [simplification-17] removed 120712 irredundant clauses 12.4% (851339 remain 47%)
c [simplification-17] maximum reduction of 19% = max (19%, 12%)
c [simplification-17] large reduction 19% >= 5% limit
c [simplification-17] new conflict interval 6105 = min (610523/100, 86391)
c [simplification-17] penalized conflict interval 6105 = 1 * 6105
c [simplification-17] new conflict limit 616628
c [tabula-rasa-1] number clauses 851339 drops below limit 907094
c [flush-cache] 0 binary, 0 ternary, 16525 large
c [flushphases] 27992 phases reset fully
c [phase-2] phase bias: 159 positive 17%, 762 negative 83%
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 6998 and clause limit 425669
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  517.7   27992   851339    615244    2224   7247 42303   2 28.0 493.6   64
c 
c [simplification-18] limit of 616690 conflicts hit after 616697 conflicts
c [ternres-16] limit 69095509 with penalty 0 = 0 + 0
c [ternres-16] 2689 schedulable variables 10%
c [ternres-16] 3514 ternary resolvents (6 bin, 3508 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-27] removed 49 variables
c [simpleprobe-5] 21984 schedulable variables 79%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-28] removed 413 variables
c [simpleprobe-5] 2644 variables remain 10% (24886 retained)
c [simpleprobe-5] removed 413 variables, found 31513 hbrs, 136 units
c [cgrclsr-6] limit 431846 penalty 4 = 4 + 0
c [cgrclsr-6] all 27530 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 8362 probes 30%
c [lift-15] 1 units, 15 impls, 30 eqs in 1 rounds
c [lift-15] 12044 variables remain 44% (15455 retained)
c [lift-15] removed 31 variables
c [cliff-15] limit of 55276407 steps penalty 0 = 0 + 0
c [cliff-15] failed 18, lifted 12
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 626 transitive binary clauses
c [elim-15] 70 variables 0% will be scheduled this time
c [elim-15] scheduled 70 variables 0%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] incomplete 129 not tried 0% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 50 = 0% variables out of 27469
c [bca-17] limit of 10000000 steps
c [bca-17] 46815 out of 54840 literals actually usable 85%
c [bca-17] added 1587 blocked clauses in 168644 steps
c [rephase-6] after 616697 conflicts (new increment 20000, next 636697)
c [flushphases] 5143 phases reset
c [phase-3] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-18] removed 573 variables 2.0% (27419 remain 29%)
c [simplification-18] removed 10256 irredundant clauses 1.2% (841083 remain 46%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-18] new conflict interval 26666
c [simplification-18] penalized conflict interval 26666 = 1 * 26666
c [simplification-18] new conflict limit 643363
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  537.5   27418   841083    618390    4956  10585 64869   3 28.0 493.3   65
c -  537.7   27418   841083    618860    2872  10592 64871   1 28.0 493.2   64
c i  538.5   27417   841083    621776    5403  10653 64875   1 27.9 492.6   64
c -  538.8   27409   841083    623256    3690  10694 64879   3 27.9 492.5   64
c -  539.8   27409   841083    627781    4138  10825 64882   1 27.9 491.9   64
c -  541.5   27409   841083    633082    4890  10894 64893   1 27.8 492.3   64
c i  541.5   27408   841083    633151    4954  10894 64894   1 27.8 492.2   64
c i  541.5   27407   841082    633198    4982  10899 64896   1 27.8 492.2   64
c i  541.7   27406   841082    633775    5503  10903 64898   1 27.8 492.1   64
c -  542.4   27406   841082    639136    5708  11031 64904   5 27.8 491.8   64
c 
c [simplification-19] limit of 643529 conflicts hit after 643530 conflicts
c [ternres-17] limit 71307705 with penalty 0 = 0 + 0
c [ternres-17] all 27406 free variables schedulable
c [ternres-17] 46 ternary resolvents (0 bin, 46 trn)
c [ternres-17] 13992 variables remain 51% (13414 retained)
c [decomp-29] removed 41 variables
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 4357 probes 16%
c [lift-16] 19 units, 16 impls, 39 eqs in 1 rounds
c [lift-16] 7777 variables remain 28% (19543 retained)
c [lift-16] removed 58 variables
c [cliff-16] limit of 57046164 steps penalty 0 = 0 + 0
c [cliff-16] failed 27, lifted 12
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 339 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 27281 variables 100%
c [block-10] limit of 356538529 steps penalty 1 = 1 + 0
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 584 blocked clauses
c [block-10] 584 < 1/1000 * 839801 = 839 considered unsuccessful
c [cce-7] limit of 8913463 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 1 clauses out of 9 (11%) of length 82
c [cce-7-1] eliminated 1 clauses out of 33 (3%) of length 63
c [cce-7-1] eliminated 1 clauses out of 52 (2%) of length 61
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 3 large clauses in 8913464 steps
c [cce-7-1] allowing another 4456732 steps for small clauses
c [cce-7] scheduling 271478 clauses = 267300 binary + 4178 ternary
c [cce-7] tried to eliminate 270 small clauses 0%
c [cce-7] eliminated 107 small clauses 0%
c [cce-7] eliminated 107 binary clauses 0%
c [cce-7-1] eliminated 107 small clauses in 8913464 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 110 covered clauses in round 1
c [cce-7] eliminated 110 covered clauses in TOTAL during 1 rounds
c [cce-7] 110 < 1/1000 * 838284 = 838 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 27278 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] incomplete 68 not tried 0% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 108 = 0% variables out of 27278
c [bca-18] limit of 10000000 steps
c [bca-18] 43366 out of 54342 literals actually usable 80%
c [bca-18] added 247 blocked clauses in 173719 steps
c [rephase-7] after 643530 conflicts (new increment 40000, next 683530)
c [flushphases] 4947 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-19] removed 236 variables 0.9% (27170 remain 28%)
c [simplification-19] removed 7254 irredundant clauses 0.9% (833828 remain 46%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-19] new conflict interval 39999
c [simplification-19] penalized conflict interval 39999 = 1 * 39999
c [simplification-19] new conflict limit 683529
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  558.3   27170   833828    645650    6154  10452 62233   3 27.8 491.4   64
c -  560.0   27170   833828    652728    6849  10609 62247   1 27.8 490.1   64
c -  561.8   27170   833828    660579    7501  10756 62251   2 27.7 488.6   64
c i  562.5   27169   833828    663739   10200  10812 62262   1 27.7 488.1   65
c -  563.6   27157   833828    669004    8327  10856 62271   3 27.7 487.8   64
c -  565.9   27157   833828    677614    8935  10948 62284   2 27.7 487.3   64
c 
c [simplification-20] limit of 683627 conflicts hit after 683628 conflicts
c [ternres-18] limit 74835993 with penalty 0 = 0 + 0
c [ternres-18] 13869 schedulable variables 51%
c [ternres-18] 54 ternary resolvents (0 bin, 54 trn)
c [ternres-18] 535 variables remain 2% (26622 retained)
c [decomp-30] removed 54 variables
c [lift-17] limit 20000000 with penalty 0 = 0 + 0
c [lift-17] using 232 probes 1%
c [lift-17-1] found 74 units 2 impls in round 1
c [lift-17-2] found 1 units 3 impls in round 2
c [lift-17-3] found 18 units 4 impls in round 3
c [lift-17-4] found 23 units 2 impls in round 4
c [lift-17-5] found 0 units 2 impls in round 5
c [lift-17] 116 units, 13 impls, 47 eqs in 6 rounds
c [lift-17] 7406 variables remain 27% (19547 retained)
c [lift-17] removed 163 variables
c [cliff-17] limit of 59868794 steps penalty 0 = 0 + 0
c [cliff-17] failed 30, lifted 5
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 317 transitive binary clauses
c [elim-17] 46 variables 0% will be scheduled this time
c [elim-17] scheduled 46 variables 0%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] incomplete 44 not tried 0% in round 1
c [elim-17] transition to [ all 0 rem 1 ] state
c [elim-17] eliminated 71 = 0% variables out of 26881
c [bca-19] limit of 10000000 steps
c [bca-19] 39880 out of 53622 literals actually usable 74%
c [bca-19] added 52 blocked clauses in 148856 steps
c [rephase-8] after 683628 conflicts (new increment 80000, next 763628)
c [flushphases] 4845 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-20] removed 347 variables 1.3% (26810 remain 28%)
c [simplification-20] removed 11943 irredundant clauses 1.4% (821885 remain 45%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 19999 = 39999 / 2
c [simplification-20] new conflict interval 59998
c [simplification-20] penalized conflict interval 59998 = 1 * 59998
c [simplification-20] new conflict limit 743626
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  580.2   26809   821885    683993   13041  10915 59367   2 27.6 486.0   66
c i  580.6   26808   821885    685804   14504  10982 59372   2 27.6 485.7   66
c i  580.7   26806   821885    685813   14510  10982 59373   2 27.6 485.7   66
c i  580.7   26804   821885    685821   14512  10982 59375   1 27.6 485.7   66
c i  580.7   26795   821885    685824   14513  10982 59376   1 27.6 485.7   66
c -  581.3   26787   821885    688568    9260  11047 59381   5 27.6 485.4   64
c i  581.4   26786   821885    688834    9474  11053 59382   2 27.6 485.3   64
c i  583.0   26778   821885    699712   17759  11227 59426   3 27.4 483.3   66
c -  583.2   26629   821885    700309   10403  11260 59435   6 27.4 483.3   64
c i  583.5   26628   821885    704385   13920  11282 59445   2 27.4 483.2   66
c -  584.1   26621   821885    710527   10829  11328 59445   4 27.3 482.5   64
c i  586.1   26620   821885    719892   18984  11386 59448   1 27.3 481.3   67
c i  586.2   26607   821885    720230   19254  11387 59448   1 27.3 481.1   67
c -  586.5   26604   821885    721763   11506  11404 59449   2 27.2 480.7   64
c i  588.0   26603   821885    728052   16852  11473 59458   2 27.2 479.6   66
c i  588.0   26599   821885    728198   16921  11478 59461   1 27.2 479.6   66
c -  589.1   26564   821885    734348   12350  11552 59467   2 27.1 478.1   64
c 
c [simplification-21] limit of 744044 conflicts hit after 744045 conflicts
c [ternres-19] limit 78403845 with penalty 0 = 0 + 0
c [ternres-19] 520 schedulable variables 2%
c [ternres-19] 30 ternary resolvents (4 bin, 26 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 2450120 penalty 4 = 4 + 0
c [card-6] found 4641 at-most-one constraints of average size 3.6
c [card-6] found 106 at-most-two constraints of average size 4.5
c [card-6] using previous limit 2450120 for elimination
c [card-6] 4747 out of 4747 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-31] removed 1079 variables
c [lift-18] limit 20000000 with penalty 0 = 0 + 0
c [lift-18] using 229 probes 1%
c [lift-18-1] found 29 units 37 impls in round 1
c [lift-18-2] found 49 units 17 impls in round 2
c [lift-18-3] found 0 units 9 impls in round 3
c [lift-18-4] found 0 units 2 impls in round 4
c [lift-18-5] found 0 units 2 impls in round 5
c [lift-18] 78 units, 67 impls, 93 eqs in 6 rounds
c [lift-18] 6912 variables remain 27% (18643 retained)
c [lift-18] removed 176 variables
c [cliff-18] limit of 62723076 steps penalty 0 = 0 + 0
c [cliff-18] failed 19, lifted 14
c [unhide-11] limit 980048 with penalty 4 = 4 + 0
c [unhide-11-12] 0 units, 0 failed, 7350 tauts, 0 hbrs, 6567 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 190 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 25514 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18] incomplete 31 not tried 0% in round 1
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 3082 = 12% variables out of 25514
c [bca-20] limit of 10000000 steps
c [bca-20] 33496 out of 44866 literals actually usable 75%
c [bca-20] added 5368 blocked clauses in 118230 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-21] removed 4132 variables 15.6% (22432 remain 23%)
c [simplification-21] removed 95115 irredundant clauses 11.6% (726770 remain 40%)
c [simplification-21] maximum reduction of 16% = max (16%, 12%)
c [simplification-21] large reduction 16% >= 5% limit
c [simplification-21] new conflict interval 7440 = min (744045/100, 59998)
c [simplification-21] penalized conflict interval 7440 = 1 * 7440
c [simplification-21] new conflict limit 751485
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  608.6   22431   726770    746884   15579   2677 32297   2 26.9 475.0   63
c i  608.6   22025   726770    746885   15579   2677 32297   2 26.9 475.0   63
c i  608.7   21878   726770    747455   16012   2685 32300   2 26.9 474.8   63
c i  608.7   20548   726770    747463   16018   2685 32300   2 26.9 474.8   63
c i  608.7   18895   726770    747501   16028   2693 32304   2 26.9 474.8   63
c i  608.7   17687   726770    747516   16039   2695 32305   2 26.9 474.8   63
c i  608.7   17686   726770    747517   16039   2695 32305   2 26.9 474.8   63
c i  608.7   17685   726770    747518   16039   2695 32305   2 26.9 474.8   63
c i  608.7   17684   726770    747544   16040   2702 32309   2 26.9 474.8   63
c i  608.7   17255   726770    747547   16041   2702 32309   2 26.9 474.8   63
c i  608.7   17254   726770    747548   16041   2702 32309   2 26.9 474.8   63
c i  608.7   17253   726770    747549   16041   2702 32309   2 26.9 474.8   63
c i  608.7   17252   726770    747550   16041   2702 32309   2 26.9 474.8   63
c 0  608.7   17219   726770    747550   16041   2702 32309   2 26.9 474.8   63
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 281 basic ate = 272 trn 97% + 9 lrg 3% in 2 updates
c bcas: 20 count, 62804 added (36206 skipped), 4894358 steps
c bkwd: tried 54744 clauses, 109383 lits, 2.00 lits/clause
c bkwd: checked 253101749 occs, 4623.37 occs/clause, 2313.90 occs/lit
c bkwd: subsumed 0 binary, 1 ternary, 87 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 19 large (0% self)
c blkd: 10 bces, 183897 removed, 54648745 resolutions, 201089580 steps
c blkd: 32317 blocking literals 17%, 1364 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 6 count, 0 units, 0 am1, 18784857 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 45680 subsumed
c card: 46504 at-most-one constraints found, average size 3.37
c card: 46504 at-most-one constraints used 100%, average size 3.37
c card: 382 at-most-two constraints found, average size 4.21
c card: 382 at-most-two constraints used 100%, average size 4.21
c cces: 7 cces, 1013 eliminated, 951 ate 94%, 62 abce 6%
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, 4026849 esteps, 5022380 csteps
c cgrs: 0 eqs, 1 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: 5139 extracted (5013 ands 98%, 0 xors 0%, 126 ites 2%)
c clff: 18 cliffs, 6575 lifted, 158 failed
c clff: 204213 decisions, 571049869 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 7094690 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 143 gcs, 0 rescored clauses, 375 rescored vars
c dcps: 31 decompositions, 5112 equivalent 5%
c deco: 29425 decision-only clauses 4%, 58% reduction
c decs: 26476336 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 213987 flipped 0.808% (in 406 phases)
c elms: 18 elims, 45391 eliminated 47%
c elms: 19 rounds, 1.1 rounds/bve
c elms: 15358 small 34%, 28669 large 63%
c elms: 26251 tried small, 15358 succeeded 59%, 10893 failed 41%
c elms: 74555 subsumed, 176857 strengthened, 221040 blocked
c elms: 52726539 copies, 72951191 resolutions, 669773 ipos
c elms: 239459388 subchks, 267727527 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 17 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10751906 steps, 5375953 extr 50%, 51 elim 0%
c glue: 26.9 orig avg, 26.0 real avg, 4.7 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 186788 = 59621 simple + 126963 trn 32% + 204 lrg 68%, 7270 sub 0%
c hght: 475 average, 17.63 height/glue
c ints: 21904 luby (5239001 steps), 0 inout (0 steps)
c lift: 18 phases, 145103 probed (48486 level1 33%, 96617 level2 67%)
c lift: 11044 units, 459 equivalences, 361 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 713704 clauses, 58.0 length
c lrnd: 337388 uips 47%, 256103 flips 36%
c mega: 0 count, 0 failed, 0 rounds
c mins: 41400216 learned lits, 17% minimized
c mins: 650905 mins 91%, 1215 bin 0%, 32159 size 5%, 29425 deco 4%
c move: moved 713704, 162839 bin 23%, 4640 trn 1%, 0 lrg 0%
c otfs: str 120287 dyn (117854 red, 2433 irr) 33846 drv 28%, 86441 rst 72%
c otfs: sub 426 dyn (401 red, 25 irr)
c phas: 6 computed, 83600 set, 6018 pos (7%), 77582 neg (93%)
c prbs: 4 basic, 44408 probed, 307 failed, 5 lifted
c prbs: 5 simple, 224062 probed, 1093 failed, 583 eqs
c prbs: 4 treelook, 9 probed, 0 failed, 0 lifted
c prps: 906559010 props, 29 props/dec
c prps: 85% srch, 15% simp, 0% lkhd
c psns: 18619197 searches, 3604378 hits, 19% 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: 56 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 56 arith 100%, 0 double 0%
c rmbd: 44453 removed, 24067 red 54%
c rphs: 8 recomputed phases
c rsts: 21053 restarts 96%, 851 skipped 4%
c rsts: 0 saturating 0%, 0 agile 0%, 851 reuse 100%
c rsts: 34.6 avg interval, 34.6 scaled, 1.0 factor
c rsts: 17486 kept 83.1% average 13.5%
c simp: 21 count (21 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 713704 count (1000817 tried 1.4), 59745 sub out of 705532 (8.5%)
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: 28455 fixed 30%, 45 its, 16612.22 confs/it
c trvs: 13215504229 traversals, 93% srch, 9% simp, 0% lkhd
c trvs: 15.9 search traversals per propagation, 16457.2 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 19 transitive reductions, 2015 removed, 18 failed
c trds: 24337 nodes, 117121 edges, 38020984 steps
c trim: 2520014 words, 9.6 MB
c trnr: 19 count, 696 bin, 83918 trn, 644389418 steps
c unhd: 11 count, 12 rounds, 30637155 steps
c unhd: 1682 non-trivial sccs of average size 2.0
c unhd: 586 units, 586 bin, 0 trn, 0 lrg
c unhd: 20 failed, 14 stamp, 0 lits, 2 bin, 1 trn, 0 lrg
c unhd: 44994 tauts, 434 bin 1%, 14739 trn 33%, 6299 lrg 14%
c unhd: 44994 tauts, 23522 stamp 52%, 20002 red 44%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 290860 str, 586 bin 0%, 13732 trn 5%, 276542 lrg 95%, 82851 red 28%
c vars: 17219 remaining 18% and 78958 removed 82% out of 96177
c vars: 28455 fixed 30%, 45391 eliminated 47%, 5112 equivalent 5%
c vsts: 8762338880 visits, 90% srch, 10% simp, 0% lkhd
c vsts: 10.1 search visits per propagation, 10500.2 per conflict
c wchs: 821555460 pushed, 78883986 enlarged, 219 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    705532 100    561688 100  25585633 100   6268269 100    497381 100
c 
c  0      14007   2         0   0   5225856  20    434904   7     20197   4 
c  1      14785   2         0   0   5884628  23    669824  11     30197   6 
c  2      66084   9     38983   7  10503794  41<  2569748  41    105927  21 
c  3     110940  16     96631  17   1486741   6    768140  12<    70130  14 
c  4     137421  19    119389  21   1117828   4    644960  10     74252  15<
c  5     133754  19<   117497  21<   646759   3    460070   7     63165  13 
c  6      96164  14     83804  15    360185   1    311701   5     54066  11 
c  7      61593   9     52868   9    180034   1    190697   3     36778   7 
c  8      37850   5     30799   5    103258   0    125454   2     26300   5 
c  9      15136   2     11686   2     39958   0     49368   1     10171   2 
c 10      11301   2      6969   1     25627   0     30208   0      5197   1 
c 11       6154   1      2885   1     10550   0     12602   0       977   0 
c 12        343   0       177   0       415   0       593   0        24   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             4.7           4.9           1.7           2.9           4.0
c std             2.1           1.8           1.5           2.0           2.3
c 
c  238.812  39% elim
c   39.791   7% cce
c   36.785   6% decide
c   30.840   5% block
c   22.178   4% gc
c   21.775   4% analysis
c   15.978   3% probe
c   13.582   2% lift
c   12.546   2% decomp
c   11.964   2% cliff
c   10.474   2% defrag
c    9.247   2% backward
c    6.118   1% bca
c    6.012   1% ternres
c    5.827   1% unhide
c    5.799   1% restart
c    4.665   1% card
c    3.393   1% cgrclsr
c    2.521   0% bump
c    1.859   0% mincls
c    1.562   0% gauss
c    1.283   0% transred
c    0.845   0% reduce
c    0.564   0% phase
c    0.094   0% tabularasa
c    0.033   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    7.057   1% probe simple     44%
c    4.109   1% probe basic      26%
c    4.812   1% probe tree-look  30%
c ==================================
c   18.724   3% preprocessing     5%
c  373.670  61% inprocessing     95%
c ==================================
c  392.394  64% simplifying
c  216.270  36% search
c ==================================
c  608.666 100% all
c 
c 26476336 decisions, 43499.0 decisions/sec
c 747550 conflicts, 1228.2 conflicts/sec
c 906559010 propagations, 1.5 megaprops/sec
c 608.7 seconds, 135.1 MB
c launch: done
