c launch: /data/cnf/sc2014/app/ctl_4291_567_5_unsat_pre.cnf.bz2
c host: atom26
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/ctl_4291_567_5_unsat_pre.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ctl_4291_567_5_unsat_pre.cnf.bz2
c no embedded options
c found 'p cnf 15232 134756' header
c read 15232 variables, 134756 clauses, 462322 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 15232 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   15232   134756         0       0      0     0   0  0.0   0.0    7
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [simpleprobe-1] all 15232 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] fully completed simple probing
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 615 tauts, 0 hbrs, 2677 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 15232 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] no variable eliminated in round 1 in 22856165 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 0 = 0% variables out of 15232
c [phase-1] phase bias: 7314 positive 48%, 7918 negative 52%
c [simplification-1] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-1] removed 615 irredundant clauses 0.5% (134141 remain 100%)
c [simplification-1] maximum reduction of 0% = max (0%, 0%)
c [simplification-1] full geometric conflict interval increment 20000
c [simplification-1] new conflict interval 20000
c [simplification-1] penalized conflict interval 20000 = 1 * 20000
c [simplification-1] new conflict limit 20000
c [cut-width] 41584, max 56362, min4 44151 at 44%, min10 9534 at 11%
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    0.7   15232   134141         6       6      0     0   3 16.2  29.2    9
c -    1.3   15232   134141      4198    2075      0     0  15 13.3  20.3    9
c -    1.8   15232   134141      7349    2627      1     0  13 12.6  19.3    9
c -    2.3   15232   134141     10970    3153      1     0  16 12.6  19.1    9
c -    2.9   15232   134141     15084    3678      1     0  13 12.6  18.8    9
c -    3.6   15232   134141     19817    4241      3     0  17 12.2  18.6    9
c 
c [simplification-2] limit of 20000 conflicts hit after 20000 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 27083 literals 89%
c [treelook-1] scheduling used 300164 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300171 steps
c [treelook-1] 26879 literals remain 88%
c [treelook-1] 15232 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 300 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 39 probes remain 0% after last round
c [basicprobe-1-0] removed 0 variables, found 4071 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 15232 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 0 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 47110 clauses = 27737 binary + 19373 ternary
c [cce-1] tried to eliminate 18274 small clauses 39%
c [cce-1] eliminated 1531 small clauses 3%
c [cce-1] eliminated 1531 binary clauses 6%
c [cce-1-1] eliminated 1531 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1531 covered clauses in round 1
c [cce-1] eliminated 1531 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps
c [bca-1] 28480 out of 30466 literals actually usable 93%
c [bca-1] added 0 blocked clauses in 64165 steps
c [rephase-1] after 20000 conflicts (new increment 20000, next 40000)
c [flushphases] 9302 phases reset
c [phase-2] phase bias: 344 positive 48%, 369 negative 52%
c [simplification-2] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-2] removed 1531 irredundant clauses 1.1% (132610 remain 98%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 30000
c [simplification-2] penalized conflict interval 30000 = 1 * 30000
c [simplification-2] new conflict limit 50000
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   11.8   15232   132610     25335    4785      3  5545  12 11.7  17.8   10
c -   12.5   15232   132610     31256    5364      5  5545  10 11.2  17.1   10
c -   13.2   15232   132610     37611    5937      6  5545  11 11.0  16.7   10
c -   14.1   15232   132610     44655    6610     11  5545  12 10.7  16.4   10
c 
c [simplification-3] limit of 50000 conflicts hit after 50001 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 15232 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 414 at-most-one constraints of average size 4.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 414 out of 414 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 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-2] all 15232 free variables schedulable
c [simpleprobe-2] limit 4437214 penalty 1 = 1 + 0
c [simpleprobe-2] 6652 variables remain 44% (8580 retained)
c [cgrclsr-1] limit 221860 penalty 0 = 0 + 0
c [cgrclsr-1] all 15232 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 1331164 with penalty 0 = 0 + 0
c [lift-1] using 15203 probes 100%
c [lift-1] 0 units, 11 impls, 0 eqs in 1 rounds
c [lift-1] 15043 variables remain 99% (189 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 221860 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 2269 tauts, 0 hbrs, 81102 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 2569 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 44461 clauses = 26213 binary + 18248 ternary
c [cce-2] tried to eliminate 1633 small clauses 4%
c [cce-2] eliminated 46 small clauses 0%
c [cce-2] eliminated 46 binary clauses 0%
c [cce-2-1] eliminated 46 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 46 covered clauses in round 1
c [cce-2] eliminated 46 covered clauses in TOTAL during 1 rounds
c [cce-2] 46 < 1/1000 * 131382 = 131 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 15232 variables 100%
c [elim-2] limit of 22186072 steps penalty 1 = 1 + 0
c [elim-2] incomplete 154 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 15232
c [rephase-2] after 50001 conflicts (new increment 40000, next 90001)
c [flushphases] 9156 phases reset
c [phase-3] phase bias: 442 positive 49%, 462 negative 51%
c [simplification-3] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-3] removed 1274 irredundant clauses 1.0% (131336 remain 97%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-3] new conflict interval 45000
c [simplification-3] penalized conflict interval 45000 = 1 * 45000
c [simplification-3] new conflict limit 95001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   17.1   15232   131336     52348    7327     18  2941  15 10.4  16.0   10
c -   18.3   15232   131336     60354    7913     19  2941  14 10.3  16.0   10
c -   19.4   15232   131336     68916    8503     21  2941  13 10.2  15.9   10
c -   20.7   15232   131336     78054    9079     21  2941  13 10.1  15.7   10
c -   21.9   15232   131336     87592    9678     26  2941  17 10.1  15.7   10
c 
c [simplification-4] limit of 95001 conflicts hit after 95001 conflicts
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 773 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 15232 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [bca-2] limit of 10000000 steps
c [bca-2] 27935 out of 30466 literals actually usable 92%
c [bca-2] added 0 blocked clauses in 75249 steps
c [rephase-3] after 95001 conflicts (new increment 80000, next 175001)
c [flushphases] 9098 phases reset
c [phase-4] phase bias: 30 positive 38%, 48 negative 62%
c [simplification-4] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-4] removed 376 irredundant clauses 0.3% (130960 remain 97%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 45000
c [simplification-4] new conflict interval 90000
c [simplification-4] penalized conflict interval 90000 = 1 * 90000
c [simplification-4] new conflict limit 185001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.7   15232   130960     97802   10329     29  2544  15 10.2  15.7   10
c -   25.1   15232   130960    108427   11050     29  2544  16 10.2  15.6   10
c -   27.0   15232   130960    119553   11882     29  2544  17 10.2  15.4   10
c -   28.7   15232   130960    131262   12617     29  2544  14 10.2  15.3   11
c -   30.5   15232   130960    143454   13331     29  2544  15 10.1  15.2   11
c -   32.5   15232   130960    156185   14102     29  2544  15 10.1  15.0   11
c -   34.6   15232   130960    169651   14877     29  2544  17 10.0  14.9   11
c -   36.9   15232   130960    183551   15630     30  2544  18 10.0  14.8   11
c 
c [simplification-5] limit of 185001 conflicts hit after 185001 conflicts
c [ternres-2] limit 5301653 with penalty 1 = 1 + 0
c [ternres-2] all 15232 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 1060330 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 265082 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 24966 literals 82%
c [treelook-2] scheduling used 265633 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 265082 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 274328 steps
c [treelook-2] 24908 literals remain 82%
c [treelook-2] 15159 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 84 hbrs
c [cgrclsr-2] limit 530165 penalty 1 = 1 + 0
c [cgrclsr-2] all 15232 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-2] limit 3180992 with penalty 1 = 1 + 0
c [lift-2] using 15014 probes 99%
c [lift-2] 0 units, 22 impls, 0 eqs in 1 rounds
c [lift-2] 14612 variables remain 96% (620 retained)
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 597 transitive binary clauses
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 29338 clauses = 25820 binary + 3518 ternary
c [cce-3] tried to eliminate 1104 small clauses 4%
c [cce-3] eliminated 26 small clauses 0%
c [cce-3] eliminated 26 binary clauses 0%
c [cce-3-1] eliminated 26 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 26 covered clauses in round 1
c [cce-3] eliminated 26 covered clauses in TOTAL during 1 rounds
c [cce-3] 26 < 1/1000 * 130770 = 130 considered unsuccessful
c [rephase-4] after 185001 conflicts (new increment 160000, next 345001)
c [flushphases] 9028 phases reset
c [phase-5] phase bias: 111 positive 46%, 130 negative 54%
c [simplification-5] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-5] removed 216 irredundant clauses 0.2% (130744 remain 97%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 90000
c [simplification-5] new conflict interval 180000
c [simplification-5] penalized conflict interval 180000 = 1 * 180000
c [simplification-5] new conflict limit 365001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   40.7   15232   130744    198757   16484     51  2918  14  9.9  14.6   11
c -   43.4   15232   130744    213587   17255     70  2918  16  9.9  14.5   11
c -   46.1   15232   130744    229024   17943     98  2918  16  9.8  14.4   11
c -   48.7   15232   130744    245340   18723    111  2918  15  9.7  14.3   11
c -   51.7   15232   130744    262036   19400    124  2918  13  9.7  14.1   11
c -   54.8   15232   130744    279117   20166    131  2918  16  9.6  14.0   11
c -   57.6   15232   130744    296494   20871    133  2918  14  9.7  14.1   18
c -   60.3   15232   130744    314299   21650    135  2918  14  9.7  14.3   18
c -   63.4   15232   130744    332552   22324    137  2918  15  9.7  14.5   18
c -   66.6   15232   130744    351660   23094    143  2918  15  9.7  14.6   18
c 
c [simplification-6] limit of 365001 conflicts hit after 365001 conflicts
c [card-3] limit 3078183 penalty 2 = 2 + 0
c [card-3] found 249 at-most-one constraints of average size 4.2
c [card-3] found 2 at-most-two constraints of average size 4.0
c [card-3] using previous limit 3078183 for elimination
c [card-3] 251 out of 251 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 1231273 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 74 tauts, 0 hbrs, 199353 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 329 transitive binary clauses
c [elim-3] 154 variables 1% will be scheduled this time
c [elim-3] scheduled 154 variables 1%
c [elim-3] limit of 123127332 steps penalty 2 = 2 + 0
c [elim-3-1] no variable eliminated in round 1 in 1788648 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 15232
c [rephase-5] after 365001 conflicts (new increment 320000, next 685001)
c [flushphases] 8966 phases reset
c [phase-6] phase bias: 89 positive 44%, 111 negative 56%
c [simplification-6] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-6] removed 145 irredundant clauses 0.1% (130599 remain 97%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 180000
c [simplification-6] new conflict interval 360000
c [simplification-6] penalized conflict interval 360000 = 1 * 360000
c [simplification-6] new conflict limit 725001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   70.5   15232   130599    371128   23838    186  2660  15  9.8  14.7   12
c -   74.0   15232   130599    391263   24639    194  2660  14  9.8  14.6   12
c -   77.4   15232   130599    411921   25405    200  2660  14  9.8  14.7   12
c -   81.1   15232   130599    432867   26108    204  2660  18  9.8  14.7   12
c -   84.8   15232   130599    454804   26847    208  2660  14  9.8  14.6   12
c -   88.4   15232   130599    476844   27490    217  2660  17  9.9  14.7   13
c -   92.3   15232   130599    499090   28201    227  2660  13  9.9  14.8   20
c -   96.3   15232   130599    522145   28893    231  2660  15 10.0  14.8   20
c -  100.5   15232   130599    545699   29660    231  2660  15 10.0  14.8   20
c -  104.6   15232   130599    569559   30303    233  2660  16 10.0  15.0   20
c -  109.0   15232   130599    594111   31072    234  2660  16 10.0  14.9   20
c -  114.0   15232   130599    618776   31731    239  2660  16 10.0  15.0   20
c -  118.8   15232   130599    644049   32375    240  2660  16 10.1  15.0   20
c -  124.0   15232   130599    669900   33157    250  2660  15 10.1  15.1   21
c -  129.3   15232   130599    696482   33988    264  2660  17 10.2  15.2   21
c -  134.6   15232   130599    723604   34764    272  2660  13 10.2  15.2   21
c 
c [simplification-7] limit of 725001 conflicts hit after 725001 conflicts
c [basicprobe-2] limit 28308273 penalty 1 = 1 + 0
c [basicprobe-2-0] 39 sched 0%, 0 failed, 0 lifted, 372 hbrs
c [basicprobe-2-1] 256 sched 2%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 372 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 291 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 15232 variables 100%
c [block-3] limit of 141541367 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 27687 out of 30466 literals actually usable 91%
c [bca-3] added 0 blocked clauses in 94085 steps
c [rephase-6] after 725001 conflicts (new increment 640000, next 1365001)
c [flushphases] 8892 phases reset
c [phase-7] phase bias: 50 positive 68%, 24 negative 32%
c [simplification-7] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-7] removed 76 irredundant clauses 0.1% (130523 remain 97%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 360000
c [simplification-7] new conflict interval 720000
c [simplification-7] penalized conflict interval 720000 = 1 * 720000
c [simplification-7] new conflict limit 1445001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  140.1   15232   130523    751909   35799    275  2782  15 10.2  15.2   14
c -  145.1   15232   130523    780225   36630    284  2782  15 10.2  15.3   14
c -  150.7   15232   130523    809038   37399    295  2782  16 10.2  15.3   14
c -  156.6   15232   130523    838500   38132    296  2782  16 10.2  15.4   14
c -  162.6   15232   130523    868518   38935    302  2782  15 10.2  15.4   21
c -  168.4   15232   130523    898889   39729    306  2782  19 10.2  15.4   21
c -  174.5   15232   130523    929875   40563    307  2782  16 10.2  15.4   21
c -  180.5   15232   130523    961633   41287    311  2782  15 10.2  15.4   21
c -  186.5   15232   130523    993786   42146    317  2782  13 10.1  15.4   21
c -  192.9   15232   130523   1026092   43009    321  2782  13 10.1  15.3   21
c -  200.0   15232   130523   1058678   43828    333  2782  16 10.2  15.4   22
c -  207.4   15232   130523   1091619   44579    333  2782  14 10.2  15.4   22
c -  214.3   15232   130523   1125417   45414    335  2782  13 10.2  15.4   22
c -  221.3   15232   130523   1159451   46234    335  2782  16 10.2  15.3   22
c -  228.2   15232   130523   1193826   47031    335  2782  16 10.2  15.3   22
c -  235.1   15232   130523   1230103   47886    351  2782  18 10.2  15.2   22
c -  242.4   15232   130523   1266126   48694    358  2782  16 10.2  15.2   22
c -  250.0   15232   130523   1303088   49551    369  2782  15 10.2  15.2   22
c -  257.5   15232   130523   1340267   50334    380  2782  15 10.2  15.3   22
c -  265.3   15232   130523   1378059   51169    396  2782  17 10.2  15.3   22
c -  273.5   15232   130523   1416663   52108    423  2782  14 10.2  15.2   22
c 
c [simplification-8] limit of 1445001 conflicts hit after 1445001 conflicts
c [ternres-3] limit 33536582 with penalty 2 = 2 + 0
c [ternres-3] all 15232 free variables schedulable
c [ternres-3] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 6707316 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-3] limit 2000000 penalty 2 = 2 + 0
c [cgrclsr-3] all 15232 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 5000000 with penalty 2 = 2 + 0
c [lift-3] using 14584 probes 96%
c [lift-3] 0 units, 22 impls, 0 eqs in 1 rounds
c [lift-3] 14058 variables remain 92% (1174 retained)
c [cliff-3] limit of 25000000 steps penalty 2 = 2 + 0
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 306 transitive binary clauses
c [cce-4] limit of 67073164 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 33536582 steps for small clauses
c [cce-4] scheduling 29778 clauses = 26402 binary + 3376 ternary
c [cce-4] tried to eliminate 4828 small clauses 16%
c [cce-4] eliminated 42 small clauses 0%
c [cce-4] eliminated 42 binary clauses 0%
c [cce-4-1] eliminated 42 small clauses in 67073165 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 42 covered clauses in round 1
c [cce-4] eliminated 42 covered clauses in TOTAL during 1 rounds
c [cce-4] 42 < 1/1000 * 130470 = 130 considered unsuccessful
c [rephase-7] after 1445001 conflicts (new increment 1280000, next 2725001)
c [flushphases] 8767 phases reset
c [phase-8] phase bias: 146 positive 40%, 215 negative 60%
c [simplification-8] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-8] removed 95 irredundant clauses 0.1% (130428 remain 97%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 720000
c [simplification-8] conflict interval soft limit 1000000 reached
c [simplification-8] new conflict interval 1000000
c [simplification-8] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-8] new conflict limit 2445001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  286.0   15232   130428   1454949   52893    426  3199  17 10.2  15.2   17
c -  295.2   15232   130428   1494235   53795    440  3199  16 10.2  15.2   17
c -  304.2   15232   130428   1534213   54818    455  3199  14 10.2  15.2   17
c -  313.5   15232   130428   1574290   55661    458  3199  14 10.2  15.2   27
c -  322.6   15232   130428   1614864   56556    465  3199  13 10.1  15.2   27
c -  331.8   15232   130428   1655785   57518    470  3199  16 10.1  15.2   27
c -  341.4   15232   130428   1697778   58686    487  3199  15 10.1  15.2   27
c -  350.1   15232   130428   1739883   59751    490  3199  17 10.0  15.2   27
c -  359.8   15232   130428   1782697   60929    491  3199  17 10.0  15.2   27
c -  369.6   15232   130428   1825945   62090    491  3199  17 10.0  15.2   27
c -  379.6   15232   130428   1869555   63377    491  3199  14  9.9  15.2   27
c -  389.4   15232   130428   1913737   64482    491  3199  16  9.9  15.3   27
c -  399.6   15232   130428   1958507   65603    491  3199  13  9.9  15.3   27
c -  409.7   15232   130428   2003630   66575    492  3199  14  9.9  15.4   27
c -  420.8   15232   130428   2048791   67223    492  3199  14  9.9  15.4   27
c -  431.6   15232   130428   2094367   67989    492  3199  12  9.9  15.5   27
c -  442.4   15232   130428   2140948   68984    493  3199  17  9.9  15.6   27
c -  453.4   15232   130428   2188215   69909    494  3199  17  9.9  15.6   27
c -  465.0   15232   130428   2236025   70925    496  3199  15  9.9  15.7   27
c -  476.6   15232   130428   2283874   71732    497  3199  14  9.9  15.7   46
c -  488.4   15232   130428   2332277   72788    497  3199  15  9.9  15.8   46
c -  500.5   15232   130428   2381123   73733    497  3199  12  9.9  15.8   46
c -  513.1   15232   130428   2430322   74474    497  3199  17  9.9  15.9   46
c 
c [simplification-9] limit of 2445001 conflicts hit after 2445001 conflicts
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 187 transitive binary clauses
c [phase-9] phase bias: 7 positive 29%, 17 negative 71%
c [simplification-9] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-9] removed 39 irredundant clauses 0.0% (130389 remain 97%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 1000000
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 3445001
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  525.6   15232   130389   2481393   75469    511  3051  15  9.9  15.9   20
c -  537.4   15232   130389   2532587   76470    520  3051  14  9.9  15.9   20
c -  550.7   15232   130389   2583924   77347    534  3051  16  9.9  15.8   30
c -  563.8   15232   130389   2635654   78286    535  3051  17  9.9  15.8   30
c -  576.9   15232   130389   2688123   79144    543  3051  17 10.0  15.8   30
c -  590.9   15232   130389   2740952   79981    568  3051  17 10.0  15.8   30
c -  604.3   15232   130389   2794451   81062    570  3051  17 10.0  15.7   30
c -  616.8   15232   130389   2848765   82392    571  3051  15  9.9  15.7   30
c -  629.5   15232   130389   2902980   83459    571  3051  15  9.9  15.7   30
c -  641.6   15232   130389   2958019   84598    572  3051  14 10.0  15.7   30
c -  654.9   15232   130389   3013294   85641    573  3051  15 10.0  15.7   30
c -  668.5   15232   130389   3069026   86631    573  3051  15 10.0  15.7   30
c -  683.1   15232   130389   3125151   87592    573  3051  16 10.0  15.7   31
c -  697.3   15232   130389   3182716   89010    574  3052  16  9.9  15.6   31
c -  712.8   15232   130389   3240739   90165    587  3052  16  9.9  15.6   31
c -  727.2   15232   130389   3299183   91356    587  3052  17  9.9  15.6   50
c -  741.6   15232   130389   3358675   92637    587  3052  16  9.9  15.6   50
c -  756.0   15232   130389   3418650   93926    587  3052  16  9.8  15.7   50
c 
c [simplification-10] limit of 3445003 conflicts hit after 3445004 conflicts
c [ternres-4] limit 100000000 with penalty 1 = 1 + 0
c [ternres-4] all 15232 free variables schedulable
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [card-4] limit 26728569 penalty 3 = 3 + 0
c [card-4] found 193 at-most-one constraints of average size 3.7
c [card-4] found 19 at-most-two constraints of average size 4.3
c [card-4] using previous limit 26728569 for elimination
c [card-4] 212 out of 212 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 6652 schedulable variables 44%
c [simpleprobe-3] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 233 tauts, 0 hbrs, 911827 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 101 transitive binary clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 15232 variables 100%
c [elim-4] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-4-1] no variable eliminated in round 1 in 23753408 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 15232
c [rephase-8] after 3445004 conflicts (new increment 2560000, next 6005004)
c [flushphases] 8543 phases reset
c [phase-10] phase bias: 48 positive 39%, 74 negative 61%
c [simplification-10] removed 0 variables 0.0% (15232 remain 100%)
c [simplification-10] removed 26 irredundant clauses 0.0% (130363 remain 97%)
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 4445004
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  773.7   15232   130363   3479623   95077    651  2744  17  9.8  15.6   21
c -  789.8   15232   130363   3539825   96042    651  2744  11  9.8  15.6   33
c -  806.5   15232   130363   3600029   97147    651  2744  16  9.8  15.6   33
c -  822.3   15232   130363   3661421   98372    651  2744  14  9.8  15.6   33
c -  841.1   15232   130363   3723218   99679    668  2744  14  9.8  15.6   34
c -  859.5   15232   130363   3784852  100484    685  2744  13  9.8  15.6   34
c -  878.5   15232   130363   3847414  101408    697  2745  14  9.8  15.5   34
c -  895.0   15232   130363   3912356  102499    702  2745  16  9.8  15.5   34
c -  912.8   15232   130363   3976380  103445    708  2745  15  9.8  15.5   34
c -  930.8   15232   130363   4041084  104452    715  2745  17  9.8  15.4   34
c -  949.7   15232   130363   4106056  105422    730  2745  16  9.8  15.4   34
c -  967.6   15232   130363   4171427  106338    733  2745  17  9.9  15.4   35
c -  985.6   15232   130363   4237275  107160    738  2745  16  9.9  15.4   57
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 0 added (0 skipped), 233499 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 3 bces, 0 removed, 1368427 resolutions, 4603334 steps
c blkd: 8 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 39875084 steps
c card: 21 rescheduled, 198 eliminated, 123760 resolved, 14132 subsumed
c card: 856 at-most-one constraints found, average size 4.08
c card: 856 at-most-one constraints used 100%, average size 4.08
c card: 21 at-most-two constraints found, average size 4.29
c card: 21 at-most-two constraints used 100%, average size 4.29
c cces: 4 cces, 1645 eliminated, 1641 ate 100%, 4 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: 3 count, 2752025 esteps, 0 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: 0 extracted (0 ands 0%, 0 xors 0%, 0 ites 0%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 43231 decisions, 40003457 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 597078 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 32 gcs, 0 rescored clauses, 2256 rescored vars
c dcps: 16 decompositions, 0 equivalent 0%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 5041738 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 22 flipped 0.000% (in 1 phases)
c elms: 4 elims, 0 eliminated 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 55 tried small, 0 succeeded 0%, 55 failed 100%
c elms: 0 subsumed, 0 strengthened, 0 blocked
c elms: 1592110 copies, 1411491 resolutions, 1421 ipos
c elms: 666054 subchks, 304842 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15466244 steps, 7733122 extr 50%, 0 elim 0%
c glue: 9.9 orig avg, 9.9 real avg, 2.9 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 8225 = 0 simple + 8225 trn 0% + 0 lrg 100%, 1586 sub 0%
c hght: 15 average, 1.56 height/glue
c ints: 110586 luby (32734727 steps), 0 inout (0 steps)
c lift: 3 phases, 7011 probed (2348 level1 33%, 4663 level2 67%)
c lift: 0 units, 0 equivalences, 55 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4288461 clauses, 19.1 length
c lrnd: 2284347 uips 53%, 1858468 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 82068927 learned lits, 35% minimized
c mins: 4263768 mins 99%, 1 bin 0%, 24692 size 1%, 0 deco 0%
c move: moved 4288461, 1645 bin 0%, 0 trn 0%, 0 lrg 0%
c otfs: str 10302 dyn (10302 red, 0 irr) 5074 drv 49%, 5228 rst 51%
c otfs: sub 14 dyn (14 red, 0 irr)
c phas: 10 computed, 17949 set, 8581 pos (48%), 9368 neg (52%)
c prbs: 2 basic, 1024 probed, 0 failed, 0 lifted
c prbs: 3 simple, 67071 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 262 probed, 0 failed, 0 lifted
c prps: 2506027235 props, 496 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 228586884 searches, 16017252 hits, 7% 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: 123 count, 0 reset, 123 acts 100%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 123 arith 100%, 0 double 0%
c rmbd: 0 removed, 0 red 0%
c rphs: 8 recomputed phases
c rsts: 1 restarts 0%, 110585 skipped 100%
c rsts: 110584 saturating 100%, 0 agile 0%, 1 reuse 0%
c rsts: 4224000.0 avg interval, 4224000.0 scaled, 1.0 factor
c rsts: 1 kept 100.0% average 100.0%
c simp: 10 count (10 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 4288461 count (591831 tried 0.1), 129917 sub out of 4287831 (3.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 0 count
c tops: 0 fixed 0%, 0 its, 0.00 confs/it
c trvs: 80387860652 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 32.1 search traversals per propagation, 18710.9 per conflict
c trvs: 1.4 search traversals per search visit
c trds: 8 transitive reductions, 5153 removed, 0 failed
c trds: 155865 nodes, 141424 edges, 16001046 steps
c trim: 453986 words, 1.7 MB
c trnr: 4 count, 0 bin, 1 trn, 6191353 steps
c unhd: 4 count, 4 rounds, 7176732 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 3191 tauts, 37 bin 1%, 0 trn 0%, 0 lrg 0%
c unhd: 3191 tauts, 3154 stamp 99%, 2539 red 80%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1194959 str, 0 bin 0%, 4038 trn 0%, 1190921 lrg 100%, 1190916 red 100%
c vars: 15232 remaining 100% and 0 removed 0% out of 15232
c vars: 0 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 57825425757 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 23.1 search visits per propagation, 13455.9 per conflict
c wchs: 12469776014 pushed, 6011259 enlarged, 64 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   4287831 100   3996262 100  36432950 100  18427946 100    929709 100
c 
c  0      44941   1         0   0  24035194  66   6022873  33    366121  39 
c  1      74992   2     73635   2   1490447   4<   769528   4     45029   5 
c  2     681491  16    662655  17   4872727  13   3395527  18<   181241  19<
c  3    2773983  65<  2621274  66<  5062775  14   6709308  36    264520  28 
c  4     710082  17    636739  16    968642   3   1525789   8     72468   8 
c  5       2342   0      1959   0      3165   0      4921   0       330   0 
c  6          0   0         0   0         0   0         0   0         0   0 
c  7          0   0         0   0         0   0         0   0         0   0 
c  8          0   0         0   0         0   0         0   0         0   0 
c  9          0   0         0   0         0   0         0   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             2.9           3.0           0.8           1.8           1.6
c std             0.7           0.6           1.2           1.4           1.4
c 
c   44.804   4% analysis
c   14.868   1% mincls
c   10.679   1% cce
c    8.524   1% bump
c    3.973   0% decide
c    3.217   0% reduce
c    1.235   0% elim
c    1.108   0% gc
c    1.042   0% transred
c    1.017   0% cliff
c    0.970   0% decomp
c    0.893   0% probe
c    0.803   0% unhide
c    0.557   0% lift
c    0.539   0% card
c    0.422   0% defrag
c    0.310   0% block
c    0.285   0% gauss
c    0.266   0% phase
c    0.263   0% cgrclsr
c    0.159   0% bca
c    0.110   0% restart
c    0.044   0% ternres
c    0.004   0% cutwidth
c    0.000   0% backward
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.552   0% probe simple     62%
c    0.160   0% probe basic      18%
c    0.181   0% probe tree-look  20%
c ==================================
c    0.680   0% preprocessing     4%
c   18.350   2% inprocessing     96%
c ==================================
c   19.030   2% simplifying
c  980.902  98% search
c ==================================
c  999.932 100% all
c 
c 5041738 decisions, 5042.1 decisions/sec
c 4293535 conflicts, 4293.8 conflicts/sec
c 2506027235 propagations, 2.5 megaprops/sec
c 999.9 seconds, 73.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
