c launch: /data/cnf/sc2014/app/reg_s_2_unknown.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/reg_s_2_unknown.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/reg_s_2_unknown.cnf.bz2
c no embedded options
c found 'p cnf 235620 1695584' header
c read 235620 variables, 1695584 clauses, 5555127 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 235620 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  235620  1695584         0       0      0     0   0  0.0   0.0  102
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 [decomp-1] removed 56 variables
c [simpleprobe-1] all 235564 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 1 variables
c [simpleprobe-1] 162768 variables remain 69% (72795 retained)
c [simpleprobe-1] removed 1 variables, found 30777 hbrs, 0 units
c [unhide-1] limit 847735 based on 1695470 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 11970 tauts, 0 hbrs, 42964 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 235563 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] eliminated 2045 variables 1% in round 1 in 196431044 steps
c [elim-1-1] backward subsumption/strengthening limit 392862088
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 84660661 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2045 = 1% variables out of 235563
c [phase-1] phase bias: 104646 positive 45%, 128872 negative 55%
c [simplification-1] removed 2102 variables 0.9% (233518 remain 99%)
c [simplification-1] removed 12608 irredundant clauses 0.7% (1682976 remain 99%)
c [simplification-1] maximum reduction of 1% = max (1%, 1%)
c [simplification-1] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-1] new conflict interval 10000
c [simplification-1] penalized conflict interval 20000 = 2 * 10000
c [simplification-1] new conflict limit 20000
c [cut-width] 207637, max 350806, min4 91299 at 25%, min10 71162 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   10.3  233518  1682976         5       5      0 28825   4  4.6  53.9  110
c R   10.3  233518  1682976        21      20      1 28825   7  4.0  42.6  110
c R   10.3  233518  1682976        62      55      5 28825  14  3.7  49.7  110
c R   10.3  233518  1682976       167     158      6 28825  17  4.2  38.5  110
c R   10.4  233518  1682976       416     387     14 28836  18  4.5  34.3  110
c R   10.6  233518  1682976      1020     956     26 28843  21  5.4  29.6  110
c R   11.0  233518  1682976      2327    2190     60 28863  20  5.5  36.2  112
c R   12.0  233518  1682976      5271    4934    147 28931  22  5.5  31.2  112
c -   12.3  233518  1682976      5916    3537    165 28937  17  5.5  29.3  112
c -   13.9  233518  1682976     10214    5144    240 28998  19  5.6  30.5  112
c R   14.3  233518  1682976     11792    6633    271 29024  20  5.8  32.4  113
c -   15.6  233518  1682976     14986    6669    327 29052  18  5.8  29.4  112
c -   18.2  233518  1682976     20396    8309    416 29117  20  5.9  27.9  112
c 
c [simplification-2] limit of 20586 conflicts hit after 20587 conflicts
c [simpleprobe-2] 161408 schedulable variables 69%
c [simpleprobe-2] limit 7394539 penalty 0 = 0 + 0
c [simpleprobe-2] 124354 variables remain 53% (109164 retained)
c [simpleprobe-2] removed 0 variables, found 7556 hbrs, 0 units
c [treelook-1] limit 420744 based on 1682976 irredundant clauses
c [treelook-1] scheduled 48071 literals 10%
c [treelook-1] scheduling used 420747 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 420744 based on 1682976 irredundant clauses
c [treelook-1] used 424504 steps
c [treelook-1] 47937 literals remain 10%
c [treelook-1] 41396 variables remain to probed next time 18%
c [treelook-1] removed 0 variables, found 2463 hbrs
c [basicprobe-1] limit 3365952 based on 1682976 irredundant clauses
c [basicprobe-1-0] 3795 probes remain 2% after last round
c [basicprobe-1-0] removed 0 variables, found 21308 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 233518 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] eliminated 19 clauses out of 20 (95%) of length 6
c [cce-1-1] eliminated 43 clauses out of 59 (73%) of length 5
c [cce-1-1] eliminated 1685 clauses out of 885412 (0%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1747 large clauses in 300000001 steps
c [cce-1-1] allowing another 150000000 steps for small clauses
c [cce-1] scheduling 504540 clauses = 449691 binary + 54849 ternary
c [cce-1] tried to eliminate 10921 small clauses 2%
c [cce-1] eliminated 2763 small clauses 1%
c [cce-1] eliminated 2497 binary clauses 1%
c [cce-1] eliminated 266 ternary clauses 0%
c [cce-1-1] eliminated 2763 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4510 covered clauses in round 1
c [cce-1] eliminated 4510 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 233518 variables 100%
c [elim-2] limit of 36972695 steps penalty 0 = 0 + 0
c [elim-2] incomplete 106297 not tried 46% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 90 = 0% variables out of 233518
c [elim-2] 90 < 1/1000 * 233518 = 233 considered unsuccessful
c [bca-1] limit of 10000000 steps
c [bca-1] 431251 out of 466858 literals actually usable 92%
c [bca-1] added 9 blocked clauses in 895740 steps
c [rephase-1] after 20587 conflicts (new increment 20000, next 40587)
c [flushphases] 173735 phases reset
c [phase-2] phase bias: 3465 positive 47%, 3940 negative 53%
c [simplification-2] removed 90 variables 0.0% (233428 remain 99%)
c [simplification-2] removed 4562 irredundant clauses 0.3% (1678414 remain 99%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 30000
c [simplification-2] penalized conflict interval 60000 = 2 * 30000
c [simplification-2] new conflict limit 80587
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   39.0  233428  1678414     26197   13915    750 62385  18  6.1  29.5  115
c -   39.1  233428  1678414     26248    9967    750 62385  13  6.1  29.5  113
c -   42.1  233428  1678414     33227   12137    879 62432  17  6.0  27.8  113
c -   44.8  233428  1678414     40233   13880    983 62476  21  6.2  31.5  114
c -   47.9  233428  1678414     47959   15811   1056 62514  19  6.3  30.0  115
c -   50.8  233428  1678414     56110   17773   1137 62553  21  6.5  36.7  115
c R   51.3  233428  1678414     57532   19149   1154 62562  20  6.5  37.1  116
c -   54.6  233428  1678414     64961   19810   1227 62595  17  6.6  35.0  115
c -   59.0  233428  1678414     74418   21952   1328 62647  21  6.6  34.3  115
c 
c [simplification-3] limit of 81237 conflicts hit after 81237 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 38493830 with penalty 0 = 0 + 0
c [ternres-1] all 233428 free variables schedulable
c [ternres-1] 243 ternary resolvents (0 bin, 243 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1924691 penalty 1 = 1 + 0
c [card-2] found 4720 at-most-one constraints of average size 3.9
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1924691 for elimination
c [card-2] 4720 out of 4720 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 1 xors of average arity 2.0
c [gauss-1] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-6] removed 3 variables
c [cgrclsr-1] limit 839207 based on 1678414 irredundant clauses
c [cgrclsr-1] all 233425 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 4619260 with penalty 0 = 0 + 0
c [lift-1] using 233010 probes 100%
c [lift-1] 0 units, 25 impls, 9 eqs in 1 rounds
c [lift-1] 233224 variables remain 100% (192 retained)
c [lift-1] removed 9 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [unhide-2] limit 839207 based on 1678414 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 24193 tauts, 0 hbrs, 267540 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 2798 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 5 clauses out of 6 (83%) of length 6
c [cce-2-1] eliminated 40 clauses out of 59 (68%) of length 5
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 45 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 741604 clauses = 463142 binary + 278462 ternary
c [cce-2] tried to eliminate 825 small clauses 0%
c [cce-2] eliminated 206 small clauses 0%
c [cce-2] eliminated 143 binary clauses 0%
c [cce-2] eliminated 63 ternary clauses 0%
c [cce-2-1] eliminated 206 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 251 covered clauses in round 1
c [cce-2] eliminated 251 covered clauses in TOTAL during 1 rounds
c [cce-2] 251 < 1/1000 * 1676253 = 1676 considered unsuccessful
c [bca-2] limit of 10000000 steps
c [bca-2] 409712 out of 466834 literals actually usable 88%
c [bca-2] added 6 blocked clauses in 871109 steps
c [rephase-2] after 81237 conflicts (new increment 40000, next 121237)
c [flushphases] 118788 phases reset
c [phase-3] phase bias: 3694 positive 51%, 3519 negative 49%
c [simplification-3] removed 12 variables 0.0% (233416 remain 99%)
c [simplification-3] removed 2412 irredundant clauses 0.1% (1676002 remain 99%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 30000
c [simplification-3] new conflict interval 60000
c [simplification-3] penalized conflict interval 120000 = 2 * 60000
c [simplification-3] new conflict limit 201237
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   71.0  233416  1676002     84178   23528   2041 56439  16  6.7  34.1  114
c -   76.6  233416  1676002     95125   26084   2180 56483  22  6.7  45.8  117
c -   82.5  233416  1676002    106078   28071   2300 56516  24  6.7  43.8  117
c -   87.2  233416  1676002    117454   30188   2366 56545  19  6.8  43.8  117
c R   90.0  233416  1676002    125506   38048   2407 56562  21  6.8  44.0  120
c -   92.1  233416  1676002    129207   31783   2441 56577  24  6.8  43.3  117
c -   98.0  233416  1676002    141446   32866   2492 56609  21  7.0  41.7  118
c -  103.9  233416  1676002    154235   34342   2583 56630  16  7.0  40.6  117
c -  111.1  233416  1676002    167888   36242   2690 56662  24  7.1  39.0  117
c -  116.2  233416  1676002    181714   38040   2757 56690  23  7.2  40.0  117
c -  123.2  233416  1676002    196359   39745   2813 56727  14  7.2  39.3  119
c 
c [simplification-4] limit of 201845 conflicts hit after 201846 conflicts
c [ternres-2] limit 22757718 with penalty 0 = 0 + 0
c [ternres-2] all 233416 free variables schedulable
c [ternres-2] 35 ternary resolvents (0 bin, 35 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-7] removed 8 variables
c [treelook-2] limit 568942 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 69550 literals 15%
c [treelook-2] scheduling used 571547 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 568942 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 591121 steps
c [treelook-2] 69541 literals remain 15%
c [treelook-2] 23516 variables remain to probed next time 10%
c [treelook-2] removed 0 variables, found 1077 hbrs
c [lift-2] limit 13654631 with penalty 0 = 0 + 0
c [lift-2] using 232804 probes 100%
c [lift-2] 0 units, 71 impls, 30 eqs in 1 rounds
c [lift-2] 232636 variables remain 100% (742 retained)
c [lift-2] removed 30 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 2789 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 233378 variables 100%
c [block-2] limit of 113788594 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 [elim-3] 106276 variables 46% will be scheduled this time
c [elim-3] scheduled 106276 variables 46%
c [elim-3] limit of 227577188 steps penalty 1 = 1 + 0
c [elim-3-1] no variable eliminated in round 1 in 179881357 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 233378
c [bca-3] limit of 10000000 steps
c [bca-3] 381446 out of 466758 literals actually usable 82%
c [bca-3] added 0 blocked clauses in 829806 steps
c [rephase-3] after 201846 conflicts (new increment 80000, next 281846)
c [flushphases] 83865 phases reset
c [phase-4] phase bias: 1445 positive 54%, 1244 negative 46%
c [simplification-4] removed 38 variables 0.0% (233378 remain 99%)
c [simplification-4] removed 1878 irredundant clauses 0.1% (1674124 remain 99%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 60000
c [simplification-4] new conflict interval 120000
c [simplification-4] penalized conflict interval 240000 = 2 * 120000
c [simplification-4] new conflict limit 441846
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  139.6  233378  1674124    211431   41524   2909 84897  24  7.3  37.9  119
c -  146.7  233378  1674124    227106   42956   2970 84925  20  7.3  36.8  119
c -  152.9  233378  1674124    242776   44631   3025 84942  25  7.4  36.3  119
c -  158.4  233378  1674124    258704   46175   3088 84960  22  7.4  36.2  119
c R  163.2  233378  1674124    271734   58905   3146 84977  21  7.4  36.0  123
c -  165.5  233378  1674124    275961   48171   3155 84984  22  7.4  35.7  119
c -  175.2  233378  1674124    293951   50366   3240 85015  22  7.4  34.6  120
c -  184.3  233378  1674124    312516   52184   3317 85043  23  7.5  33.9  120
c -  191.4  233378  1674124    330977   53602   3371 85056  20  7.5  33.3  120
c -  201.3  233378  1674124    350860   55289   3419 85078  18  7.5  32.5  120
c -  211.3  233378  1674124    371061   56878   3474 85099  25  7.5  31.8  120
c -  220.5  233378  1674124    391445   58789   3547 85122  20  7.5  31.5  120
c -  231.8  233378  1674124    412924   60417   3629 85151  23  7.6  30.9  120
c -  242.6  233378  1674124    435009   61992   3685 85176  24  7.6  30.2  120
c 
c [simplification-5] limit of 442446 conflicts hit after 442446 conflicts
c [ternres-3] limit 55824730 with penalty 0 = 0 + 0
c [ternres-3] all 233378 free variables schedulable
c [ternres-3] 36 ternary resolvents (2 bin, 34 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 5582473 penalty 1 = 1 + 0
c [gauss-2] extracted 12 xors of average arity 2.0
c [gauss-2] connected 24 occurrences of 20 variables (average 1.2)
c [gauss-2] limit 5582473 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 15 variables
c [cgrclsr-2] limit 2791236 penalty 1 = 1 + 0
c [cgrclsr-2] all 233363 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [lift-3] limit 20000000 with penalty 0 = 0 + 0
c [lift-3] using 232210 probes 100%
c [lift-3] 0 units, 86 impls, 31 eqs in 1 rounds
c [lift-3] 231824 variables remain 99% (1508 retained)
c [lift-3] removed 31 variables
c [cliff-2] limit of 22329892 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 2711 transitive binary clauses
c [cce-3] limit of 55824730 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 27912365 steps for small clauses
c [cce-3] scheduling 738170 clauses = 462120 binary + 276050 ternary
c [cce-3] tried to eliminate 1538 small clauses 0%
c [cce-3] eliminated 354 small clauses 0%
c [cce-3] eliminated 256 binary clauses 0%
c [cce-3] eliminated 98 ternary clauses 0%
c [cce-3-1] eliminated 354 small clauses in 55824731 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 354 covered clauses in round 1
c [cce-3] eliminated 354 covered clauses in TOTAL during 1 rounds
c [cce-3] 354 < 1/1000 * 1672520 = 1672 considered unsuccessful
c [rephase-4] after 442446 conflicts (new increment 160000, next 602446)
c [flushphases] 83834 phases reset
c [phase-5] phase bias: 1327 positive 50%, 1316 negative 50%
c [simplification-5] removed 46 variables 0.0% (233332 remain 99%)
c [simplification-5] removed 1958 irredundant clauses 0.1% (1672166 remain 99%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 120000
c [simplification-5] new conflict interval 240000
c [simplification-5] penalized conflict interval 480000 = 2 * 240000
c [simplification-5] new conflict limit 922446
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  262.5  233332  1672166    457296   64116   3847 114515  25  7.6  29.7  123
c -  274.5  233332  1672166    479950   65892   3907 114526  25  7.6  29.2  123
c -  287.8  233332  1672166    503346   67598   3974 114540  26  7.7  28.6  123
c -  296.8  233332  1672166    526197   69399   4029 114555  20  7.7  28.6  123
c -  307.0  233332  1672166    549488   71182   4073 114570  29  7.7  28.6  123
c -  317.2  233332  1672166    573065   72859   4118 114588  25  7.8  28.5  123
c R  323.7  233332  1672166    584819   84388   4134 114595  25  7.8  28.6  127
c -  331.0  233332  1672166    598272   74845   4161 114605  23  7.8  28.3  124
c -  345.1  233332  1672166    624605   76504   4212 114614  28  7.8  27.8  124
c -  358.3  233332  1672166    651194   78310   4277 114627  24  7.9  27.5  124
c -  374.2  233332  1672166    678455   80247   4335 114645  20  7.9  27.1  124
c -  386.8  233332  1672166    705482   82048   4392 114657  20  7.9  26.9  124
c -  402.8  233332  1672166    733763   83916   4446 114678  28  7.9  26.5  124
c -  419.5  233332  1672166    762282   85817   4511 114692  20  7.9  26.2  124
c -  436.2  233332  1672166    791289   87684   4563 114704  19  7.9  26.0  124
c -  453.4  233332  1672166    821096   89741   4624 114711  23  7.9  25.8  124
c -  466.2  233332  1672166    850147   91684   4664 114727  29  8.0  25.7  124
c -  483.6  233332  1672166    881389   93797   4723 114744  21  8.0  25.5  124
c -  501.4  233332  1672166    913146   95521   4776 114755  21  8.0  25.2  124
c 
c [simplification-6] limit of 922954 conflicts hit after 922955 conflicts
c [ternres-4] limit 132556729 with penalty 0 = 0 + 0
c [ternres-4] all 233332 free variables schedulable
c [ternres-4] 44 ternary resolvents (1 bin, 43 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 16569591 penalty 2 = 2 + 0
c [card-3] found 4761 at-most-one constraints of average size 3.8
c [card-3] found 19 at-most-two constraints of average size 4.3
c [card-3] using previous limit 16569591 for elimination
c [card-3] 4780 out of 4780 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 27 variables
c [basicprobe-2] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-2-0] 1129 probes remain 0% after last round
c [basicprobe-2-0] removed 0 variables, found 75461 hbrs
c [bate-1] eliminated 3 asymmetric tautologies during probing
c [lift-4] limit 20000000 with penalty 0 = 0 + 0
c [lift-4] using 231387 probes 99%
c [lift-4] 0 units, 81 impls, 68 eqs in 1 rounds
c [lift-4] 231050 variables remain 99% (2187 retained)
c [lift-4] removed 68 variables
c [unhide-3] limit 5000000 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 11371 tauts, 0 hbrs, 517874 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 2167 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 375363 out of 466476 literals actually usable 80%
c [bca-4] added 5 blocked clauses in 875502 steps
c [rephase-5] after 922955 conflicts (new increment 320000, next 1242955)
c [flushphases] 83806 phases reset
c [phase-6] phase bias: 4111 positive 54%, 3526 negative 46%
c [simplification-6] removed 95 variables 0.0% (233237 remain 99%)
c [simplification-6] removed 10037 irredundant clauses 0.6% (1662129 remain 98%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 120000 = 240000 / 2
c [simplification-6] new conflict interval 360000
c [simplification-6] penalized conflict interval 720000 = 2 * 360000
c [simplification-6] new conflict limit 1642955
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  530.3  233237  1662129    945072   96216   5698 195264  25  8.0  24.9  127
c -  547.9  233237  1662129    977605   98500   5764 195282  23  8.0  24.8  127
c -  566.6  233237  1662129   1010665  100479   5835 195292  21  8.0  24.6  127
c -  587.8  233237  1662129   1044244  102676   5923 195304  22  8.0  24.4  127
c -  609.4  233237  1662129   1078497  104676   6005 195317  25  8.1  24.2  127
c -  625.8  233237  1662129   1112547  106756   6073 195328  22  8.1  24.1  127
c -  642.2  233237  1662129   1146500  109213   6144 195337  27  8.1  24.2  127
c -  658.1  233237  1662129   1180875  111312   6196 195346  23  8.1  24.3  127
c -  673.8  233237  1662129   1215421  113209   6231 195348  26  8.2  24.3  127
c -  687.8  233237  1662129   1250751  115321   6257 195353  24  8.2  24.3  127
c R  688.2  233237  1662129   1252448  116992   6259 195354  16  8.2  24.3  130
c -  712.3  233237  1662129   1288299  117467   6346 195380  29  8.2  24.1  127
c -  735.8  233237  1662129   1326308  119676   6425 195393  25  8.2  23.9  127
c -  760.9  233237  1662129   1364980  121886   6486 195405  28  8.2  23.8  127
c -  783.7  233237  1662129   1403815  124186   6556 195417  24  8.2  23.7  128
c -  809.9  233237  1662129   1443314  126089   6632 195435  20  8.2  23.5  128
c -  838.3  233237  1662129   1484241  128407   6719 195450  23  8.2  23.2  128
c -  858.5  233237  1662129   1523964  131267   6789 195462  22  8.2  23.3  128
c -  886.6  233237  1662129   1565303  133457   6864 195476  25  8.2  23.2  128
c -  914.9  233237  1662129   1607273  135840   6952 195484  25  8.2  23.0  128
c 
c [simplification-7] limit of 1643419 conflicts hit after 1643419 conflicts
c [ternres-5] limit 200000000 with penalty 0 = 0 + 0
c [ternres-5] all 233237 free variables schedulable
c [ternres-5] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-11] removed 629 variables
c [lift-5] limit 20000000 with penalty 0 = 0 + 0
c [lift-5] using 230022 probes 99%
c [lift-5] 0 units, 68 impls, 23 eqs in 1 rounds
c [lift-5] 229735 variables remain 99% (2850 retained)
c [lift-5] removed 23 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2104 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 232585 variables 100%
c [block-3] limit of 200000000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 4 blocked clauses
c [block-3] 4 < 1/1000 * 1661304 = 1661 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 232585 variables 100%
c [elim-4] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-4] incomplete 543 not tried 0% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 536 = 0% variables out of 232585
c [bca-5] limit of 10000000 steps
c [bca-5] 369723 out of 464100 literals actually usable 80%
c [bca-5] added 3 blocked clauses in 930841 steps
c [rephase-6] after 1643419 conflicts (new increment 640000, next 2283419)
c [flushphases] 83197 phases reset
c [phase-7] phase bias: 584 positive 55%, 477 negative 45%
c [simplification-7] removed 1188 variables 0.5% (232049 remain 98%)
c [simplification-7] removed 1291 irredundant clauses 0.1% (1660838 remain 98%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 180000 = 360000 / 2
c [simplification-7] new conflict interval 540000
c [simplification-7] penalized conflict interval 1080000 = 2 * 540000
c [simplification-7] new conflict limit 2723419
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  951.3  232049  1660838   1649113  138274   6934 202415  20  8.2  22.9  135
c -  982.4  232049  1660838   1692147  140792   7015 202429  26  8.2  22.7  135
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3 basic ate = 2 trn 67% + 1 lrg 33% in 1 updates
c bcas: 5 count, 23 added (122 skipped), 4402998 steps
c bkwd: tried 1682976 clauses, 3365952 lits, 2.00 lits/clause
c bkwd: checked 46484446 occs, 27.62 occs/clause, 13.81 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, 4 removed, 16892712 resolutions, 55562338 steps
c blkd: 124 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 3 count, 0 units, 0 am1, 25496443 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 20489 subsumed
c card: 9481 at-most-one constraints found, average size 3.87
c card: 9481 at-most-one constraints used 100%, average size 3.87
c card: 19 at-most-two constraints found, average size 4.26
c card: 19 at-most-two constraints used 100%, average size 4.26
c cces: 3 cces, 5115 eliminated, 5080 ate 99%, 35 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 2 count, 3630559 esteps, 4230 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: 231 extracted (231 ands 100%, 0 xors 0%, 0 ites 0%)
c clff: 2 cliffs, 0 lifted, 0 failed
c clff: 28601 decisions, 32338495 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 7250711 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 28 gcs, 0 rescored clauses, 902 rescored vars
c dcps: 11 decompositions, 900 equivalent 0%
c deco: 110 decision-only clauses 0%, 76% reduction
c decs: 2752839 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 0 flipped 0.000% (in 0 phases)
c elms: 4 elims, 2671 eliminated 1%
c elms: 5 rounds, 1.2 rounds/bve
c elms: 2622 small 98%, 49 large 2%
c elms: 23288 tried small, 2622 succeeded 11%, 20666 failed 89%
c elms: 649 subsumed, 286 strengthened, 0 blocked
c elms: 20181351 copies, 17905123 resolutions, 726921 ipos
c elms: 4227697 subchks, 2804453 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 2 extractions, 13 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15165446 steps, 7582723 extr 50%, 47 elim 0%
c glue: 8.2 orig avg, 8.2 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 244427 = 38333 simple + 205481 trn 16% + 613 lrg 84%, 10102 sub 0%
c hght: 23 average, 2.75 height/glue
c ints: 47557 luby (12665060 steps), 0 inout (0 steps)
c lift: 5 phases, 16989 probed (5720 level1 34%, 11269 level2 66%)
c lift: 0 units, 161 equivalences, 331 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1715240 clauses, 34.1 length
c lrnd: 621330 uips 36%, 991541 flips 58%
c mega: 0 count, 0 failed, 0 rounds
c mins: 58509366 learned lits, 36% minimized
c mins: 1700081 mins 99%, 1516 bin 0%, 13533 size 1%, 110 deco 0%
c move: moved 1715240, 2897 bin 0%, 636 trn 0%, 0 lrg 0%
c otfs: str 8867 dyn (8849 red, 18 irr) 2389 drv 27%, 6478 rst 73%
c otfs: sub 57 dyn (57 red, 0 irr)
c phas: 7 computed, 262166 set, 119272 pos (45%), 142894 neg (55%)
c prbs: 2 basic, 5682 probed, 0 failed, 0 lifted
c prbs: 2 simple, 420092 probed, 0 failed, 1 eqs
c prbs: 2 treelook, 143 probed, 0 failed, 0 lifted
c prps: 2924263300 props, 1055 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c psns: 549325312 searches, 28935640 hits, 5% 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: 73 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 73 arith 100%, 0 double 0%
c rmbd: 251 removed, 247 red 98%
c rphs: 6 recomputed phases
c rsts: 44168 restarts 93%, 3389 skipped 7%
c rsts: 0 saturating 0%, 101 agile 3%, 3288 reuse 97%
c rsts: 38.1 avg interval, 38.1 scaled, 1.0 factor
c rsts: 26640 kept 60.3% average 48.0%
c simp: 7 count (7 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 1715240 count (1244921 tried 0.7), 82438 sub out of 1708219 (4.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 0 count
c tops: 0 fixed 0%, 0 its, 0.00 confs/it
c trvs: 43642022631 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 15.0 search traversals per propagation, 25312.5 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 5 transitive reductions, 12569 removed, 0 failed
c trds: 76348 nodes, 71419 edges, 10001101 steps
c trim: 536597 words, 2.0 MB
c trnr: 5 count, 3 bin, 431 trn, 76490533 steps
c unhd: 3 count, 3 rounds, 47554529 steps
c unhd: 16 non-trivial sccs of average size 2.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: 47534 tauts, 3783 bin 8%, 430 trn 1%, 1807 lrg 4%
c unhd: 47534 tauts, 41514 stamp 87%, 28224 red 59%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 828378 str, 0 bin 0%, 71711 trn 9%, 756667 lrg 91%, 754287 red 91%
c vars: 232049 remaining 98% and 3571 removed 2% out of 235620
c vars: 0 fixed 0%, 2671 eliminated 1%, 900 equivalent 0%
c vsts: 27721259363 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 9.5 search visits per propagation, 16043.5 per conflict
c wchs: 6988577459 pushed, 53865228 enlarged, 53 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   1708219 100   1459325 100  63387547 100  11427844 100    401026 100
c 
c  0     106157   6         0   0  59345770  94<  7378634  65    231654  58 
c  1     105645   6     63949   4   1336283   2    619651   5<    33861   8<
c  2     531347  31<   497948  34   1261623   2   1342966  12     50722  13 
c  3     791863  46    735700  50<  1196092   2   1718801  15     66533  17 
c  4     164449  10    153576  11    235054   0    348959   3     17124   4 
c  5       8513   0      8015   1     12360   0     18249   0      1064   0 
c  6        183   0       120   0       296   0       424   0        35   0 
c  7         39   0         8   0        43   0        89   0        16   0 
c  8         14   0         5   0        16   0        36   0         6   0 
c  9          6   0         2   0         7   0        30   0        11   0 
c 10          1   0         0   0         1   0         2   0         0   0 
c 11          2   0         2   0         2   0         3   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.5           2.7           0.1           0.9           1.0
c std             1.0           0.7           0.6           1.3           1.3
c 
c   98.348  10% analysis
c   33.057   3% mincls
c   22.526   2% bump
c   20.796   2% decide
c   16.217   2% elim
c   15.668   2% cce
c   10.847   1% gc
c    9.261   1% restart
c    8.422   1% probe
c    6.893   1% decomp
c    6.615   1% lift
c    4.483   0% block
c    4.181   0% bca
c    3.876   0% defrag
c    2.891   0% reduce
c    2.500   0% unhide
c    1.796   0% backward
c    1.677   0% cgrclsr
c    1.651   0% gauss
c    1.647   0% card
c    1.388   0% phase
c    0.984   0% transred
c    0.904   0% ternres
c    0.896   0% cliff
c    0.060   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c    0.000   0% tabularasa
c ----------------------------------
c    3.316   0% probe simple     39%
c    2.811   0% probe basic      33%
c    2.295   0% probe tree-look  27%
c ==================================
c   10.231   1% preprocessing    14%
c   63.897   6% inprocessing     86%
c ==================================
c   74.128   7% simplifying
c  924.794  93% search
c ==================================
c  998.925 100% all
c 
c 2752839 decisions, 2755.8 decisions/sec
c 1717629 conflicts, 1719.5 conflicts/sec
c 2924263300 propagations, 2.9 megaprops/sec
c 998.9 seconds, 211.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
