c launch: /data/cnf/sc2014/app/atco_enc1_opt1_03_56.cnf.bz2
c host: atom08
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/atco_enc1_opt1_03_56.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt1_03_56.cnf.bz2
c no embedded options
c found 'p cnf 43998 276198' header
c read 43998 variables, 276198 clauses, 955587 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 43569 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   43569   264249         0       0      0     0   0  0.0   0.0   14
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 8567 at-most-one constraints of average size 3.0
c [card-1] found 47 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 8614 out of 8614 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 10439 variables
c [simpleprobe-1] all 33559 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 5170 variables
c [simpleprobe-1] 18970 variables remain 67% (9419 retained)
c [simpleprobe-1] removed 5170 variables, found 7242 hbrs, 460 units
c [unhide-1] limit 116764 based on 233528 irredundant clauses
c [unhide-1-1] 1 units, 364 failed, 1800 tauts, 0 hbrs, 2408 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 27984 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 11880 variables 42% in round 1 in 26944356 steps
c [elim-1-1] backward subsumption/strengthening limit 53888712
c [elim-1-1] subsumed 588 and strengthened 214 clauses in 53888847 steps
c [elim-1-1] rescheduled 645 variables 2% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 388002 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 11880 = 42% variables out of 27984
c [phase-1] phase bias: 7785 positive 48%, 8319 negative 52%
c [simplification-1] removed 27342 variables 62.9% (16104 remain 37%)
c [simplification-1] removed 61517 irredundant clauses 23.3% (202732 remain 77%)
c [simplification-1] maximum reduction of 63% = max (63%, 23%)
c [simplification-1] large reduction 63% >= 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] 87256, max 221377, min4 64153 at 75%, min10 31730 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    3.2   16104   202732         6       5      1  1582   3 13.7 181.9   15
c R    3.2   16104   202732        21      18      3  1582   4  7.7 154.5   15
c R    3.2   16104   202732        61      50      6  1585   5  7.1 185.0   15
c R    3.2   16104   202732       165     137     12  1591   6  5.6 271.9   15
c R    3.3   16104   202732       411     344     30  1598   9  5.7 303.2   15
c R    3.4   16104   202732       985     830     43  1645   4  6.0 290.5   15
c 
c [simplification-2] limit of 1140 conflicts hit after 1140 conflicts
c [decomp-3] removed 378 variables
c [simpleprobe-2] 11112 schedulable variables 71%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 9 variables
c [simpleprobe-2] 11224 variables remain 71% (4493 retained)
c [simpleprobe-2] removed 9 variables, found 390 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19804 literals 63%
c [treelook-1] scheduling used 300024 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 342427 steps
c [treelook-1] 19742 literals remain 63%
c [treelook-1] 14551 variables remain to probed next time 93%
c [treelook-1] removed 0 variables, found 176 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6028 probes remain 38% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 2854 hbrs
c [unhide-2] limit 100878 based on 201757 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 1146 tauts, 0 hbrs, 1159 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 15716 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 21423 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 7 clauses out of 99 (7%) of length 14
c [cce-1-1] eliminated 2 clauses out of 110 (2%) of length 13
c [cce-1-1] eliminated 173 clauses out of 1319 (13%) of length 12
c [cce-1-1] eliminated 79 clauses out of 521 (15%) of length 11
c [cce-1-1] eliminated 20 clauses out of 563 (4%) of length 10
c [cce-1-1] eliminated 71 clauses out of 3119 (2%) of length 9
c [cce-1-1] eliminated 236 clauses out of 5928 (4%) of length 8
c [cce-1-1] eliminated 347 clauses out of 10492 (3%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 935 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 32641 clauses = 30339 binary + 2302 ternary
c [cce-1] tried to eliminate 32641 small clauses 100%
c [cce-1] eliminated 2832 small clauses 9%
c [cce-1] eliminated 2711 binary clauses 9%
c [cce-1] eliminated 121 ternary clauses 5%
c [cce-1-1] eliminated 2832 small clauses in 291564333 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 3767 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 4217834 steps for small clauses
c [cce-1] scheduling 29809 clauses = 27628 binary + 2181 ternary
c [cce-1] tried to eliminate 1167 small clauses 4%
c [cce-1-2] incomplete small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 3767 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 15716 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 1039 not tried 7% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1868 = 12% variables out of 15716
c [bca-1] limit of 10000000 steps
c [bca-1] 25235 out of 27698 literals actually usable 91%
c [bca-1] added 3439 blocked clauses in 103435 steps
c [phase-2] phase bias: 3 positive 50%, 3 negative 50%
c [simplification-2] removed 2256 variables 14.0% (13848 remain 32%)
c [simplification-2] removed 30414 irredundant clauses 15.0% (172318 remain 65%)
c [simplification-2] maximum reduction of 15% = max (14%, 15%)
c [simplification-2] large reduction 15% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 3140
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   13.2   13848   172318      2295    1725   2185 12923   7  7.4 242.2   14
c 
c [simplification-3] limit of 3216 conflicts hit after 3216 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 13848 free variables schedulable
c [ternres-1] 1709 ternary resolvents (0 bin, 1709 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3678 at-most-one constraints of average size 3.4
c [card-2] found 121 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3799 out of 3799 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 470 xors of average arity 2.6
c [gauss-1] connected 1208 occurrences of 671 variables (average 1.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-6] removed 112 variables
c [gauss-1] exported 0 unary, 1 binary and 4 ternary equations
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 13736 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 1 variables
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 8562 probes 62%
c [lift-1] 3 units, 8 impls, 8 eqs in 1 rounds
c [lift-1] 13638 variables remain 99% (86 retained)
c [lift-1] removed 11 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 212669 with penalty 0 = 0 + 0
c [transred-1] removed 220 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 13724 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 112 blocked clauses
c [block-2] 112 < 1/1000 * 172141 = 172 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 87 (1%) of length 14
c [cce-2-1] eliminated 4 clauses out of 1149 (0%) of length 12
c [cce-2-1] eliminated 21 clauses out of 654 (3%) of length 11
c [cce-2-1] eliminated 14 clauses out of 836 (2%) of length 10
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 40 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 28474 clauses = 24809 binary + 3665 ternary
c [cce-2] tried to eliminate 3254 small clauses 11%
c [cce-2] eliminated 124 small clauses 0%
c [cce-2] eliminated 82 binary clauses 0%
c [cce-2] eliminated 42 ternary clauses 1%
c [cce-2-1] eliminated 124 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 164 covered clauses in round 1
c [cce-2] eliminated 164 covered clauses in TOTAL during 1 rounds
c [cce-2] 164 < 1/1000 * 172029 = 172 considered unsuccessful
c [elim-3] 981 variables 7% will be scheduled this time
c [elim-3] scheduled 981 variables 7%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 727 not tried 5% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 29 = 0% variables out of 13724
c [bca-2] limit of 10000000 steps
c [bca-2] 22735 out of 27392 literals actually usable 83%
c [bca-2] added 36 blocked clauses in 90801 steps
c [phase-3] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-3] removed 153 variables 1.1% (13695 remain 31%)
c [simplification-3] removed 504 irredundant clauses 0.3% (171814 remain 65%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] new conflict limit 13216
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.8   13695   171814      5224    2461   3882 12769   6  7.7 225.3   15
c R   15.8   13695   171814      5229    2466   3882 12769   6  7.7 225.4   15
c -   16.4   13695   171814      8599    3114   3896 12843   5  7.6 203.0   15
c R   16.7   13695   171814     11762    6096   3910 12871   6  8.2 203.4   15
c -   16.9   13695   171814     12569    3866   3920 12878   4  8.2 198.9   15
c 
c [simplification-4] limit of 13526 conflicts hit after 13527 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 13695 free variables schedulable
c [ternres-2] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-2] 3426 variables remain 25% (10269 retained)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 346 xors of average arity 2.8
c [gauss-2] connected 965 occurrences of 584 variables (average 1.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 44 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 8461 literals 31%
c [treelook-2] scheduling used 151504 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 173421 steps
c [treelook-2] 8421 literals remain 31%
c [treelook-2] 6994 variables remain to probed next time 51%
c [treelook-2] removed 0 variables, found 33 hbrs
c [cgrclsr-2] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-2] all 13651 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cgrclsr-2] removed 4 variables
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 8398 probes 62%
c [lift-2] 3 units, 1 impls, 5 eqs in 1 rounds
c [lift-2] 13478 variables remain 99% (161 retained)
c [lift-2] removed 8 variables
c [unhide-3] limit 85827 based on 171654 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 279 tauts, 0 hbrs, 962 literals
c [transred-2] limit 832661 with penalty 0 = 0 + 0
c [transred-2] removed 676 transitive binary clauses
c [transred-2] found 2 units
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 13636 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 906 not tried 7% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 28 = 0% variables out of 13636
c [bca-3] limit of 10000000 steps
c [bca-3] 20953 out of 27218 literals actually usable 77%
c [bca-3] added 98 blocked clauses in 83312 steps
c [rephase-1] after 13527 conflicts (new increment 20000, next 33527)
c [flushphases] 5 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 87 variables 0.6% (13608 remain 31%)
c [simplification-4] removed 631 irredundant clauses 0.4% (171183 remain 65%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20000
c [simplification-4] penalized conflict interval 20000 = 1 * 20000
c [simplification-4] new conflict limit 33527
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   18.9   13608   171183     17057    4605   3528 12486   5  8.1 189.2   15
c -   19.8   13608   171183     22171    5507   3552 12524   6  8.1 184.4   15
c R   20.1   13608   171183     26062    9197   3554 12532   6  8.6 184.3   16
c -   20.4   13608   171183     27610    6171   3561 12546   4  8.6 182.1   15
c 
c [simplification-5] limit of 33753 conflicts hit after 33754 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 3406 schedulable variables 25%
c [ternres-3] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-10] removed 101 variables
c [basicprobe-2] limit 2100044 penalty 0 = 0 + 0
c [basicprobe-2-0] 2714 probes remain 20% after last round
c [basicprobe-2-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 4 variables, found 2749 hbrs
c [bate-1] eliminated 4 asymmetric tautologies during probing
c [cgrclsr-3] limit 210004 penalty 0 = 0 + 0
c [cgrclsr-3] all 13503 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 5 variables
c [lift-3] limit 1260026 with penalty 0 = 0 + 0
c [lift-3] using 8169 probes 61%
c [lift-3] 0 units, 4 impls, 18 eqs in 1 rounds
c [lift-3] 13104 variables remain 97% (376 retained)
c [lift-3] removed 18 variables
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1190 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 13480 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 4 blocked clauses
c [block-3] 4 < 1/1000 * 170838 = 170 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 19
c [cce-3-1] eliminated 5 clauses out of 7 (71%) of length 18
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 17
c [cce-3-1] eliminated 9 clauses out of 11 (82%) of length 16
c [cce-3-1] eliminated 40 clauses out of 70 (57%) of length 15
c [cce-3-1] eliminated 30 clauses out of 110 (27%) of length 14
c [cce-3-1] eliminated 46 clauses out of 133 (35%) of length 13
c [cce-3-1] eliminated 37 clauses out of 1262 (3%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 174 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 73214 clauses = 24629 binary + 48585 ternary
c [cce-3] tried to eliminate 1380 small clauses 2%
c [cce-3] eliminated 156 small clauses 0%
c [cce-3] eliminated 24 binary clauses 0%
c [cce-3] eliminated 132 ternary clauses 0%
c [cce-3-1] eliminated 156 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 330 covered clauses in round 1
c [cce-3] eliminated 330 covered clauses in TOTAL during 1 rounds
c [elim-5] 611 variables 5% will be scheduled this time
c [elim-5] scheduled 611 variables 5%
c [elim-5] limit of 42000889 steps penalty 0 = 0 + 0
c [elim-5] incomplete 324 not tried 2% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 10 = 0% variables out of 13480
c [elim-5] 10 < 1/1000 * 13480 = 13 considered unsuccessful
c [bca-4] limit of 10000000 steps
c [bca-4] 19307 out of 26942 literals actually usable 72%
c [bca-4] added 45 blocked clauses in 83957 steps
c [rephase-2] after 33754 conflicts (new increment 40000, next 73754)
c [flushphases] 4 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 138 variables 1.0% (13470 remain 31%)
c [simplification-5] removed 700 irredundant clauses 0.4% (170483 remain 65%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 30000
c [simplification-5] penalized conflict interval 30000 = 1 * 30000
c [simplification-5] new conflict limit 63754
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.3   13470   170483     33878    7116   3473 14087   5  8.6 177.0   15
c -   24.6   13470   170483     40611    8069   3501 14101   4  8.6 175.1   15
c -   26.0   13470   170483     47992    9236   3518 14120   6  8.7 170.5   15
c -   26.7   13470   170483     55593   10069   3530 14125  13  9.3 170.7   15
c R   26.8   13470   170483     57297   11703   3532 14125  14  9.4 170.8   16
c 
c [simplification-6] limit of 63848 conflicts hit after 63849 conflicts
c [ternres-4] limit 4094060 with penalty 0 = 0 + 0
c [ternres-4] all 13470 free variables schedulable
c [ternres-4] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-4] 4308 variables remain 32% (9162 retained)
c [card-3] limit 511757 penalty 2 = 2 + 0
c [card-3] found 3398 at-most-one constraints of average size 3.4
c [card-3] found 2 at-most-two constraints of average size 4.0
c [card-3] using previous limit 511757 for elimination
c [card-3] 3400 out of 3400 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 262 xors of average arity 2.4
c [gauss-3] connected 638 occurrences of 462 variables (average 1.4)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 142 variables
c [simpleprobe-3] 9497 schedulable variables 71%
c [simpleprobe-3] limit 16376241 penalty 0 = 0 + 0
c [decomp-12] removed 13 variables
c [simpleprobe-3] 6689 variables remain 50% (6626 retained)
c [simpleprobe-3] removed 13 variables, found 1490 hbrs, 0 units
c [cgrclsr-4] limit 409406 penalty 0 = 0 + 0
c [cgrclsr-4] all 13315 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-4] limit 2456436 with penalty 0 = 0 + 0
c [lift-4] using 7729 probes 58%
c [lift-4] 5 units, 6 impls, 7 eqs in 1 rounds
c [lift-4] 12569 variables remain 94% (734 retained)
c [lift-4] removed 12 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1304 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 15 clauses out of 85 (18%) of length 16
c [cce-4-1] eliminated 60 clauses out of 290 (21%) of length 14
c [cce-4-1] eliminated 24 clauses out of 1366 (2%) of length 12
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 99 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 72846 clauses = 24448 binary + 48398 ternary
c [cce-4] tried to eliminate 2672 small clauses 4%
c [cce-4] eliminated 313 small clauses 0%
c [cce-4] eliminated 55 binary clauses 0%
c [cce-4] eliminated 258 ternary clauses 1%
c [cce-4-1] eliminated 313 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 412 covered clauses in round 1
c [cce-4] eliminated 412 covered clauses in TOTAL during 1 rounds
c [bca-5] limit of 10000000 steps
c [bca-5] 18498 out of 26608 literals actually usable 70%
c [bca-5] added 41 blocked clauses in 87744 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 167 variables 1.2% (13303 remain 31%)
c [simplification-6] removed 806 irredundant clauses 0.5% (169677 remain 64%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-6] new conflict interval 45000
c [simplification-6] penalized conflict interval 45000 = 1 * 45000
c [simplification-6] new conflict limit 108849
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   30.0   13303   169677     63849   11012   3560 14618   4  9.5 165.6   11
c -   31.8   13303   169677     72834   12150   3574 14639   4  9.6 161.3   16
c -   33.4   13303   169677     82450   13390   3588 14649   4  9.8 158.2   16
c -   35.6   13303   169677     92573   14594   3610 14654   3  9.8 153.0   16
c -   37.7   13303   169677    103142   15705   3628 14659   4  9.9 149.1   16
c 
c [simplification-7] limit of 108933 conflicts hit after 108934 conflicts
c [ternres-5] limit 7570330 with penalty 0 = 0 + 0
c [ternres-5] 4259 schedulable variables 32%
c [ternres-5] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-13] removed 14 variables
c [lift-5] limit 4542198 with penalty 0 = 0 + 0
c [lift-5] using 7338 probes 55%
c [lift-5] 2 units, 12 impls, 11 eqs in 1 rounds
c [lift-5] 11881 variables remain 89% (1394 retained)
c [lift-5] removed 14 variables
c [unhide-4] limit 378516 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 864 tauts, 0 hbrs, 17240 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 455 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 32 clauses out of 1347 (2%) of length 12
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 32 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 72413 clauses = 24326 binary + 48087 ternary
c [cce-5] tried to eliminate 2781 small clauses 4%
c [cce-5] eliminated 284 small clauses 0%
c [cce-5] eliminated 52 binary clauses 0%
c [cce-5] eliminated 232 ternary clauses 0%
c [cce-5-1] eliminated 284 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 316 covered clauses in round 1
c [cce-5] eliminated 316 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 13275 variables 100%
c [elim-6] limit of 75703308 steps penalty 1 = 1 + 0
c [elim-6] incomplete 336 not tried 3% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 67 = 1% variables out of 13275
c [bca-6] limit of 10000000 steps
c [bca-6] 18779 out of 26418 literals actually usable 71%
c [bca-6] added 3 blocked clauses in 90409 steps
c [rephase-3] after 108934 conflicts (new increment 80000, next 188934)
c [flushphases] 0 phases reset
c [simplification-7] removed 95 variables 0.7% (13208 remain 30%)
c [simplification-7] removed 941 irredundant clauses 0.6% (168736 remain 64%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-7] new conflict interval 67500
c [simplification-7] penalized conflict interval 67500 = 1 * 67500
c [simplification-7] new conflict limit 176434
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   42.1   13208   168736    117021   16499   3647 13641  11 12.3 148.3   16
c R   42.6   13208   168736    124867   24008   3648 13641  10 12.6 148.5   17
c -   43.4   13208   168736    128120   17163   3657 13642   4 12.6 147.0   16
c -   45.9   13208   168736    140029   18145   3686 13647   4 12.4 143.2   16
c -   48.5   13208   168736    152796   19275   3708 13655   4 12.7 140.2   16
c -   51.4   13208   168736    165816   20255   3725 13655   3 12.7 136.6   25
c 
c [simplification-8] limit of 176472 conflicts hit after 176472 conflicts
c [ternres-6] limit 12859851 with penalty 0 = 0 + 0
c [ternres-6] all 13208 free variables schedulable
c [ternres-6] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-14] removed 12 variables
c [cgrclsr-5] limit 642992 penalty 1 = 1 + 0
c [cgrclsr-5] all 13196 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-6] limit 7715910 with penalty 0 = 0 + 0
c [lift-6] using 6601 probes 50%
c [lift-6] 3 units, 15 impls, 21 eqs in 1 rounds
c [lift-6] 10659 variables remain 81% (2513 retained)
c [lift-6] removed 24 variables
c [cliff-3] limit of 2571970 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 406 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 13172 variables 100%
c [block-4] limit of 32149628 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 2 blocked clauses
c [block-4] 2 < 1/1000 * 168631 = 168 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 28362 clauses = 24071 binary + 4291 ternary
c [cce-6] tried to eliminate 3039 small clauses 11%
c [cce-6] eliminated 317 small clauses 1%
c [cce-6] eliminated 160 binary clauses 1%
c [cce-6] eliminated 157 ternary clauses 4%
c [cce-6-1] eliminated 317 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 317 covered clauses in round 1
c [cce-6] eliminated 317 covered clauses in TOTAL during 1 rounds
c [elim-7] 298 variables 2% will be scheduled this time
c [elim-7] scheduled 298 variables 2%
c [elim-7] limit of 257197030 steps penalty 0 = 0 + 0
c [elim-7] incomplete 56 not tried 0% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 4 = 0% variables out of 13172
c [elim-7] 4 < 1/1000 * 13172 = 13 considered unsuccessful
c [bca-7] limit of 10000000 steps
c [bca-7] 18240 out of 26338 literals actually usable 69%
c [bca-7] added 3 blocked clauses in 99486 steps
c [simplification-8] removed 40 variables 0.3% (13168 remain 30%)
c [simplification-8] removed 890 irredundant clauses 0.5% (167846 remain 64%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 33750 = 67500 / 2
c [simplification-8] new conflict interval 101250
c [simplification-8] penalized conflict interval 101250 = 1 * 101250
c [simplification-8] new conflict limit 277722
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   58.1   13168   167846    180028   21262   3872 14099   8 12.7 135.0   17
c -   60.9   13168   167846    194131   22297   3877 14100   4 12.7 132.3   17
c 1   63.3   13168   167846    204993   32732   3885 14103   5 12.6 130.7   18
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s SATISFIABLE
c
c bate: 4 basic ate = 4 trn 100% + 0 lrg 0% in 1 updates
c bcas: 7 count, 3665 added (373 skipped), 639144 steps
c bkwd: tried 148069 clauses, 295346 lits, 1.99 lits/clause
c bkwd: checked 28819742 occs, 194.64 occs/clause, 97.58 occs/lit
c bkwd: subsumed 179 binary, 47 ternary, 362 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 214 large (0% self)
c blkd: 4 bces, 21541 removed, 3349345 resolutions, 10875601 steps
c blkd: 9797 blocking literals 11%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 3 count, 0 units, 0 am1, 4761850 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 35639 subsumed
c card: 15643 at-most-one constraints found, average size 3.17
c card: 15643 at-most-one constraints used 100%, average size 3.17
c card: 170 at-most-two constraints found, average size 4.00
c card: 170 at-most-two constraints used 100%, average size 4.00
c cces: 6 cces, 5306 eliminated, 4341 ate 82%, 965 abce 18%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 5 count, 1662424 esteps, 23141 csteps
c cgrs: 5 eqs, 0 units
c cgrs: 5 matched (5 ands 100%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 1122 extracted (969 ands 86%, 76 xors 7%, 77 ites 7%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 93765 decisions, 17572299 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1231785 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 107 rescored vars
c dcps: 14 decompositions, 15039 equivalent 34%
c deco: 1669 decision-only clauses 1%, 48% reduction
c decs: 1979231 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 80201 flipped 4.052% (in 563 phases)
c elms: 7 elims, 13886 eliminated 32%
c elms: 8 rounds, 1.1 rounds/bve
c elms: 10089 small 73%, 3797 large 27%
c elms: 12416 tried small, 10089 succeeded 81%, 2327 failed 19%
c elms: 7269 subsumed, 5675 strengthened, 1129 blocked
c elms: 2909537 copies, 3878513 resolutions, 226228 ipos
c elms: 5159706 subchks, 1435393 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 1078 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 1 binary and 4 ternary equations
c gaus: 0 gc, 10002734 steps, 5001367 extr 50%, 43470 elim 0%
c glue: 12.6 orig avg, 12.4 real avg, 2.9 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 17641 = 9122 simple + 8486 trn 52% + 33 lrg 48%, 569 sub 0%
c hght: 131 average, 10.35 height/glue
c ints: 7164 luby (1482105 steps), 0 inout (0 steps)
c lift: 6 phases, 15272 probed (5101 level1 33%, 10171 level2 67%)
c lift: 16 units, 70 equivalences, 46 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 203400 clauses, 24.7 length
c lrnd: 97092 uips 48%, 82473 flips 41%
c mega: 0 count, 0 failed, 0 rounds
c mins: 5023235 learned lits, 17% minimized
c mins: 195390 mins 96%, 488 bin 0%, 5853 size 3%, 1669 deco 1%
c move: moved 203400, 11993 bin 6%, 10112 trn 5%, 0 lrg 0%
c otfs: str 4147 dyn (3828 red, 319 irr) 1593 drv 38%, 2554 rst 62%
c otfs: sub 8 dyn (8 red, 0 irr)
c phas: 6 computed, 16111 set, 7788 pos (48%), 8323 neg (52%)
c prbs: 2 basic, 10163 probed, 4 failed, 0 lifted
c prbs: 3 simple, 66552 probed, 461 failed, 4285 eqs
c prbs: 2 treelook, 102 probed, 0 failed, 0 lifted
c prps: 103653469 props, 51 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c psns: 4114009 searches, 789423 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: 22 count, 0 reset, 5 acts 23%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 22 arith 100%, 0 double 0%
c rmbd: 5506 removed, 587 red 11%
c rphs: 3 recomputed phases
c rsts: 7110 restarts 99%, 54 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 54 reuse 100%
c rsts: 28.4 avg interval, 28.4 scaled, 1.0 factor
c rsts: 979 kept 13.8% average 18.5%
c simp: 8 count (8 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 203400 count (110390 tried 0.5), 6769 sub out of 202467 (3.3%)
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: 0 count
c tops: 1905 fixed 4%, 0 its, 0.00 confs/it
c trvs: 2560665678 traversals, 99% srch, 2% simp, 0% lkhd
c trvs: 25.2 search traversals per propagation, 12307.1 per conflict
c trvs: 1.7 search traversals per search visit
c trds: 6 transitive reductions, 4251 removed, 2 failed
c trds: 120517 nodes, 184243 edges, 6362917 steps
c trim: 106465 words, 0.4 MB
c trnr: 6 count, 0 bin, 1737 trn, 24636946 steps
c unhd: 4 count, 4 rounds, 5694453 steps
c unhd: 272 non-trivial sccs of average size 2.1
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 364 failed, 364 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 4089 tauts, 579 bin 14%, 740 trn 18%, 26 lrg 1%
c unhd: 4089 tauts, 2744 stamp 67%, 2908 red 71%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 21769 str, 1 bin 0%, 2925 trn 13%, 18843 lrg 87%, 18247 red 84%
c vars: 13168 remaining 30% and 30830 removed 70% out of 43998
c vars: 1905 fixed 4%, 13886 eliminated 32%, 15039 equivalent 34%
c vsts: 1558054149 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 15.2 search visits per propagation, 7416.1 per conflict
c wchs: 372922359 pushed, 17036024 enlarged, 84 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    202467 100    159249 100   2078586 100    858107 100     97569 100
c 
c  0      10494   5         0   0    980841  47    247968  29     31235  32 
c  1      15608   8      3166   2    448930  22<   133107  16     20480  21 
c  2      61916  31     55690  35    380301  18    204086  24<    24782  25<
c  3      52535  26<    47682  30<   149038   7    129981  15     10317  11 
c  4      37510  19     32981  21     70759   3     84538  10      5301   5 
c  5      13000   6     10931   7     23797   1     28575   3      1912   2 
c  6       5290   3      4224   3      9776   0     12613   1      1382   1 
c  7       2250   1      1839   1      4819   0      5879   1       917   1 
c  8        566   0       511   0      3518   0      2682   0       333   0 
c  9        758   0       670   0      2491   0      2713   0       374   0 
c 10       1581   1      1006   1      2612   0      3634   0       322   0 
c 11        959   0       549   0      1704   0      2331   0       214   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.0           3.2           1.1           1.9           1.6
c std             1.7           1.4           1.4           1.8           1.7
c 
c   12.564  20% cce
c    7.491  12% elim
c    2.382   4% analysis
c    2.100   3% decide
c    1.897   3% gc
c    1.629   3% backward
c    1.005   2% decomp
c    0.977   2% probe
c    0.942   1% lift
c    0.754   1% restart
c    0.738   1% block
c    0.719   1% defrag
c    0.558   1% transred
c    0.463   1% bca
c    0.450   1% unhide
c    0.446   1% cgrclsr
c    0.440   1% cliff
c    0.412   1% mincls
c    0.379   1% bump
c    0.290   0% gauss
c    0.184   0% ternres
c    0.167   0% card
c    0.141   0% phase
c    0.109   0% reduce
c    0.008   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    0.000   0% tabularasa
c ----------------------------------
c    0.606   1% probe simple     62%
c    0.121   0% probe basic      12%
c    0.250   0% probe tree-look  26%
c ==================================
c    3.165   5% preprocessing    12%
c   23.553  37% inprocessing     88%
c ==================================
c   26.718  42% simplifying
c   36.612  58% search
c ==================================
c   63.335 100% all
c 
c 1979231 decisions, 31250.3 decisions/sec
c 204993 conflicts, 3236.7 conflicts/sec
c 103653469 propagations, 1.6 megaprops/sec
c 63.3 seconds, 34.2 MB
c launch: done
