c launch: /data/cnf/sc2014/app/vmpc_33.cnf.bz2
c host: atom27
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/vmpc_33.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/vmpc_33.cnf.bz2
c no embedded options
c found 'p cnf 1089 177375' header
c read 1089 variables, 177375 clauses, 464310 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 1089 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    1089   177375         0       0      0     0   0  0.0   0.0   16
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 34 at-most-one constraints of average size 33.0
c [card-1] found 1283 at-most-two constraints of average size 6.6
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1317 out of 1317 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 1089 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 2 variables
c [simpleprobe-1] 638 variables remain 59% (449 retained)
c [simpleprobe-1] removed 2 variables, found 146 hbrs, 2 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-3] 0 units, 0 failed, 1773 tauts, 0 hbrs, 1408 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1087 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 0 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 1087
c [phase-1] phase bias: 0 positive 0%, 1087 negative 100%
c [simplification-1] removed 2 variables 0.2% (1087 remain 100%)
c [simplification-1] removed 36767 irredundant clauses 20.7% (140608 remain 79%)
c [simplification-1] maximum reduction of 21% = max (0%, 21%)
c [simplification-1] large reduction 21% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] new conflict limit 1000
c [cut-width] 111886, max 168807, min4 124423 at 75%, min10 59187 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.0    1087   140608         5       4      0    84   1 19.0  96.5    3
c R    1.0    1087   140608        20      17      1    84   1 11.1  75.1    3
c R    1.0    1087   140608        63      44      2    84   1  9.1  53.1    3
c R    1.0    1087   140608       168     125      6    84   2 14.5  38.8    3
c R    1.1    1087   140608       422     304     10    84   4 12.2  30.5    7
c 
c [simplification-2] limit of 1000 conflicts hit after 1000 conflicts
c [simpleprobe-2] 638 schedulable variables 59%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 573 variables remain 53% (514 retained)
c [simpleprobe-2] removed 0 variables, found 11 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 1641 literals 75%
c [treelook-1] scheduling used 300131 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 321330 steps
c [treelook-1] 1626 literals remain 75%
c [treelook-1] 1081 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 55 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 877 probes remain 81% after last round
c [basicprobe-1-0] removed 0 variables, found 557 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 1087 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] completed large round (ATE)
c [cce-1-1] allowing another 115359 steps for small clauses
c [cce-1] scheduling 88482 clauses = 36172 binary + 52310 ternary
c [cce-1] tried to eliminate 22618 small clauses 26%
c [cce-1] eliminated 11643 small clauses 13%
c [cce-1] eliminated 1878 binary clauses 5%
c [cce-1] eliminated 9765 ternary clauses 19%
c [cce-1-1] eliminated 11643 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 11643 covered clauses in round 1
c [cce-1] eliminated 11643 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps
c [bca-1] 715 out of 2176 literals actually usable 33%
c [bca-1] added 0 blocked clauses in 2209 steps
c [simplification-2] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-2] removed 11643 irredundant clauses 8.3% (128965 remain 73%)
c [simplification-2] maximum reduction of 8% = max (0%, 8%)
c [simplification-2] geometric conflict interval increment 2222 = 20000 / 9
c [simplification-2] new conflict interval 2222
c [simplification-2] penalized conflict interval 2222 = 1 * 2222
c [simplification-2] new conflict limit 3222
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    5.8    1087   128965      1017     791   9792  1989   5 14.0  27.3    4
c R    6.1    1087   128965      2335    1842   9846  1991   5 17.1  34.3    7
c 
c [simplification-3] limit of 3226 conflicts hit after 3227 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 1087 free variables schedulable
c [ternres-1] 7031 ternary resolvents (0 bin, 7031 trn)
c [ternres-1] 677 variables remain 62% (410 retained)
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 132 at-most-one constraints of average size 23.0
c [card-2] found 680 at-most-two constraints of average size 8.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 811 out of 812 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 [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 1087 free variables schedulable
c [cgrclsr-1] 820 variables remain 75% (267 retained)
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 1087 probes 100%
c [lift-1] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-1] 1071 variables remain 99% (16 retained)
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 64482 based on 128965 irredundant clauses
c [unhide-2-4] 0 units, 0 failed, 292 tauts, 0 hbrs, 1331 literals
c [transred-1] limit 600124 with penalty 0 = 0 + 0
c [transred-1] removed 116 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] completed large round (ABCE)
c [cce-2-1] allowing another 125055 steps for small clauses
c [cce-2] scheduling 87199 clauses = 36795 binary + 50404 ternary
c [cce-2] tried to eliminate 1805 small clauses 2%
c [cce-2] eliminated 796 small clauses 1%
c [cce-2] eliminated 116 binary clauses 0%
c [cce-2] eliminated 680 ternary clauses 1%
c [cce-2-1] eliminated 796 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 796 covered clauses in round 1
c [cce-2] eliminated 796 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 1087 variables 100%
c [elim-2] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-2] incomplete 1013 not tried 93% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 1087
c [simplification-3] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-3] removed 2706 irredundant clauses 2.1% (126259 remain 71%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 8888
c [simplification-3] penalized conflict interval 8888 = 1 * 8888
c [simplification-3] new conflict limit 12115
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    8.1    1087   126259      5319    4227  17333  2100   5 16.9  32.6    8
c -    8.2    1087   126259      5596    2456  17334  2100   5 16.8  32.5    7
c -    9.2    1087   126259      9736    3288  17425  2100   5 16.0  30.0    7
c R    9.6    1087   126259     11926    4916  17440  2100   5 17.7  32.3    8
c 
c [simplification-4] limit of 12115 conflicts hit after 12115 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 677 schedulable variables 62%
c [ternres-2] 1219 ternary resolvents (0 bin, 1219 trn)
c [ternres-2] 593 variables remain 55% (494 retained)
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1202 literals 55%
c [treelook-2] scheduling used 150231 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 178787 steps
c [treelook-2] 1194 literals remain 55%
c [treelook-2] 1074 variables remain to probed next time 99%
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 622 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1087 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 [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] allowing another 128344 steps for small clauses
c [cce-3] scheduling 77521 clauses = 37051 binary + 40470 ternary
c [cce-3] tried to eliminate 1767 small clauses 2%
c [cce-3] eliminated 560 small clauses 1%
c [cce-3] eliminated 131 binary clauses 0%
c [cce-3] eliminated 429 ternary clauses 1%
c [cce-3-1] eliminated 560 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 560 covered clauses in round 1
c [cce-3] eliminated 560 covered clauses in TOTAL during 1 rounds
c [bca-2] limit of 10000000 steps
c [bca-2] 71 out of 2176 literals actually usable 3%
c [bca-2] not enough literals usable
c [bca-2] added 0 blocked clauses in 5087 steps
c [rephase-1] after 12115 conflicts (new increment 20000, next 32115)
c [flushphases] 0 phases reset
c [simplification-4] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-4] removed 1117 irredundant clauses 0.9% (125142 remain 71%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 18888
c [simplification-4] penalized conflict interval 18888 = 1 * 18888
c [simplification-4] new conflict limit 31003
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   11.2    1087   125142     14595    4105  19143  2161   5 17.0  30.9    8
c -   12.5    1087   125142     20285    5039  19214  2161   5 17.8  31.5    8
c R   13.7    1087   125142     26419    9899  19260  2161   5 17.7  31.7    9
c -   13.7    1087   125142     26444    5921  19260  2161   5 17.7  31.7    8
c 
c [simplification-5] limit of 31005 conflicts hit after 31005 conflicts
c [ternres-3] limit 5718843 with penalty 0 = 0 + 0
c [ternres-3] 593 schedulable variables 55%
c [ternres-3] 1698 ternary resolvents (0 bin, 1698 trn)
c [ternres-3] 475 variables remain 44% (612 retained)
c [gauss-2] limit 1000000 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 [cgrclsr-2] limit 285942 penalty 1 = 1 + 0
c [cgrclsr-2] 820 schedulable variables 75%
c [cgrclsr-2] 264 variables remain 24% (823 retained)
c [lift-2] limit 1715653 with penalty 1 = 1 + 0
c [lift-2] using 1071 probes 99%
c [lift-2] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-2] 1014 variables remain 93% (73 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 365 transitive binary clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] completed large round (ACCE)
c [cce-4-1] allowing another 130357 steps for small clauses
c [cce-4] scheduling 84721 clauses = 36616 binary + 48105 ternary
c [cce-4] tried to eliminate 1687 small clauses 2%
c [cce-4] eliminated 699 small clauses 1%
c [cce-4] eliminated 98 binary clauses 0%
c [cce-4] eliminated 601 ternary clauses 1%
c [cce-4-1] eliminated 699 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 699 covered clauses in round 1
c [cce-4] eliminated 699 covered clauses in TOTAL during 1 rounds
c [simplification-5] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-5] removed 1015 irredundant clauses 0.8% (124127 remain 70%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 28888
c [simplification-5] penalized conflict interval 28888 = 1 * 28888
c [simplification-5] new conflict limit 59893
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   16.5    1087   124127     33200    6944  21625  2207   5 17.3  31.0    9
c -   18.2    1087   124127     40783    7942  21681  2209   5 17.3  30.6    9
c -   20.0    1087   124127     49030    9056  21787  2210   5 17.1  30.0    9
c -   21.8    1087   124127     57799   10028  21843  2210   5 17.5  30.4    9
c R   21.8    1087   124127     57915   10125  21844  2210   5 17.5  30.4    9
c 
c [simplification-6] limit of 59895 conflicts hit after 59900 conflicts
c [ternres-4] limit 11020052 with penalty 0 = 0 + 0
c [ternres-4] 475 schedulable variables 44%
c [ternres-4] 2971 ternary resolvents (0 bin, 2971 trn)
c [ternres-4] 317 variables remain 29% (770 retained)
c [card-3] limit 1377506 penalty 2 = 2 + 0
c [card-3] found 209 at-most-one constraints of average size 16.9
c [card-3] found 1217 at-most-two constraints of average size 8.2
c [card-3] using previous limit 1377506 for elimination
c [card-3] 1422 out of 1426 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 5510026 penalty 1 = 1 + 0
c [basicprobe-2-0] 266 probes remain 24% after last round
c [basicprobe-2-0] removed 0 variables, found 6 hbrs
c [unhide-3] limit 551002 with penalty 2 = 2 + 0
c [unhide-3-8] 0 units, 0 failed, 1726 tauts, 0 hbrs, 3870 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 177 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] allowing another 130846 steps for small clauses
c [cce-5] scheduling 75628 clauses = 36184 binary + 39444 ternary
c [cce-5] tried to eliminate 1596 small clauses 2%
c [cce-5] eliminated 409 small clauses 1%
c [cce-5] eliminated 88 binary clauses 0%
c [cce-5] eliminated 321 ternary clauses 1%
c [cce-5-1] eliminated 409 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 409 covered clauses in round 1
c [cce-5] eliminated 409 covered clauses in TOTAL during 1 rounds
c [elim-3] 1013 variables 93% will be scheduled this time
c [elim-3] scheduled 1013 variables 93%
c [elim-3] limit of 55100262 steps penalty 2 = 2 + 0
c [elim-3] incomplete 824 not tried 76% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 1087
c [rephase-2] after 59900 conflicts (new increment 40000, next 99900)
c [flushphases] 0 phases reset
c [simplification-6] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-6] removed 3670 irredundant clauses 3.0% (120457 remain 68%)
c [simplification-6] maximum reduction of 3% = max (0%, 3%)
c [simplification-6] geometric conflict interval increment 7222 = 28888 / 4
c [simplification-6] new conflict interval 36110
c [simplification-6] penalized conflict interval 36110 = 1 * 36110
c [simplification-6] new conflict limit 96010
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   26.0    1087   120457     67264   11177  24524  2109   5 17.4  30.2    9
c -   28.2    1087   120457     77558   12373  24607  2109   5 17.2  29.9    9
c -   30.7    1087   120457     88436   13610  24687  2110   5 17.1  29.9    9
c 
c [simplification-7] limit of 96012 conflicts hit after 96014 conflicts
c [ternres-5] limit 17716968 with penalty 0 = 0 + 0
c [ternres-5] 317 schedulable variables 29%
c [ternres-5] 2601 ternary resolvents (0 bin, 2601 trn)
c [ternres-5] 173 variables remain 16% (914 retained)
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 403 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 1087 variables 100%
c [block-3] limit of 44292422 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 [cce-6] limit of 35433937 steps penalty 0 = 0 + 0
c [cce-6-1] completed large round (ACCE)
c [cce-6-1] allowing another 129376 steps for small clauses
c [cce-6] scheduling 82044 clauses = 36890 binary + 45154 ternary
c [cce-6] tried to eliminate 1935 small clauses 2%
c [cce-6] eliminated 620 small clauses 1%
c [cce-6] eliminated 82 binary clauses 0%
c [cce-6] eliminated 538 ternary clauses 1%
c [cce-6-1] eliminated 620 small clauses in 35433938 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 620 covered clauses in round 1
c [cce-6] eliminated 620 covered clauses in TOTAL during 1 rounds
c [bca-3] limit of 10000000 steps
c [bca-3] 15 out of 2176 literals actually usable 1%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 19698 steps
c [simplification-7] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-7] removed 947 irredundant clauses 0.8% (119510 remain 67%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 18055 = 36110 / 2
c [simplification-7] new conflict interval 54165
c [simplification-7] penalized conflict interval 54165 = 1 * 54165
c [simplification-7] new conflict limit 150179
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.4    1087   119510    100044   14953  27931  2112   5 17.1  29.8   11
c -   37.0    1087   119510    112100   16260  28001  2112   5 17.0  29.7   11
c -   39.5    1087   119510    124834   17400  28047  2113   5 17.5  30.2   11
c R   39.7    1087   119510    126120   18509  28051  2113   5 17.5  30.3   12
c -   42.4    1087   119510    138254   18746  28133  2113   5 17.5  30.3   11
c 
c [simplification-8] limit of 150181 conflicts hit after 150185 conflicts
c [ternres-6] limit 27575481 with penalty 0 = 0 + 0
c [ternres-6] 173 schedulable variables 16%
c [ternres-6] 3367 ternary resolvents (0 bin, 3367 trn)
c [ternres-6] 86 variables remain 8% (1001 retained)
c [gauss-3] limit 1378774 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 [simpleprobe-3] 573 schedulable variables 53%
c [simpleprobe-3] limit 55150963 penalty 1 = 1 + 0
c [simpleprobe-3] 61 variables remain 6% (1026 retained)
c [simpleprobe-3] removed 0 variables, found 370 hbrs, 0 units
c [cgrclsr-3] limit 689387 penalty 2 = 2 + 0
c [cgrclsr-3] 264 schedulable variables 24%
c [cgrclsr-3] fully completed congruence closure
c [lift-3] limit 4136322 with penalty 2 = 2 + 0
c [lift-3] using 1014 probes 93%
c [lift-3] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-3] 883 variables remain 81% (204 retained)
c [cliff-3] limit of 5515096 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 347 transitive binary clauses
c [cce-7] limit of 55150963 steps penalty 0 = 0 + 0
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] allowing another 131706 steps for small clauses
c [cce-7] scheduling 81180 clauses = 36576 binary + 44604 ternary
c [cce-7] tried to eliminate 2742 small clauses 3%
c [cce-7] eliminated 879 small clauses 1%
c [cce-7] eliminated 138 binary clauses 0%
c [cce-7] eliminated 741 ternary clauses 2%
c [cce-7-1] eliminated 879 small clauses in 55150964 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 879 covered clauses in round 1
c [cce-7] eliminated 879 covered clauses in TOTAL during 1 rounds
c [rephase-3] after 150185 conflicts (new increment 80000, next 230185)
c [flushphases] 0 phases reset
c [simplification-8] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-8] removed 1129 irredundant clauses 0.9% (118381 remain 67%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 27082 = 54165 / 2
c [simplification-8] new conflict interval 81247
c [simplification-8] penalized conflict interval 81247 = 1 * 81247
c [simplification-8] new conflict limit 231432
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   47.9    1087   118381    152594   20242  32317  2524   5 17.4  30.0   12
c -   51.4    1087   118381    167405   21752  32413  2524   5 17.3  29.9   12
c -   54.7    1087   118381    183312   23170  32483  2525   5 17.3  29.9   12
c -   58.5    1087   118381    199468   24843  32562  2525   5 17.2  29.7   12
c -   62.3    1087   118381    217017   26471  32660  2525   5 17.5  30.0   12
c 
c [simplification-9] limit of 231432 conflicts hit after 231434 conflicts
c [ternres-7] limit 43058442 with penalty 0 = 0 + 0
c [ternres-7] 86 schedulable variables 8%
c [ternres-7] 4485 ternary resolvents (0 bin, 4485 trn)
c [ternres-7] 46 variables remain 4% (1041 retained)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 215 transitive binary clauses
c [cce-8] limit of 86116884 steps penalty 0 = 0 + 0
c [cce-8-1] completed large round (ACCE)
c [cce-8-1] allowing another 133916 steps for small clauses
c [cce-8] scheduling 74310 clauses = 36301 binary + 38009 ternary
c [cce-8] tried to eliminate 4468 small clauses 6%
c [cce-8] eliminated 1112 small clauses 1%
c [cce-8] eliminated 400 binary clauses 1%
c [cce-8] eliminated 712 ternary clauses 2%
c [cce-8-1] eliminated 1112 small clauses in 86116885 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 1112 covered clauses in round 1
c [cce-8] eliminated 1112 covered clauses in TOTAL during 1 rounds
c [rephase-4] after 231434 conflicts (new increment 160000, next 391434)
c [flushphases] 0 phases reset
c [simplification-9] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-9] removed 1260 irredundant clauses 1.1% (117121 remain 66%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 40623 = 81247 / 2
c [simplification-9] new conflict interval 121870
c [simplification-9] penalized conflict interval 121870 = 1 * 121870
c [simplification-9] new conflict limit 353304
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   68.4    1087   117121    234575   28203  37937  2858   5 17.3  29.8   12
c -   72.3    1087   117121    253209   29722  38009  2859   5 17.6  30.2   12
c -   76.1    1087   117121    271992   31448  38061  2862   5 17.6  30.1   12
c R   76.3    1087   117121    272864   32183  38063  2862   5 17.5  30.1   13
c -   80.6    1087   117121    291176   33191  38153  2862   5 17.5  30.0   13
c -   85.3    1087   117121    311269   34973  38252  2864   5 17.4  30.0   13
c -   90.0    1087   117121    332155   36675  38338  2864   5 17.4  29.9   13
c 
c [simplification-10] limit of 353306 conflicts hit after 353308 conflicts
c [ternres-8] limit 66062242 with penalty 0 = 0 + 0
c [ternres-8] 46 schedulable variables 4%
c [ternres-8] 7883 ternary resolvents (2 bin, 7881 trn)
c [ternres-8] 14 variables remain 1% (1073 retained)
c [card-4] limit 4128890 penalty 3 = 3 + 0
c [card-4] found 220 at-most-one constraints of average size 16.6
c [card-4] found 1506 at-most-two constraints of average size 7.8
c [card-4] using previous limit 4128890 for elimination
c [card-4] 1726 out of 1726 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1651556 with penalty 3 = 3 + 0
c [unhide-4-11] 0 units, 0 failed, 1409 tauts, 0 hbrs, 13620 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 115 transitive binary clauses
c [cce-9] limit of 132124485 steps penalty 0 = 0 + 0
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] allowing another 135080 steps for small clauses
c [cce-9] scheduling 79391 clauses = 35784 binary + 43607 ternary
c [cce-9] tried to eliminate 6680 small clauses 8%
c [cce-9] eliminated 1726 small clauses 2%
c [cce-9] eliminated 328 binary clauses 1%
c [cce-9] eliminated 1398 ternary clauses 3%
c [cce-9-1] eliminated 1726 small clauses in 132124486 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1726 covered clauses in round 1
c [cce-9] eliminated 1726 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 1087 variables 100%
c [elim-4] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-4] incomplete 536 not tried 49% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 0 = 0% variables out of 1087
c [simplification-10] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-10] removed 2523 irredundant clauses 2.2% (114598 remain 65%)
c [simplification-10] maximum reduction of 2% = max (0%, 2%)
c [simplification-10] geometric conflict interval increment 40623 = 121870 / 3
c [simplification-10] new conflict interval 162493
c [simplification-10] penalized conflict interval 162493 = 1 * 162493
c [simplification-10] new conflict limit 515801
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   99.9    1087   114598    353904   38731  47078  2715   5 17.3  29.7   14
c -  105.0    1087   114598    376296   40771  47199  2715   5 17.3  29.8   14
c -  110.1    1087   114598    399338   42598  47294  2715   5 17.3  29.8   14
c -  115.7    1087   114598    422749   44748  47409  2715   6 17.4  29.9   14
c -  121.4    1087   114598    447254   46853  47519  2716   5 17.5  30.0   14
c -  127.3    1087   114598    472317   48960  47629  2717   5 17.4  29.9   14
c -  133.4    1087   114598    497880   51062  47757  2718   5 17.4  30.0   14
c 
c [simplification-11] limit of 515801 conflicts hit after 515801 conflicts
c [ternres-9] limit 97527347 with penalty 0 = 0 + 0
c [ternres-9] 14 schedulable variables 1%
c [ternres-9] 12778 ternary resolvents (4 bin, 12774 trn)
c [ternres-9] 4 variables remain 0% (1083 retained)
c [treelook-3] limit 1219091 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 2162 literals 99%
c [treelook-3] scheduling used 729248 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1219091 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1231964 steps
c [treelook-3] 2113 literals remain 97%
c [treelook-3] 1074 variables remain to probed next time 99%
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 284 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 1087 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-10] limit of 195054695 steps penalty 0 = 0 + 0
c [cce-10-1] completed large round (ACCE)
c [cce-10-1] allowing another 136659 steps for small clauses
c [cce-10] scheduling 72734 clauses = 36104 binary + 36630 ternary
c [cce-10] tried to eliminate 9936 small clauses 14%
c [cce-10] eliminated 1342 small clauses 2%
c [cce-10] eliminated 429 binary clauses 1%
c [cce-10] eliminated 913 ternary clauses 2%
c [cce-10-1] eliminated 1342 small clauses in 195054696 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 1342 covered clauses in round 1
c [cce-10] eliminated 1342 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps
c [bca-4] 2 out of 2176 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 65457 steps
c [rephase-5] after 515801 conflicts (new increment 320000, next 835801)
c [flushphases] 0 phases reset
c [simplification-11] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-11] removed 1570 irredundant clauses 1.4% (113028 remain 64%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 81246 = 162493 / 2
c [simplification-11] new conflict interval 243739
c [simplification-11] penalized conflict interval 243739 = 1 * 243739
c [simplification-11] new conflict limit 759540
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  143.5    1087   113028    524138   53254  61539  3097   5 17.4  29.9   15
c -  149.5    1087   113028    552941   55117  61625  3100   6 17.9  30.6   16
c -  156.0    1087   113028    583884   56938  61690  3101   6 18.6  31.6   16
c -  162.7    1087   113028    616273   58728  61760  3101   5 19.3  32.5   16
c -  169.8    1087   113028    649842   60537  61832  3103   6 20.0  33.5   16
c -  177.3    1087   113028    684150   62444  61906  3106   6 20.8  34.6   16
c -  184.4    1087   113028    719532   64301  61979  3109   6 21.5  35.6   16
c -  192.3    1087   113028    757211   66047  62038  3113   5 22.4  36.7   17
c 
c [simplification-12] limit of 759542 conflicts hit after 759543 conflicts
c [ternres-10] limit 140009578 with penalty 0 = 0 + 0
c [ternres-10] 4 schedulable variables 0%
c [ternres-10] 20048 ternary resolvents (22 bin, 20026 trn)
c [ternres-10] 1 variables remain 0% (1086 retained)
c [gauss-4] limit 3500239 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 1087 free variables schedulable
c [cgrclsr-4] 302 variables remain 28% (785 retained)
c [lift-4] limit 2500000 with penalty 3 = 3 + 0
c [lift-4] using 883 probes 81%
c [lift-4] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-4] 812 variables remain 75% (275 retained)
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 187 transitive binary clauses
c [cce-11] limit of 280019157 steps penalty 0 = 0 + 0
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] allowing another 140524 steps for small clauses
c [cce-11] scheduling 77143 clauses = 35583 binary + 41560 ternary
c [cce-11] tried to eliminate 13746 small clauses 18%
c [cce-11] eliminated 2679 small clauses 3%
c [cce-11] eliminated 453 binary clauses 1%
c [cce-11] eliminated 2226 ternary clauses 5%
c [cce-11-1] eliminated 2679 small clauses in 280019158 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 2679 covered clauses in round 1
c [cce-11] eliminated 2679 covered clauses in TOTAL during 1 rounds
c [simplification-12] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-12] removed 2791 irredundant clauses 2.5% (110237 remain 62%)
c [simplification-12] maximum reduction of 2% = max (0%, 2%)
c [simplification-12] geometric conflict interval increment 81246 = 243739 / 3
c [simplification-12] new conflict interval 324985
c [simplification-12] penalized conflict interval 324985 = 1 * 324985
c [simplification-12] new conflict limit 1084528
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  206.5    1087   110237    792623   68120  84382  3518   6 22.6  37.1   19
c -  215.0    1087   110237    830533   70191  84449  3522   5 23.0  37.4   19
c -  223.1    1087   110237    865422   71945  84514  3523   5 23.1  37.5   19
c -  231.0    1087   110237    899129   73867  84584  3525   5 23.0  37.4   20
c -  240.7    1087   110237    937732   75381  84615  3526   6 23.3  37.6   20
c -  248.6    1087   110237    973059   77155  84672  3528   6 23.3  37.7   20
c -  256.6    1087   110237   1009270   79055  84737  3529   6 23.4  37.8   20
c -  264.3    1087   110237   1044807   80975  84803  3531   6 23.3  37.7   20
c 
c [simplification-13] limit of 1084530 conflicts hit after 1084531 conflicts
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] 1 schedulable variables 0%
c [ternres-11] 26725 ternary resolvents (99 bin, 26626 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 163 transitive binary clauses
c [cce-12] limit of 403712673 steps penalty 0 = 0 + 0
c [cce-12-1] completed large round (ACCE)
c [cce-12-1] allowing another 146978 steps for small clauses
c [cce-12] scheduling 70762 clauses = 35072 binary + 35690 ternary
c [cce-12] tried to eliminate 19268 small clauses 27%
c [cce-12] eliminated 2186 small clauses 3%
c [cce-12] eliminated 583 binary clauses 2%
c [cce-12] eliminated 1603 ternary clauses 4%
c [cce-12-1] eliminated 2186 small clauses in 403712674 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 2186 covered clauses in round 1
c [cce-12] eliminated 2186 covered clauses in TOTAL during 1 rounds
c [rephase-6] after 1084531 conflicts (new increment 640000, next 1724531)
c [flushphases] 0 phases reset
c [simplification-13] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-13] removed 2273 irredundant clauses 2.1% (107964 remain 61%)
c [simplification-13] maximum reduction of 2% = max (0%, 2%)
c [simplification-13] geometric conflict interval increment 108328 = 324985 / 3
c [simplification-13] new conflict interval 433313
c [simplification-13] penalized conflict interval 433313 = 1 * 433313
c [simplification-13] new conflict limit 1517844
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  281.7    1087   107964   1085280   82735 113096  4139   5 23.5  37.9   23
c -  290.3    1087   107964   1122922   84891 113158  4139   6 23.4  37.9   24
c -  300.4    1087   107964   1163391   86834 113212  4139   5 23.5  38.0   24
c -  309.6    1087   107964   1202424   88757 113278  4141   6 23.5  38.0   24
c -  318.4    1087   107964   1241000   90707 113330  4144   6 23.4  38.0   24
c -  327.2    1087   107964   1282275   92726 113394  4147   6 23.5  38.0   24
c -  337.3    1087   107964   1324887   94853 113471  4147   6 23.5  38.1   24
c -  347.7    1087   107964   1368064   96698 113523  4149   5 23.5  38.2   24
c -  358.3    1087   107964   1410256   98737 113585  4151   6 23.5  38.2   24
c -  368.2    1087   107964   1452456  100870 113634  4152   6 23.4  38.1   24
c -  379.6    1087   107964   1502698  102795 113688  4152   5 23.7  38.5   25
c 
c [simplification-14] limit of 1517844 conflicts hit after 1517844 conflicts
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 1087 free variables schedulable
c [ternres-12] 23069 ternary resolvents (53 bin, 23016 trn)
c [ternres-12] 243 variables remain 22% (844 retained)
c [basicprobe-3] limit 25000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 266 sched 24%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 127 transitive binary clauses
c [cce-13] limit of 573427193 steps penalty 0 = 0 + 0
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] allowing another 149093 steps for small clauses
c [cce-13] scheduling 73774 clauses = 34464 binary + 39310 ternary
c [cce-13] tried to eliminate 26507 small clauses 36%
c [cce-13] eliminated 3093 small clauses 4%
c [cce-13] eliminated 457 binary clauses 1%
c [cce-13] eliminated 2636 ternary clauses 7%
c [cce-13-1] eliminated 3093 small clauses in 573427194 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 3093 covered clauses in round 1
c [cce-13] eliminated 3093 covered clauses in TOTAL during 1 rounds
c [simplification-14] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-14] removed 3137 irredundant clauses 2.9% (104827 remain 59%)
c [simplification-14] maximum reduction of 3% = max (0%, 3%)
c [simplification-14] geometric conflict interval increment 108328 = 433313 / 4
c [simplification-14] new conflict interval 541641
c [simplification-14] penalized conflict interval 541641 = 1 * 541641
c [simplification-14] new conflict limit 2059485
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  400.3    1087   104827   1546815  104906 139397  4581   5 23.7  38.4   27
c -  411.5    1087   104827   1592703  107461 139479  4583   5 23.6  38.4   27
c -  422.7    1087   104827   1638828  109550 139546  4586   5 23.6  38.4   27
c -  434.4    1087   104827   1685637  111489 139600  4589   5 23.6  38.3   28
c -  446.3    1087   104827   1735303  113668 139691  4590   6 23.7  38.5   28
c -  459.3    1087   104827   1787725  115736 139763  4591   5 23.9  38.7   28
c -  471.8    1087   104827   1836953  117806 139801  4591   5 23.8  38.7   28
c -  484.6    1087   104827   1887916  119817 139860  4592   6 23.9  38.7   28
c -  496.9    1087   104827   1939501  122066 139931  4597   5 23.9  38.7   28
c -  512.4    1087   104827   1999149  124518 140007  4600   5 24.1  39.1   28
c -  525.3    1087   104827   2049837  126826 140074  4605   6 24.1  39.0   28
c 
c [simplification-15] limit of 2059487 conflicts hit after 2059487 conflicts
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] 243 schedulable variables 22%
c [ternres-13] 24279 ternary resolvents (50 bin, 24229 trn)
c [ternres-13] 123 variables remain 11% (964 retained)
c [card-5] limit 12420144 penalty 4 = 4 + 0
c [card-5] found 205 at-most-one constraints of average size 18.6
c [card-5] found 1643 at-most-two constraints of average size 8.7
c [card-5] using previous limit 12420144 for elimination
c [card-5] 1848 out of 1848 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [unhide-5] limit 1250000 with penalty 4 = 4 + 0
c [unhide-5-13] 0 units, 0 failed, 1780 tauts, 0 hbrs, 8900 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 93 transitive binary clauses
c [cce-14] limit of 794889267 steps penalty 0 = 0 + 0
c [cce-14-1] completed large round (ACCE)
c [cce-14-1] allowing another 148996 steps for small clauses
c [cce-14] scheduling 67967 clauses = 33959 binary + 34008 ternary
c [cce-14] tried to eliminate 37703 small clauses 55%
c [cce-14] eliminated 2184 small clauses 3%
c [cce-14] eliminated 475 binary clauses 1%
c [cce-14] eliminated 1709 ternary clauses 5%
c [cce-14-1] eliminated 2184 small clauses in 794889268 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 2184 covered clauses in round 1
c [cce-14] eliminated 2184 covered clauses in TOTAL during 1 rounds
c [elim-5] 534 variables 49% will be scheduled this time
c [elim-5] scheduled 534 variables 49%
c [elim-5] limit of 50000000 steps penalty 4 = 4 + 0
c [elim-5] incomplete 263 not tried 24% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 1087
c [rephase-7] after 2059487 conflicts (new increment 1280000, next 3339487)
c [flushphases] 0 phases reset
c [simplification-15] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-15] removed 2386 irredundant clauses 2.3% (102441 remain 58%)
c [simplification-15] maximum reduction of 2% = max (0%, 2%)
c [simplification-15] geometric conflict interval increment 180547 = 541641 / 3
c [simplification-15] new conflict interval 722188
c [simplification-15] penalized conflict interval 722188 = 1 * 722188
c [simplification-15] new conflict limit 2781675
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  554.8    1087   102441   2101872  129231 164723  4702   6 24.0  38.9   31
c -  567.5    1087   102441   2154069  131759 164826  4704   5 24.0  38.8   31
c -  579.9    1087   102441   2205482  134284 164901  4705   5 23.9  38.7   31
c -  593.1    1087   102441   2261485  136936 164987  4707   5 23.9  38.8   31
c -  607.2    1087   102441   2317435  139553 165068  4711   6 23.9  38.8   31
c -  620.3    1087   102441   2371906  142057 165140  4719   5 23.9  38.8   31
c -  635.9    1087   102441   2434346  144453 165226  4721   5 24.0  38.9   31
c -  650.0    1087   102441   2490371  146993 165311  4726   6 24.0  38.9   31
c -  665.9    1087   102441   2553869  149256 165383  4729   5 24.1  39.1   32
c -  679.6    1087   102441   2609555  151577 165480  4733   5 24.1  39.0   31
c -  697.8    1087   102441   2680460  153724 165554  4735   6 24.3  39.4   32
c -  713.7    1087   102441   2745920  155912 165609  4738   6 24.5  39.6   32
c 
c [simplification-16] limit of 2781677 conflicts hit after 2781678 conflicts
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] 123 schedulable variables 11%
c [ternres-14] 27229 ternary resolvents (113 bin, 27116 trn)
c [ternres-14] 76 variables remain 7% (1011 retained)
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 178 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 1087 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-15] limit of 1089935099 steps penalty 0 = 0 + 0
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] allowing another 150686 steps for small clauses
c [cce-15] scheduling 70122 clauses = 33740 binary + 36382 ternary
c [cce-15] tried to eliminate 50927 small clauses 73%
c [cce-15] eliminated 2482 small clauses 4%
c [cce-15] eliminated 273 binary clauses 1%
c [cce-15] eliminated 2209 ternary clauses 6%
c [cce-15-1] eliminated 2482 small clauses in 1089935100 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 2482 covered clauses in round 1
c [cce-15] eliminated 2482 covered clauses in TOTAL during 1 rounds
c [bca-5] limit of 10000000 steps
c [bca-5] 1 out of 2176 literals actually usable 0%
c [bca-5] not enough literals usable
c [bca-5] added 0 blocked clauses in 178486 steps
c [simplification-16] removed 0 variables 0.0% (1087 remain 100%)
c [simplification-16] removed 2562 irredundant clauses 2.5% (99879 remain 56%)
c [simplification-16] maximum reduction of 3% = max (0%, 3%)
c [simplification-16] geometric conflict interval increment 180547 = 722188 / 4
c [simplification-16] new conflict interval 902735
c [simplification-16] penalized conflict interval 902735 = 1 * 902735
c [simplification-16] new conflict limit 3684413
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  748.2    1087    99879   2813626  157789 194990  5028   6 24.8  40.1   36
c -  764.8    1087    99879   2877723  159644 195051  5030   5 24.9  40.2   36
c -  783.1    1087    99879   2946850  162471 195141  5033   5 25.0  40.5   36
c -  802.5    1087    99879   3014425  164871 195221  5037   5 25.1  40.7   36
c -  819.1    1087    99879   3079431  167095 195283  5040   5 25.2  40.7   36
c -  837.9    1087    99879   3152143  169188 195332  5044   6 25.4  41.0   36
c -  854.9    1087    99879   3216540  171622 195398  5051   5 25.3  41.0   36
c -  873.4    1087    99879   3283786  174115 195470  5053   6 25.3  41.0   35
c -  890.8    1087    99879   3350580  176625 195547  5055   5 25.3  41.0   35
c -  910.3    1087    99879   3422817  179527 195617  5066   5 25.4  41.1   36
c -  931.5    1087    99879   3501257  181944 195678  5073   6 25.7  41.5   36
c -  950.5    1087    99879   3569054  184516 195756  5080   6 25.6  41.4   36
c -  970.5    1087    99879   3639058  186952 195832  5083   5 25.6  41.4   36
c 
c [simplification-17] limit of 3684413 conflicts hit after 3684413 conflicts
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] 76 schedulable variables 7%
c [ternres-15] 27350 ternary resolvents (41 bin, 27309 trn)
c [ternres-15] 45 variables remain 4% (1042 retained)
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 61 schedulable variables 6%
c [simpleprobe-4] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-4] 11 variables remain 1% (1076 retained)
c [simpleprobe-4] removed 0 variables, found 161 hbrs, 0 units
c [cgrclsr-5] limit 500000 penalty 4 = 4 + 0
c [cgrclsr-5] 302 schedulable variables 28%
c [cgrclsr-5] fully completed congruence closure
c [lift-5] limit 1250000 with penalty 4 = 4 + 0
c [lift-5] using 812 probes 75%
c [lift-5] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-5] 782 variables remain 72% (305 retained)
c [cliff-5] limit of 6250000 steps penalty 4 = 4 + 0
c [cliff-5] failed 0, lifted 0
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 167 transitive binary clauses
c [cce-16] limit of 1484537811 steps penalty 0 = 0 + 0
c [cce-16-1] completed large round (ACCE)
c [cce-16-1] allowing another 152120 steps for small clauses
c [cce-16] scheduling 67631 clauses = 33464 binary + 34167 ternary
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: 5 count, 0 added (0 skipped), 270937 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: 5 bces, 0 removed, 1689643 resolutions, 5890665 steps
c blkd: 72 blocking literals 3%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 0 am1, 31849994 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 29440 subsumed
c card: 800 at-most-one constraints found, average size 18.92
c card: 800 at-most-one constraints used 100%, average size 18.92
c card: 6329 at-most-two constraints found, average size 7.96
c card: 6324 at-most-two constraints used 100%, average size 7.97
c cces: 16 cces, 33219 eliminated, 33072 ate 100%, 147 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: 5 count, 2678688 esteps, 4335961 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: 1098 extracted (1098 ands 100%, 0 xors 0%, 0 ites 0%)
c clff: 5 cliffs, 0 lifted, 0 failed
c clff: 4216 decisions, 39806742 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 641685 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 54 gcs, 0 rescored clauses, 1927 rescored vars
c dcps: 22 decompositions, 0 equivalent 0%
c deco: 732162 decision-only clauses 20%, 63% reduction
c decs: 8479985 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 31590 flipped 0.373% (in 433 phases)
c elms: 5 elims, 0 eliminated 0%
c elms: 5 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 3484 subsumed, 3526 strengthened, 0 blocked
c elms: 922069 copies, 908419 resolutions, 0 ipos
c elms: 7213953 subchks, 2582058 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 22103732 steps, 11051866 extr 50%, 0 elim 0%
c glue: 25.6 orig avg, 24.3 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 3629 = 688 simple + 2941 trn 19% + 0 lrg 81%, 2857 sub 0%
c hght: 41 average, 1.62 height/glue
c ints: 94968 luby (27520788 steps), 0 inout (0 steps)
c lift: 5 phases, 1830 probed (610 level1 33%, 1220 level2 67%)
c lift: 0 units, 0 equivalences, 0 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3664232 clauses, 52.5 length
c lrnd: 1353168 uips 37%, 1850750 flips 51%
c mega: 0 count, 0 failed, 0 rounds
c mins: 192531522 learned lits, 42% minimized
c mins: 2846109 mins 78%, 1 bin 0%, 85960 size 2%, 732162 deco 20%
c move: moved 3664232, 6017 bin 0%, 28138 trn 1%, 0 lrg 0%
c otfs: str 70221 dyn (70039 red, 182 irr) 20181 drv 29%, 50040 rst 71%
c otfs: sub 610 dyn (610 red, 0 irr)
c phas: 1 computed, 1087 set, 0 pos (0%), 1087 neg (100%)
c prbs: 3 basic, 1990 probed, 0 failed, 0 lifted
c prbs: 4 simple, 3412 probed, 2 failed, 0 eqs
c prbs: 3 treelook, 72 probed, 0 failed, 0 lifted
c prps: 533204435 props, 63 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 126981069 searches, 24432594 hits, 19% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 97 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 97 arith 100%, 0 double 0%
c rmbd: 36564 removed, 719 red 2%
c rphs: 7 recomputed phases
c rsts: 14858 restarts 16%, 80110 skipped 84%
c rsts: 78585 saturating 98%, 0 agile 0%, 1525 reuse 2%
c rsts: 242.3 avg interval, 242.3 scaled, 1.0 factor
c rsts: 11630 kept 78.3% average 33.1%
c simp: 17 count (17 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 3664232 count (3664604 tried 1.0), 912415 sub out of 3656689 (25.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: 2 fixed 0%, 0 its, 0.00 confs/it
c trvs: 102012334082 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 191.4 search traversals per propagation, 27671.3 per conflict
c trvs: 1.4 search traversals per search visit
c trds: 15 transitive reductions, 3559 removed, 0 failed
c trds: 22735 nodes, 378079 edges, 28600745 steps
c trim: 23315285 words, 88.9 MB
c trnr: 15 count, 384 bin, 192349 trn, 1432688964 steps
c unhd: 5 count, 13 rounds, 4819541 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: 6980 tauts, 22 bin 0%, 3635 trn 52%, 0 lrg 0%
c unhd: 6980 tauts, 3323 stamp 48%, 4342 red 62%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 29129 str, 0 bin 0%, 4816 trn 17%, 24313 lrg 83%, 25547 red 88%
c vars: 1087 remaining 100% and 2 removed 0% out of 1089
c vars: 2 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 74286880471 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 139.3 search visits per propagation, 20146.2 per conflict
c wchs: 3556949342 pushed, 917662 enlarged, 357 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   3656689 100   2520889 100  26376727 100  12864489 100   1616688 100
c 
c  0     138719   4         0   0   7915712  30   1751263  14     76697   5 
c  1      54529   1      2083   0   1650521   6    467100   4     84908   5 
c  2     175714   5    161530   6   1373354   5    621340   5     84784   5 
c  3     582891  16    536215  21   4713173  18<  2227589  17    362589  22 
c  4     819018  22    726911  29<  5860848  22   3019860  23<   449399  28<
c  5     799318  22<   717168  28   2850881  11   2307071  18    296891  18 
c  6     477647  13    239714  10   1007408   4   1150459   9    132517   8 
c  7     312473   9     74110   3    533149   2    689473   5     68042   4 
c  8     196816   5     42107   2    315286   1    422064   3     40971   3 
c  9      78138   2     16259   1    123198   0    163948   1     15716   1 
c 10      21117   1      4699   0     32728   0     43716   0      4123   0 
c 11        309   0        93   0       469   0       606   0        51   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             4.6           4.3           2.7           3.8           4.0
c std             1.9           1.3           2.2           2.2           1.8
c 
c   57.385   6% cce
c   34.750   3% analysis
c   21.560   2% ternres
c    8.966   1% mincls
c    7.301   1% bump
c    7.028   1% decide
c    6.906   1% transred
c    5.499   1% defrag
c    4.035   0% card
c    1.839   0% elim
c    1.738   0% decomp
c    1.695   0% gc
c    1.426   0% probe
c    1.024   0% unhide
c    0.836   0% reduce
c    0.806   0% cgrclsr
c    0.626   0% cliff
c    0.556   0% lift
c    0.325   0% block
c    0.296   0% restart
c    0.271   0% gauss
c    0.031   0% bca
c    0.012   0% phase
c    0.002   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    1.136   0% probe simple     80%
c    0.152   0% probe basic      11%
c    0.138   0% probe tree-look  10%
c ==================================
c    0.969   0% preprocessing     1%
c   97.722  10% inprocessing     99%
c ==================================
c   98.691  10% simplifying
c  901.256  90% search
c ==================================
c  999.947 100% all
c 
c 8479985 decisions, 8480.4 decisions/sec
c 3684413 conflicts, 3684.6 conflicts/sec
c 533204435 propagations, 0.5 megaprops/sec
c 999.9 seconds, 75.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
