c launch: /data/cnf/sc2014/app/bjrb07amba10andenv.cnf.bz2
c host: atom11
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/bjrb07amba10andenv.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/bjrb07amba10andenv.cnf.bz2
c no embedded options
c found 'p cnf 196289 588610' header
c read 196289 variables, 588610 clauses, 1373422 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 196282 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  196282   588609         0       0      0     0   0  0.0   0.0   34
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 196282 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 12 variables
c [simpleprobe-1] 168151 variables remain 86% (28119 retained)
c [simpleprobe-1] removed 12 variables, found 117 hbrs, 0 units
c [unhide-1] limit 294285 based on 588571 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 196270 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 161741 variables 82% in round 1 in 534309774 steps
c [elim-1-1] backward subsumption/strengthening limit 265690226
c [elim-1-1] subsumed 2 and strengthened 68 clauses in 265705461 steps
c [elim-1] incomplete 115 not tried 0% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 161742 = 82% variables out of 196270
c [phase-1] phase bias: 2988 positive 9%, 31540 negative 91%
c [simplification-1] removed 161754 variables 82.4% (34528 remain 18%)
c [simplification-1] removed 335752 irredundant clauses 57.0% (252857 remain 43%)
c [simplification-1] maximum reduction of 82% = max (82%, 57%)
c [simplification-1] large reduction 82% >= 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] 246541, max 483404, min4 118191 at 75%, min10 51812 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c [tabula-rasa-1] number variables 34528 drops below limit 49070
c [tabula-rasa-1] number clauses 252857 drops below limit 294304
c [flush-cache] 0 binary, 0 ternary, 0 large
c [flushphases] 34528 phases reset fully
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] conflict limit 20000 does not change
c [tabula-rasa-1] new variable limit 8632 and clause limit 126428
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   23.7   34528   252857         5       2      3    36   7  2.8  13.2   28
c R   23.8   34528   252854        20      11      4    37  22  2.9  33.0   29
c R   23.8   34528   252845        62      30      6    40   8  3.1  47.2   29
c i   23.9   34527   252842       139      68     20    47  10  4.5  47.1   29
c i   23.9   34526   252842       141      68     20    47   8  4.5  46.9   29
c i   23.9   34525   252842       145      68     21    48   8  4.4  46.8   29
c i   24.0   34524   252842       152      69     23    49   8  4.3  46.2   29
c i   24.0   34523   252842       154      69     23    50   6  4.2  46.1   29
c i   24.0   34522   252842       159      70     23    50   5  4.1  45.8   29
c R   24.0   34522   252842       164      75     23    50   4  4.3  45.6   29
c R   24.2   34522   252818       418     211     43    51  11  8.9  39.7   29
c R   24.6   34522   252758       996     509     96    78  13  8.6  35.7   29
c 
c [simplification-2] limit of 1177 conflicts hit after 1177 conflicts
c [decomp-3] removed 22 variables
c [simpleprobe-2] 29686 schedulable variables 86%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 26586 variables remain 77% (7920 retained)
c [simpleprobe-2] removed 0 variables, found 5 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24594 literals 36%
c [treelook-1] scheduling used 300012 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 1241166 steps
c [treelook-1] 24591 literals remain 36%
c [treelook-1] 23608 variables remain to probed next time 68%
c [treelook-1] removed 0 variables, found 487 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 29217 probes remain 85% after last round
c [basicprobe-1-0] removed 0 variables, found 1455 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 34506 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 161 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 122 = 0% variables out of 34506
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-2] removed 138 variables 0.4% (34384 remain 18%)
c [simplification-2] removed 292 irredundant clauses 0.1% (252442 remain 43%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 40000
c [simplification-2] penalized conflict interval 40000 = 1 * 40000
c [simplification-2] new conflict limit 41177
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   27.0   34384   252378      2311    1149    179  2012   7  9.2  33.0   29
c R   28.5   34384   252280      5296    3084    313  2082  12 11.4  30.9   30
c -   29.7   34384   252232      7714    2698    459  2153   9 12.0  29.6   29
c R   30.8   34384   252092     11831    5450    642  2252   9 11.8  28.1   30
c -   31.7   34384   251983     13123    3707    738  2293   9 11.5  27.9   30
c -   34.5   34384   251792     19500    4736   1070  2470   9 11.1  26.5   30
c -   36.5   34384   251641     26040    5760   1346  2590   9 11.4  25.8   30
c R   36.6   34384   251639     26189    5885   1351  2591  11 11.4  25.8   30
c -   40.4   34384   251537     34013    6776   1660  2776   8 11.5  25.1   30
c -   43.8   34384   251362     42366    7895   1935  2951   7 11.6  24.9   30
c 
c [simplification-3] limit of 42679 conflicts hit after 42679 conflicts
c [card-2] limit 1209385 penalty 1 = 1 + 0
c [card-2] found 44 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1209385 for elimination
c [card-2] 44 out of 44 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 340 variables
c [unhide-2] limit 483754 with penalty 1 = 1 + 0
c [unhide-2-2] 1 units, 0 failed, 174 tauts, 0 hbrs, 8606 literals
c [elim-3] 136 variables 0% will be scheduled this time
c [elim-3] scheduled 136 variables 0%
c [elim-3] limit of 96750861 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 151 variables 0% in round 1 in 14807961 steps
c [elim-3-1] backward subsumption/strengthening limit 29615922
c [elim-3-1] subsumed 5 and strengthened 1 clauses in 29626918 steps
c [elim-3-1] rescheduled 10 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 71399 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 151 = 0% variables out of 34043
c [rephase-1] after 42679 conflicts (new increment 20000, next 62679)
c [flushphases] 0 phases reset
c [simplification-3] removed 492 variables 1.4% (33892 remain 17%)
c [simplification-3] removed 2127 irredundant clauses 0.8% (249233 remain 42%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 20000 = 40000 / 2
c [simplification-3] new conflict interval 60000
c [simplification-3] penalized conflict interval 60000 = 1 * 60000
c [simplification-3] new conflict limit 102679
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   48.5   33892   249021     51236    8517   1869  2703  12 11.6  24.6   30
c R   50.5   33892   248926     57475   13220   1999  2754   9 11.9  24.8   31
c -   51.6   33892   248892     60316    9521   2102  2814  10 11.9  24.5   30
c -   56.0   33892   248692     71744   10751   2469  3004  10 11.8  24.1   30
c -   60.0   33892   248593     82889   12149   2694  3126  17 12.0  23.8   30
c -   65.9   33892   248446     96146   13352   3122  3452  15 12.0  23.4   31
c 
c [simplification-4] limit of 104145 conflicts hit after 104145 conflicts
c [decomp-7] removed 344 variables
c [treelook-2] limit 285525 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 21928 literals 33%
c [treelook-2] scheduling used 286841 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 285525 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 1555157 steps
c [treelook-2] 21909 literals remain 33%
c [treelook-2] 21062 variables remain to probed next time 63%
c [decomp-8] removed 1 variables
c [treelook-2] removed 1 variables, found 339 hbrs
c [unhide-3] limit 2284204 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 6883 tauts, 0 hbrs, 4082 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 33547 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1142102450 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1941 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 2 clauses out of 15 (13%) of length 20
c [cce-1-1] eliminated 1 clauses out of 19 (5%) of length 19
c [cce-1-1] eliminated 3 clauses out of 24 (12%) of length 18
c [cce-1-1] eliminated 3 clauses out of 65 (5%) of length 17
c [cce-1-1] eliminated 12 clauses out of 108 (11%) of length 16
c [cce-1-1] eliminated 22 clauses out of 174 (13%) of length 15
c [cce-1-1] eliminated 34 clauses out of 298 (11%) of length 14
c [cce-1-1] eliminated 65 clauses out of 511 (13%) of length 13
c [cce-1-1] eliminated 31 clauses out of 791 (4%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 173 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 63406 clauses = 39823 binary + 23583 ternary
c [cce-1] tried to eliminate 4925 small clauses 8%
c [cce-1] eliminated 55 small clauses 0%
c [cce-1] eliminated 23 binary clauses 0%
c [cce-1] eliminated 32 ternary clauses 0%
c [cce-1-1] eliminated 55 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 228 covered clauses in round 1
c [cce-1] eliminated 228 covered clauses in TOTAL during 1 rounds
c [cce-1] 228 < 1/1000 * 239909 = 239 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 33413 variables 100%
c [elim-4] limit of 228420491 steps penalty 0 = 0 + 0
c [elim-4-1] eliminated 1613 variables 5% in round 1 in 55156869 steps
c [elim-4-1] backward subsumption/strengthening limit 110313738
c [elim-4-1] subsumed 1 and strengthened 6 clauses in 110337338 steps
c [elim-4-1] rescheduled 15 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 8257 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1614 = 5% variables out of 33413
c [bca-1] limit of 10000000 steps
c [bca-1] 47481 out of 63600 literals actually usable 75%
c [bca-1] added 50 blocked clauses in 188253 steps
c [rephase-2] after 104145 conflicts (new increment 40000, next 144145)
c [flushphases] 0 phases reset
c [simplification-4] removed 2093 variables 6.2% (31799 remain 16%)
c [simplification-4] removed 13773 irredundant clauses 5.5% (234571 remain 40%)
c [simplification-4] maximum reduction of 6% = max (6%, 6%)
c [simplification-4] large reduction 6% >= 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 106145
c 
c [simplification-5] limit of 106215 conflicts hit after 106215 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 57966450 with penalty 0 = 0 + 0
c [ternres-1] all 31799 free variables schedulable
c [ternres-1] 43030 ternary resolvents (318 bin, 42712 trn)
c [ternres-1] 43 variables remain 0% (31756 retained)
c [gauss-1] limit 2318658 penalty 0 = 0 + 0
c [gauss-1] extracted 169 xors of average arity 2.1
c [gauss-1] connected 348 occurrences of 134 variables (average 2.6)
c [gauss-1] limit 2318658 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 61 variables
c [cgrclsr-1] limit 1159329 penalty 0 = 0 + 0
c [cgrclsr-1] all 31738 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 26 variables
c [lift-1] limit 6955974 with penalty 0 = 0 + 0
c [lift-1] using 27307 probes 86%
c [lift-1] 5 units, 15 impls, 3 eqs in 1 rounds
c [lift-1] 31523 variables remain 99% (181 retained)
c [lift-1] removed 8 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 82 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 31704 variables 100%
c [block-2] limit of 115932909 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 31704 variables 100%
c [elim-5] limit of 231865818 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 32 variables 0% in round 1 in 67644577 steps
c [elim-5-1] backward subsumption/strengthening limit 135289154
c [elim-5-1] subsumed 0 and strengthened 5 clauses in 135302871 steps
c [elim-5-1] rescheduled 14 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 5903 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 32 = 0% variables out of 31704
c [bca-2] limit of 10000000 steps
c [bca-2] 46942 out of 63346 literals actually usable 74%
c [bca-2] added 1 blocked clauses in 191292 steps
c [simplification-5] removed 127 variables 0.4% (31672 remain 16%)
c [simplification-5] removed 713 irredundant clauses 0.3% (233844 remain 40%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 60000
c [simplification-5] new conflict interval 120000
c [simplification-5] penalized conflict interval 120000 = 1 * 120000
c [simplification-5] new conflict limit 226215
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   98.5   31672   233830    110824   13958  45589 10834  10 12.1  23.2   33
c -  103.4   31672   233792    124113   15446  45831 10965  16 12.4  23.1   33
c R  103.7   31672   233792    125238   16392  45839 10967  16 12.4  23.1   33
c -  109.8   31672   233691    138692   16730  46145 11095   9 12.4  22.8   33
c -  116.6   31672   233603    153402   18172  46449 11234  13 12.5  22.8   33
c -  124.1   31672   233457    168629   19588  46814 11401  12 12.5  22.7   33
c -  131.0   31672   233395    186908   21063  47115 11544  13 12.3  22.3   33
c -  140.2   31672   233257    205492   22747  47554 11764  11 12.2  22.1   34
c -  147.9   31672   233172    223823   24095  47813 11911   8 12.2  21.9   34
c 
c [simplification-6] limit of 227799 conflicts hit after 227800 conflicts
c [ternres-2] limit 28313877 with penalty 0 = 0 + 0
c [ternres-2] 43 schedulable variables 0%
c [ternres-2] 6489 ternary resolvents (64 bin, 6425 trn)
c [ternres-2] 25 variables remain 0% (31647 retained)
c [card-3] limit 3539234 penalty 2 = 2 + 0
c [card-3] found 89 at-most-one constraints of average size 3.0
c [card-3] found 29 at-most-two constraints of average size 4.0
c [card-3] using previous limit 3539234 for elimination
c [card-3] 118 out of 118 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 315 variables
c [basicprobe-2] limit 14156938 penalty 1 = 1 + 0
c [basicprobe-2-0] 23941 probes remain 76% after last round
c [basicprobe-2-0] removed 0 variables, found 10921 hbrs
c [bate-1] eliminated 73 asymmetric tautologies during probing
c [cgrclsr-2] limit 2831387 penalty 0 = 0 + 0
c [cgrclsr-2] all 31357 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 119 variables
c [lift-2] limit 16988326 with penalty 0 = 0 + 0
c [lift-2] using 26991 probes 86%
c [lift-2] 0 units, 25 impls, 18 eqs in 1 rounds
c [lift-2] 30628 variables remain 98% (592 retained)
c [lift-2] removed 18 variables
c [unhide-4] limit 2831387 with penalty 1 = 1 + 0
c [unhide-4-5] 0 units, 3 failed, 4751 tauts, 0 hbrs, 6583 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 8 transitive binary clauses
c [cce-2] limit of 28313877 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-2-1] eliminated 1 clauses out of 22 (5%) of length 20
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 3 large clauses in 28313878 steps
c [cce-2-1] allowing another 14156939 steps for small clauses
c [cce-2] scheduling 59036 clauses = 37523 binary + 21513 ternary
c [cce-2] tried to eliminate 526 small clauses 1%
c [cce-2] eliminated 7 small clauses 0%
c [cce-2] eliminated 6 binary clauses 0%
c [cce-2] eliminated 1 ternary clauses 0%
c [cce-2-1] eliminated 7 small clauses in 28313878 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 10 covered clauses in round 1
c [cce-2] eliminated 10 covered clauses in TOTAL during 1 rounds
c [cce-2] 10 < 1/1000 * 231925 = 231 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 31219 variables 100%
c [elim-6] limit of 566277545 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 399 variables 1% in round 1 in 185318254 steps
c [elim-6-1] backward subsumption/strengthening limit 370636508
c [elim-6-1] subsumed 0 and strengthened 11 clauses in 370637856 steps
c [elim-6-1] rescheduled 19 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 1301495 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 399 = 1% variables out of 31219
c [bca-3] limit of 10000000 steps
c [bca-3] 39278 out of 61642 literals actually usable 64%
c [bca-3] added 66 blocked clauses in 161161 steps
c [rephase-3] after 227800 conflicts (new increment 80000, next 307800)
c [flushphases] 0 phases reset
c [simplification-6] removed 852 variables 2.7% (30820 remain 16%)
c [simplification-6] removed 4243 irredundant clauses 1.8% (228903 remain 39%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 30000 = 120000 / 4
c [simplification-6] new conflict interval 150000
c [simplification-6] penalized conflict interval 150000 = 1 * 150000
c [simplification-6] new conflict limit 377800
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  173.9   30820   228865    243160   24205  49651 19806  11 12.2  21.8   34
c -  180.5   30820   228783    261696   25734  49921 19930  15 12.1  21.6   34
c R  184.6   30820   228763    270841   32773  50091 19983  13 12.0  21.5   35
c -  190.2   30820   228716    280785   27387  50278 20066  11 12.1  21.5   34
c -  200.5   30820   228629    302066   29105  50621 20194  13 12.1  21.4   34
c -  211.2   30820   228563    323139   30733  51017 20349  12 12.1  21.3   34
c -  223.2   30820   228476    347010   32725  51469 20556  11 12.0  21.2   34
c -  235.4   30820   228405    369896   34507  51806 20667  12 12.0  21.1   35
c 
c [simplification-7] limit of 379246 conflicts hit after 379246 conflicts
c [ternres-3] limit 51404435 with penalty 0 = 0 + 0
c [ternres-3] 24 schedulable variables 0%
c [ternres-3] 13452 ternary resolvents (71 bin, 13381 trn)
c [ternres-3] 21 variables remain 0% (30799 retained)
c [gauss-2] limit 5140443 penalty 1 = 1 + 0
c [gauss-2] extracted 1455 xors of average arity 2.0
c [gauss-2] connected 2940 occurrences of 843 variables (average 3.5)
c [gauss-2] limit 5140443 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-11] removed 400 variables
c [gauss-2] exported 0 unary, 9 binary and 0 ternary equations
c [decomp-12] removed 1 variables
c [cgrclsr-3] limit 5140443 penalty 0 = 0 + 0
c [cgrclsr-3] all 30419 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 459 variables
c [lift-3] limit 20000000 with penalty 0 = 0 + 0
c [lift-3] using 25671 probes 86%
c [lift-3] 1 units, 29 impls, 9 eqs in 1 rounds
c [lift-3] 28915 variables remain 97% (1035 retained)
c [lift-3] removed 10 variables
c [cliff-2] limit of 20561774 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [unhide-5] limit 10280887 with penalty 0 = 0 + 0
c [unhide-5-10] 0 units, 0 failed, 9993 tauts, 0 hbrs, 9012 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 34 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 29950 variables 100%
c [block-3] limit of 257022178 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 804 blocked clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 29932 variables 100%
c [elim-7] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 502 variables 2% in round 1 in 188240794 steps
c [elim-7-1] backward subsumption/strengthening limit 376481588
c [elim-7-1] subsumed 0 and strengthened 13 clauses in 376498672 steps
c [elim-7-1] rescheduled 26 variables 0% by backward subsumption
c [elim-7-2] no variable eliminated in round 2 in 5929016 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 502 = 2% variables out of 29932
c [bca-4] limit of 10000000 steps
c [bca-4] 30520 out of 58862 literals actually usable 52%
c [bca-4] added 58 blocked clauses in 144631 steps
c [rephase-4] after 379246 conflicts (new increment 160000, next 539246)
c [flushphases] 0 phases reset
c [simplification-7] removed 1390 variables 4.5% (29430 remain 15%)
c [simplification-7] removed 7099 irredundant clauses 3.1% (221284 remain 38%)
c [simplification-7] maximum reduction of 5% = max (5%, 3%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] new conflict interval 3792 = min (379246/100, 150000)
c [simplification-7] penalized conflict interval 3792 = 1 * 3792
c [simplification-7] new conflict limit 383038
c 
c [simplification-8] limit of 383052 conflicts hit after 383052 conflicts
c [ternres-4] limit 51951234 with penalty 0 = 0 + 0
c [ternres-4] 20 schedulable variables 0%
c [ternres-4] 9718 ternary resolvents (74 bin, 9644 trn)
c [ternres-4] 7 variables remain 0% (29423 retained)
c [gauss-3] limit 10390246 penalty 0 = 0 + 0
c [gauss-3] extracted 696 xors of average arity 2.1
c [gauss-3] connected 1428 occurrences of 339 variables (average 4.2)
c [gauss-3] limit 10390246 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 141 variables
c [simpleprobe-3] 22591 schedulable variables 77%
c [simpleprobe-3] limit 100000000 penalty 1 = 1 + 0
c [decomp-14] removed 17 variables
c [simpleprobe-3] 21181 variables remain 72% (8091 retained)
c [simpleprobe-3] removed 17 variables, found 467 hbrs, 0 units
c [cgrclsr-4] limit 5195123 penalty 0 = 0 + 0
c [cgrclsr-4] all 29272 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [cgrclsr-4] removed 259 variables
c [lift-4] limit 20000000 with penalty 0 = 0 + 0
c [lift-4] using 24377 probes 84%
c [lift-4] 4 units, 34 impls, 8 eqs in 1 rounds
c [lift-4] 27482 variables remain 95% (1519 retained)
c [lift-4] removed 12 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 331 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 29001 variables 100%
c [block-4] limit of 519512346 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 29001 variables 100%
c [elim-8] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 15 variables 0% in round 1 in 334702469 steps
c [elim-8-1] backward subsumption/strengthening limit 465297531
c [elim-8-1] subsumed 0 and strengthened 15 clauses in 465320104 steps
c [elim-8] incomplete 23 not tried 0% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 15 = 0% variables out of 29001
c [elim-8] 15 < 1/1000 * 29001 = 29 considered unsuccessful
c [bca-5] limit of 10000000 steps
c [bca-5] 29533 out of 57974 literals actually usable 51%
c [bca-5] added 1 blocked clauses in 144203 steps
c [simplification-8] removed 444 variables 1.5% (28986 remain 15%)
c [simplification-8] removed 1921 irredundant clauses 0.9% (219363 remain 37%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 50000 = 150000 / 3
c [simplification-8] new conflict interval 200000
c [simplification-8] penalized conflict interval 200000 = 1 * 200000
c [simplification-8] new conflict limit 583052
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  284.5   28986   219336    394899   34055  63846 26650   8 12.0  21.0   36
c -  297.2   28986   219284    419750   35720  64247 26804   9 12.1  21.0   36
c -  308.8   28986   219251    446047   37112  64574 26907  10 12.0  20.8   36
c -  322.5   28986   219159    471559   38949  64919 27085   8 12.0  20.7   36
c -  335.7   28986   219091    498234   40558  65204 27204  11 12.0  20.6   36
c -  347.3   28986   219072    525103   42203  65534 27319  13 12.1  20.7   36
c -  357.4   28986   219039    550105   43528  65767 27408  13 12.1  20.6   36
c -  369.2   28986   218990    579360   45431  66067 27521  12 12.1  20.5   36
c 
c [simplification-9] limit of 584252 conflicts hit after 584252 conflicts
c [ternres-5] limit 82351988 with penalty 0 = 0 + 0
c [ternres-5] 7 schedulable variables 0%
c [ternres-5] 27351 ternary resolvents (37 bin, 27314 trn)
c [ternres-5] 6 variables remain 0% (28980 retained)
c [decomp-15] removed 243 variables
c [treelook-3] limit 4117599 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 48175 literals 84%
c [treelook-3] scheduling used 1054149 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 4117599 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 4299142 steps
c [treelook-3] 47928 literals remain 83%
c [treelook-3] 18572 variables remain to probed next time 65%
c [decomp-16] removed 4 variables
c [treelook-3] removed 4 variables, found 1113 hbrs
c [cgrclsr-5] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-5] all 28739 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [cgrclsr-5] removed 450 variables
c [lift-5] limit 20000000 with penalty 0 = 0 + 0
c [lift-5] using 23477 probes 83%
c [lift-5] 0 units, 30 impls, 4 eqs in 1 rounds
c [lift-5] 26421 variables remain 93% (1864 retained)
c [lift-5] removed 4 variables
c [unhide-6] limit 8235198 with penalty 1 = 1 + 0
c [unhide-6-14] 0 units, 0 failed, 6191 tauts, 0 hbrs, 7701 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 147 transitive binary clauses
c [cce-3] limit of 41175994 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 31 (3%) of length 20
c [cce-3-1] eliminated 1 clauses out of 45 (2%) of length 19
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2 large clauses in 41175995 steps
c [cce-3-1] allowing another 20587997 steps for small clauses
c [cce-3] scheduling 53200 clauses = 33361 binary + 19839 ternary
c [cce-3] tried to eliminate 342 small clauses 1%
c [cce-3] eliminated 8 small clauses 0%
c [cce-3] eliminated 5 binary clauses 0%
c [cce-3] eliminated 3 ternary clauses 0%
c [cce-3-1] eliminated 8 small clauses in 41175995 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 10 covered clauses in round 1
c [cce-3] eliminated 10 covered clauses in TOTAL during 1 rounds
c [cce-3] 10 < 1/1000 * 217579 = 217 considered unsuccessful
c [bca-6] limit of 10000000 steps
c [bca-6] 24117 out of 56572 literals actually usable 43%
c [bca-6] added 8 blocked clauses in 128896 steps
c [rephase-5] after 584252 conflicts (new increment 320000, next 904252)
c [flushphases] 0 phases reset
c [simplification-9] removed 701 variables 2.4% (28285 remain 14%)
c [simplification-9] removed 1404 irredundant clauses 0.6% (217569 remain 37%)
c [simplification-9] maximum reduction of 2% = max (2%, 1%)
c [simplification-9] geometric conflict interval increment 66666 = 200000 / 3
c [simplification-9] new conflict interval 266666
c [simplification-9] penalized conflict interval 266666 = 1 * 266666
c [simplification-9] new conflict limit 850918
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  390.3   28285   217526    612797   45617  88964 25525  12 12.0  20.4   38
c -  405.0   28285   217484    646406   47538  89406 25679  11 11.9  20.1   38
c -  419.2   28285   217427    679553   49964  89841 25818  11 11.7  19.9   39
c i  427.8   28284   217401    697189   60730  90028 25885  10 11.6  19.8   40
c -  436.3   28242   217381    714142   51865  90170 25939  14 11.6  19.7   39
c -  455.2   28242   217335    750544   53878  90634 26090  19 11.5  19.6   39
c -  475.2   28242   217307    788878   55803  91075 26239  15 11.4  19.4   39
c -  494.6   28242   217285    824784   57621  91438 26387  16 11.4  19.2   39
c 
c [simplification-10] limit of 852380 conflicts hit after 852383 conflicts
c [ternres-6] limit 129389601 with penalty 0 = 0 + 0
c [ternres-6] 6 schedulable variables 0%
c [ternres-6] 12001 ternary resolvents (72 bin, 11929 trn)
c [ternres-6] 2 variables remain 0% (28240 retained)
c [card-4] limit 8086850 penalty 3 = 3 + 0
c [card-4] found 239 at-most-one constraints of average size 3.0
c [card-4] found 65 at-most-two constraints of average size 4.0
c [card-4] using previous limit 8086850 for elimination
c [card-4] 304 out of 304 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-4] limit 12938960 penalty 1 = 1 + 0
c [gauss-4] extracted 1640 xors of average arity 2.0
c [gauss-4] connected 3316 occurrences of 808 variables (average 4.1)
c [gauss-4] limit 12938960 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 365 variables
c [cgrclsr-6] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-6] all 27877 free variables schedulable
c [cgrclsr-6] fully completed congruence closure
c [cgrclsr-6] removed 325 variables
c [lift-6] limit 20000000 with penalty 0 = 0 + 0
c [lift-6] using 22749 probes 83%
c [lift-6] 0 units, 29 impls, 31 eqs in 1 rounds
c [lift-6] 25307 variables remain 92% (2214 retained)
c [lift-6] removed 31 variables
c [cliff-3] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 353 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 27521 variables 100%
c [block-5] limit of 400000000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 7644 blocked clauses
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 27246 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] incomplete 33 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 3348 = 12% variables out of 27246
c [bca-7] limit of 10000000 steps
c [bca-7] 16901 out of 47798 literals actually usable 35%
c [bca-7] added 64 blocked clauses in 117495 steps
c [simplification-10] removed 4344 variables 15.4% (23898 remain 12%)
c [simplification-10] removed 28751 irredundant clauses 13.2% (188526 remain 32%)
c [simplification-10] maximum reduction of 15% = max (15%, 13%)
c [simplification-10] large reduction 15% >= 5% limit
c [simplification-10] new conflict interval 8523 = min (852383/100, 266666)
c [simplification-10] penalized conflict interval 8523 = 1 * 8523
c [simplification-10] new conflict limit 860906
c 
c [simplification-11] limit of 860936 conflicts hit after 860938 conflicts
c [ternres-7] limit 130851029 with penalty 0 = 0 + 0
c [ternres-7] 2 schedulable variables 0%
c [ternres-7] 9822 ternary resolvents (49 bin, 9773 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-18] removed 27 variables
c [cgrclsr-7] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-7] all 23871 free variables schedulable
c [cgrclsr-7] fully completed congruence closure
c [cgrclsr-7] removed 206 variables
c [lift-7] limit 20000000 with penalty 0 = 0 + 0
c [lift-7] using 19178 probes 81%
c [lift-7] 0 units, 20 impls, 6 eqs in 1 rounds
c [lift-7] 21365 variables remain 90% (2294 retained)
c [lift-7] removed 6 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 467 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 23659 variables 100%
c [block-6] limit of 800000000 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [elim-10] 30 variables 0% will be scheduled this time
c [elim-10] scheduled 30 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 6 variables 0% in round 1 in 747679374 steps
c [elim-10-1] backward subsumption/strengthening limit 52320626
c [elim-10-1] subsumed 4 and strengthened 0 clauses in 52331451 steps
c [elim-10] incomplete 5 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 6 = 0% variables out of 23659
c [elim-10] 6 < 1/1000 * 23659 = 23 considered unsuccessful
c [bca-8] limit of 10000000 steps
c [bca-8] 16180 out of 47308 literals actually usable 34%
c [bca-8] added 0 blocked clauses in 120280 steps
c [simplification-11] removed 245 variables 1.0% (23653 remain 12%)
c [simplification-11] removed 818 irredundant clauses 0.4% (187707 remain 32%)
c [simplification-11] maximum reduction of 1% = max (1%, 0%)
c [simplification-11] geometric conflict interval increment 133333 = 266666 / 2
c [simplification-11] new conflict interval 399999
c [simplification-11] penalized conflict interval 399999 = 1 * 399999
c [simplification-11] new conflict limit 1260937
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  539.0   23653   187695    873647   54427  86477 29411  14 11.3  19.1   38
c -  551.1   23653   187676    902442   55657  86606 29426  13 11.3  19.2   37
c -  564.5   23653   187641    937001   57252  86864 29504  12 11.3  19.1   37
c i  578.4   23652   187630    971428   79223  87221 29607  11 11.2  19.0   41
c -  581.5   22593   187626    978158   59317  87285 29645  13 11.2  19.0   38
c i  590.5   22592   187618   1000757   73342  87533 29738  11 11.1  18.8   40
c -  599.6   22578   187611   1020518   61710  87742 29828  13 11.0  18.8   39
c i  602.9   22577   187608   1028477   66674  87858 29868  10 11.0  18.7   39
c i  605.4   22171   187603   1035064   70647  87985 29900  11 11.0  18.7   41
c i  607.1   22151   187591   1038353   72673  88024 29926  14 11.0  18.7   41
c i  607.1   20942   187591   1038463   72717  88036 29931  12 11.0  18.7   41
c i  607.1   20570   187591   1038464   72717  88036 29931  12 11.0  18.7   41
c 0  607.1   20351   187591   1038464   72717  88036 29931  12 11.0  18.7   41
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 73 basic ate = 21 trn 29% + 52 lrg 71% in 1 updates
c bcas: 8 count, 248 added (51 skipped), 1196211 steps
c bkwd: tried 109711 clauses, 219304 lits, 2.00 lits/clause
c bkwd: checked 1041208169 occs, 9490.46 occs/clause, 4747.78 occs/lit
c bkwd: subsumed 4 binary, 6 ternary, 2 large
c bkwd: strengthened 0 binary, 18 ternary (100% self), 101 large (0% self)
c blkd: 6 bces, 10389 removed, 8860675 resolutions, 44529870 steps
c blkd: 3781 blocking literals 1%, 427 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 17423425 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1065 subsumed
c card: 372 at-most-one constraints found, average size 3.00
c card: 372 at-most-one constraints used 100%, average size 3.00
c card: 94 at-most-two constraints found, average size 4.00
c card: 94 at-most-two constraints used 100%, average size 4.00
c cces: 3 cces, 248 eliminated, 243 ate 98%, 5 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 7 count, 38327992 esteps, 28002500 csteps
c cgrs: 139 eqs, 0 units
c cgrs: 1667 matched (1618 ands 97%, 0 xors 0%, 49 ites 3%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 80340 extracted (73596 ands 92%, 39 xors 0%, 6705 ites 8%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 12466 decisions, 55617177 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1962032 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 56 gcs, 0 rescored clauses, 532 rescored vars
c dcps: 18 decompositions, 4210 equivalent 2%
c deco: 335 decision-only clauses 0%, 57% reduction
c decs: 2252226 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 20285 flipped 0.901% (in 331 phases)
c elms: 10 elims, 168355 eliminated 86%
c elms: 18 rounds, 1.8 rounds/bve
c elms: 157310 small 93%, 10618 large 6%
c elms: 166365 tried small, 157310 succeeded 95%, 9055 failed 5%
c elms: 20165 subsumed, 10255 strengthened, 5635 blocked
c elms: 8375642 copies, 15465591 resolutions, 2384978 ipos
c elms: 16854738 subchks, 15468621 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 3960 extracted, 2.0 size, 3 max
c gaus: exported 0 units, 9 binary and 0 ternary equations
c gaus: 0 gc, 51955740 steps, 25977870 extr 50%, 393358 elim 1%
c glue: 11.0 orig avg, 11.0 real avg, 3.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 53490 = 589 simple + 51871 trn 1% + 1030 lrg 97%, 1883 sub 2%
c hght: 19 average, 1.70 height/glue
c ints: 30843 luby (7885209 steps), 0 inout (0 steps)
c lift: 7 phases, 16636 probed (5590 level1 34%, 11046 level2 66%)
c lift: 10 units, 79 equivalences, 182 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1012880 clauses, 15.5 length
c lrnd: 343268 uips 34%, 489055 flips 48%
c mega: 0 count, 0 failed, 0 rounds
c mins: 15655825 learned lits, 35% minimized
c mins: 966136 mins 95%, 2882 bin 0%, 43527 size 4%, 335 deco 0%
c move: moved 1012880, 1119 bin 0%, 3853 trn 0%, 0 lrg 0%
c otfs: str 55211 dyn (41732 red, 13479 irr) 25584 drv 46%, 29627 rst 54%
c otfs: sub 10256 dyn (6131 red, 4125 irr)
c phas: 3 computed, 34528 set, 2988 pos (9%), 31540 neg (91%)
c prbs: 2 basic, 3758 probed, 0 failed, 0 lifted
c prbs: 3 simple, 188227 probed, 0 failed, 28 eqs
c prbs: 3 treelook, 269 probed, 0 failed, 0 lifted
c prps: 1454840753 props, 641 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c psns: 20640072 searches, 530090 hits, 3% 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: 46 count, 0 reset, 2 acts 4%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 46 arith 100%, 0 double 0%
c rmbd: 17033 removed, 13548 red 80%
c rphs: 5 recomputed phases
c rsts: 14649 restarts 47%, 16194 skipped 53%
c rsts: 13276 saturating 82%, 29 agile 0%, 2889 reuse 18%
c rsts: 69.7 avg interval, 69.7 scaled, 1.0 factor
c rsts: 13912 kept 95.0% average 58.2%
c simp: 11 count (11 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 1012880 count (703121 tried 0.7), 277649 sub out of 992734 (28.0%)
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: 3367 fixed 2%, 14 its, 74176.00 confs/it
c trvs: 26247763486 traversals, 99% srch, 1% simp, 0% lkhd
c trvs: 18.0 search traversals per propagation, 25087.0 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 7 transitive reductions, 1422 removed, 0 failed
c trds: 54551 nodes, 33963 edges, 14002095 steps
c trim: 1216989 words, 4.6 MB
c trnr: 7 count, 685 bin, 121178 trn, 532228618 steps
c unhd: 6 count, 14 rounds, 34292482 steps
c unhd: 998 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 27992 tauts, 26 bin 0%, 15231 trn 54%, 6686 lrg 24%
c unhd: 27992 tauts, 6049 stamp 22%, 20729 red 74%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 35984 str, 1 bin 0%, 2646 trn 7%, 33337 lrg 93%, 27569 red 77%
c vars: 20357 remaining 10% and 175932 removed 90% out of 196289
c vars: 3367 fixed 2%, 168355 eliminated 86%, 4210 equivalent 2%
c vsts: 16174684456 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 11.1 search visits per propagation, 15387.1 per conflict
c wchs: 2755172126 pushed, 44597076 enlarged, 142 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    992734 100    609349 100  54588481 100   4428870 100    349424 100
c 
c  0      56174   6         0   0  42766246  78<   793165  18     63848  18 
c  1      33565   3     23814   4   7770424  14    525937  12     40327  12 
c  2     133538  13     73169  12   2083327   4    894377  20<    74477  21<
c  3     402021  40<   263431  43<  1237398   2   1281023  29    102647  29 
c  4     317175  32    211121  35    644334   1    817941  18     60552  17 
c  5      49099   5     36977   6     84988   0    113960   3      7414   2 
c  6       1077   0       800   0      1649   0      2295   0       149   0 
c  7         79   0        35   0       105   0       160   0         9   0 
c  8          6   0         2   0        10   0        12   0         1   0 
c  9          0   0         0   0         0   0         0   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.1           3.3           0.3           2.3           2.2
c std             1.1           0.9           0.8           1.4           1.4
c 
c   89.989  15% elim
c   51.990   9% backward
c   38.090   6% analysis
c   16.081   3% cce
c    5.924   1% lift
c    4.330   1% cgrclsr
c    4.154   1% gc
c    4.116   1% probe
c    3.455   1% ternres
c    3.156   1% mincls
c    2.674   0% unhide
c    2.620   0% decomp
c    2.369   0% block
c    2.276   0% defrag
c    2.261   0% decide
c    2.060   0% bump
c    1.954   0% restart
c    1.821   0% cliff
c    1.365   0% gauss
c    1.282   0% transred
c    1.062   0% bca
c    0.780   0% card
c    0.418   0% reduce
c    0.096   0% phase
c    0.036   0% tabularasa
c    0.015   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c    2.398   0% probe simple     58%
c    0.839   0% probe basic      20%
c    0.878   0% probe tree-look  21%
c ==================================
c   23.693   4% preprocessing    17%
c  113.987  19% inprocessing     83%
c ==================================
c  137.681  23% simplifying
c  469.455  77% search
c ==================================
c  607.139 100% all
c 
c 2252226 decisions, 3709.6 decisions/sec
c 1038464 conflicts, 1710.4 conflicts/sec
c 1454840753 propagations, 2.4 megaprops/sec
c 607.1 seconds, 79.5 MB
c launch: done
