c launch: /data/cnf/sc2014/app/006-80-4.cnf.bz2
c host: atom19
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/006-80-4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/006-80-4.cnf.bz2
c no embedded options
c found 'p cnf 13408 478480' header
c read 13408 variables, 478480 clauses, 3138512 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 13025 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   13025   308391         0       0      0     0   0  0.0   0.0   17
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 404 variables
c [simpleprobe-1] all 13004 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 12 variables
c [simpleprobe-1] 5742 variables remain 44% (7250 retained)
c [simpleprobe-1] removed 12 variables, found 2 hbrs, 4 units
c [unhide-1] limit 154125 based on 308250 irredundant clauses
c [unhide-1-1] 0 units, 9 failed, 805 tauts, 0 hbrs, 16 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12989 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 468 variables 4% in round 1 in 3933687 steps
c [elim-1-1] backward subsumption/strengthening limit 7867374
c [elim-1-1] subsumed 967 and strengthened 46 clauses in 7867517 steps
c [elim-1-1] rescheduled 3621 variables 28% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 41290 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 468 = 4% variables out of 12989
c [phase-1] phase bias: 4973 positive 40%, 7548 negative 60%
c [simplification-1] removed 504 variables 3.9% (12521 remain 96%)
c [simplification-1] removed 6106 irredundant clauses 2.0% (302285 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] new conflict limit 4000
c [cut-width] 16009, max 26785, min4 13655 at 75%, min10 8175 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    1.5   12521   302285         5       4      0     1   0  3.0  16.7   23
c R    1.5   12521   302285        21      12      1     2   1  2.8  28.7   23
c R    1.5   12521   302285        65      44      5     2   1  3.5  77.2   23
c R    1.5   12521   302285       168     130      7     2   1  4.5 130.8   23
c R    1.5   12521   302285       412     329     14     3   2  5.4 171.6   23
c R    1.5   12521   302285       980     797     28     3   4  5.2 196.2   23
c R    1.6   12521   302285      2277    1895     46     3   7  5.3 253.1   23
c 
c [simplification-2] limit of 4006 conflicts hit after 4006 conflicts
c [simpleprobe-2] 5541 schedulable variables 44%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 5543 variables remain 44% (6977 retained)
c [simpleprobe-2] removed 1 variables, found 1 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6005 literals 24%
c [treelook-1] scheduling used 300034 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300291 steps
c [treelook-1] 4999 literals remain 20%
c [treelook-1] 4988 variables remain to probed next time 40%
c [treelook-1] removed 0 variables, found 1 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 514 sched 4%, 2 failed, 0 lifted, 13 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 520 sched 4%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 519 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 2 variables, found 15 hbrs
c [unhide-2] limit 151125 based on 302250 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 11 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12518 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 1054 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 17506 clauses out of 103769 (17%) of length 7
c [cce-1-1] eliminated 428 clauses out of 85437 (1%) of length 6
c [cce-1-1] eliminated 11872 clauses out of 66782 (18%) of length 5
c [cce-1-1] eliminated 153 clauses out of 34007 (0%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 29959 large clauses in 183655333 steps
c [cce-1-1] allowing another 91827666 steps for small clauses
c [cce-1] scheduling 10793 clauses = 312 binary + 10481 ternary
c [cce-1] tried to eliminate 10793 small clauses 100%
c [cce-1] eliminated 1052 small clauses 10%
c [cce-1] eliminated 4 binary clauses 1%
c [cce-1] eliminated 1048 ternary clauses 10%
c [cce-1-1] eliminated 1052 small clauses in 95417868 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 31011 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 9741 clauses = 308 binary + 9433 ternary
c [cce-1] tried to eliminate 9741 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 31011 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12518 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 9799 not tried 78% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 205 = 2% variables out of 12518
c [bca-1] limit of 10000000 steps
c [bca-1] 21103 out of 24628 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 176674 steps
c [phase-2] phase bias: 29 positive 9%, 280 negative 91%
c [simplification-2] removed 208 variables 1.7% (12313 remain 95%)
c [simplification-2] removed 36535 irredundant clauses 12.1% (265750 remain 86%)
c [simplification-2] maximum reduction of 12% = max (2%, 12%)
c [simplification-2] large reduction 12% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 6006
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    8.2   12313   265750      5199    4057   1128    17   7  5.4 312.3   22
c -    8.2   12313   265750      6000    2735   1146    18   6  5.4 306.7   22
c 
c [simplification-3] limit of 6008 conflicts hit after 6008 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12313 free variables schedulable
c [ternres-1] 147 ternary resolvents (13 bin, 134 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 at-most-one constraints of average size 3.0
c [card-2] found 4 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5 out of 5 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 1869 xors of average arity 5.0
c [gauss-1] connected 9309 occurrences of 512 variables (average 18.2)
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-8] removed 1 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 12312 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 2782 probes 23%
c [lift-1-1] found 0 units 22 impls in round 1
c [lift-1] 0 units, 29 impls, 3 eqs in 2 rounds
c [lift-1] 9530 variables remain 77% (2779 retained)
c [lift-1] removed 3 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 265741 based on 265741 irredundant clauses
c [transred-1] removed 3 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12309 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 715 clauses = 308 binary + 407 ternary
c [cce-2] tried to eliminate 715 small clauses 100%
c [cce-2] eliminated 32 small clauses 4%
c [cce-2] eliminated 1 binary clauses 0%
c [cce-2] eliminated 31 ternary clauses 8%
c [cce-2-1] eliminated 32 small clauses in 15199332 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] eliminated 32 covered clauses in round 1
c [cce-2-2] incomplete large round (ACCE)
c [cce-2-2] allowing another 7400334 steps for small clauses
c [cce-2] scheduling 683 clauses = 307 binary + 376 ternary
c [cce-2] tried to eliminate 683 small clauses 100%
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 32 covered clauses in TOTAL during 2 rounds
c [cce-2] 32 < 1/1000 * 265741 = 265 considered unsuccessful
c [elim-3] 9791 variables 80% will be scheduled this time
c [elim-3] scheduled 9791 variables 80%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 7784 not tried 63% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 12309
c [phase-3] phase bias: 17 positive 74%, 6 negative 26%
c [simplification-3] removed 4 variables 0.0% (12309 remain 95%)
c [simplification-3] removed 67 irredundant clauses 0.0% (265683 remain 86%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] new conflict limit 30008
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   11.9   12309   265683      9985    3657   1329    75   7  5.6 342.4   21
c R   12.0   12309   265683     11675    5119   1345    79   7  5.8 369.9   21
c -   12.4   12309   265683     14384    4522   1383    83   5  5.9 386.6   21
c -   12.9   12309   265683     19577    5545   1446    94   7  6.2 390.7   21
c -   13.4   12309   265683     25287    6675   1493    98   9  6.6 410.5   21
c R   13.5   12309   265683     25922    7265   1493   100  10  6.7 413.6   21
c 
c [simplification-4] limit of 30060 conflicts hit after 30060 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12309 free variables schedulable
c [ternres-2] 15 ternary resolvents (8 bin, 7 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1842 literals 7%
c [treelook-2] scheduling used 150007 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150017 steps
c [treelook-2] 1284 literals remain 5%
c [treelook-2] 1273 variables remain to probed next time 10%
c [treelook-2] removed 0 variables, found 2 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 168 probes 1%
c [lift-2-1] found 0 units 2 impls in round 1
c [lift-2-2] found 0 units 0 impls in round 2
c [lift-2-3] found 0 units 1 impls in round 3
c [lift-2-4] found 0 units 0 impls in round 4
c [lift-2-5] found 0 units 0 impls in round 5
c [lift-2] 0 units, 3 impls, 0 eqs in 6 rounds
c [lift-2] 9362 variables remain 76% (2947 retained)
c [unhide-3] limit 132841 based on 265683 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 17 tauts, 0 hbrs, 13 literals
c [transred-2] limit 453370 with penalty 0 = 0 + 0
c [transred-2] removed 6 transitive binary clauses
c [bca-2] limit of 10000000 steps
c [bca-2] 18955 out of 24620 literals actually usable 77%
c [bca-2] added 0 blocked clauses in 165778 steps
c [rephase-1] after 30060 conflicts (new increment 20000, next 50060)
c [flushphases] 6871 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-4] removed 6 irredundant clauses 0.0% (265677 remain 86%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 24000
c [simplification-4] new conflict interval 48000
c [simplification-4] penalized conflict interval 48000 = 1 * 48000
c [simplification-4] new conflict limit 78060
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   14.7   12309   265677     31363    7548   1583   113   8  6.7 405.4   21
c -   15.5   12309   265677     38011    8502   1651   118   8  6.9 411.2   21
c -   16.4   12309   265677     45482    9625   1762   119   6  7.0 411.3   22
c -   17.1   12309   265677     53377   10819   1834   123  11  7.2 421.3   22
c R   17.4   12309   265677     56941   14087   1861   125  12  7.4 426.8   22
c -   18.0   12309   265677     61812   12024   1920   125   9  7.5 425.8   22
c -   19.1   12309   265677     70776   13197   1985   127  10  7.6 423.4   22
c 
c [simplification-5] limit of 78078 conflicts hit after 78078 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12309 free variables schedulable
c [ternres-3] 7 ternary resolvents (3 bin, 4 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8 xors of average arity 3.0
c [gauss-2] connected 24 occurrences of 3 variables (average 8.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 1483221 penalty 0 = 0 + 0
c [basicprobe-2-0] 605 sched 5%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-2-1] 610 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 6 hbrs
c [cgrclsr-2] limit 132838 based on 265677 irredundant clauses
c [cgrclsr-2] all 12309 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [cliff-2] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 1483221 with penalty 0 = 0 + 0
c [transred-3] removed 1 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12309 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 732 clauses = 311 binary + 421 ternary
c [cce-3] tried to eliminate 732 small clauses 100%
c [cce-3] eliminated 1 small clauses 0%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses in 7730604 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 1 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3634698 steps for small clauses
c [cce-3] scheduling 731 clauses = 310 binary + 421 ternary
c [cce-3] tried to eliminate 731 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 1 covered clauses in TOTAL during 2 rounds
c [cce-3] 1 < 1/1000 * 265677 = 265 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12309 variables 100%
c [elim-4] limit of 14832215 steps penalty 1 = 1 + 0
c [elim-4] incomplete 9558 not tried 78% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 0 = 0% variables out of 12309
c [rephase-2] after 78078 conflicts (new increment 40000, next 118078)
c [flushphases] 6533 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-5] removed 39 irredundant clauses 0.0% (265638 remain 86%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 48000
c [simplification-5] new conflict interval 96000
c [simplification-5] penalized conflict interval 96000 = 1 * 96000
c [simplification-5] new conflict limit 174078
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   22.9   12309   265638     80287   14354   2083   138  12  7.8 422.6   22
c -   24.1   12309   265638     90566   15668   2180   138  10  7.9 418.9   22
c -   25.6   12309   265638    101412   16978   2299   140   8  8.1 418.3   22
c -   26.7   12309   265638    112606   18398   2373   144  17  8.4 424.4   22
c -   27.6   12309   265638    124012   19561   2442   144  15  9.1 430.3   23
c R   27.6   12309   265638    124080   19627   2442   144  15  9.1 430.3   23
c -   29.3   12309   265638    136233   20775   2544   144  12  9.3 428.3   23
c -   31.0   12309   265638    149066   22130   2637   146  16  9.4 427.0   23
c -   32.9   12309   265638    162488   23424   2727   148   9  9.6 425.1   23
c 
c [simplification-6] limit of 174092 conflicts hit after 174092 conflicts
c [ternres-4] limit 4013626 with penalty 0 = 0 + 0
c [ternres-4] all 12309 free variables schedulable
c [ternres-4] 3 ternary resolvents (2 bin, 1 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 501703 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 4 at-most-two constraints of average size 4.0
c [card-3] using previous limit 501703 for elimination
c [card-3] 7 out of 7 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 5451 schedulable variables 44%
c [simpleprobe-3] limit 16054506 penalty 0 = 0 + 0
c [simpleprobe-3] 3689 variables remain 30% (8620 retained)
c [simpleprobe-3] removed 0 variables, found 6 hbrs, 0 units
c [lift-3] limit 1204087 with penalty 1 = 1 + 0
c [lift-3] using 414 probes 3%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 0 impls in round 2
c [lift-3-3] found 0 units 0 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-3] 8948 variables remain 73% (3361 retained)
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 2 transitive binary clauses
c [rephase-3] after 174092 conflicts (new increment 80000, next 254092)
c [flushphases] 6209 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-6] removed 0 irredundant clauses 0.0% (265638 remain 86%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 96000
c [simplification-6] new conflict interval 192000
c [simplification-6] penalized conflict interval 192000 = 1 * 192000
c [simplification-6] new conflict limit 366092
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   35.4   12309   265638    177268   25641   2829   157  11  9.7 425.6   23
c -   36.8   12309   265638    193200   27569   3064   157   7  9.5 425.0   23
c -   38.5   12309   265638    209726   29554   3302   157   6  9.3 424.4   23
c -   40.5   12309   265638    226658   31545   3536   160   8  9.2 421.4   23
c -   41.9   12309   265638    243768   33425   3728   162  12  9.3 427.0   24
c -   43.3   12309   265638    261818   36022   3854   168  13  9.3 434.3   24
c R   43.9   12309   265638    268664   42269   3895   170  16  9.4 436.2   24
c -   45.4   12309   265638    279408   37410   4023   174  13  9.3 434.7   24
c -   47.9   12309   265638    297915   39113   4229   178   8  9.4 433.4   24
c -   50.7   12309   265638    317422   41192   4479   183  14  9.3 433.5   24
c -   52.9   12309   265638    336864   42783   4612   186  17  9.5 435.1   25
c -   55.6   12309   265638    357294   44338   4742   187   8  9.5 435.8   25
c 
c [simplification-7] limit of 366118 conflicts hit after 366119 conflicts
c [ternres-5] limit 8436624 with penalty 0 = 0 + 0
c [ternres-5] all 12309 free variables schedulable
c [ternres-5] 7 ternary resolvents (4 bin, 3 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-4] limit 421831 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 73 tauts, 0 hbrs, 108 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1 transitive binary clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 7315 out of 24620 literals actually usable 30%
c [bca-3] added 0 blocked clauses in 103230 steps
c [rephase-4] after 366119 conflicts (new increment 160000, next 526119)
c [flushphases] 2105 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-7] removed 0 irredundant clauses 0.0% (265638 remain 86%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 192000
c [simplification-7] new conflict interval 384000
c [simplification-7] penalized conflict interval 384000 = 1 * 384000
c [simplification-7] new conflict limit 750119
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   58.8   12309   265638    378644   46196   4815   198  15  9.6 438.1   25
c -   61.1   12309   265638    399956   47692   4955   201   9  9.8 442.3   25
c -   64.3   12309   265638    421812   49391   5103   204  11  9.9 442.4   25
c -   67.3   12309   265638    444030   51063   5207   206  14 10.0 440.9   25
c -   70.7   12309   265638    466921   52905   5387   211  11 10.0 441.6   26
c -   74.4   12309   265638    490768   54781   5568   216   9 10.1 442.8   26
c -   76.7   12309   265638    514269   56438   5689   220  22 10.5 445.5   26
c -   78.4   12309   265638    537722   57682   5749   222  24 11.0 448.8   25
c -   80.6   12309   265638    562713   60504   5864   224  22 11.2 451.5   26
c R   81.9   12309   265638    578484   75179   5951   227  24 11.4 453.4   29
c -   83.7   12309   265638    588079   62301   6068   230   8 11.4 452.3   26
c -   87.9   12309   265638    614953   64795   6357   231  12 11.3 451.1   26
c -   91.8   12309   265638    641473   66836   6534   232  12 11.3 450.3   27
c -   96.5   12309   265638    668520   68911   6705   232  11 11.3 448.6   27
c -  100.4   12309   265638    696466   71445   6865   233  15 11.4 449.4   26
c -  103.6   12309   265638    724929   72911   6942   233  19 11.5 448.3   27
c 
c [simplification-8] limit of 750151 conflicts hit after 750151 conflicts
c [ternres-6] limit 19656932 with penalty 0 = 0 + 0
c [ternres-6] all 12309 free variables schedulable
c [ternres-6] 29 ternary resolvents (2 bin, 27 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 982846 penalty 2 = 2 + 0
c [gauss-3] extracted 6 xors of average arity 3.0
c [gauss-3] connected 18 occurrences of 3 variables (average 6.0)
c [gauss-3] limit 982846 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-3] limit 491423 penalty 2 = 2 + 0
c [cgrclsr-3] all 12309 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cliff-3] limit of 3931386 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 1 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12309 variables 100%
c [block-4] limit of 49142330 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 3 blocked clauses
c [block-4] 3 < 1/1000 * 265638 = 265 considered unsuccessful
c [cce-4] limit of 9828466 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 4914233 steps for small clauses
c [cce-4] scheduling 946 clauses = 316 binary + 630 ternary
c [cce-4] tried to eliminate 946 small clauses 100%
c [cce-4] eliminated 6 small clauses 1%
c [cce-4] eliminated 6 ternary clauses 1%
c [cce-4-1] eliminated 6 small clauses in 5295260 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 6 covered clauses in round 1
c [cce-4-2] incomplete large round (ACCE)
c [cce-4-2] allowing another 2266603 steps for small clauses
c [cce-4] scheduling 940 clauses = 316 binary + 624 ternary
c [cce-4] tried to eliminate 940 small clauses 100%
c [cce-4-2] completed small round (ACCE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 6 covered clauses in TOTAL during 2 rounds
c [cce-4] 6 < 1/1000 * 265635 = 265 considered unsuccessful
c [elim-5] 7777 variables 63% will be scheduled this time
c [elim-5] scheduled 7777 variables 63%
c [elim-5] limit of 98284660 steps penalty 2 = 2 + 0
c [elim-5] incomplete 3874 not tried 31% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 12309
c [rephase-5] after 750151 conflicts (new increment 320000, next 1070151)
c [flushphases] 2064 phases reset
c [phase-8] phase bias: 19 positive 56%, 15 negative 44%
c [simplification-8] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-8] removed 300 irredundant clauses 0.1% (265338 remain 86%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 384000
c [simplification-8] new conflict interval 768000
c [simplification-8] penalized conflict interval 768000 = 1 * 768000
c [simplification-8] new conflict limit 1518151
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  110.2   12309   265338    754072   74347   7059   234  27 11.6 447.9   28
c -  113.4   12309   265338    783590   75513   7119   234  17 11.8 447.0   28
c -  116.9   12309   265338    813884   76777   7174   234  19 11.9 446.9   28
c -  118.5   12309   265338    843748   77824   7209   234  22 12.1 449.4   28
c -  122.0   12309   265338    875028   78874   7257   234  11 12.2 448.6   29
c -  125.5   12309   265338    907037   80247   7294   234  13 12.3 447.8   28
c -  129.8   12309   265338    939121   81262   7344   234  10 12.4 447.2   29
c -  133.3   12309   265338    972003   83174   7411   235  19 12.5 448.4   29
c -  139.2   12309   265338   1004429   85056   7540   235  11 12.6 446.0   29
c -  144.6   12309   265338   1037615   87200   7666   236  17 12.7 444.4   29
c -  150.6   12309   265338   1071285   89305   7780   236  15 12.8 442.1   29
c -  153.4   12309   265338   1108337   92019   7911   236  35 12.9 443.0   29
c -  155.1   12309   265338   1142967   93013   7962   236  21 13.2 444.3   29
c -  157.5   12309   265338   1180516   95526   8184   237  14 13.3 447.0   29
c -  159.5   12309   265338   1216459   97118   8237   237  33 13.5 449.1   29
c -  161.2   12309   265338   1251988   97677   8255   237  36 13.8 450.0   30
c -  163.5   12309   265338   1288275   98324   8275   237  45 14.1 449.9   30
c -  165.6   12309   265338   1324737   98968   8282   237  52 14.4 450.2   30
c -  168.1   12309   265338   1362197  100006   8290   237  43 14.6 450.7   31
c -  170.3   12309   265338   1400907  100913   8331   237  49 14.7 451.0   29
c -  171.7   12309   265338   1439049  101482   8347   237  46 14.9 451.7   29
c -  175.4   12309   265338   1476428  102008   8347   237  51 15.5 452.0   30
c -  177.4   12309   265338   1516091  102625   8365   237  45 15.9 452.6   30
c 
c [simplification-9] limit of 1518151 conflicts hit after 1518151 conflicts
c [ternres-7] limit 37234882 with penalty 0 = 0 + 0
c [ternres-7] all 12309 free variables schedulable
c [ternres-7] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-3] limit 465436 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1379 literals 6%
c [treelook-3] scheduling used 465442 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 465436 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 383708 steps
c [treelook-3] 0 literals remain 0%
c [treelook-3] 0 variables remain to probed next time 0%
c [treelook-3] removed 0 variables, found 4 hbrs
c [lift-4] limit 5000000 with penalty 2 = 2 + 0
c [lift-4] using 1271 probes 10%
c [lift-4-1] found 0 units 0 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 0 impls in round 5
c [lift-4] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-4] 7677 variables remain 62% (4632 retained)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [rephase-6] after 1518151 conflicts (new increment 640000, next 2158151)
c [flushphases] 563 phases reset
c [phase-9] phase bias: 1 positive 100%, 0 negative 0%
c [simplification-9] removed 0 variables 0.0% (12309 remain 95%)
c [simplification-9] removed 0 irredundant clauses 0.0% (265338 remain 86%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 768000
c [simplification-9] new conflict interval 1536000
c [simplification-9] penalized conflict interval 1536000 = 1 * 1536000
c [simplification-9] new conflict limit 3054151
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  179.9   12309   265338   1556914  103629   8381   242  52 16.0 453.3   31
c -  181.9   12309   265338   1598905  104170   8381   242  48 16.2 453.9   31
c -  183.7   12309   265338   1640937  104594   8391   242  47 16.5 454.6   31
c -  187.4   12309   265338   1682789  105168   8391   242  50 17.0 454.6   48
c -  191.0   12309   265338   1724273  105723   8391   242  51 17.5 454.5   48
c -  195.4   12309   265338   1767013  106262   8391   242  51 18.0 454.5   48
c -  199.3   12309   265338   1809700  106775   8391   242  51 18.4 454.4   48
c -  204.2   12309   265338   1852813  107298   8391   242  48 18.8 454.3   48
c -  209.2   12309   265338   1896159  107909   8396   242  42 19.1 454.3   48
c -  211.4   12309   265338   1941655  108642   8414   242  25 19.2 455.2   33
c -  215.8   12309   265338   1989476  110041   8563   242  15 19.1 455.0   33
c -  219.5   12309   265338   2036699  111393   8590   242  39 19.2 455.5   32
c -  222.7   12309   265338   2084527  112785   8716   242  37 19.3 455.9   32
c -  228.3   12309   265338   2134922  114635   9069   242  12 19.2 454.3   32
c -  234.3   12309   265338   2186618  116985   9324   242  17 19.1 453.1   33
c -  238.2   12309   265338   2236786  118002   9411   242  11 19.1 452.9   32
c -  242.4   12309   265338   2287955  119611   9499   242  36 19.1 452.3   32
c -  245.6   12309   265338   2338973  120528   9520   242  37 19.1 452.3   33
c -  249.9   12309   265338   2386517  120858   9521   242  40 19.1 452.8   34
c -  254.2   12309   265338   2436396  121750   9527   242  37 19.4 453.4   34
c -  257.2   12309   265338   2487383  122410   9532   242  46 19.6 454.1   34
c -  264.2   12309   265338   2538768  122758   9532   242  45 19.9 454.8   54
c -  267.0   12309   265338   2591529  123926   9617   246  40 20.0 455.3   53
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  270.0   12309   265338   2649038  129100   9824   253  21 19.9 456.4   33
c R  270.1   12309   265338   2650479  130458   9830   253  22 19.9 456.4   35
c -  278.5   12309   265338   2706642  133171  10741   309  17 19.8 452.8   34
c i  278.7   12308   265338   2708192  134580  10765   309  10 19.8 452.6   35
c -  286.1   12308   265338   2763990  136497  11120   322  31 19.6 449.9   33
c -  293.6   12308   265338   2821498  139152  11427   331  10 19.5 446.9   34
c -  301.9   12308   265338   2877554  142818  11679   331  37 19.6 445.1   34
c -  311.7   12308   265338   2928909  143286  11682   331  39 21.0 445.6   36
c -  323.3   12308   265338   2981010  143879  11683   331  37 22.5 446.1   36
c -  333.4   12308   265338   3033620  144525  11685   331  38 24.0 446.6   36
c 
c [simplification-10] limit of 3054279 conflicts hit after 3054279 conflicts
c [ternres-8] limit 90931500 with penalty 0 = 0 + 0
c [ternres-8] all 12308 free variables schedulable
c [ternres-8] 166 ternary resolvents (10 bin, 156 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 5683218 penalty 3 = 3 + 0
c [card-4] found 5 at-most-one constraints of average size 3.0
c [card-4] found 15 at-most-two constraints of average size 4.0
c [card-4] using previous limit 5683218 for elimination
c [card-4] 19 out of 20 constraints (95%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-19] removed 5 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 7 transitive binary clauses
c [rephase-7] after 3054279 conflicts (new increment 1280000, next 4334279)
c [flushphases] 0 phases reset
c [simplification-10] removed 4 variables 0.0% (12304 remain 94%)
c [simplification-10] removed 13 irredundant clauses 0.0% (265325 remain 86%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 1536000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] new conflict limit 4054279
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  342.9   12304   265325   3092109  147560  12074   321  10 23.9 444.0   36
c -  353.0   12304   265325   3151215  151227  12238   322  25 23.7 442.1   36
c -  356.6   12304   265325   3210709  152424  12298   322  30 23.7 443.4   35
c -  362.3   12304   265325   3273134  153884  12421   326  14 23.7 442.4   37
c -  366.1   12304   265325   3333370  154934  12450   326  47 23.7 442.3   37
c -  369.1   12304   265325   3393257  156107  12473   327  42 23.7 442.8   35
c -  374.4   12304   265325   3454296  156756  12479   327  35 23.8 443.2   35
c -  379.0   12304   265325   3516410  157751  12546   327  14 23.7 443.1   35
c -  388.2   12304   265325   3580604  160911  12699   328  17 23.6 440.2   37
c -  396.2   12304   265325   3643296  163217  12761   328  24 23.5 439.3   38
c -  405.0   12304   265325   3709343  165188  12859   328  30 23.4 437.3   37
c -  410.7   12304   265325   3774780  166792  12918   328  39 23.4 436.9   36
c -  414.4   12304   265325   3839773  168092  12950   328  37 23.4 437.6   36
c -  420.2   12304   265325   3904671  170029  12999   329  21 23.4 437.5   38
c -  429.8   12304   265325   3966149  171604  13023   329  36 23.9 437.5   36
c -  438.6   12304   265325   4027420  172197  13027   330  35 25.0 437.7   36
c 
c [simplification-11] limit of 4054291 conflicts hit after 4054291 conflicts
c [ternres-9] limit 121949819 with penalty 0 = 0 + 0
c [ternres-9] all 12304 free variables schedulable
c [ternres-9] 89 ternary resolvents (5 bin, 84 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-3] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 785 sched 6%, 1 failed, 0 lifted, 7 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-1] 785 sched 6%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 1 variables, found 7 hbrs
c [bate-1] eliminated 32 asymmetric tautologies during probing
c [unhide-5] limit 2500000 with penalty 3 = 3 + 0
c [unhide-5-7] 0 units, 0 failed, 162 tauts, 0 hbrs, 126539 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 7 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 90 out of 24608 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 198437 steps
c [simplification-11] removed 1 variables 0.0% (12303 remain 94%)
c [simplification-11] removed 40 irredundant clauses 0.0% (265285 remain 86%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] new conflict limit 5054291
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  451.1   12303   265285   4091698  173628  13013   326  13 25.3 436.5   39
c -  459.2   12303   265285   4159376  176891  13090   326  34 25.2 435.3   39
c -  468.3   12303   265285   4226974  178746  13175   326  46 25.1 433.5   39
c -  473.4   12303   265285   4295417  179691  13183   326  14 25.1 433.7   40
c -  481.3   12303   265285   4365510  181605  13235   326  43 25.0 432.2   39
c -  486.3   12303   265285   4434944  182882  13251   326  40 24.9 431.8   39
c -  491.0   12303   265285   4504323  183500  13252   326  36 24.8 432.2   41
c -  495.1   12303   265285   4573371  184098  13253   326  38 24.7 432.5   41
c -  505.0   12303   265285   4645351  186245  13319   326  14 24.7 431.2   40
c -  509.5   12303   265285   4715776  187356  13322   326  45 24.6 431.3   37
c -  515.5   12303   265285   4785287  187980  13322   326  48 24.5 431.7   61
c -  522.0   12303   265285   4855928  188540  13322   326  47 24.4 432.0   61
c -  529.0   12303   265285   4927758  189057  13322   326  49 24.4 432.3   61
c -  534.9   12303   265285   4999236  189694  13322   326  41 24.3 432.7   61
c 
c [simplification-12] limit of 5054291 conflicts hit after 5054292 conflicts
c [ternres-10] limit 155538006 with penalty 0 = 0 + 0
c [ternres-10] all 12303 free variables schedulable
c [ternres-10] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3888450 penalty 3 = 3 + 0
c [gauss-4] extracted 1201 xors of average arity 4.9
c [gauss-4] connected 5933 occurrences of 362 variables (average 16.4)
c [gauss-4] limit 3888450 penalty 3 = 3 + 0
c [gauss-4] fully completed
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 12303 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [cliff-4] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-4] failed 0, lifted 0
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 0 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 12303 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-5] limit of 38884501 steps penalty 3 = 3 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 19442251 steps for small clauses
c [cce-5] scheduling 1103 clauses = 351 binary + 752 ternary
c [cce-5] tried to eliminate 1103 small clauses 100%
c [cce-5] eliminated 11 small clauses 1%
c [cce-5] eliminated 1 binary clauses 0%
c [cce-5] eliminated 10 ternary clauses 1%
c [cce-5-1] eliminated 11 small clauses in 19878975 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 11 covered clauses in round 1
c [cce-5-2] eliminated 261 clauses out of 91558 (0%) of length 6
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] eliminated 261 large clauses in 19005527 steps
c [cce-5-2] allowing another 9502763 steps for small clauses
c [cce-5] scheduling 1092 clauses = 350 binary + 742 ternary
c [cce-5] tried to eliminate 1092 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 261 covered clauses in round 2
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] allowing another 4534700 steps for small clauses
c [cce-5] scheduling 1092 clauses = 350 binary + 742 ternary
c [cce-5] tried to eliminate 1092 small clauses 100%
c [cce-5-3] completed small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 272 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 12303 variables 100%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6] incomplete 3567 not tried 29% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1 = 0% variables out of 12303
c [elim-6] 1 < 1/1000 * 12303 = 12 considered unsuccessful
c [rephase-8] after 5054292 conflicts (new increment 2560000, next 7614292)
c [flushphases] 0 phases reset
c [simplification-12] removed 1 variables 0.0% (12302 remain 94%)
c [simplification-12] removed 451 irredundant clauses 0.2% (264834 remain 86%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 6054292
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  544.9   12302   264834   5071620  190408  13354   327  44 24.2 433.0   43
c -  552.2   12302   264834   5146145  191016  13354   327  47 24.3 433.4   43
c -  561.4   12302   264834   5221223  191640  13354   327  42 24.4 433.9   43
c -  566.6   12302   264834   5295430  192687  13361   327  36 24.4 434.3   66
c -  572.2   12302   264834   5369604  193130  13361   327  43 24.5 434.5   66
c -  578.9   12302   264834   5444833  193868  13361   327  40 24.4 434.8   42
c -  585.9   12302   264834   5520531  194678  13361   327  41 24.5 435.1   42
c -  601.9   12302   264834   5598433  195266  13361   327  41 24.6 435.4   42
c -  614.2   12302   264834   5675545  196157  13361   327  43 24.7 435.7   42
c -  626.7   12302   264834   5752506  196900  13361   327  39 24.7 436.0   42
c -  638.3   12302   264834   5829439  197669  13361   327  40 25.0 436.3   64
c -  646.4   12302   264834   5906590  198167  13362   327  14 25.0 436.5   42
c -  661.8   12302   264834   5987748  201820  13457   327  15 25.0 434.4   42
c 
c [simplification-13] limit of 6054292 conflicts hit after 6054292 conflicts
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 12302 free variables schedulable
c [ternres-11] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-11] fully completed ternary resolution
c [simpleprobe-4] 3686 schedulable variables 30%
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 8 hbrs, 0 units
c [lift-5] limit 2500000 with penalty 3 = 3 + 0
c [lift-5] using 884 probes 7%
c [lift-5-1] found 0 units 0 impls in round 1
c [lift-5-2] found 0 units 0 impls in round 2
c [lift-5-3] found 0 units 0 impls in round 3
c [lift-5-4] found 0 units 0 impls in round 4
c [lift-5-5] found 0 units 0 impls in round 5
c [lift-5] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-5] 6792 variables remain 55% (5510 retained)
c [simplification-13] removed 0 variables 0.0% (12302 remain 94%)
c [simplification-13] removed 0 irredundant clauses 0.0% (264834 remain 86%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] new conflict limit 8054292
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  671.7   12302   264834   6068812  205270  13513   335  45 24.9 434.0   42
c -  677.2   12302   264834   6148865  206168  13515   335  46 24.8 434.1   42
c -  695.8   12302   264834   6230674  209312  13539   335  34 25.4 434.7   42
c -  742.3   12302   264834   6308821  210443  13541   335  34 26.6 435.3   42
c -  799.9   12302   264834   6386877  211169  13544   335  34 28.0 435.7   42
c -  832.7   12302   264834   6467583  211745  13548   335  49 28.7 435.8   43
c -  846.8   12302   264834   6551315  214374  13600   335  16 28.6 433.6   44
c -  859.3   12302   264834   6637036  217227  13651   335  21 28.5 432.8   44
c -  875.8   12302   264834   6722874  220792  13731   335  38 28.4 430.6   44
c -  881.0   12302   264834   6807968  221706  13737   335  40 28.3 431.1   44
c -  894.9   12302   264834   6891344  222691  13738   335  35 28.8 431.7   44
c -  910.9   12302   264834   6975837  223751  13740   335  36 29.2 432.2   44
c -  924.8   12302   264834   7059593  224716  13740   335  38 29.6 432.7   44
c -  933.0   12302   264834   7144758  225555  13742   335  39 29.7 433.3   70
c -  941.2   12302   264834   7231098  226760  13746   335  37 29.8 433.8   70
c -  952.8   12302   264834   7317847  227646  13750   335  14 29.9 434.0   45
c -  966.7   12302   264834   7406896  230770  13791   335  33 29.8 433.0   44
c -  980.2   12302   264834   7492069  231886  13805   335  11 30.1 432.8   45
c -  997.5   12302   264834   7584960  235999  13853   335  30 30.0 431.6   45
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 32 basic ate = 29 trn 91% + 3 lrg 9% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 644119 steps
c bkwd: tried 24694 clauses, 48378 lits, 1.96 lits/clause
c bkwd: checked 3052170 occs, 123.60 occs/clause, 63.09 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 967 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 44 large (0% self)
c blkd: 5 bces, 1057 removed, 24373374 resolutions, 42815067 steps
c blkd: 124 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 9736278 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 704 subsumed
c card: 12 at-most-one constraints found, average size 3.00
c card: 12 at-most-one constraints used 100%, average size 3.00
c card: 29 at-most-two constraints found, average size 4.03
c card: 28 at-most-two constraints used 97%, average size 4.04
c cces: 5 cces, 31322 eliminated, 31322 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 1824262 esteps, 39814 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: 1259 extracted (7 ands 1%, 1215 xors 97%, 37 ites 3%)
c clff: 4 cliffs, 0 lifted, 0 failed
c clff: 1699886 decisions, 30653557 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3616992 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 54 gcs, 0 rescored clauses, 3755 rescored vars
c dcps: 24 decompositions, 37 equivalent 0%
c deco: 5773 decision-only clauses 0%, 46% reduction
c decs: 87938655 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3500042 flipped 3.980% (in 6375 phases)
c elms: 6 elims, 674 eliminated 5%
c elms: 7 rounds, 1.2 rounds/bve
c elms: 672 small 100%, 2 large 0%
c elms: 3326 tried small, 672 succeeded 20%, 2654 failed 80%
c elms: 2303 subsumed, 5588 strengthened, 4 blocked
c elms: 2963168 copies, 8411247 resolutions, 984547 ipos
c elms: 522392 subchks, 251928 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 3084 extracted, 5.0 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15743394 steps, 7871697 extr 50%, 69238 elim 0%
c glue: 30.1 orig avg, 30.0 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 74 = 17 simple + 52 trn 23% + 5 lrg 70%, 35 sub 7%
c hght: 432 average, 14.36 height/glue
c ints: 184919 luby (57722773 steps), 0 inout (0 steps)
c lift: 5 phases, 109644 probed (36554 level1 33%, 73090 level2 67%)
c lift: 0 units, 3 equivalences, 32 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 7139003 clauses, 71.4 length
c lrnd: 1892616 uips 27%, 4569859 flips 64%
c mega: 0 count, 0 failed, 0 rounds
c mins: 509943589 learned lits, 1% minimized
c mins: 6477427 mins 91%, 106 bin 0%, 655697 size 9%, 5773 deco 0%
c move: moved 7139003, 7 bin 0%, 1413 trn 0%, 0 lrg 0%
c otfs: str 1470275 dyn (1459660 red, 10615 irr) 461690 drv 31%, 1008585 rst 69%
c otfs: sub 24177 dyn (24177 red, 0 irr)
c phas: 9 computed, 12888 set, 5039 pos (39%), 7849 neg (61%)
c prbs: 3 basic, 8674 probed, 3 failed, 0 lifted
c prbs: 4 simple, 36166 probed, 5 failed, 0 eqs
c prbs: 3 treelook, 2943 probed, 0 failed, 0 lifted
c prps: 815891477 props, 9 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 97430268 searches, 8874435 hits, 9% 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: 161 count, 0 reset, 3 acts 2%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 161 arith 100%, 0 double 0%
c rmbd: 32 removed, 22 red 69%
c rphs: 8 recomputed phases
c rsts: 81171 restarts 44%, 103748 skipped 56%
c rsts: 0 saturating 0%, 94194 agile 91%, 9554 reuse 9%
c rsts: 92.5 avg interval, 92.5 scaled, 1.0 factor
c rsts: 20611 kept 25.4% average 51.0%
c simp: 13 count (13 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 7139003 count (12644775 tried 1.8), 97876 sub out of 7134400 (1.4%)
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: 395 fixed 3%, 1 its, 7600693.00 confs/it
c trvs: 54486719922 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 66.9 search traversals per propagation, 7164.2 per conflict
c trvs: 1.8 search traversals per search visit
c trds: 10 transitive reductions, 29 removed, 0 failed
c trds: 244395 nodes, 5361 edges, 6615 steps
c trim: 1952816 words, 7.4 MB
c trnr: 11 count, 47 bin, 459 trn, 22233919 steps
c unhd: 5 count, 7 rounds, 5107529 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 9 failed, 9 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1057 tauts, 0 bin 0%, 763 trn 72%, 286 lrg 27%
c unhd: 1057 tauts, 8 stamp 1%, 525 red 50%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 126687 str, 0 bin 0%, 50 trn 0%, 126637 lrg 100%, 126625 red 100%
c vars: 12302 remaining 92% and 1106 removed 8% out of 13408
c vars: 395 fixed 3%, 674 eliminated 5%, 37 equivalent 0%
c vsts: 31030792202 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 38.1 search visits per propagation, 4078.2 per conflict
c wchs: 11415820371 pushed, 29849653 enlarged, 397 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   7134400 100   6752388 100 179422209 100  62320667 100   3570538 100
c 
c  0     162722   2         0   0  95307463  53  20253725  32    503910  14 
c  1     351780   5    262146   4  43520892  24< 10964623  18    456627  13 
c  2    1040456  15   1029436  15  15613070   9   7879700  13<   624226  17 
c  3    1220602  17   1205403  18  10592662   6   7485582  12    583828  16 
c  4    1260726  18   1237624  18   6477055   4   5607848   9    381639  11<
c  5    1006094  14<   976073  14<  3615461   2   3592504   6    196162   5 
c  6     680600  10    666311  10   1723812   1   2181721   4    199889   6 
c  7     426619   6    420043   6    845333   0   1266902   2    145684   4 
c  8     317029   4    310912   5    581551   0    985433   2    140083   4 
c  9     182411   3    177015   3    331031   0    577284   1     88852   2 
c 10     211129   3    204755   3    330430   0    613679   1     89575   3 
c 11     231513   3    225313   3    397687   0    747969   1    126504   4 
c 12      31736   0     29684   0     62273   0    133908   0     31699   1 
c 13      10983   0      7673   0     23489   0     29789   0      1860   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             4.6           4.7           1.0           2.3           3.6
c std             2.6           2.5           1.6           2.5           3.0
c 
c  116.178  12% analysis
c   81.746   8% decide
c   20.546   2% bump
c   13.259   1% mincls
c    8.401   1% defrag
c    7.946   1% cce
c    7.410   1% restart
c    5.391   1% elim
c    4.900   0% gc
c    3.541   0% decomp
c    3.200   0% reduce
c    3.069   0% block
c    3.003   0% probe
c    1.781   0% cliff
c    1.166   0% unhide
c    0.863   0% lift
c    0.717   0% gauss
c    0.660   0% cgrclsr
c    0.469   0% bca
c    0.412   0% phase
c    0.213   0% backward
c    0.208   0% card
c    0.149   0% ternres
c    0.048   0% transred
c    0.017   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c    0.000   0% tabularasa
c ----------------------------------
c    1.429   0% probe simple     48%
c    0.856   0% probe basic      29%
c    0.718   0% probe tree-look  24%
c ==================================
c    1.484   0% preprocessing     5%
c   27.437   3% inprocessing     95%
c ==================================
c   28.921   3% simplifying
c  970.675  97% search
c ==================================
c  999.596 100% all
c 
c 87938655 decisions, 87974.2 decisions/sec
c 7600693 conflicts, 7603.8 conflicts/sec
c 815891477 propagations, 0.8 megaprops/sec
c 999.6 seconds, 278.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
