c launch: /data/cnf/sc2014/app/atco_enc2_opt2_05_4.cnf.bz2
c host: atom09
c Lingeling SAT Solver
c 
c Version ayv 86bf266b9332599f1b876e28a02fe8427aeaa2db
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat Oct 11 12:11:52 CEST 2014
c compiled Sat Oct 11 12:11:52 CEST 2014
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNDBLSCR  -I../yalsat -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT
c -DNLGLDRUPLIG
c Linux cluster2 3.13.0-36-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc2_opt2_05_4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_05_4.cnf.bz2
c no embedded options
c found 'p cnf 14636 386147' header
c read 14636 variables, 386147 clauses, 1652660 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 14409 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   14409   371028         0       0      0     0   0  0.0   0.0   23
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 3123 at-most-one constraints of average size 3.0
c [card-1] found 64 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3187 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1111 variables
c [simpleprobe-1] all 13525 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 258 variables
c [simpleprobe-1] 11184 variables remain 84% (2083 retained)
c [simpleprobe-1] removed 258 variables, found 1963 hbrs, 7 units
c [unhide-1] limit 181229 based on 362458 irredundant clauses
c [unhide-1-1] 57 units, 20 failed, 4914 tauts, 0 hbrs, 63 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13192 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 3562 variables 27% in round 1 in 19299978 steps
c [elim-1-1] backward subsumption/strengthening limit 38599956
c [elim-1-1] subsumed 1537 and strengthened 73 clauses in 38600011 steps
c [elim-1-1] rescheduled 307 variables 2% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 125913 steps
c [elim-1-2] backward subsumption/strengthening limit 251826
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 252521 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 3564 = 27% variables out of 13192
c [phase-1] phase bias: 4656 positive 48%, 4972 negative 52%
c [simplification-1] removed 4536 variables 32.0% (9628 remain 67%)
c [simplification-1] removed 25852 irredundant clauses 7.0% (345176 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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] 191106, max 546194, min4 96861 at 75%, min10 9862 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    2.3    9628   345176         5       2      0   880   1 12.0 397.3   24
c R    2.3    9628   345176        20      15      1   880   3  8.6 334.1   24
c R    2.3    9628   345176        62      50      3   885   4  6.3 301.8   24
c R    2.3    9628   345176       167     139      5   891   5  6.8 267.8   24
c R    2.3    9628   345176       420     341     14   914   6  7.2 207.0   24
c R    2.4    9628   345176       997     862     22   933   8  8.4 158.3   24
c 
c [simplification-2] limit of 1135 conflicts hit after 1137 conflicts
c [decomp-3] removed 12 variables
c [simpleprobe-2] 8164 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 8183 variables remain 85% (1433 retained)
c [simpleprobe-2] removed 0 variables, found 118 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6911 literals 36%
c [treelook-1] scheduling used 301174 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302916 steps
c [treelook-1] 6889 literals remain 36%
c [treelook-1] 5660 variables remain to probed next time 59%
c [treelook-1] removed 1 variables, found 146 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1418 probes remain 15% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5 variables, found 1693 hbrs
c [unhide-2] limit 172571 based on 345143 irredundant clauses
c [unhide-2-2] 1 units, 59 failed, 578 tauts, 0 hbrs, 1737 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9598 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 1048 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 265 clauses out of 1021 (26%) of length 12
c [cce-1-1] eliminated 107 clauses out of 159 (67%) of length 11
c [cce-1-1] eliminated 58 clauses out of 508 (11%) of length 10
c [cce-1-1] eliminated 112 clauses out of 1581 (7%) of length 9
c [cce-1-1] eliminated 475 clauses out of 3659 (13%) of length 8
c [cce-1-1] eliminated 13 clauses out of 7550 (0%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1030 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 23681 clauses = 19942 binary + 3739 ternary
c [cce-1] tried to eliminate 9970 small clauses 42%
c [cce-1] eliminated 1026 small clauses 4%
c [cce-1] eliminated 895 binary clauses 4%
c [cce-1] eliminated 131 ternary clauses 4%
c [cce-1-1] eliminated 1026 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2056 covered clauses in round 1
c [cce-1] eliminated 2056 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 9598 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 2467 not tried 26% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 160 = 2% variables out of 9598
c [bca-1] limit of 10000000 steps
c [bca-1] 17731 out of 18878 literals actually usable 94%
c [bca-1] added 811 blocked clauses in 43420 steps
c [phase-2] phase bias: 31 positive 44%, 40 negative 56%
c [simplification-2] removed 190 variables 2.0% (9438 remain 66%)
c [simplification-2] removed 4484 irredundant clauses 1.3% (340692 remain 92%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] new conflict limit 7803
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   11.7    9438   340692      2319    1924   1039  3480   9  8.5 111.2   23
c -   11.9    9438   340692      4866    2203   1080  3568   8  8.8  79.5   23
c R   11.9    9438   340692      5259    2532   1082  3573   8  9.3  78.5   23
c 
c [simplification-3] limit of 8257 conflicts hit after 8257 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 9438 free variables schedulable
c [ternres-1] 1143 ternary resolvents (1 bin, 1142 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1361 at-most-one constraints of average size 3.1
c [card-2] found 357 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1718 out of 1718 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 144 xors of average arity 2.7
c [gauss-1] connected 382 occurrences of 300 variables (average 1.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 54 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6579 literals 35%
c [treelook-2] scheduling used 300090 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 319626 steps
c [treelook-2] 6561 literals remain 35%
c [treelook-2] 4119 variables remain to probed next time 44%
c [treelook-2] removed 0 variables, found 28 hbrs
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 9384 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 8773 probes 93%
c [lift-1] 1 units, 3 impls, 1 eqs in 1 rounds
c [lift-1] 9324 variables remain 99% (54 retained)
c [lift-1] removed 6 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-3] limit 170305 based on 340611 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 654 tauts, 0 hbrs, 5765 literals
c [transred-1] limit 339641 based on 339641 irredundant clauses
c [transred-1] removed 541 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 9375 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 6 blocked clauses
c [block-2] 6 < 1/1000 * 339523 = 339 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 14
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-2-1] eliminated 39 clauses out of 932 (4%) of length 12
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 45 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 22551 clauses = 18139 binary + 4412 ternary
c [cce-2] tried to eliminate 966 small clauses 4%
c [cce-2] eliminated 114 small clauses 1%
c [cce-2] eliminated 77 binary clauses 0%
c [cce-2] eliminated 37 ternary clauses 1%
c [cce-2-1] eliminated 114 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 159 covered clauses in round 1
c [cce-2] eliminated 159 covered clauses in TOTAL during 1 rounds
c [cce-2] 159 < 1/1000 * 339484 = 339 considered unsuccessful
c [elim-3] 2420 variables 26% will be scheduled this time
c [elim-3] scheduled 2420 variables 26%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 1502 not tried 16% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9375
c [bca-2] limit of 10000000 steps
c [bca-2] 16589 out of 18752 literals actually usable 88%
c [bca-2] added 83 blocked clauses in 43694 steps
c [phase-3] phase bias: 19 positive 51%, 18 negative 49%
c [simplification-3] removed 63 variables 0.7% (9375 remain 65%)
c [simplification-3] removed 1679 irredundant clauses 0.5% (339013 remain 91%)
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 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] new conflict limit 24923
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.3    9375   339013      8297    2785   2252  3853   7  9.2  64.4   23
c R   15.6    9375   339013     11827    5987   2262  3881   8  9.6  60.7   24
c -   15.6    9375   339013     12282    3404   2262  3889   7  9.6  59.5   24
c -   16.0    9375   339013     16876    4103   2295  3938   9 10.1  53.4   24
c -   16.5    9375   339013     21914    4813   2322  3977   8 10.1  49.5   24
c 
c [simplification-4] limit of 25197 conflicts hit after 25197 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 9375 free variables schedulable
c [ternres-2] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-2] 6516 variables remain 70% (2859 retained)
c [decomp-8] removed 33 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 1004 probes remain 11% after last round
c [basicprobe-2-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1 variables, found 1037 hbrs
c [bate-1] eliminated 8 asymmetric tautologies during probing
c [lift-2] limit 521665 with penalty 0 = 0 + 0
c [lift-2] using 8683 probes 93%
c [lift-2] 2 units, 0 impls, 1 eqs in 1 rounds
c [lift-2] 9221 variables remain 99% (117 retained)
c [lift-2] removed 3 variables
c [unhide-4] limit 173888 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 2 failed, 788 tauts, 0 hbrs, 20519 literals
c [transred-2] limit 869442 with penalty 0 = 0 + 0
c [transred-2] removed 613 transitive binary clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 16177 out of 18676 literals actually usable 87%
c [bca-3] added 41 blocked clauses in 45034 steps
c [rephase-1] after 25197 conflicts (new increment 20000, next 45197)
c [flushphases] 901 phases reset
c [phase-4] phase bias: 3 positive 50%, 3 negative 50%
c [simplification-4] removed 38 variables 0.4% (9337 remain 65%)
c [simplification-4] removed 234 irredundant clauses 0.1% (338779 remain 91%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 36666
c [simplification-4] penalized conflict interval 36666 = 1 * 36666
c [simplification-4] new conflict limit 61863
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   17.6    9337   338779     26224    8672   2298  3876   8 11.1  51.3   25
c -   17.8    9337   338779     27514    5386   2302  3886   7 11.0  50.3   24
c -   18.4    9337   338779     33637    6066   2317  3915   7 10.8  48.9   24
c -   19.0    9337   338779     40325    6794   2328  3932   7 10.7  46.2   24
c -   19.8    9337   338779     47517    7458   2359  3958   8 10.5  46.0   24
c -   20.4    9337   338779     55507    8146   2367  3967   8 10.4  45.2   24
c R   20.5    9337   338779     57558    9976   2373  3968   8 10.3  44.9   25
c 
c [simplification-5] limit of 62059 conflicts hit after 62060 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 6494 schedulable variables 70%
c [ternres-3] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-3] 3744 variables remain 40% (5593 retained)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 101 xors of average arity 2.6
c [gauss-2] connected 263 occurrences of 210 variables (average 1.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 93 variables
c [cgrclsr-2] limit 169343 based on 338686 irredundant clauses
c [cgrclsr-2] all 9244 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 1335394 with penalty 0 = 0 + 0
c [lift-3] using 8525 probes 92%
c [lift-3] 1 units, 6 impls, 2 eqs in 1 rounds
c [lift-3] 8966 variables remain 97% (275 retained)
c [lift-3] removed 3 variables
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [unhide-5] limit 445131 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 200 tauts, 0 hbrs, 19771 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 373 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 9241 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 9 blocked clauses
c [block-3] 9 < 1/1000 * 338528 = 338 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 104696 clauses = 17868 binary + 86828 ternary
c [cce-3] tried to eliminate 491 small clauses 0%
c [cce-3] eliminated 69 small clauses 0%
c [cce-3] eliminated 8 binary clauses 0%
c [cce-3] eliminated 61 ternary clauses 0%
c [cce-3-1] eliminated 69 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 69 covered clauses in round 1
c [cce-3] eliminated 69 covered clauses in TOTAL during 1 rounds
c [cce-3] 69 < 1/1000 * 338519 = 338 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9241 variables 100%
c [elim-4] limit of 22256578 steps penalty 1 = 1 + 0
c [elim-4] incomplete 2093 not tried 23% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 66 = 1% variables out of 9241
c [bca-4] limit of 10000000 steps
c [bca-4] 15936 out of 18352 literals actually usable 87%
c [bca-4] added 94 blocked clauses in 48254 steps
c [rephase-2] after 62060 conflicts (new increment 40000, next 102060)
c [flushphases] 530 phases reset
c [phase-5] phase bias: 1 positive 33%, 2 negative 67%
c [simplification-5] removed 162 variables 1.7% (9175 remain 64%)
c [simplification-5] removed 522 irredundant clauses 0.2% (338257 remain 91%)
c [simplification-5] maximum reduction of 2% = max (2%, 0%)
c [simplification-5] geometric conflict interval increment 12222 = 36666 / 3
c [simplification-5] new conflict interval 48888
c [simplification-5] penalized conflict interval 48888 = 1 * 48888
c [simplification-5] new conflict limit 110948
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.9    9175   338257     67120    8786   2415  4045   7 10.3  43.1   24
c -   24.8    9175   338257     76023    9449   2436  4061   7 10.2  42.0   24
c -   25.8    9175   338257     85539   10197   2449  4079   7 10.4  42.8   24
c -   27.0    9175   338257     95555   10963   2489  4133   7 10.4  44.3   25
c -   28.3    9175   338257    105980   11681   2518  4157   7 10.4  44.5   25
c 
c [simplification-6] limit of 111260 conflicts hit after 111260 conflicts
c [ternres-4] limit 4531888 with penalty 0 = 0 + 0
c [ternres-4] 3674 schedulable variables 40%
c [ternres-4] 37 ternary resolvents (0 bin, 37 trn)
c [ternres-4] 784 variables remain 9% (8391 retained)
c [card-3] limit 566486 penalty 2 = 2 + 0
c [card-3] found 1237 at-most-one constraints of average size 3.1
c [card-3] found 139 at-most-two constraints of average size 4.0
c [card-3] using previous limit 566486 for elimination
c [card-3] 1376 out of 1376 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 37 variables
c [simpleprobe-3] 7780 schedulable variables 85%
c [simpleprobe-3] limit 9063776 penalty 1 = 1 + 0
c [decomp-11] removed 1 variables
c [simpleprobe-3] 6641 variables remain 73% (2496 retained)
c [simpleprobe-3] removed 1 variables, found 481 hbrs, 0 units
c [lift-4] limit 2719133 with penalty 0 = 0 + 0
c [lift-4] using 8260 probes 90%
c [lift-4] 8 units, 7 impls, 4 eqs in 1 rounds
c [lift-4] 8533 variables remain 94% (592 retained)
c [lift-4] removed 12 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 842 transitive binary clauses
c [elim-5] 1340 variables 15% will be scheduled this time
c [elim-5] scheduled 1340 variables 15%
c [elim-5] limit of 90637769 steps penalty 0 = 0 + 0
c [elim-5] incomplete 747 not tried 8% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 7 = 0% variables out of 9125
c [elim-5] 7 < 1/1000 * 9125 = 9 considered unsuccessful
c [bca-5] limit of 10000000 steps
c [bca-5] 14324 out of 18238 literals actually usable 79%
c [bca-5] added 5 blocked clauses in 48641 steps
c [rephase-3] after 111260 conflicts (new increment 80000, next 191260)
c [flushphases] 36 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 57 variables 0.6% (9118 remain 63%)
c [simplification-6] removed 402 irredundant clauses 0.1% (337855 remain 91%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 24444 = 48888 / 2
c [simplification-6] new conflict interval 73332
c [simplification-6] penalized conflict interval 73332 = 1 * 73332
c [simplification-6] new conflict limit 184592
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   31.3    9118   337855    117216   12425   2573  4540   7 10.5  47.3   25
c R   32.0    9118   337855    125444   19909   2585  4562   8 10.6  47.9   27
c -   32.5    9118   337855    128999   13223   2592  4565   7 10.5  47.3   25
c -   33.9    9118   337855    141212   14003   2615  4584   7 10.4  47.0   25
c -   35.4    9118   337855    154036   14906   2637  4606   7 10.4  46.7   25
c -   37.2    9118   337855    167556   15922   2650  4620   6 10.3  45.8   25
c -   38.9    9118   337855    181652   16892   2670  4639   7 10.5  46.8   25
c 
c [simplification-7] limit of 184802 conflicts hit after 184802 conflicts
c [ternres-5] limit 8328126 with penalty 0 = 0 + 0
c [ternres-5] 778 schedulable variables 9%
c [ternres-5] 52 ternary resolvents (1 bin, 51 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-12] removed 30 variables
c [lift-5] limit 4996876 with penalty 0 = 0 + 0
c [lift-5] using 7892 probes 87%
c [lift-5] 9 units, 12 impls, 6 eqs in 1 rounds
c [lift-5] 7834 variables remain 86% (1230 retained)
c [lift-5] removed 24 variables
c [unhide-6] limit 832812 with penalty 1 = 1 + 0
c [unhide-6-6] 0 units, 0 failed, 781 tauts, 0 hbrs, 30736 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 305 transitive binary clauses
c [bca-6] limit of 10000000 steps
c [bca-6] 14314 out of 18130 literals actually usable 79%
c [bca-6] added 22 blocked clauses in 52026 steps
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 54 variables 0.6% (9064 remain 63%)
c [simplification-7] removed 259 irredundant clauses 0.1% (337596 remain 91%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 36666 = 73332 / 2
c [simplification-7] new conflict interval 109998
c [simplification-7] penalized conflict interval 109998 = 1 * 109998
c [simplification-7] new conflict limit 294800
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   41.9    9064   337596    196100   17784   2726  4377   6 10.5  47.1   26
c -   43.9    9064   337596    211532   18999   2741  4388   7 10.4  46.6   26
c -   46.5    9064   337596    227431   20100   2789  4410   6 10.3  46.8   26
c -   49.0    9064   337596    243897   20974   2817  4429   5 10.7  48.5   26
c -   51.7    9064   337596    261646   21842   2846  4441   8 11.6  50.2   26
c R   53.3    9064   337596    271383   29924   2863  4447   6 12.4  51.0   29
c -   54.9    9064   337596    279685   22620   2886  4455   6 12.3  50.9   43
c 
c [simplification-8] limit of 295032 conflicts hit after 295032 conflicts
c [ternres-6] limit 17522717 with penalty 0 = 0 + 0
c [ternres-6] all 9064 free variables schedulable
c [ternres-6] 130 ternary resolvents (8 bin, 122 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 876135 penalty 2 = 2 + 0
c [gauss-3] extracted 58 xors of average arity 2.8
c [gauss-3] connected 165 occurrences of 148 variables (average 1.1)
c [gauss-3] limit 876135 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 22 variables
c [treelook-3] limit 438067 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 8560 literals 47%
c [treelook-3] scheduling used 443648 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 438067 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 442126 steps
c [treelook-3] 8551 literals remain 47%
c [treelook-3] 3575 variables remain to probed next time 40%
c [treelook-3] removed 0 variables, found 76 hbrs
c [cgrclsr-3] limit 438067 penalty 2 = 2 + 0
c [cgrclsr-3] all 9042 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-6] limit 10513630 with penalty 0 = 0 + 0
c [lift-6] using 7215 probes 80%
c [lift-6] 10 units, 28 impls, 9 eqs in 1 rounds
c [lift-6] 6593 variables remain 73% (2424 retained)
c [lift-6] removed 25 variables
c [cliff-3] limit of 3504543 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 612 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 9017 variables 100%
c [block-4] limit of 43806792 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 21 blocked clauses
c [block-4] 21 < 1/1000 * 337350 = 337 considered unsuccessful
c [cce-4] limit of 8761358 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 4380679 steps for small clauses
c [cce-4] scheduling 25292 clauses = 17800 binary + 7492 ternary
c [cce-4] tried to eliminate 214 small clauses 1%
c [cce-4] eliminated 34 small clauses 0%
c [cce-4] eliminated 13 binary clauses 0%
c [cce-4] eliminated 21 ternary clauses 0%
c [cce-4-1] eliminated 34 small clauses in 8761359 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 34 covered clauses in round 1
c [cce-4] eliminated 34 covered clauses in TOTAL during 1 rounds
c [cce-4] 34 < 1/1000 * 337329 = 337 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 9017 variables 100%
c [elim-6] limit of 175227170 steps penalty 1 = 1 + 0
c [elim-6] incomplete 686 not tried 8% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 42 = 0% variables out of 9017
c [bca-7] limit of 10000000 steps
c [bca-7] 13240 out of 17952 literals actually usable 74%
c [bca-7] added 1 blocked clauses in 64204 steps
c [rephase-4] after 295032 conflicts (new increment 160000, next 455032)
c [flushphases] 0 phases reset
c [simplification-8] removed 89 variables 1.0% (8975 remain 62%)
c [simplification-8] removed 455 irredundant clauses 0.1% (337141 remain 91%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 54999 = 109998 / 2
c [simplification-8] new conflict interval 164997
c [simplification-8] penalized conflict interval 164997 = 1 * 164997
c [simplification-8] new conflict limit 460029
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   62.7    8975   337141    299982   23645   2989  5372   6 12.2  51.5   27
c -   66.9    8975   337141    318972   25117   3042  5396   7 12.1  51.6   27
c -   71.0    8975   337141    338146   26353   3108  5424   6 12.0  52.4   26
c -   76.2    8975   337141    358206   27810   3188  5451   6 11.9  52.7   27
c -   82.8    8975   337141    379134   29438   3283  5495   7 11.9  53.1   27
c -   87.9    8975   337141    401740   30377   3313  5511   7 12.4  53.4   45
c -   95.1    8975   337141    423283   31858   3395  5539   5 12.3  53.3   44
c -  102.9    8975   337141    445303   33278   3498  5565   5 12.2  53.0   44
c 
c [simplification-9] limit of 460401 conflicts hit after 460401 conflicts
c [ternres-7] limit 38345850 with penalty 0 = 0 + 0
c [ternres-7] all 8975 free variables schedulable
c [ternres-7] 624 ternary resolvents (28 bin, 596 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-15] removed 42 variables
c [basicprobe-3] limit 38345850 penalty 0 = 0 + 0
c [basicprobe-3-0] 933 sched 10%, 35 failed, 0 lifted, 2103 hbrs
c [decomp-16] removed 41 variables
c [basicprobe-3-1] 1387 sched 16%, 29 failed, 0 lifted, 1107 hbrs
c [decomp-17] removed 50 variables
c [basicprobe-3-2] 1399 sched 16%, 19 failed, 0 lifted, 220 hbrs
c [decomp-18] removed 40 variables
c [basicprobe-3-3] 1408 sched 16%, 8 failed, 0 lifted, 59 hbrs
c [decomp-19] removed 18 variables
c [basicprobe-3-4] 1408 sched 16%, 3 failed, 0 lifted, 239 hbrs
c [decomp-20] removed 9 variables
c [basicprobe-3-5] 1404 sched 16%, 1 failed, 0 lifted, 36 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-6] 540 probes remain 6% after last round
c [basicprobe-3-6] 95 units = 95 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 159 variables, found 3774 hbrs
c [bate-2] eliminated 518 asymmetric tautologies during probing
c [lift-7] limit 20000000 with penalty 0 = 0 + 0
c [lift-7] using 5803 probes 66%
c [lift-7] 1 units, 54 impls, 3 eqs in 1 rounds
c [lift-7] 4130 variables remain 47% (4640 retained)
c [lift-7] removed 4 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1615 transitive binary clauses
c [elim-7] 611 variables 7% will be scheduled this time
c [elim-7] scheduled 611 variables 7%
c [elim-7] limit of 766917014 steps penalty 0 = 0 + 0
c [elim-7] incomplete 112 not tried 1% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 48 = 1% variables out of 8770
c [bca-8] limit of 10000000 steps
c [bca-8] 12539 out of 17446 literals actually usable 72%
c [bca-8] added 47 blocked clauses in 73143 steps
c [rephase-5] after 460401 conflicts (new increment 320000, next 780401)
c [flushphases] 0 phases reset
c [simplification-9] removed 253 variables 2.8% (8722 remain 61%)
c [simplification-9] removed 10580 irredundant clauses 3.1% (326561 remain 88%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 41249 = 164997 / 4
c [simplification-9] new conflict interval 206246
c [simplification-9] penalized conflict interval 206246 = 1 * 206246
c [simplification-9] new conflict limit 666647
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  120.7    8722   326561    469107   33681   3515  7732   5 12.3  52.7   28
c -  129.2    8722   326561    492047   34908   3578  7743   5 12.3  52.2   28
c -  135.9    8722   326561    515520   36153   3614  7747   6 12.3  51.8   27
c -  142.8    8722   326561    539955   37238   3622  7750   4 12.4  51.4   27
c -  148.0    8722   326561    564475   38307   3631  7750   4 12.5  50.9   27
c R  152.3    8722   326561    583564   55931   3637  7750   5 12.5  50.5   31
c -  155.1    8722   326561    589355   39401   3645  7753   5 12.5  50.3   27
c -  166.5    8722   326561    614895   40978   3683  7761   4 12.4  49.5   45
c -  177.0    8722   326561    641122   42346   3713  7768   4 12.3  48.7   45
c 
c [simplification-10] limit of 666709 conflicts hit after 666709 conflicts
c [ternres-8] limit 71099805 with penalty 0 = 0 + 0
c [ternres-8] all 8722 free variables schedulable
c [ternres-8] 12493 ternary resolvents (213 bin, 12280 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4443737 penalty 3 = 3 + 0
c [card-4] found 1239 at-most-one constraints of average size 3.1
c [card-4] found 114 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4443737 for elimination
c [card-4] 1352 out of 1353 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-22] removed 15 variables
c [simpleprobe-4] 6328 schedulable variables 73%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-23] removed 31 variables
c [simpleprobe-4] 4337 variables remain 50% (4339 retained)
c [simpleprobe-4] removed 31 variables, found 3853 hbrs, 9 units
c [lift-8] limit 20000000 with penalty 0 = 0 + 0
c [lift-8] using 3488 probes 40%
c [lift-8] 56 units, 64 impls, 10 eqs in 1 rounds
c [lift-8] 2093 variables remain 24% (6462 retained)
c [lift-8] removed 121 variables
c [unhide-7] limit 3554990 with penalty 2 = 2 + 0
c [unhide-7-7] 0 units, 1 failed, 5830 tauts, 0 hbrs, 39595 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2262 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8554 variables 100%
c [elim-8] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-8] incomplete 162 not tried 2% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 131 = 2% variables out of 8554
c [bca-9] limit of 10000000 steps
c [bca-9] 12122 out of 16848 literals actually usable 72%
c [bca-9] added 28 blocked clauses in 87602 steps
c [simplification-10] removed 299 variables 3.4% (8423 remain 58%)
c [simplification-10] removed 15440 irredundant clauses 4.7% (311121 remain 84%)
c [simplification-10] maximum reduction of 5% = max (3%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] new conflict interval 6667 = min (666709/100, 206246)
c [simplification-10] penalized conflict interval 6667 = 1 * 6667
c [simplification-10] new conflict limit 673376
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  200.1    8423   311121    671592   41611  13511  9314   4 12.2  47.7   29
c 
c [simplification-11] limit of 673376 conflicts hit after 673376 conflicts
c [ternres-9] limit 72302489 with penalty 0 = 0 + 0
c [ternres-9] all 8423 free variables schedulable
c [ternres-9] 4585 ternary resolvents (85 bin, 4500 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-24] removed 6 variables
c [lift-9] limit 20000000 with penalty 0 = 0 + 0
c [lift-9] using 1485 probes 18%
c [lift-9-1] found 16 units 43 impls in round 1
c [lift-9] 17 units, 58 impls, 0 eqs in 2 rounds
c [lift-9] 563 variables remain 7% (7837 retained)
c [lift-9] removed 17 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1314 transitive binary clauses
c [elim-9] 83 variables 1% will be scheduled this time
c [elim-9] scheduled 83 variables 1%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 10 variables 0% in round 1 in 628710487 steps
c [elim-9-1] backward subsumption/strengthening limit 171289513
c [elim-9-1] subsumed 223 and strengthened 283 clauses in 171289659 steps
c [elim-9] incomplete 204 not tried 2% in round 1
c [elim-9] transition to [ all 0 rem 1 ] state
c [elim-9] eliminated 10 = 0% variables out of 8400
c [bca-10] limit of 10000000 steps
c [bca-10] 12143 out of 16782 literals actually usable 72%
c [bca-10] added 43 blocked clauses in 70231 steps
c [simplification-11] removed 33 variables 0.4% (8390 remain 58%)
c [simplification-11] removed 3155 irredundant clauses 1.0% (307966 remain 83%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 103123 = 206246 / 2
c [simplification-11] new conflict interval 309369
c [simplification-11] penalized conflict interval 309369 = 1 * 309369
c [simplification-11] new conflict limit 982745
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  222.0    8390   307966    698968   42691  16660  8758   4 12.2  47.0   28
c -  232.8    8390   307966    727290   43809  16680  8759   4 12.1  46.3   28
c -  244.3    8390   307966    755492   44961  16707  8763   4 12.1  45.6   28
c -  255.7    8390   307966    784563   46029  16723  8763   4 12.0  44.9   28
c -  267.8    8390   307966    813882   47108  16738  8764   4 12.0  44.2   28
c -  276.2    8390   307966    846278   48071  16747  8764   4 12.0  43.8   27
c -  287.8    8390   307966    877697   49137  16751  8767   4 11.9  43.1   45
c -  299.9    8390   307966    909180   50185  16765  8767   4 11.9  42.5   45
c -  312.4    8390   307966    940978   51132  16769  8767   4 11.8  41.9   45
c -  325.0    8390   307966    974284   52134  16774  8768   4 11.8  41.4   45
c 
c [simplification-12] limit of 982765 conflicts hit after 982765 conflicts
c [ternres-10] limit 125585326 with penalty 0 = 0 + 0
c [ternres-10] all 8390 free variables schedulable
c [ternres-10] 3818 ternary resolvents (72 bin, 3746 trn)
c [ternres-10] 1 variables remain 0% (8389 retained)
c [gauss-4] limit 3139633 penalty 3 = 3 + 0
c [gauss-4] extracted 100 xors of average arity 3.0
c [gauss-4] connected 299 occurrences of 247 variables (average 1.2)
c [gauss-4] limit 3139633 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 3 variables
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 8387 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 7788 probes 93%
c [lift-10] 17 units, 59 impls, 2 eqs in 1 rounds
c [lift-10] 6397 variables remain 76% (1968 retained)
c [lift-10] removed 22 variables
c [cliff-4] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-4] failed 1, lifted 0
c [unhide-8] limit 10000000 with penalty 1 = 1 + 0
c [unhide-8-11] 0 units, 0 failed, 12969 tauts, 0 hbrs, 56500 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 457 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 8364 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 57 blocked clauses
c [block-5] 57 < 1/1000 * 301724 = 301 considered unsuccessful
c [cce-5] limit of 31396331 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 417 clauses out of 817 (51%) of length 12
c [cce-5-1] eliminated 163 clauses out of 246 (66%) of length 11
c [cce-5-1] eliminated 1 clauses out of 477 (0%) of length 10
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 581 large clauses in 31396332 steps
c [cce-5-1] allowing another 15698166 steps for small clauses
c [cce-5] scheduling 22320 clauses = 16099 binary + 6221 ternary
c [cce-5] tried to eliminate 770 small clauses 3%
c [cce-5] eliminated 185 small clauses 1%
c [cce-5] eliminated 65 binary clauses 0%
c [cce-5] eliminated 120 ternary clauses 2%
c [cce-5-1] eliminated 185 small clauses in 31396332 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 766 covered clauses in round 1
c [cce-5] eliminated 766 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8363 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] incomplete 77 not tried 1% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 26 = 0% variables out of 8363
c [bca-11] limit of 10000000 steps
c [bca-11] 12050 out of 16676 literals actually usable 72%
c [bca-11] added 32 blocked clauses in 82356 steps
c [rephase-6] after 982765 conflicts (new increment 640000, next 1622765)
c [flushphases] 0 phases reset
c [simplification-12] removed 53 variables 0.6% (8337 remain 58%)
c [simplification-12] removed 10783 irredundant clauses 3.5% (297183 remain 80%)
c [simplification-12] maximum reduction of 4% = max (1%, 4%)
c [simplification-12] geometric conflict interval increment 61873 = 309369 / 5
c [simplification-12] new conflict interval 371242
c [simplification-12] penalized conflict interval 371242 = 1 * 371242
c [simplification-12] new conflict limit 1354007
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  351.2    8337   297183   1009696   50858  15358  6771   3 11.8  40.8   28
c -  363.6    8337   297183   1043781   51820  15367  6771   4 11.8  40.3   28
c -  377.1    8337   297183   1077903   52695  15381  6771   4 11.7  39.8   28
c -  388.8    8337   297183   1113954   53687  15386  6772   3 11.7  39.3   28
c -  398.4    8337   297183   1152952   54424  15386  6772   4 11.7  39.0   27
c -  409.7    8337   297183   1195142   55263  15387  6772   3 11.6  38.6   27
c -  421.7    8337   297183   1236917   56217  15398  6774   4 11.5  38.2   28
c R  424.5    8337   297183   1249841   67049  15399  6776   4 11.5  38.0   30
c -  436.5    8337   297183   1275122   57478  15407  6780   4 11.5  37.7   47
c -  452.6    8337   297183   1313993   58507  15420  6781   4 11.5  37.2   46
c -  469.8    8337   297183   1353432   59474  15434  6783   4 11.5  36.8   46
c 
c [simplification-13] limit of 1354029 conflicts hit after 1354031 conflicts
c [ternres-11] limit 189874692 with penalty 0 = 0 + 0
c [ternres-11] 1 schedulable variables 0%
c [ternres-11] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-26] removed 1 variables
c [treelook-4] limit 2373433 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 13336 literals 80%
c [treelook-4] scheduling used 777497 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2373433 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 2379231 steps
c [treelook-4] 13219 literals remain 79%
c [treelook-4] 3091 variables remain to probed next time 37%
c [decomp-27] removed 2 variables
c [treelook-4] removed 2 variables, found 553 hbrs
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 5779 probes 69%
c [lift-11] 56 units, 60 impls, 5 eqs in 1 rounds
c [lift-11] 4462 variables remain 54% (3806 retained)
c [lift-11] removed 66 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 988 transitive binary clauses
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 8268 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] incomplete 97 not tried 1% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 26 = 0% variables out of 8268
c [bca-12] limit of 10000000 steps
c [bca-12] 12057 out of 16486 literals actually usable 73%
c [bca-12] added 24 blocked clauses in 86395 steps
c [simplification-13] removed 95 variables 1.1% (8242 remain 57%)
c [simplification-13] removed 5811 irredundant clauses 2.0% (291372 remain 79%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 123747 = 371242 / 3
c [simplification-13] new conflict interval 494989
c [simplification-13] penalized conflict interval 494989 = 1 * 494989
c [simplification-13] new conflict limit 1849020
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  494.3    8242   291372   1395195   60281  13246  7476   4 11.5  36.3   28
c -  511.2    8242   291372   1437337   61176  13249  7476   3 11.5  35.9   28
c -  529.1    8242   291372   1479493   61983  13250  7476   4 11.5  35.5   28
c -  545.9    8242   291372   1527568   62913  13263  7477   3 11.5  35.1   46
c -  564.5    8242   291372   1568220   64023  13265  7481   4 11.4  34.7   47
c -  583.4    8242   291372   1611618   64998  13268  7481   4 11.4  34.3   47
c -  601.2    8242   291372   1655232   66194  13275  7482   3 11.4  34.0   47
c -  620.8    8242   291372   1699921   67172  13282  7483   4 11.4  33.6   47
c -  640.7    8242   291372   1745773   68029  13285  7484   4 11.4  33.2   47
c -  658.0    8242   291372   1794130   69077  13287  7485   4 11.4  32.9   47
c -  677.5    8242   291372   1844880   70046  13287  7486   4 11.4  32.6   47
c 
c [simplification-14] limit of 1849026 conflicts hit after 1849026 conflicts
c [decomp-28] removed 1 variables
c [basicprobe-4] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 583 sched 7%, 5 failed, 0 lifted, 703 hbrs
c [decomp-29] removed 6 variables
c [basicprobe-4-1] 1352 sched 16%, 1 failed, 0 lifted, 435 hbrs
c [decomp-30] removed 1 variables
c [basicprobe-4-2] 1349 sched 16%, 0 failed, 0 lifted, 61 hbrs
c [basicprobe-4-3] 1349 sched 16%, 0 failed, 0 lifted, 31 hbrs
c [basicprobe-4-4] 1349 sched 16%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-5] 1349 sched 16%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-6] 1349 sched 16%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-7] 1349 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-7] fully completed probing
c [basicprobe-4-7] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-4-7] removed 7 variables, found 1248 hbrs
c [bate-3] eliminated 520 asymmetric tautologies during probing
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 3851 probes 47%
c [lift-12] 0 units, 34 impls, 3 eqs in 1 rounds
c [lift-12] 2589 variables remain 31% (5642 retained)
c [lift-12] removed 3 variables
c [cliff-5] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-5] failed 0, lifted 0
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 873 transitive binary clauses
c [cce-6] limit of 142978032 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 35 clauses out of 429 (8%) of length 12
c [cce-6-1] eliminated 23 clauses out of 105 (22%) of length 11
c [cce-6-1] eliminated 117 clauses out of 463 (25%) of length 10
c [cce-6-1] eliminated 215 clauses out of 1091 (20%) of length 9
c [cce-6-1] eliminated 21 clauses out of 1805 (1%) of length 8
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 411 large clauses in 142978033 steps
c [cce-6-1] allowing another 71489016 steps for small clauses
c [cce-6] scheduling 22128 clauses = 16381 binary + 5747 ternary
c [cce-6] tried to eliminate 4384 small clauses 20%
c [cce-6] eliminated 858 small clauses 4%
c [cce-6] eliminated 412 binary clauses 3%
c [cce-6] eliminated 446 ternary clauses 8%
c [cce-6-1] eliminated 858 small clauses in 142978033 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 1269 covered clauses in round 1
c [cce-6] eliminated 1269 covered clauses in TOTAL during 1 rounds
c [elim-12] 97 variables 1% will be scheduled this time
c [elim-12] scheduled 97 variables 1%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] incomplete 139 not tried 2% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 4 = 0% variables out of 8231
c [elim-12] 4 < 1/1000 * 8231 = 8 considered unsuccessful
c [bca-13] limit of 10000000 steps
c [bca-13] 12053 out of 16456 literals actually usable 73%
c [bca-13] added 23 blocked clauses in 100541 steps
c [rephase-7] after 1849026 conflicts (new increment 1280000, next 3129026)
c [flushphases] 0 phases reset
c [simplification-14] removed 15 variables 0.2% (8227 remain 57%)
c [simplification-14] removed 5938 irredundant clauses 2.0% (285434 remain 77%)
c [simplification-14] maximum reduction of 2% = max (0%, 2%)
c [simplification-14] geometric conflict interval increment 164996 = 494989 / 3
c [simplification-14] new conflict interval 659985
c [simplification-14] penalized conflict interval 659985 = 1 * 659985
c [simplification-14] new conflict limit 2509011
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  716.0    8227   285434   1891352   71053  12911  8717   4 11.4  32.3   31
c -  739.0    8227   285434   1937729   72022  12913  8717   5 11.4  32.0   31
c -  760.4    8227   285434   1987847   72962  12916  8717   4 11.4  31.7   49
c -  784.6    8227   285434   2036570   74019  12920  8718   3 11.4  31.3   49
c -  806.8    8227   285434   2086671   75095  12921  8718   4 11.4  31.1   49
c -  830.0    8227   285434   2139648   76071  12934  8719   3 11.3  30.7   49
c -  854.8    8227   285434   2191520   77195  12956  8721   3 11.3  30.4   49
c i  861.1    8226   285434   2205469   89165  12977  8726   4 11.3  30.3   54
c -  878.5    8123   285434   2244193   78302  12980  8726   3 11.3  30.1   49
c -  905.1    8123   285434   2301925   79215  12980  8726   4 11.3  29.8   49
c -  931.9    8123   285434   2361041   80317  12997  8729   4 11.2  29.5   49
c i  935.4    8122   285434   2372564   88943  13042  8738   4 11.2  29.5   54
c i  946.6    8076   285434   2402223  111722  13099  8747   3 11.2  29.4   55
c i  952.8    8048   285434   2417684  122451  13143  8758   4 11.2  29.3   55
c i  953.3    8047   285434   2418860  123141  13161  8765   4 11.2  29.3   55
c i  954.4    8020   285434   2421043  124444  13193  8770   3 11.2  29.3   55
c i  954.6    7744   285434   2421468  124719  13206  8776   3 11.2  29.3   55
c i  954.6    7186   285434   2421490  124726  13210  8778   4 11.2  29.3   55
c i  954.6    7153   285434   2421513  124736  13213  8780   4 11.2  29.3   55
c i  954.6    7125   285434   2421516  124737  13213  8781   4 11.2  29.3   55
c i  954.6    7070   285434   2421529  124742  13216  8783   4 11.2  29.3   55
c i  954.6    6833   285434   2421534  124741  13217  8785   4 11.2  29.3   55
c 0  954.6    6225   285434   2421534  124741  13217  8785   4 11.2  29.3   55
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
s UNSATISFIABLE
c
c bate: 1046 basic ate = 286 trn 27% + 760 lrg 73% in 3 updates
c bcas: 13 count, 1254 added (183 skipped), 845541 steps
c bkwd: tried 207095 clauses, 412118 lits, 1.99 lits/clause
c bkwd: checked 109576353 occs, 529.11 occs/clause, 265.89 occs/lit
c bkwd: subsumed 0 binary, 166 ternary, 1594 large
c bkwd: strengthened 0 binary, 63 ternary (100% self), 293 large (0% self)
c blkd: 5 bces, 1141 removed, 7406332 resolutions, 24452942 steps
c blkd: 2125 blocking literals 7%, 1 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 9618038 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 18542 subsumed
c card: 6960 at-most-one constraints found, average size 3.07
c card: 6960 at-most-one constraints used 100%, average size 3.07
c card: 674 at-most-two constraints found, average size 4.01
c card: 672 at-most-two constraints used 100%, average size 4.01
c cces: 6 cces, 4353 eliminated, 3479 ate 80%, 874 abce 20%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 1807412 esteps, 6142 csteps
c cgrs: 0 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 298 extracted (259 ands 87%, 20 xors 7%, 19 ites 6%)
c clff: 5 cliffs, 0 lifted, 1 failed
c clff: 132306 decisions, 56013881 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2038807 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 89 gcs, 0 rescored clauses, 1266 rescored vars
c dcps: 35 decompositions, 1296 equivalent 9%
c deco: 13869 decision-only clauses 1%, 55% reduction
c decs: 5303500 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 134638 flipped 2.539% (in 3513 phases)
c elms: 12 elims, 4085 eliminated 28%
c elms: 15 rounds, 1.2 rounds/bve
c elms: 2210 small 54%, 1874 large 46%
c elms: 3393 tried small, 2210 succeeded 65%, 1183 failed 35%
c elms: 24254 subsumed, 4928 strengthened, 3006 blocked
c elms: 7885507 copies, 9213298 resolutions, 75545 ipos
c elms: 25812384 subchks, 6972132 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 403 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 14050914 steps, 7025457 extr 50%, 3275 elim 0%
c glue: 11.2 orig avg, 11.1 real avg, 3.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 26872 = 6415 simple + 20227 trn 24% + 230 lrg 75%, 1839 sub 1%
c hght: 29 average, 2.62 height/glue
c ints: 65534 luby (18677775 steps), 0 inout (0 steps)
c lift: 12 phases, 86323 probed (28830 level1 33%, 57493 level2 67%)
c lift: 178 units, 46 equivalences, 385 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2408311 clauses, 21.1 length
c lrnd: 718939 uips 30%, 1472119 flips 61%
c mega: 0 count, 0 failed, 0 rounds
c mins: 50695365 learned lits, 32% minimized
c mins: 2371155 mins 98%, 1077 bin 0%, 22210 size 1%, 13869 deco 1%
c move: moved 2408311, 1619 bin 0%, 3701 trn 0%, 0 lrg 0%
c otfs: str 41600 dyn (41530 red, 70 irr) 13223 drv 32%, 28377 rst 68%
c otfs: sub 491 dyn (491 red, 0 irr)
c phas: 7 computed, 9745 set, 4710 pos (48%), 5035 neg (52%)
c prbs: 4 basic, 38738 probed, 107 failed, 0 lifted
c prbs: 4 simple, 30731 probed, 16 failed, 249 eqs
c prbs: 4 treelook, 165 probed, 1 failed, 0 lifted
c prps: 994922692 props, 186 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c psns: 54383043 searches, 8457876 hits, 16% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 85 count, 0 reset, 27 acts 32%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 85 arith 100%, 0 double 0%
c rmbd: 1235 removed, 558 red 45%
c rphs: 7 recomputed phases
c rsts: 64030 restarts 98%, 1504 skipped 2%
c rsts: 0 saturating 0%, 0 agile 0%, 1504 reuse 100%
c rsts: 38.4 avg interval, 38.4 scaled, 1.0 factor
c rsts: 26909 kept 42.0% average 26.4%
c simp: 14 count (14 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2408311 count (1089968 tried 0.5), 307412 sub out of 2405025 (12.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 0 count
c tops: 3030 fixed 21%, 12 its, 201794.50 confs/it
c trvs: 68743292409 traversals, 100% srch, 1% simp, 0% lkhd
c trvs: 69.5 search traversals per propagation, 28267.2 per conflict
c trvs: 1.7 search traversals per search visit
c trds: 12 transitive reductions, 10795 removed, 0 failed
c trds: 200446 nodes, 254218 edges, 8518856 steps
c trim: 1621447 words, 6.2 MB
c trnr: 11 count, 408 bin, 22516 trn, 341944126 steps
c unhd: 8 count, 11 rounds, 34102280 steps
c unhd: 276 non-trivial sccs of average size 2.0
c unhd: 58 units, 58 bin, 0 trn, 0 lrg
c unhd: 83 failed, 80 stamp, 0 lits, 1 bin, 2 trn, 0 lrg
c unhd: 26714 tauts, 902 bin 3%, 7410 trn 28%, 7596 lrg 28%
c unhd: 26714 tauts, 10806 stamp 40%, 13004 red 49%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 174686 str, 58 bin 0%, 960 trn 1%, 173668 lrg 99%, 169277 red 97%
c vars: 6225 remaining 43% and 8411 removed 57% out of 14636
c vars: 3030 fixed 21%, 4085 eliminated 28%, 1296 equivalent 9%
c vsts: 40765888213 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 41.1 search visits per propagation, 16713.6 per conflict
c wchs: 13019664617 pushed, 25882542 enlarged, 154 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2405025 100   1954555 100  44012845 100  19417420 100   1605997 100
c 
c  0      45641   2         0   0  23876380  54   7006594  36    521884  32 
c  1      84274   4     72670   4   8714743  20<  3246394  17<   291252  18<
c  2     541413  23    489262  25   6951045  16   4324363  22    427868  27 
c  3     963709  40<   798662  41<  3189148   7   3116238  16    260190  16 
c  4     633979  26    486997  25   1060088   2   1427081   7     85372   5 
c  5     106784   4     88865   5    168754   0    228883   1     14482   1 
c  6      15369   1     11623   1     26698   0     35571   0      2941   0 
c  7       5247   0      2731   0      8111   0     11635   0       829   0 
c  8       2070   0       956   0      2951   0      4403   0       300   0 
c  9       1615   0       760   0      6841   0      5364   0       307   0 
c 10       4796   0      1965   0      7928   0     10646   0       564   0 
c 11        128   0        64   0       158   0       248   0         8   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.1           0.9           1.5           1.5
c std             1.1           1.0           1.1           1.4           1.3
c 
c   49.665   5% elim
c   24.530   3% analysis
c   13.765   1% cce
c    8.208   1% probe
c    6.393   1% lift
c    5.951   1% gc
c    5.544   1% backward
c    5.389   1% mincls
c    4.557   0% decomp
c    4.235   0% decide
c    3.727   0% ternres
c    3.679   0% bump
c    2.559   0% defrag
c    2.511   0% unhide
c    2.349   0% restart
c    1.627   0% block
c    1.493   0% bca
c    1.223   0% cliff
c    1.147   0% reduce
c    1.063   0% transred
c    0.580   0% cgrclsr
c    0.508   0% gauss
c    0.449   0% card
c    0.308   0% phase
c    0.012   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    1.632   0% probe simple     20%
c    5.667   1% probe basic      69%
c    0.909   0% probe tree-look  11%
c ==================================
c    2.261   0% preprocessing     2%
c   91.801  10% inprocessing     98%
c ==================================
c   94.062  10% simplifying
c  860.577  90% search
c ==================================
c  954.640 100% all
c 
c 5303500 decisions, 5555.5 decisions/sec
c 2421534 conflicts, 2536.6 conflicts/sec
c 994922692 propagations, 1.0 megaprops/sec
c 954.6 seconds, 69.2 MB
c launch: done
