c launch: /data/cnf/sc2014/app/002-80-12.cnf.bz2
c host: atom16
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/002-80-12.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/002-80-12.cnf.bz2
c no embedded options
c found 'p cnf 13408 478488' header
c read 13408 variables, 478488 clauses, 3138520 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 13017 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   13017   308391         0       0      0     0   0  0.0   0.0   17
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 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 424 variables
c [simpleprobe-1] all 12984 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 23 variables
c [simpleprobe-1] 5083 variables remain 39% (7878 retained)
c [simpleprobe-1] removed 23 variables, found 2 hbrs, 9 units
c [unhide-1] limit 154081 based on 308162 irredundant clauses
c [unhide-1-1] 0 units, 18 failed, 796 tauts, 0 hbrs, 18 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12955 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 437 variables 3% in round 1 in 3942599 steps
c [elim-1-1] backward subsumption/strengthening limit 7885198
c [elim-1-1] subsumed 968 and strengthened 88 clauses in 7885387 steps
c [elim-1-1] rescheduled 3693 variables 29% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 40664 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 438 = 3% variables out of 12955
c [phase-1] phase bias: 4972 positive 40%, 7545 negative 60%
c [simplification-1] removed 500 variables 3.8% (12517 remain 96%)
c [simplification-1] removed 6117 irredundant clauses 2.0% (302274 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] new conflict limit 4000
c [cut-width] 16126, max 27064, min4 13658 at 75%, min10 8176 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    1.5   12517   302274         5       4      0     2   0  3.0  16.7   23
c R    1.5   12517   302274        20      13      0     2   1  2.9  29.7   23
c R    1.5   12517   302274        62      46      4     3   1  3.5  79.1   23
c R    1.5   12517   302274       162     126     10     3   1  4.3 119.6   23
c R    1.5   12517   302274       407     325     14     4   2  4.5 140.6   23
c R    1.5   12517   302274       982     793     37     4   4  4.9 173.1   23
c R    1.6   12517   302274      2280    1858     53     7   6  5.3 226.5   23
c 
c [simplification-2] limit of 4012 conflicts hit after 4013 conflicts
c [decomp-3] removed 1 variables
c [simpleprobe-2] 4910 schedulable variables 39%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 4904 variables remain 39% (7612 retained)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5969 literals 24%
c [treelook-1] scheduling used 300026 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300149 steps
c [treelook-1] 4978 literals remain 20%
c [treelook-1] 4971 variables remain to probed next time 40%
c [treelook-1] removed 0 variables, found 3 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 534 sched 4%, 2 failed, 0 lifted, 19 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 545 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-1] removed 2 variables, found 19 hbrs
c [unhide-2] limit 151123 based on 302247 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 21 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12514 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 1102 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 17469 clauses out of 103629 (17%) of length 7
c [cce-1-1] eliminated 455 clauses out of 85445 (1%) of length 6
c [cce-1-1] eliminated 11868 clauses out of 66824 (18%) of length 5
c [cce-1-1] eliminated 167 clauses out of 33986 (0%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 29959 large clauses in 183999223 steps
c [cce-1-1] allowing another 91999611 steps for small clauses
c [cce-1] scheduling 738 clauses = 324 binary + 414 ternary
c [cce-1] tried to eliminate 738 small clauses 100%
c [cce-1] eliminated 43 small clauses 6%
c [cce-1] eliminated 4 binary clauses 1%
c [cce-1] eliminated 39 ternary clauses 9%
c [cce-1-1] eliminated 43 small clauses in 92161914 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 30002 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 695 clauses = 320 binary + 375 ternary
c [cce-1] tried to eliminate 695 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 30002 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12514 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 9797 not tried 78% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 196 = 2% variables out of 12514
c [bca-1] limit of 10000000 steps
c [bca-1] 22132 out of 24638 literals actually usable 90%
c [bca-1] added 0 blocked clauses in 188262 steps
c [phase-2] phase bias: 31 positive 9%, 298 negative 91%
c [simplification-2] removed 199 variables 1.6% (12318 remain 95%)
c [simplification-2] removed 35329 irredundant clauses 11.7% (266945 remain 87%)
c [simplification-2] maximum reduction of 12% = max (2%, 12%)
c [simplification-2] large reduction 12% >= 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 6013
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    7.9   12318   266945      5199    3993    118    28   8  5.6 311.1   22
c -    8.0   12318   266945      6018    2685    131    30   6  5.5 322.7   22
c 
c [simplification-3] limit of 6029 conflicts hit after 6029 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12318 free variables schedulable
c [ternres-1] 174 ternary resolvents (22 bin, 152 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 4 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4 out of 4 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 1930 xors of average arity 4.9
c [gauss-1] connected 9530 occurrences of 529 variables (average 18.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 2 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 12316 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 2782 probes 23%
c [lift-1-1] found 2 units 16 impls in round 1
c [lift-1] 2 units, 24 impls, 0 eqs in 2 rounds
c [lift-1] 9533 variables remain 77% (2781 retained)
c [lift-1] removed 2 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 266924 based on 266924 irredundant clauses
c [transred-1] removed 8 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12314 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 0 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 10767 clauses = 325 binary + 10442 ternary
c [cce-2] tried to eliminate 10767 small clauses 100%
c [cce-2] eliminated 1041 small clauses 10%
c [cce-2] eliminated 1 binary clauses 0%
c [cce-2] eliminated 1040 ternary clauses 10%
c [cce-2-1] eliminated 1041 small clauses in 19281395 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] eliminated 1041 covered clauses in round 1
c [cce-2-2] incomplete large round (ACCE)
c [cce-2-2] allowing another 5359303 steps for small clauses
c [cce-2] scheduling 9726 clauses = 324 binary + 9402 ternary
c [cce-2] tried to eliminate 9726 small clauses 100%
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 1041 covered clauses in TOTAL during 2 rounds
c [elim-3] 9797 variables 80% will be scheduled this time
c [elim-3] scheduled 9797 variables 80%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 7784 not tried 63% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 12314
c [phase-3] phase bias: 9 positive 56%, 7 negative 44%
c [simplification-3] removed 4 variables 0.0% (12314 remain 95%)
c [simplification-3] removed 1066 irredundant clauses 0.4% (265879 remain 86%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] new conflict limit 30029
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   11.9   12314   265879     10191    3850   1362    84  10  6.0 354.9   21
c R   12.0   12314   265879     11662    5159   1374    84  10  6.3 377.2   21
c -   12.3   12314   265879     14550    4592   1442    89   5  6.2 383.6   21
c -   13.0   12314   265879     19797    5672   1532    92   6  6.2 397.4   21
c -   13.4   12314   265879     25757    6952   1601    98  11  6.4 400.6   21
c R   13.4   12314   265879     25899    7090   1601    98  10  6.5 401.1   21
c 
c [simplification-4] limit of 30065 conflicts hit after 30066 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12314 free variables schedulable
c [ternres-2] 21 ternary resolvents (7 bin, 14 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-8] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1846 literals 7%
c [treelook-2] scheduling used 150024 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150189 steps
c [treelook-2] 1310 literals remain 5%
c [treelook-2] 1293 variables remain to probed next time 11%
c [treelook-2] removed 0 variables, found 6 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 173 probes 1%
c [lift-2-1] found 0 units 1 impls in round 1
c [lift-2-2] found 0 units 1 impls in round 2
c [lift-2-3] found 0 units 0 impls in round 3
c [lift-2-4] found 0 units 1 impls in round 4
c [lift-2-5] found 0 units 0 impls in round 5
c [lift-2] 0 units, 3 impls, 0 eqs in 6 rounds
c [lift-2] 9360 variables remain 76% (2953 retained)
c [unhide-3] limit 132939 based on 265878 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 23 tauts, 0 hbrs, 35 literals
c [transred-2] limit 446157 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 717 clauses = 329 binary + 388 ternary
c [cce-3] tried to eliminate 717 small clauses 100%
c [cce-3] eliminated 4 small clauses 1%
c [cce-3] eliminated 4 ternary clauses 1%
c [cce-3-1] eliminated 4 small clauses in 15216769 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 4 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 7391616 steps for small clauses
c [cce-3] scheduling 713 clauses = 329 binary + 384 ternary
c [cce-3] tried to eliminate 713 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 4 covered clauses in TOTAL during 2 rounds
c [cce-3] 4 < 1/1000 * 265870 = 265 considered unsuccessful
c [bca-2] limit of 10000000 steps
c [bca-2] 18840 out of 24628 literals actually usable 76%
c [bca-2] added 0 blocked clauses in 164741 steps
c [rephase-1] after 30066 conflicts (new increment 20000, next 50066)
c [flushphases] 6869 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 1 variables 0.0% (12313 remain 95%)
c [simplification-4] removed 13 irredundant clauses 0.0% (265866 remain 86%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 24000
c [simplification-4] new conflict interval 48000
c [simplification-4] penalized conflict interval 48000 = 1 * 48000
c [simplification-4] new conflict limit 78066
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.8   12313   265866     31719    7793   1667   118   7  6.6 401.5   21
c -   16.6   12313   265866     38536    8869   1759   119   8  6.9 410.2   21
c -   17.5   12313   265866     46014   10055   1842   120   8  7.1 411.2   21
c -   18.2   12313   265866     53916   11322   1899   120  13  7.4 420.9   22
c R   18.4   12313   265866     56910   14072   1924   120  12  7.6 426.3   22
c -   19.0   12313   265866     62257   12342   1982   121   8  7.6 422.5   22
c -   20.1   12313   265866     71401   13607   2086   125   7  7.8 417.5   22
c 
c [simplification-5] limit of 78076 conflicts hit after 78076 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12313 free variables schedulable
c [ternres-3] 37 ternary resolvents (10 bin, 27 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 28 xors of average arity 3.0
c [gauss-2] connected 84 occurrences of 15 variables (average 5.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 1446991 penalty 0 = 0 + 0
c [basicprobe-2-0] 625 sched 5%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-2-1] 628 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 5 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [cgrclsr-2] limit 132932 based on 265865 irredundant clauses
c [cgrclsr-2] all 12313 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1446991 with penalty 0 = 0 + 0
c [transred-3] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12313 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 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12313 variables 100%
c [elim-4] limit of 14469911 steps penalty 1 = 1 + 0
c [elim-4] incomplete 9617 not tried 78% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 3 = 0% variables out of 12313
c [elim-4] 3 < 1/1000 * 12313 = 12 considered unsuccessful
c [rephase-2] after 78076 conflicts (new increment 40000, next 118076)
c [flushphases] 6588 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 3 variables 0.0% (12310 remain 95%)
c [simplification-5] removed 36 irredundant clauses 0.0% (265830 remain 86%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 48000
c [simplification-5] new conflict interval 96000
c [simplification-5] penalized conflict interval 96000 = 1 * 96000
c [simplification-5] new conflict limit 174076
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.1   12310   265830     80935   14817   2146   130  14  8.0 418.7   22
c -   24.3   12310   265830     91103   16096   2252   131   8  8.1 413.6   22
c -   25.7   12310   265830    101904   17516   2347   135  10  8.3 412.7   22
c -   26.7   12310   265830    112825   18661   2413   135  17  8.8 417.9   22
c -   27.5   12310   265830    123916   19712   2441   136  17  9.5 424.3   22
c R   27.5   12310   265830    124075   19862   2441   136  17  9.5 424.4   23
c -   29.1   12310   265830    136037   20866   2517   137  11  9.6 419.2   22
c -   30.7   12310   265830    149008   22478   2617   139  13  9.7 417.0   22
c -   32.4   12310   265830    162100   23584   2706   142  13  9.9 414.3   23
c 
c [simplification-6] limit of 174098 conflicts hit after 174098 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 12310 free variables schedulable
c [ternres-4] 16 ternary resolvents (3 bin, 13 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 1 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [lift-3] limit 1168349 with penalty 1 = 1 + 0
c [lift-3] using 407 probes 3%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 0 impls in round 2
c [lift-3-3] found 0 units 0 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-3] 8953 variables remain 73% (3357 retained)
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 3 transitive binary clauses
c [cce-4] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 7500000 steps for small clauses
c [cce-4] scheduling 9793 clauses = 333 binary + 9460 ternary
c [cce-4] tried to eliminate 9793 small clauses 100%
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 0 covered clauses in round 1
c [cce-4] eliminated 0 covered clauses in TOTAL during 1 rounds
c [rephase-3] after 174098 conflicts (new increment 80000, next 254098)
c [flushphases] 6224 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (12310 remain 95%)
c [simplification-6] removed 0 irredundant clauses 0.0% (265830 remain 86%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 96000
c [simplification-6] new conflict interval 192000
c [simplification-6] penalized conflict interval 192000 = 1 * 192000
c [simplification-6] new conflict limit 366098
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   35.1   12310   265830    175860   24883   2803   144  17 10.2 413.6   23
c -   36.9   12310   265830    190476   26319   2897   147  11 10.4 412.4   23
c -   38.8   12310   265830    205613   27906   3001   148  22 10.6 412.7   23
c -   40.9   12310   265830    220914   29112   3094   150  14 10.7 410.8   23
c -   43.0   12310   265830    236902   30685   3169   151  20 10.9 412.8   24
c -   44.0   12310   265830    255266   33173   3238   151  17 11.1 419.0   24
c R   44.7   12310   265830    268695   45413   3269   151  19 11.4 421.7   25
c -   45.2   12310   265830    272373   34176   3293   151  12 11.4 420.4   23
c -   47.6   12310   265830    290551   35710   3374   153  15 11.5 417.6   24
c -   49.9   12310   265830    308857   37120   3487   155  10 11.7 416.1   24
c -   51.5   12310   265830    328498   38447   3604   156  12 11.8 417.6   24
c -   53.6   12310   265830    349140   39869   3721   158  24 11.9 415.9   24
c 
c [simplification-7] limit of 366112 conflicts hit after 366112 conflicts
c [ternres-5] limit 8223644 with penalty 0 = 0 + 0
c [ternres-5] all 12310 free variables schedulable
c [ternres-5] 3 ternary resolvents (3 bin, 0 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 4819 schedulable variables 39%
c [simpleprobe-3] limit 16447288 penalty 1 = 1 + 0
c [simpleprobe-3] 2649 variables remain 22% (9661 retained)
c [simpleprobe-3] removed 0 variables, found 4 hbrs, 0 units
c [unhide-4] limit 411182 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 81 tauts, 0 hbrs, 335 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 5 transitive binary clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 8814 out of 24622 literals actually usable 36%
c [bca-3] added 0 blocked clauses in 121654 steps
c [rephase-4] after 366112 conflicts (new increment 160000, next 526112)
c [flushphases] 500 phases reset
c [phase-7] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-7] removed 0 variables 0.0% (12310 remain 95%)
c [simplification-7] removed 0 irredundant clauses 0.0% (265830 remain 86%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 192000
c [simplification-7] new conflict interval 384000
c [simplification-7] penalized conflict interval 384000 = 1 * 384000
c [simplification-7] new conflict limit 750112
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   56.6   12310   265830    369666   40969   3738   164  10 12.0 415.2   24
c -   57.8   12310   265830    390362   42234   3782   164  28 12.3 417.9   25
c -   59.4   12310   265830    411468   42897   3824   164  12 12.6 417.7   24
c -   61.2   12310   265830    434040   43813   3879   164  11 12.8 417.9   24
c -   63.7   12310   265830    456138   45061   3948   164  14 12.9 418.1   25
c -   66.8   12310   265830    479112   46501   4046   164  13 13.0 418.3   25
c -   69.8   12310   265830    503421   48310   4168   171   7 13.0 419.3   25
c -   72.0   12310   265830    529050   50894   4392   189  12 12.8 427.3   25
c -   74.1   12310   265830    554306   53198   4563   196  17 12.8 434.8   25
c R   76.0   12310   265830    579109   76309   4687   198  22 12.9 439.5   29
c -   76.0   12310   265830    579172   54858   4688   198  20 12.9 439.5   25
c -   80.3   12310   265830    606633   57270   5032   201   8 12.8 441.6   25
c -   84.2   12310   265830    633862   59859   5232   202  19 12.7 442.7   26
c -   87.8   12310   265830    662022   62006   5633   213  12 12.5 442.0   26
c -   91.8   12310   265830    691170   64930   5988   215  13 12.4 442.0   26
c -   95.5   12310   265830    719995   67361   6247   215  10 12.3 442.8   26
c -  100.3   12310   265830    748877   69383   6516   215  11 12.2 442.0   26
c 
c [simplification-8] limit of 750178 conflicts hit after 750178 conflicts
c [ternres-6] limit 18173477 with penalty 0 = 0 + 0
c [ternres-6] all 12310 free variables schedulable
c [ternres-6] 8 ternary resolvents (3 bin, 5 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 908673 penalty 2 = 2 + 0
c [gauss-3] extracted 18 xors of average arity 3.0
c [gauss-3] connected 54 occurrences of 9 variables (average 6.0)
c [gauss-3] limit 908673 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-3] limit 454336 penalty 2 = 2 + 0
c [cgrclsr-3] all 12310 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-3] limit of 3634695 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 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12310 variables 100%
c [block-4] limit of 45433694 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1 blocked clauses
c [block-4] 1 < 1/1000 * 265830 = 265 considered unsuccessful
c [elim-5] 7784 variables 63% will be scheduled this time
c [elim-5] scheduled 7784 variables 63%
c [elim-5] limit of 90867389 steps penalty 2 = 2 + 0
c [elim-5] incomplete 4171 not tried 34% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 12310
c [rephase-5] after 750178 conflicts (new increment 320000, next 1070178)
c [flushphases] 479 phases reset
c [phase-8] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-8] removed 0 variables 0.0% (12310 remain 95%)
c [simplification-8] removed 230 irredundant clauses 0.1% (265600 remain 86%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 384000
c [simplification-8] new conflict interval 768000
c [simplification-8] penalized conflict interval 768000 = 1 * 768000
c [simplification-8] new conflict limit 1518178
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  107.2   12310   265600    778662   71999   6721   216  10 12.2 441.9   28
c -  112.2   12310   265600    808671   74401   6912   216  22 12.2 440.9   28
c -  114.6   12310   265600    838012   76423   6967   216  26 12.6 442.9   28
c -  117.9   12310   265600    872084   80410   7449   218  12 12.5 442.4   28
c -  121.4   12310   265600    907095   84328   8211   264  10 12.4 439.3   28
c -  125.6   12310   265600    941618   87869   8838   285  15 12.2 435.2   29
c -  128.8   12310   265600    974520   90559   9139   291  10 12.3 434.0   29
c -  134.3   12310   265600   1007036   92837   9216   291  11 12.3 431.9   29
c -  139.4   12310   265600   1040613   95620   9343   292  14 12.3 431.8   29
c -  145.3   12310   265600   1074504   97893   9487   292  11 12.3 431.0   29
c -  148.5   12310   265600   1108246  100454   9545   293  20 12.7 432.3   30
c -  152.0   12310   265600   1143139  103732   9618   293  22 13.2 433.8   29
c -  153.8   12310   265600   1177742  104573   9676   294  24 13.4 435.4   29
c -  155.3   12310   265600   1214896  105469   9687   294  47 13.6 436.7   29
c -  157.9   12310   265600   1249966  106041   9687   294  49 14.1 437.1   30
c -  160.7   12310   265600   1286691  106556   9693   294   9 14.5 437.7   31
c -  164.6   12310   265600   1326556  108270   9833   296  11 14.5 437.9   30
c -  169.0   12310   265600   1365766  110527   9934   296  10 14.6 438.3   30
c -  175.0   12310   265600   1406426  112837  10091   298  12 14.5 437.6   31
c -  179.6   12310   265600   1447492  114864  10203   298  33 14.6 437.4   31
c -  182.4   12310   265600   1486189  115537  10226   298  53 14.6 437.5   30
c 
c [simplification-9] limit of 1518288 conflicts hit after 1518289 conflicts
c [ternres-7] limit 38392329 with penalty 0 = 0 + 0
c [ternres-7] all 12310 free variables schedulable
c [ternres-7] 186 ternary resolvents (16 bin, 170 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-16] removed 4 variables
c [lift-4] limit 5000000 with penalty 2 = 2 + 0
c [lift-4] using 1573 probes 13%
c [lift-4-1] found 1 units 0 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 1 impls in round 5
c [lift-4] 1 units, 1 impls, 0 eqs in 6 rounds
c [lift-4] 7380 variables remain 60% (4925 retained)
c [lift-4] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3 transitive binary clauses
c [cce-5] limit of 19196164 steps penalty 2 = 2 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 9598082 steps for small clauses
c [cce-5] scheduling 10073 clauses = 374 binary + 9699 ternary
c [cce-5] tried to eliminate 10073 small clauses 100%
c [cce-5] eliminated 35 small clauses 0%
c [cce-5] eliminated 3 binary clauses 1%
c [cce-5] eliminated 32 ternary clauses 0%
c [cce-5-1] eliminated 35 small clauses in 14282076 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 35 covered clauses in round 1
c [cce-5-2] eliminated 68 clauses out of 90577 (0%) of length 6
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] eliminated 68 large clauses in 4914089 steps
c [cce-5-2] allowing another 2457044 steps for small clauses
c [cce-5] scheduling 10038 clauses = 371 binary + 9667 ternary
c [cce-5] tried to eliminate 5277 small clauses 53%
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 68 covered clauses in round 2
c [cce-5] eliminated 103 covered clauses in TOTAL during 2 rounds
c [cce-5] 103 < 1/1000 * 265588 = 265 considered unsuccessful
c [rephase-6] after 1518289 conflicts (new increment 640000, next 2158289)
c [flushphases] 0 phases reset
c [simplification-9] removed 5 variables 0.0% (12305 remain 95%)
c [simplification-9] removed 115 irredundant clauses 0.0% (265485 remain 86%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 768000
c [simplification-9] conflict interval soft limit 1000000 reached
c [simplification-9] new conflict interval 1000000
c [simplification-9] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-9] new conflict limit 2518289
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  185.9   12305   265485   1526713  116298  10324   301  45 14.9 438.1   33
c -  189.6   12305   265485   1568368  117550  10371   302  32 15.1 438.6   33
c -  196.6   12305   265485   1610530  119602  10479   303  14 15.1 437.7   33
c -  203.0   12305   265485   1651214  121506  10529   303  14 15.5 437.0   33
c -  210.7   12305   265485   1693491  124195  10600   303  18 15.6 435.9   33
c -  219.2   12305   265485   1736167  126933  10665   303  15 15.6 434.0   33
c -  223.1   12305   265485   1780131  130011  10784   303  32 15.8 435.4   34
c -  229.1   12305   265485   1820727  130662  10788   303  39 17.0 436.1   34
c -  235.5   12305   265485   1861624  131251  10790   303  38 18.1 436.8   35
c -  243.5   12305   265485   1903015  131813  10790   303  37 19.5 437.4   35
c -  252.1   12305   265485   1945406  132594  10791   303  37 20.7 438.1   35
c -  260.3   12305   265485   1987835  133061  10792   303  36 21.9 438.8   35
c -  269.1   12305   265485   2030923  133631  10795   303  38 23.0 439.5   35
c -  278.7   12305   265485   2074527  134092  10795   303  36 24.3 440.2   35
c -  287.8   12305   265485   2118342  134655  10795   303  37 25.4 440.9   35
c -  297.6   12305   265485   2162955  135259  10795   303  36 26.4 441.6   35
c -  307.2   12305   265485   2208193  135820  10795   303  38 27.9 442.3   35
c -  316.7   12305   265485   2253652  136303  10795   303  37 28.8 443.0   35
c -  326.4   12305   265485   2299827  136858  10795   303  35 29.7 443.7   35
c -  334.0   12305   265485   2346628  137636  10796   303  36 30.4 444.4   35
c -  345.3   12305   265485   2394506  138429  10796   303  40 31.5 445.2   55
c -  356.0   12305   265485   2442553  139021  10796   303  40 32.7 445.9   55
c -  366.9   12305   265485   2490910  139577  10796   303  36 33.7 446.6   55
c 
c [simplification-10] limit of 2518291 conflicts hit after 2518292 conflicts
c [ternres-8] limit 108361031 with penalty 0 = 0 + 0
c [ternres-8] all 12305 free variables schedulable
c [ternres-8] 51 ternary resolvents (4 bin, 47 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6772564 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 10 at-most-two constraints of average size 4.1
c [card-4] using previous limit 6772564 for elimination
c [card-4] 12 out of 12 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-17] removed 1 variables
c [treelook-3] limit 1354512 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 2670 literals 11%
c [treelook-3] scheduling used 1027658 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1354512 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 755142 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 10 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [rephase-7] after 2518292 conflicts (new increment 1280000, next 3798292)
c [flushphases] 0 phases reset
c [simplification-10] removed 1 variables 0.0% (12304 remain 95%)
c [simplification-10] removed 2 irredundant clauses 0.0% (265483 remain 86%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 1000000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] new conflict limit 3518292
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  374.3   12304   265483   2540687  140878  10844   313  31 34.2 447.7   37
c -  379.1   12304   265483   2591674  142819  10881   313  36 34.3 448.7   37
c -  389.5   12304   265483   2641702  143430  10883   313  33 35.3 449.3   37
c -  396.0   12304   265483   2692007  144162  10888   313  35 35.5 450.0   37
c -  403.4   12304   265483   2742865  144743  10889   313  34 35.9 450.7   37
c -  409.8   12304   265483   2798593  147400  11268   314  15 35.7 448.6   36
c -  417.8   12304   265483   2857925  151208  11771   315  20 35.2 445.5   36
c -  424.5   12304   265483   2913523  153787  11975   315  35 35.3 444.2   36
c -  432.5   12304   265483   2969744  155581  12184   317  18 35.3 442.8   36
c -  440.9   12304   265483   3028116  158356  12386   317  29 35.1 440.8   37
c -  445.6   12304   265483   3087373  159299  12426   317  14 34.9 441.4   37
c -  452.2   12304   265483   3148047  160721  12464   317  14 34.6 440.9   37
c -  456.3   12304   265483   3207058  161667  12468   317  41 34.4 441.4   36
c -  459.8   12304   265483   3265678  162244  12468   317  47 34.2 442.0   38
c -  462.4   12304   265483   3325775  162835  12473   317  52 33.9 442.5   38
c -  465.8   12304   265483   3385875  163731  12473   317  38 33.8 442.9   38
c -  469.8   12304   265483   3445315  164327  12478   317  38 33.6 443.3   38
c -  472.7   12304   265483   3507341  165275  12485   317  35 33.3 444.1   36
c 
c [simplification-11] limit of 3518298 conflicts hit after 3518298 conflicts
c [ternres-9] limit 140299304 with penalty 0 = 0 + 0
c [ternres-9] all 12304 free variables schedulable
c [ternres-9] 29 ternary resolvents (0 bin, 29 trn)
c [ternres-9] fully completed ternary resolution
c [lift-5] limit 10000000 with penalty 1 = 1 + 0
c [lift-5] using 435 probes 4%
c [lift-5-1] found 0 units 0 impls in round 1
c [lift-5-2] found 0 units 1 impls in round 2
c [lift-5-3] found 0 units 0 impls in round 3
c [lift-5-4] found 0 units 0 impls in round 4
c [lift-5-5] found 0 units 0 impls in round 5
c [lift-5] 0 units, 1 impls, 0 eqs in 6 rounds
c [lift-5] 6945 variables remain 56% (5359 retained)
c [unhide-5] limit 2500000 with penalty 3 = 3 + 0
c [unhide-5-8] 0 units, 0 failed, 184 tauts, 0 hbrs, 487 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 131 out of 24610 literals actually usable 1%
c [bca-4] added 0 blocked clauses in 175426 steps
c [simplification-11] removed 0 variables 0.0% (12304 remain 95%)
c [simplification-11] removed 9 irredundant clauses 0.0% (265474 remain 86%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] new conflict limit 4518298
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  478.2   12304   265474   3570923  166387  12433   315  41 33.1 444.3   38
c -  481.5   12304   265474   3632413  166701  12436   315  24 32.9 444.9   38
c -  488.9   12304   265474   3698886  168323  12488   316  13 32.6 443.9   38
c -  496.5   12304   265474   3764568  171412  12572   316  25 32.4 443.5   38
c -  503.7   12304   265474   3827182  174366  12611   316  25 32.6 443.8   38
c -  511.9   12304   265474   3892689  179326  12676   316  35 32.7 444.3   38
c -  520.0   12304   265474   3956452  180671  12782   316  18 32.6 443.0   39
c -  531.4   12304   265474   4023330  184421  12936   316  15 32.4 441.4   39
c -  540.5   12304   265474   4091474  187314  13042   316  36 32.1 439.8   39
c -  550.0   12304   265474   4157169  190157  13096   316  31 32.1 438.8   39
c -  558.0   12304   265474   4222035  192205  13103   316  34 32.6 439.5   40
c -  569.1   12304   265474   4287909  193796  13137   316  31 32.7 439.0   40
c -  575.4   12304   265474   4356992  195340  13175   316  47 32.5 438.1   39
c -  583.9   12304   265474   4425508  196130  13175   316  38 32.3 438.6   39
c -  589.5   12304   265474   4494155  196893  13175   316  50 32.1 439.0   39
c 
c [simplification-12] limit of 4518300 conflicts hit after 4518302 conflicts
c [ternres-10] limit 177044392 with penalty 0 = 0 + 0
c [ternres-10] all 12304 free variables schedulable
c [ternres-10] 54 ternary resolvents (0 bin, 54 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 4426109 penalty 3 = 3 + 0
c [gauss-4] extracted 2599 xors of average arity 5.0
c [gauss-4] connected 12875 occurrences of 650 variables (average 19.8)
c [gauss-4] limit 4426109 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 812 sched 7%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [bate-2] eliminated 1 asymmetric tautologies during probing
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 12304 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [cliff-4] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-4] failed 0, lifted 0
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 12304 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 1 blocked clauses
c [block-5] 1 < 1/1000 * 265473 = 265 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 12304 variables 100%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6] incomplete 3699 not tried 30% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 2 = 0% variables out of 12304
c [elim-6] 2 < 1/1000 * 12304 = 12 considered unsuccessful
c [rephase-8] after 4518302 conflicts (new increment 2560000, next 7078302)
c [flushphases] 0 phases reset
c [simplification-12] removed 2 variables 0.0% (12302 remain 95%)
c [simplification-12] removed 204 irredundant clauses 0.1% (265270 remain 86%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 5518302
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  598.0   12302   265270   4562637  197497  13215   313  37 32.2 439.3   40
c -  602.4   12302   265270   4632758  198634  13217   313  46 32.2 439.8   40
c -  611.8   12302   265270   4703638  199810  13217   313  47 32.2 440.3   40
c -  615.9   12302   265270   4776318  200708  13220   313  49 32.1 440.8   42
c -  621.8   12302   265270   4859655  201165  13220   313  53 31.9 441.2   42
c -  627.6   12302   265270   4943914  201664  13220   313  53 31.7 441.6   42
c -  633.8   12302   265270   5028585  202143  13220   313  53 31.6 442.1   45
c -  639.6   12302   265270   5114268  202631  13220   313  53 31.4 442.5   45
c -  645.6   12302   265270   5200493  203138  13220   313  54 31.3 442.9   45
c -  651.5   12302   265270   5287782  203642  13220   313  54 31.1 443.4   45
c -  657.6   12302   265270   5375170  204132  13220   313  53 31.0 443.8   45
c -  664.1   12302   265270   5464193  204628  13220   313  53 30.9 444.2   45
c 
c [simplification-13] limit of 5518302 conflicts hit after 5518302 conflicts
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 12302 free variables schedulable
c [ternres-11] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1 transitive binary clauses
c [cce-6] limit of 58699384 steps penalty 3 = 3 + 0
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] allowing another 29349692 steps for small clauses
c [cce-6] scheduling 1127 clauses = 376 binary + 751 ternary
c [cce-6] tried to eliminate 1127 small clauses 100%
c [cce-6] eliminated 11 small clauses 1%
c [cce-6] eliminated 1 binary clauses 0%
c [cce-6] eliminated 10 ternary clauses 1%
c [cce-6-1] eliminated 11 small clauses in 29804701 steps
c [cce-6-1] completed small round (ACCE)
c [cce-6-1] eliminated 11 covered clauses in round 1
c [cce-6-2] eliminated 255 clauses out of 92116 (0%) of length 6
c [cce-6-2] incomplete large round (ACCE)
c [cce-6-2] eliminated 255 large clauses in 28894686 steps
c [cce-6-2] allowing another 14447343 steps for small clauses
c [cce-6] scheduling 1116 clauses = 375 binary + 741 ternary
c [cce-6] tried to eliminate 1116 small clauses 100%
c [cce-6-2] completed small round (ACCE)
c [cce-6-2] eliminated 255 covered clauses in round 2
c [cce-6-3] incomplete large round (ACCE)
c [cce-6-3] allowing another 6997489 steps for small clauses
c [cce-6] scheduling 1116 clauses = 375 binary + 741 ternary
c [cce-6] tried to eliminate 1116 small clauses 100%
c [cce-6-3] completed small round (ACCE)
c [cce-6-3] eliminated 0 covered clauses in round 3
c [cce-6] eliminated 266 covered clauses in TOTAL during 3 rounds
c [simplification-13] removed 0 variables 0.0% (12302 remain 95%)
c [simplification-13] removed 266 irredundant clauses 0.1% (265004 remain 86%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] new conflict limit 6518302
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  671.2   12302   265004   5547621  205190  13234   313  42 30.8 444.6   44
c -  677.7   12302   265004   5625858  206330  13235   313  47 30.6 445.0   44
c -  684.9   12302   265004   5704318  208179  13261   313  19 30.5 445.1   45
c -  691.7   12302   265004   5784489  209776  13297   313  39 30.4 444.7   42
c -  696.7   12302   265004   5862492  210591  13313   313  42 30.3 444.8   43
c -  701.7   12302   265004   5942857  211278  13313   313  43 30.1 445.4   46
c -  708.7   12302   265004   6021986  212138  13313   313  43 30.2 446.1   46
c -  712.9   12302   265004   6102132  213029  13314   313  47 30.1 446.7   44
c -  718.4   12302   265004   6182814  213488  13314   313  42 30.1 447.2   44
c -  727.5   12302   265004   6264473  214195  13314   313  47 29.9 447.5   69
c -  737.7   12302   265004   6345165  214898  13314   313  43 29.9 447.7   69
c -  746.2   12302   265004   6427553  215780  13321   313  25 29.8 448.2   69
c -  755.2   12302   265004   6511346  217717  13334   313  36 29.7 447.5   43
c 
c [simplification-14] limit of 6518302 conflicts hit after 6518302 conflicts
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 12302 free variables schedulable
c [ternres-12] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-12] fully completed ternary resolution
c [lift-6] limit 5000000 with penalty 2 = 2 + 0
c [lift-6] using 155 probes 1%
c [lift-6-1] found 0 units 0 impls in round 1
c [lift-6-2] found 0 units 0 impls in round 2
c [lift-6-3] found 0 units 0 impls in round 3
c [lift-6-4] found 0 units 0 impls in round 4
c [lift-6-5] found 0 units 0 impls in round 5
c [lift-6] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-6] 6790 variables remain 55% (5512 retained)
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1 transitive binary clauses
c [simplification-14] removed 0 variables 0.0% (12302 remain 95%)
c [simplification-14] removed 0 irredundant clauses 0.0% (265004 remain 86%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 1000000
c [simplification-14] new conflict interval 2000000
c [simplification-14] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-14] new conflict limit 8518302
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  772.5   12302   265004   6593681  218304  13334   312  34 29.5 447.8   42
c -  791.8   12302   265004   6675289  218962  13334   312  32 29.3 448.0   45
c -  810.6   12302   265004   6756672  219585  13334   312  33 29.1 448.3   45
c -  831.3   12302   265004   6838418  220155  13334   312  31 29.0 448.5   45
c -  850.4   12302   265004   6921278  220816  13334   312  36 28.8 448.8   45
c -  869.6   12302   265004   7005477  221492  13334   312  47 28.6 449.0   45
c -  877.4   12302   265004   7095615  222136  13334   312  48 28.5 449.4   67
c -  886.8   12302   265004   7183226  222814  13334   312  47 28.4 449.8   67
c -  893.5   12302   265004   7270211  223931  13336   312  35 28.4 450.1   64
c -  905.0   12302   265004   7354370  224685  13336   312  44 28.9 450.5   65
c -  911.4   12302   265004   7441618  225434  13337   312  48 28.9 450.9   43
c -  926.5   12302   265004   7531656  228738  13420   312  14 28.9 449.0   46
c -  948.7   12302   265004   7621348  232556  13476   312  16 28.9 447.1   46
c -  968.9   12302   265004   7709077  234260  13491   312  43 28.9 447.1   44
c -  988.9   12302   265004   7795771  234826  13491   312  41 28.9 447.7   47
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2 basic ate = 2 trn 100% + 0 lrg 0% in 2 updates
c bcas: 4 count, 0 added (0 skipped), 650083 steps
c bkwd: tried 24704 clauses, 48402 lits, 1.96 lits/clause
c bkwd: checked 3055231 occs, 123.67 occs/clause, 63.12 occs/lit
c bkwd: subsumed 1 binary, 0 ternary, 967 large
c bkwd: strengthened 1 binary, 1 ternary (100% self), 86 large (0% self)
c blkd: 5 bces, 1104 removed, 24345802 resolutions, 42809574 steps
c blkd: 129 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 10823321 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 670 subsumed
c card: 5 at-most-one constraints found, average size 3.00
c card: 5 at-most-one constraints used 100%, average size 3.00
c card: 21 at-most-two constraints found, average size 4.10
c card: 21 at-most-two constraints used 100%, average size 4.10
c cces: 6 cces, 31416 eliminated, 31416 ate 100%, 0 abce 0%
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, 1787299 esteps, 36138 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: 1154 extracted (9 ands 1%, 1109 xors 96%, 36 ites 3%)
c clff: 4 cliffs, 0 lifted, 0 failed
c clff: 1747991 decisions, 30060992 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3617008 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 56 gcs, 0 rescored clauses, 3857 rescored vars
c dcps: 22 decompositions, 56 equivalent 0%
c deco: 775 decision-only clauses 0%, 44% reduction
c decs: 77613545 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 2997784 flipped 3.862% (in 5344 phases)
c elms: 6 elims, 638 eliminated 5%
c elms: 7 rounds, 1.2 rounds/bve
c elms: 628 small 98%, 10 large 2%
c elms: 3041 tried small, 628 succeeded 21%, 2413 failed 79%
c elms: 2166 subsumed, 4931 strengthened, 3 blocked
c elms: 2877791 copies, 8330227 resolutions, 881657 ipos
c elms: 519916 subchks, 244746 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 4575 extracted, 4.9 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16670234 steps, 8335117 extr 50%, 128438 elim 1%
c glue: 28.9 orig avg, 28.9 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 83 = 6 simple + 68 trn 7% + 9 lrg 82%, 47 sub 11%
c hght: 448 average, 15.49 height/glue
c ints: 192507 luby (60649153 steps), 0 inout (0 steps)
c lift: 6 phases, 105048 probed (35022 level1 33%, 70026 level2 67%)
c lift: 3 units, 0 equivalences, 29 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 7333508 clauses, 77.3 length
c lrnd: 1780069 uips 24%, 4953120 flips 68%
c mega: 0 count, 0 failed, 0 rounds
c mins: 567222521 learned lits, 1% minimized
c mins: 6731067 mins 92%, 117 bin 0%, 601549 size 8%, 775 deco 0%
c move: moved 7333508, 9 bin 0%, 1417 trn 0%, 0 lrg 0%
c otfs: str 1569158 dyn (1558931 red, 10227 irr) 526908 drv 34%, 1042250 rst 66%
c otfs: sub 17367 dyn (17367 red, 0 irr)
c phas: 8 computed, 12864 set, 5013 pos (39%), 7851 neg (61%)
c prbs: 3 basic, 6288 probed, 2 failed, 0 lifted
c prbs: 3 simple, 27570 probed, 9 failed, 1 eqs
c prbs: 3 treelook, 4197 probed, 0 failed, 0 lifted
c prps: 769478773 props, 10 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 139217653 searches, 18013983 hits, 13% 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: 163 count, 0 reset, 2 acts 1%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 163 arith 100%, 0 double 0%
c rmbd: 23 removed, 13 red 57%
c rphs: 8 recomputed phases
c rsts: 67510 restarts 35%, 124997 skipped 65%
c rsts: 0 saturating 0%, 116442 agile 93%, 8555 reuse 7%
c rsts: 115.0 avg interval, 115.0 scaled, 1.0 factor
c rsts: 17295 kept 25.6% average 54.1%
c simp: 14 count (14 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 7333508 count (13527969 tried 1.8), 90845 sub out of 7328953 (1.2%)
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: 412 fixed 3%, 0 its, 0.00 confs/it
c trvs: 62793918511 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 81.8 search traversals per propagation, 7984.5 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 12 transitive reductions, 34 removed, 0 failed
c trds: 293128 nodes, 6987 edges, 8611 steps
c trim: 1927377 words, 7.4 MB
c trnr: 12 count, 68 bin, 513 trn, 24781214 steps
c unhd: 5 count, 8 rounds, 4983008 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 18 failed, 18 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1084 tauts, 0 bin 0%, 794 trn 73%, 287 lrg 26%
c unhd: 1084 tauts, 3 stamp 0%, 547 red 50%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 896 str, 0 bin 0%, 36 trn 4%, 860 lrg 96%, 837 red 93%
c vars: 12302 remaining 92% and 1106 removed 8% out of 13408
c vars: 412 fixed 3%, 638 eliminated 5%, 56 equivalent 0%
c vsts: 38178652248 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 49.7 search visits per propagation, 4852.9 per conflict
c wchs: 11896486515 pushed, 28526299 enlarged, 368 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   7328953 100   6915511 100 172462979 100  55831022 100   3606989 100
c 
c  0     160496   2         0   0  91575701  53  14725649  26    564076  16 
c  1     338396   5    247873   4  39474762  23<  9243675  17    449182  12 
c  2     944273  13    932323  13  17870797  10   8660432  16    569554  16 
c  3    1179476  16   1159942  17   9727877   6   6991142  13<   497469  14 
c  4    1560565  21   1520852  22   6042050   4   6198505  11    567369  16<
c  5    1127889  15<  1091524  16<  3319908   2   3667097   7    227614   6 
c  6     630126   9    610526   9   1698065   1   2028865   4    161051   4 
c  7     396715   5    384813   6   1003916   1   1316299   2    139317   4 
c  8     261534   4    253826   4    505651   0    758393   1     83263   2 
c  9     194761   3    189804   3    318492   0    536484   1     65554   2 
c 10     271480   4    268133   4    456752   0    779718   1    104220   3 
c 11     243279   3    237229   3    425800   0    845325   2    162847   5 
c 12      18423   0     17535   0     40120   0     75575   0     15232   0 
c 13       1540   0      1131   0      3088   0      3863   0       241   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             4.6           4.7           1.0           2.5           3.5
c std             2.5           2.5           1.6           2.5           3.0
c 
c  131.137  13% analysis
c   72.336   7% decide
c   21.619   2% bump
c   16.671   2% mincls
c    9.944   1% cce
c    7.624   1% defrag
c    6.220   1% restart
c    5.269   1% elim
c    5.018   1% gc
c    3.234   0% reduce
c    3.081   0% block
c    2.831   0% decomp
c    2.141   0% probe
c    1.774   0% cliff
c    1.151   0% lift
c    0.721   0% gauss
c    0.625   0% cgrclsr
c    0.600   0% bca
c    0.508   0% unhide
c    0.348   0% phase
c    0.221   0% card
c    0.215   0% backward
c    0.172   0% ternres
c    0.060   0% transred
c    0.017   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.882   0% probe simple     41%
c    0.331   0% probe basic      15%
c    0.927   0% probe tree-look  43%
c ==================================
c    1.485   0% preprocessing     5%
c   28.269   3% inprocessing     95%
c ==================================
c   29.755   3% simplifying
c  969.899  97% search
c ==================================
c  999.654 100% all
c 
c 77613545 decisions, 77640.4 decisions/sec
c 7860416 conflicts, 7863.1 conflicts/sec
c 769478773 propagations, 0.8 megaprops/sec
c 999.7 seconds, 164.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
