c launch: /data/cnf/sc2014/app/MD5-31-5.cnf.bz2
c host: atom25
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/MD5-31-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-31-5.cnf.bz2
c no embedded options
c found 'p cnf 9219 70899' header
c read 9219 variables, 70899 clauses, 277337 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
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 --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
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=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
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 --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
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 --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
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 --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 9208 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 [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0    9208    70634         0       0      0     0    0     0    4   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 2 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 122 out of 122 constraints (100%) meet size limits
c [card-1] found 2 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 30 variables
c [simpleprobe-1] all 9189 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 6 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 6 variables, found 327 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 64 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 9183 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 2660 variables 29% in round 1 in 9720883 steps
c [elim-1-1] backward subsumption/strengthening limit 9720800
c [elim-1-1-1] backward checking 6440 touched variables 70%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 26 and strengthened 42 clauses in 1303114 steps
c [elim-1-1] rescheduled 85 variables 1% by backward subsumption
c [elim-1-2] eliminated 8 variables 0% in round 2 in 223169 steps
c [elim-1-2] backward subsumption/strengthening limit 223100
c [elim-1-2-1] backward checking 69 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 9 and strengthened 37 clauses in 175964 steps
c [elim-1-2] rescheduled 39 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 111557 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2668 = 29% variables out of 9183 scheduled
c [phase-count-1] 68458 negative 99.1% of 69067 except 609 0.9%
c [phase-count-1] 66460 positive 96.2% of 69067 except 2607 3.8%
c [phase-count-1] less non-negative clauses 609 than limit 6900 (10.0%)
c [phase-count-1] non-pos/non-neg = 2607/609 = 4.28 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6515 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 6515 zero 100.00%
c [score-distribution-1] 1 different 0.02% out of total 6515 variables
c [simplification-1] removed 2693 variables 29.2% (6515 remain 71%)
c [simplification-1] removed 1567 irredundant clauses 2.2% (69067 remain 98%)
c [simplification-1] maximum reduction of 29% = max (29%, 2%)
c [simplification-1] large reduction 29% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] all 6515 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1987 variables remain 30% (4528 retained 70%)
c [simpleprobe-2] removed 0 variables, found 27 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12452 literals 96%
c [treelook-1] scheduling used 300012 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300066 steps
c [treelook-1] 9584 literals remain 74%
c [treelook-1] 6431 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 56 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 739 sched 11%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-1-1] 741 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 22 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6515 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 42 blocked clauses
c [block-1] 42 < 1/100 * 69067 = 690 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 51 clauses out of 832 (6%) of length 6
c [cce-1-1] eliminated 8660 clauses out of 27265 (32%) of length 5
c [cce-1-1] eliminated 346 clauses out of 23691 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 9057 large clauses in 11871787 steps
c [cce-1-1] allowing another 5935893 steps for small clauses
c [cce-1-1] scheduling 15232 clauses = 584 binary + 14648 ternary
c [cce-1-1] tried to eliminate 15232 small clauses 100%
c [cce-1-1] eliminated 3 binary clauses 1%
c [cce-1-1] eliminated 270 ternary clauses 2%
c [cce-1-1] eliminated 273 small clauses 2%
c [cce-1-1] eliminated 273 small clauses in 8083425 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 9330 covered clauses in round 1
c [cce-1-2] eliminated 2 clauses out of 781 (0%) of length 6
c [cce-1-2] eliminated 5 clauses out of 18605 (0%) of length 5
c [cce-1-2] eliminated 1 clauses out of 23345 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 8 large clauses in 10658376 steps
c [cce-1-2] allowing another 5329188 steps for small clauses
c [cce-1-2] scheduling 14959 clauses = 581 binary + 14378 ternary
c [cce-1-2] tried to eliminate 14959 small clauses 100%
c [cce-1-2] eliminated 2 ternary clauses 0%
c [cce-1-2] eliminated 2 small clauses 0%
c [cce-1-2] eliminated 2 small clauses in 7546384 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 10 covered clauses in round 2
c [cce-1-3] eliminated 2 clauses out of 779 (0%) of length 6
c [cce-1-3] eliminated 15 clauses out of 18600 (0%) of length 5
c [cce-1-3] eliminated 20 clauses out of 23344 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 37 large clauses in 12047989 steps
c [cce-1-3] allowing another 6023994 steps for small clauses
c [cce-1-3] scheduling 14957 clauses = 581 binary + 14376 ternary
c [cce-1-3] tried to eliminate 14957 small clauses 100%
c [cce-1-3] eliminated 18 ternary clauses 0%
c [cce-1-3] eliminated 18 small clauses 0%
c [cce-1-3] eliminated 18 small clauses in 8452743 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 55 covered clauses in round 3
c [cce-1] eliminated 9395 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6513 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 138 variables 2% in round 1 in 15446990 steps
c [elim-2-1] backward subsumption/strengthening limit 4553010
c [elim-2-1-1] backward checking 376 touched variables 6%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 2 and strengthened 23 clauses in 111829 steps
c [elim-2-1] rescheduled 44 variables 1% by backward subsumption
c [elim-2-2] eliminated 4 variables 0% in round 2 in 100838 steps
c [elim-2-2] backward subsumption/strengthening limit 100800
c [elim-2-2-1] backward checking 15 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 53222 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 142 = 2% variables out of 6513 scheduled
c [bca-1] limit of 10000000 steps and 117586 added (scaled 2)
c [bca-1] 11307 out of 12744 literals actually usable 89%
c [bca-1] added 0 blocked clauses in 46258 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1313 pos 20.6% + 5058 neg 79.4% = 6371 sched 100.0% ret 0
c [sweep-1-1] 1000214 steps 938 queries 476.99 avg class size
c [sweep-1-1] 8468 decisions 937 SAT calls 15.83 avg env size
c [sweep-1-1] 1092 variables remain 17% (5279 retained 83%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 937 queries)
c [phase-count-2] 57957 negative 99.0% of 58543 except 586 1.0%
c [phase-count-2] 56046 positive 95.7% of 58543 except 2497 4.3%
c [phase-count-2] less non-negative clauses 586 than limit 5800 (10.0%)
c [phase-count-2] non-pos/non-neg = 2497/586 = 4.26 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 449 negative 100%
c [score-distribution-2] 2187 pos 34.33%, 0 min 0.00%, 4184 zero 65.67%
c [score-distribution-2] 1085 different 17.03% out of total 6371 variables
c [simplification-2] removed 144 variables 2.2% (6371 remain 69%)
c [simplification-2] removed 10524 irredundant clauses 15.2% (58543 remain 83%)
c [simplification-2] maximum reduction of 15% = max (2%, 15%)
c [simplification-2] large reduction 15% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 23717 quaternary clauses 53% in total
c [quatres-1-1] added 4 double-self-subsuming ternary resolvents
c [quatres-1-2] added 256 single-self-subsuming ternary resolvents
c [quatres-1-2] added 511 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 6371 free variables schedulable
c [ternres-1] 3934 ternary resolvents (36 bin, 3898 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 13 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 14 out of 14 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 11890 xors of average arity 3.5
c [gauss-1] connected 41284 occurrences of 3530 variables (average 11.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 114 tauts, 0 hbrs, 98 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 14 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 45 clauses out of 18145 (0%) of length 5
c [cce-2-1] eliminated 86 clauses out of 23047 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 131 large clauses in 9881789 steps
c [cce-2-1] allowing another 4940894 steps for small clauses
c [cce-2-1] scheduling 14534 clauses = 604 binary + 13930 ternary
c [cce-2-1] tried to eliminate 14534 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 0%
c [cce-2-1] eliminated 9 ternary clauses 0%
c [cce-2-1] eliminated 12 small clauses 0%
c [cce-2-1] eliminated 12 small clauses in 7033917 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 143 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 4921785 steps for small clauses
c [cce-2-2] scheduling 14522 clauses = 601 binary + 13921 ternary
c [cce-2-2] tried to eliminate 14522 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 143 covered clauses in TOTAL during 2 rounds
c [cce-2] 143 < 1/100 * 58543 = 585 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6371 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 71 variables 1% in round 1 in 15201514 steps
c [elim-3-1] backward subsumption/strengthening limit 4798486
c [elim-3-1-1] backward checking 61 touched variables 1%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 1 and strengthened 4 clauses in 59806 steps
c [elim-3-1] rescheduled 11 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 19178 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 71 = 1% variables out of 6371 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 392 pos 36.8% + 673 neg 63.2% = 1065 sched 16.9% ret 5235
c [sweep-2-1] 164432 steps 466 queries 102.16 avg class size
c [sweep-2-1] 3700 decisions 465 SAT calls 13.98 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 2246 pos 35.7% + 4054 neg 64.3% = 6300 sched 100.0% ret 0
c [sweep-2-2] 836397 steps 680 queries 531.66 avg class size
c [sweep-2-2] 7200 decisions 682 SAT calls 18.60 avg env size
c [sweep-2-2] 1807 variables remain 29% (4493 retained 71%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 1144 queries)
c [phase-count-3] 57397 negative 99.0% of 57990 except 593 1.0%
c [phase-count-3] 55490 positive 95.7% of 57990 except 2500 4.3%
c [phase-count-3] less non-negative clauses 593 than limit 5700 (10.0%)
c [phase-count-3] non-pos/non-neg = 2500/593 = 4.22 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 29 negative 100%
c [score-distribution-3] 3614 pos 57.37%, 2 min 0.03%, 2684 zero 42.60%
c [score-distribution-3] 1598 different 25.37% out of total 6300 variables
c [simplification-3] removed 71 variables 1.1% (6300 remain 68%)
c [simplification-3] removed 553 irredundant clauses 0.9% (57990 remain 82%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c [simplification-4] limit of 1584 ternary hit after 1584 ternaries
c [quatres-2] found 24919 quaternary clauses 52% in total
c [quatres-2-1] added 4 double-self-subsuming ternary resolvents
c [quatres-2-2] added 503 single-self-subsuming ternary resolvents
c [quatres-2-2] added 794 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 6300 free variables schedulable
c [ternres-2] 920 ternary resolvents (2 bin, 918 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5718 literals 45%
c [treelook-2] scheduling used 150038 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150086 steps
c [treelook-2] 4276 literals remain 34%
c [treelook-2] 3508 variables remain to probed next time 56%
c [treelook-2] removed 0 variables, found 20 hbrs
c [transred-2] limit 267090 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 6300 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 56 blocked clauses
c [block-2] 56 < 1/100 * 57990 = 579 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 6294 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 15151743 steps
c [elim-4-1] backward subsumption/strengthening limit 15151700
c [elim-4-1-1] backward checking 25 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 48279 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 6294 scheduled
c [elim-4] 2 < 1/100 * 6294 = 62 considered unsuccessful
c [bca-2] limit of 10000000 steps and 116294 added (scaled 2)
c [bca-2] 4997 out of 12586 literals actually usable 40%
c [bca-2] added 0 blocked clauses in 27606 steps
c [phase-count-4] 57298 negative 99.0% of 57897 except 599 1.0%
c [phase-count-4] 55401 positive 95.7% of 57897 except 2496 4.3%
c [phase-count-4] less non-negative clauses 599 than limit 5700 (10.0%)
c [phase-count-4] non-pos/non-neg = 2496/599 = 4.17 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 12 negative 100%
c [score-distribution-4] 2780 pos 44.18%, 2079 min 33.04%, 1433 zero 22.77%
c [score-distribution-4] 1293 different 20.55% out of total 6292 variables
c [simplification-4] removed 8 variables 0.1% (6292 remain 68%)
c [simplification-4] removed 93 irredundant clauses 0.2% (57897 remain 82%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] forced so keeping old conflict interval 10000
c [simplification-4] conflict limit remains at 13000 (hard 23000)
c [simplification-4] new ternary interval 10000
c 
c [simplification-5] limit 13000 conflicts (hard 23000) hit after 13001 conflicts
c [quatres-3] found 25594 quaternary clauses 52% in total
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 199 single-self-subsuming ternary resolvents
c [quatres-3-2] added 638 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 6292 free variables schedulable
c [ternres-3] 198 ternary resolvents (4 bin, 194 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5034 xors of average arity 3.0
c [gauss-2] connected 15102 occurrences of 1496 variables (average 10.1)
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 [transred-3] limit 368232 with penalty 0 = 0 + 0
c [transred-3] removed 6 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 7 clauses out of 18015 (0%) of length 5
c [cce-3-1] eliminated 99 clauses out of 22767 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 106 large clauses in 11717552 steps
c [cce-3-1] allowing another 5858776 steps for small clauses
c [cce-3-1] scheduling 936 clauses = 599 binary + 337 ternary
c [cce-3-1] tried to eliminate 936 small clauses 100%
c [cce-3-1] eliminated 2 binary clauses 0%
c [cce-3-1] eliminated 15 ternary clauses 4%
c [cce-3-1] eliminated 17 small clauses 2%
c [cce-3-1] eliminated 17 small clauses in 5966933 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 123 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 4516533 steps for small clauses
c [cce-3-2] scheduling 919 clauses = 597 binary + 322 ternary
c [cce-3-2] tried to eliminate 919 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 123 covered clauses in TOTAL during 2 rounds
c [cce-3] 123 < 1/100 * 57896 = 578 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 801 pos 44.4% + 1002 neg 55.6% = 1803 sched 28.7% ret 4489
c [sweep-3-1] 394936 steps 622 queries 116.32 avg class size
c [sweep-3-1] 7268 decisions 623 SAT calls 19.06 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 2872 pos 45.6% + 3420 neg 54.4% = 6292 sched 100.0% ret 0
c [sweep-3-2] 108102 steps 65 queries 1621.17 avg class size
c [sweep-3-2] 1197 decisions 64 SAT calls 29.62 avg env size
c [sweep-3-2] 5943 variables remain 94% (349 retained 6%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 685 queries)
c [phase-count-5] 57180 negative 99.0% of 57773 except 593 1.0%
c [phase-count-5] 55277 positive 95.7% of 57773 except 2496 4.3%
c [phase-count-5] less non-negative clauses 593 than limit 5700 (10.0%)
c [phase-count-5] non-pos/non-neg = 2496/593 = 4.21 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1 negative 100%
c [score-distribution-5] 3576 pos 56.83%, 1523 min 24.21%, 1193 zero 18.96%
c [score-distribution-5] 1684 different 26.76% out of total 6292 variables
c [simplification-5] removed 0 variables 0.0% (6292 remain 68%)
c [simplification-5] removed 124 irredundant clauses 0.2% (57773 remain 82%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 30000
c [simplification-5] penalized conflict interval 30000 = 1 * 30000
c [simplification-5] hard conflict limit 58001 (soft 43001 + delta 15000)
c [simplification-5] new conflict limit 43001 (hard 58001)
c 
c [simplification-6] limit 43001 conflicts (hard 58001) hit after 43001 conflicts
c [quatres-4] found 28960 quaternary clauses 47% in total
c [quatres-4-1] added 14 double-self-subsuming ternary resolvents
c [quatres-4-2] added 716 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1172 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 6292 free variables schedulable
c [ternres-4] 1024 ternary resolvents (13 bin, 1011 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 5 at-most-one constraints of average size 3.0
c [card-3] found 22 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 27 out of 27 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 4606808 penalty 1 = 1 + 0
c [basicprobe-2-0] 1058 sched 17%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-2-1] 1071 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 37 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-3] limit 92136 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 35 tauts, 0 hbrs, 817 literals
c [transred-4] limit 1842723 with penalty 0 = 0 + 0
c [transred-4] removed 18 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 6292 variables 100%
c [elim-5] limit of 18427234 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2 variables 0% in round 1 in 15006309 steps
c [elim-5-1] backward subsumption/strengthening limit 3420925
c [elim-5-1-1] backward checking 13 touched variables 0%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 46239 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 6292 scheduled
c [elim-5] 2 < 1/100 * 6292 = 62 considered unsuccessful
c [score-distribution-6] 4005 pos 63.67%, 1444 min 22.96%, 841 zero 13.37%
c [score-distribution-6] 1923 different 30.57% out of total 6290 variables
c [simplification-6] removed 2 variables 0.0% (6290 remain 68%)
c [simplification-6] removed 104 irredundant clauses 0.2% (57669 remain 82%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30000
c [simplification-6] new conflict interval 60000
c [simplification-6] penalized conflict interval 60000 = 1 * 60000
c [simplification-6] hard conflict limit 133001 (soft 103001 + delta 30000)
c [simplification-6] new conflict limit 103001 (hard 133001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   27.6    6290    57669     91075   37945  13176   605    9   347   17   2%    765  106    9    6  154%
c 
c [simplification-7] limit 103001 conflicts (hard 133001) hit after 103002 conflicts
c [quatres-5] found 33228 quaternary clauses 42% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 10 double-self-subsuming ternary resolvents
c [quatres-5-2] added 783 single-self-subsuming ternary resolvents
c [quatres-5-2] added 1034 quaternary resolvents
c [ternres-5] limit 6284039 with penalty 0 = 0 + 0
c [ternres-5] all 6290 free variables schedulable
c [ternres-5] 831 ternary resolvents (9 bin, 822 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 14 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 6290 variables 100%
c [block-3] limit of 15710099 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps and 115838 added (scaled 2)
c [bca-3] 2478 out of 12582 literals actually usable 20%
c [bca-3] added 0 blocked clauses in 59453 steps
c [score-distribution-7] 4242 pos 67.44%, 1405 min 22.34%, 643 zero 10.22%
c [score-distribution-7] 1968 different 31.29% out of total 6290 variables
c [simplification-7] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-7] removed 0 irredundant clauses 0.0% (57669 remain 82%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 60000
c [simplification-7] new conflict interval 120000
c [simplification-7] penalized conflict interval 120000 = 1 * 120000
c [simplification-7] hard conflict limit 283002 (soft 223002 + delta 60000)
c [simplification-7] new conflict limit 223002 (hard 283002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   47.9    6290    57669    154758   54444  15772   621   10   353   12   3%    926   44   10    8  127%
c -   65.1    6290    57669    216749   68550  16666   663   11   393   13   3%    986   44   11    9  118%
c 
c [simplification-8] limit 223002 conflicts (hard 283002) hit after 223004 conflicts
c [quatres-6] found 38571 quaternary clauses 36% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 9 double-self-subsuming ternary resolvents
c [quatres-6-2] added 675 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1241 quaternary resolvents
c [ternres-6] limit 15698413 with penalty 0 = 0 + 0
c [ternres-6] all 6290 free variables schedulable
c [ternres-6] 710 ternary resolvents (8 bin, 702 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 784920 penalty 2 = 2 + 0
c [gauss-3] extracted 2312 xors of average arity 3.0
c [gauss-3] connected 6936 occurrences of 1384 variables (average 5.0)
c [gauss-3] limit 784920 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1921 schedulable variables 31%
c [simpleprobe-3] limit 31396827 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 59 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 48 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 196230170 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 118 clauses out of 17696 (1%) of length 5
c [cce-4-1] eliminated 467 clauses out of 22664 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 585 large clauses in 9498164 steps
c [cce-4-1] allowing another 4749082 steps for small clauses
c [cce-4-1] scheduling 14408 clauses = 608 binary + 13800 ternary
c [cce-4-1] tried to eliminate 14408 small clauses 100%
c [cce-4-1] eliminated 2 ternary clauses 0%
c [cce-4-1] eliminated 2 small clauses 0%
c [cce-4-1] eliminated 2 small clauses in 6814398 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 587 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 4652561 steps for small clauses
c [cce-4-2] scheduling 14406 clauses = 608 binary + 13798 ternary
c [cce-4-2] tried to eliminate 14406 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 587 covered clauses in TOTAL during 2 rounds
c [sweep-4] limit 1177381 penalty 2 = 2 + 0
c [sweep-4-1] 2842 pos 47.8% + 3100 neg 52.2% = 5942 sched 94.5% ret 348
c [sweep-4-1] 1178807 steps 321 queries 328.92 avg class size
c [sweep-4-1] 11132 decisions 320 SAT calls 59.95 avg env size
c [sweep-4-1] 1362 variables remain 22% (4928 retained 78%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 320 queries)
c [score-distribution-8] 4972 pos 79.05%, 1102 min 17.52%, 216 zero 3.43%
c [score-distribution-8] 2406 different 38.25% out of total 6290 variables
c [simplification-8] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-8] removed 587 irredundant clauses 1.0% (57082 remain 81%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 60000 = 120000 / 2
c [simplification-8] new conflict interval 180000
c [simplification-8] penalized conflict interval 180000 = 1 * 180000
c [simplification-8] hard conflict limit 493004 (soft 403004 + delta 90000)
c [simplification-8] new conflict limit 403004 (hard 493004)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   80.8    6290    57082    278173   81717  18716   695   12   404   14   3%   1009   20   12   10  113%
c -   94.3    6290    57082    339597   93423  19275   707   13   430   15   3%   1018   28   12   12  107%
c -  107.3    6290    57082    401374  104393  19782   715   13   430   16   3%   1022   11   12   13   93%
c 
c [simplification-9] limit 403004 conflicts (hard 493004) hit after 403004 conflicts
c [quatres-7] found 44016 quaternary clauses 31% in total
c [quatres-7-1] removed 11 duplicate quaternary clauses
c [quatres-7-1] added 10 double-self-subsuming ternary resolvents
c [quatres-7-2] added 601 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1230 quaternary resolvents
c [ternres-7] limit 26608072 with penalty 0 = 0 + 0
c [ternres-7] all 6290 free variables schedulable
c [ternres-7] 494 ternary resolvents (10 bin, 484 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 19 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6290 variables 100%
c [elim-6] limit of 133040361 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 14572076 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 6290 scheduled
c [score-distribution-9] 5964 pos 94.82%, 316 min 5.02%, 10 zero 0.16%
c [score-distribution-9] 3141 different 49.94% out of total 6290 variables
c [simplification-9] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-9] removed 56 irredundant clauses 0.1% (57026 remain 81%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 180000
c [simplification-9] new conflict interval 360000
c [simplification-9] penalized conflict interval 360000 = 1 * 360000
c [simplification-9] hard conflict limit 943004 (soft 763004 + delta 180000)
c [simplification-9] new conflict limit 763004 (hard 943004)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  121.0    6290    57026    462983  115038  21160   710   14   438   17   3%   1023   11   16   13  117%
c -  134.1    6290    57026    525011  124417  21450   714   16   428   18   4%   1024   -9   15   14  107%
c -  147.1    6290    57026    587786  133566  21695   719   16   457   18   3%   1024   15   18   15  118%
c -  160.4    6290    57026    651169  142609  21973   720   17   448   19   4%   1024    1   18   16  118%
c -  174.2    6290    57026    715303  151218  22225   733   16   478   20   3%   1024   27   18   16  113%
c 
c [simplification-10] limit 763004 conflicts (hard 943004) hit after 764855 conflicts
c [quatres-8] found 50756 quaternary clauses 26% in total
c [quatres-8-1] removed 38 duplicate quaternary clauses
c [quatres-8-1] added 13 double-self-subsuming ternary resolvents
c [quatres-8-2] added 569 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1076 quaternary resolvents
c [ternres-8] limit 48203656 with penalty 0 = 0 + 0
c [ternres-8] all 6290 free variables schedulable
c [ternres-8] 360 ternary resolvents (12 bin, 348 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 3012728 penalty 3 = 3 + 0
c [card-4] found 12 at-most-one constraints of average size 3.0
c [card-4] found 38 at-most-two constraints of average size 4.0
c [card-4] using previous limit 3012728 for elimination
c [card-4] 48 out of 50 constraints (96%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1205091 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 1053 tauts, 0 hbrs, 22210 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 21 transitive binary clauses
c [cce-5] limit of 120509141 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 43 clauses out of 17433 (0%) of length 5
c [cce-5-1] eliminated 223 clauses out of 22182 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 266 large clauses in 11045071 steps
c [cce-5-1] allowing another 5522535 steps for small clauses
c [cce-5-1] scheduling 1102 clauses = 612 binary + 490 ternary
c [cce-5-1] tried to eliminate 1102 small clauses 100%
c [cce-5-1] eliminated 3 binary clauses 0%
c [cce-5-1] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 5 small clauses 0%
c [cce-5-1] eliminated 5 small clauses in 5658012 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 271 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 5456278 steps for small clauses
c [cce-5-2] scheduling 1097 clauses = 609 binary + 488 ternary
c [cce-5-2] tried to eliminate 1097 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 271 covered clauses in TOTAL during 2 rounds
c [cce-5] 271 < 1/100 * 57026 = 570 considered unsuccessful
c [score-distribution-10] 5760 pos 91.57%, 530 min 8.43%, 0 zero 0.00%
c [score-distribution-10] 3206 different 50.97% out of total 6290 variables
c [simplification-10] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-10] removed 271 irredundant clauses 0.5% (56755 remain 80%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 360000
c [simplification-10] new conflict interval 720000
c [simplification-10] penalized conflict interval 720000 = 1 * 720000
c [simplification-10] hard conflict limit 1844855 (soft 1484855 + delta 360000)
c [simplification-10] new conflict limit 1484855 (hard 1844855)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  189.7    6290    56755    780176  161146  22515   761   18   454   20   4%   1024    2   18   17  111%
c -  203.8    6290    56755    844489  170794  22651   763   17   451   21   4%   1024   -4   17   17  102%
c -  217.7    6290    56755    908034  179031  22807   765   18   434   22   4%   1024  -18   17   17   99%
c -  232.4    6290    56755    971848  187247  22914   768   18   459   23   4%   1024    6   20   18  110%
c -  247.1    6290    56755   1036060  195336  23045   769   18   469   23   4%   1024   15   20   18  112%
c -  262.5    6290    56755   1100359  203059  23171   770   19   458   24   4%   1024    7   15   18   82%
c -  278.5    6290    56755   1165089  210271  23275   770   19   460   24   4%   1024    6   21   19  111%
c -  294.8    6290    56755   1230293  218030  23364   770   19   458   25   4%   1024    5   14   19   75%
c -  311.0    6290    56755   1295339  225734  23464   770   20   463   26   4%   1024    9   23   20  118%
c -  327.8    6290    56755   1360122  232140  23536   772   20   453   26   4%   1024    1   26   20  129%
c -  345.4    6290    56755   1426191  238633  23611   773   20   440   27   5%   1024  -11   19   20   97%
c 
c [simplification-11] limit 1484855 conflicts (hard 1844855) hit after 1491590 conflicts
c [quatres-9] found 57965 quaternary clauses 21% in total
c [quatres-9-1] removed 51 duplicate quaternary clauses
c [quatres-9-1] added 5 double-self-subsuming ternary resolvents
c [quatres-9-2] added 535 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1029 quaternary resolvents
c [ternres-9] limit 99890664 with penalty 0 = 0 + 0
c [ternres-9] all 6290 free variables schedulable
c [ternres-9] 283 ternary resolvents (10 bin, 273 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 2497266 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 7445 literals 59%
c [treelook-3] scheduling used 1181853 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2497266 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 843995 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 1 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 16 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6290 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-4] limit of 10000000 steps and 114010 added (scaled 2)
c [bca-4] 5 out of 12582 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 303861 steps
c [score-distribution-11] 6187 pos 98.36%, 103 min 1.64%, 0 zero 0.00%
c [score-distribution-11] 3608 different 57.36% out of total 6290 variables
c [simplification-11] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-11] removed 0 irredundant clauses 0.0% (56755 remain 80%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 720000
c [simplification-11] new conflict interval 1440000
c [simplification-11] penalized conflict interval 1440000 = 1 * 1440000
c [simplification-11] hard conflict limit 3651590 (soft 2931590 + delta 720000)
c [simplification-11] new conflict limit 2931590 (hard 3651590)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  364.4    6290    56755   1493314  245815  24484   768   20   456   27   4%   1024    3   18   20   93%
c -  383.1    6290    56755   1561082  252641  24539   769   21   445   28   5%   1024  -10   23   20  112%
c -  401.7    6290    56755   1629209  259472  24593   769   20   471   28   4%   1024   13   18   20   88%
c -  420.6    6290    56755   1697635  266387  24642   769   21   453   29   5%   1024   -6   24   21  117%
c -  440.3    6290    56755   1766139  272728  24674   772   22   460   29   5%   1024    1   22   21  106%
c -  459.5    6290    56755   1835328  279727  24724   772   21   460   30   5%   1024    1   22   21  102%
c -  480.0    6290    56755   1904247  285631  24765   772   21   437   31   5%   1024  -22   21   21   96%
c -  501.0    6290    56755   1974307  292403  24806   772   22   457   31   5%   1024   -3   20   22   93%
c -  522.0    6290    56755   2044597  298906  24838   772   22   438   32   5%   1024  -18   20   22   90%
c -  543.3    6290    56755   2115205  304872  24872   772   22   462   32   5%   1024    6   22   22  102%
c -  565.7    6290    56755   2186510  310251  24911   772   23   458   33   5%   1024    1   26   22  117%
c -  588.6    6290    56755   2259235  316328  24943   772   22   463   33   5%   1024    2   26   22  115%
c -  612.1    6290    56755   2332751  323049  24985   772   24   452   34   5%   1024   -9   27   23  120%
c -  635.6    6290    56755   2406109  329371  25012   772   23   462   34   5%   1024    4   26   23  116%
c -  659.4    6290    56755   2479854  335613  25064   773   24   443   35   5%   1024  -12   25   23  109%
c -  683.8    6290    56755   2553725  340725  25093   774   24   466   35   5%   1024    7   24   23  106%
c -  709.0    6290    56755   2629198  346649  25124   776   24   461   36   5%   1024   -0   24   23  104%
c -  735.4    6290    56755   2705216  352589  25151   776   24   455   36   5%   1024   -4   26   24  111%
c -  761.8    6290    56755   2781858  358172  25184   777   24   456   37   5%   1024   -3   22   24   93%
c -  788.6    6290    56755   2859240  364639  25220   778   24   465   37   5%   1024    4   28   24  116%
c 
c [simplification-12] limit 2931590 conflicts (hard 3651590) hit after 2931590 conflicts
c [quatres-10] found 65198 quaternary clauses 17% in total
c [quatres-10-1] removed 70 duplicate quaternary clauses
c [quatres-10-1] added 6 double-self-subsuming ternary resolvents
c [quatres-10-2] added 340 single-self-subsuming ternary resolvents
c [quatres-10-2] added 889 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 6290 free variables schedulable
c [ternres-10] 131 ternary resolvents (8 bin, 123 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5844949 penalty 3 = 3 + 0
c [gauss-4] extracted 21592 xors of average arity 3.7
c [gauss-4] connected 80152 occurrences of 6176 variables (average 13.0)
c [gauss-4] limit 5844949 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 12 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 87674242 penalty 3 = 3 + 0
c [sweep-5-1] 667 pos 49.0% + 695 neg 51.0% = 1362 sched 21.7% ret 4928
c [sweep-5-1] 2786095 steps 170 queries 36.61 avg class size
c [sweep-5-1] 15839 decisions 169 SAT calls 553.27 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 3054 pos 48.6% + 3236 neg 51.4% = 6290 sched 100.0% ret 0
c [sweep-5-2] 5648609 steps 276 queries 129.17 avg class size
c [sweep-5-2] 26267 decisions 275 SAT calls 662.93 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 3054 pos 48.6% + 3236 neg 51.4% = 6290 sched 100.0% ret 0
c [sweep-5-3] 5055377 steps 270 queries 134.33 avg class size
c [sweep-5-3] 25275 decisions 269 SAT calls 641.03 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 713 queries)
c [score-distribution-12] 5928 pos 94.24%, 362 min 5.76%, 0 zero 0.00%
c [score-distribution-12] 3180 different 50.56% out of total 6290 variables
c [simplification-12] removed 0 variables 0.0% (6290 remain 68%)
c [simplification-12] removed 0 irredundant clauses 0.0% (56755 remain 80%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1440000
c [simplification-12] new conflict interval 2880000
c [simplification-12] penalized conflict interval 2880000 = 1 * 2880000
c [simplification-12] hard conflict limit 7251590 (soft 5811590 + delta 1440000)
c [simplification-12] new conflict limit 5811590 (hard 7251590)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  819.7    6290    56755   2936419  371369  25677   778   24   458   38   5%   1024   -1   24   24  100%
c -  846.8    6290    56755   3013904  376914  25711   778   24   460   38   5%   1024    3   23   24   96%
c -  875.0    6290    56755   3092085  381683  25734   778   25   451   39   5%   1024   -8   27   24  112%
c -  904.0    6290    56755   3171935  387650  25753   778   24   459   39   5%   1024   -1   24   24  100%
c -  933.3    6290    56755   3252112  393800  25777   778   24   464   40   5%   1024    3   25   24  103%
c -  962.8    6290    56755   3332543  399023  25795   780   25   474   40   5%   1024   15   28   24  116%
c -  994.1    6290    56755   3414126  403656  25813   780   25   467   41   5%   1024    8   30   24  124%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2 basic ate = 2 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (42 skipped), 437178 steps
c bkwd: tried 17272 clauses, 34459 lits, 2.00 lits/clause
c bkwd: checked 570707 occs, 33.04 occs/clause, 16.56 occs/lit
c bkwd: subsumed 0 binary, 16 ternary, 22 large
c bkwd: strengthened 0 binary, 14 ternary (100% self), 92 large (0% self)
c blkd: 4 bces, 98 removed, 2120068 resolutions, 4505920 steps
c blkd: 38 blocking literals 0%, 8 pure
c bump: 3412183 bumped seen, 205379445 lits 60.2 on average
c card: 4 count, 2 units, 0 am1, 6909745 steps
c card: 33 rescheduled, 240 eliminated, 34953 resolved, 2350 subsumed
c card: 20 at-most-one constraints found, average size 3.00
c card: 20 at-most-one constraints used 100%, average size 3.00
c card: 193 at-most-two constraints found, average size 4.01
c card: 191 at-most-two constraints used 99%, average size 4.01
c cces: 5 cces, 10519 eliminated, 10454 ate 99%, 65 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 clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 348236 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 47 gcs, 0 rescored clauses, 1795 rescored vars
c dcps: 29 decompositions, 22 equivalent 0%
c deco: 520 decision-only clauses 0%, 41% reduction
c decs: 34134395 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 116692186 push, 116685387 pop (116685387 dec 100%)
c dsch: 1873352959 swaps, 0 down, 474691535 up
c elms: 6 elims, 2893 eliminated 31%, 8 pure 0%
c elms: 13 rounds, 2.2 rounds/bve
c elms: 2877 small 99%, 0 large 0%
c elms: 25377 tried small, 2877 succeeded 11%, 22500 failed 89%
c elms: 530 subsumed, 444 strengthened, 0 blocked
c elms: 2056183 copies, 3804391 resolutions, 2515866 ipos
c elms: 72293 subchks, 69313 strchks
c gaus: 4 extractions, 40828 extracted, 3.5 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 18289130 steps, 9144565 extr 50%, 8643279 elim 47%
c glue: 19.8 orig avg, 19.8 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 588 = 413 simple 70% + 165 trn 28% + 10 lrg 2%, 18 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3412183 clauses, 39.9 length
c lrnd: 136100944 lits = 143548770 orig - 7447826 removed 5%
c lrnd: 1576158 uips 46%, 1360130 flips 40%
c mins: 3131522 mins 92%, 62 bin 0%, 278961 size 8%
c mins: 127425322 poisoned searches, 9531978 hits, 7% hit rate
c mins: 245120479 used twice searches, 41801184 hits, 17% hit rate
c move: moved 404, 11 bin 3%, 393 trn 97%
c otfs: 19752 driving 46%, 22982 restarting 54%
c otfs: str 42734, 41965 red 98%, 769 irr 2%
c otfs: str 42734, 0 bin 0%, 359 trn 1%, 42375 lrg 99%
c otfs: sub 559, 559 red 100%, 0 irr 0%
c otfs: sub 559, 0 bin 0%, 102 trn 18%, 457 lrg 82%
c phas: 5 computed, 7006 set, 0 pos (0%), 7006 neg (100%)
c prbs: 2 basic, 7218 probed, 0 failed, 0 lifted
c prbs: 3 simple, 32535 probed, 1 failed, 17 eqs
c prbs: 3 treelook, 11755 probed, 0 failed, 0 lifted
c prom: 342270 locked 29% out of 1197738 tried
c prps: 627861519 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 9614 quat, 5177 self1, 79 self2, 172 dup
c redc: 3544 clauses 0%, 724719 tried 21%, 1 sat 0%
c redc: 3637 lits 0%, 5896451 tried 4%, 1 sat 0%
c redc: 176 times jump level reduced, 15.0 levels on average
c reds: 49 count, 70016.6 conflicts per reduce
c reds: 0 memlim 0%, 49 arith 100%
c reds: 1770663 collected 60%, 1195926 retired 40%
c rmbd: 58 removed, 58 red 100%
c rsts: 33889 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 12 count, 11 confs 92%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 8%
c subl: 3412183 count (3497840 tried 1.0), 15223 sub out of 3401248 (0.4%)
c swps: 5 count, 9 rounds, 3799 queries (422.1/round)
c swps: 3804 sat calls, 5 unsat (0.3% success rate)
c swps: 106346 decisions 28.0, 1122 conflicts 0.3
c swps; 320.6 avg class size, 135.4 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 1263 type 0 queries, 22 unsat (1.7%), 1263 sat (100.0%)
c swp1: 2536 type 1 queries, 95 unsat (3.7%), 2536 sat (100.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 75096988 calls to obtain time
c tops: 14 fixed 0%, 0 its, 0.00 confs/it
c trds: 10 transitive reductions, 179 removed, 0 failed
c trds: 125668 nodes, 12070 edges, 18502 steps
c trim: 126122 words, 0.5 MB
c trnr: 10 count, 112 bin, 8773 trn, 44999343 steps
c unhd: 4 count, 4 rounds, 2212188 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1286 tauts, 1 bin 0%, 1070 trn 83%, 204 lrg 16%
c unhd: 1286 tauts, 11 stamp 1%, 1244 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 23189 str, 0 bin 0%, 168 trn 1%, 23021 lrg 99%, 23098 red 100%
c vars: 6290 remaining 68% and 2929 removed 32% out of 9219
c vars: 14 fixed 0%, 2893 eliminated 31%, 22 equivalent 0%
c vsts: 28859035357 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 46.0 search visits per propagation, 8407.1 per conflict
c wchs: 9725316780 pushed, 16310198 enlarged, 1047 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3410862       1770663       1195926     189666038      27071851       1626578
c 
c  0 0        393149  12       592   0         0   0 173396531  91< 22766179  84<  1364958  84<   12.0
c  1 5        267424   8    129361   7    121566  10   8871676   5   1470912   5     96207   6     0.7
c  2 6        692573  20    371661  21    309635  26   3752426   2    974936   4     58916   4     1.0
c  3 9        650058  19<   372650  21    270519  23   1434267   1    636166   2     33561   2     1.2
c  4 14       458736  13    282439  16<   171511  14<   835050   0    431605   2     23420   1     1.4
c  5 21       309682   9    197239  11    108924   9    495600   0    275389   1     15413   1     1.5
c  6 30       212753   6    138140   8     72044   6    311252   0    179844   1     10397   1     1.6
c  7 41       148547   4     98202   6     48564   4    205220   0    121842   0      7556   0     1.8
c  8 54       104709   3     69991   4     33299   3    139954   0     84307   0      5559   0     1.9
c  9 69        71842   2     47603   3     23072   2     93923   0     56516   0      4036   0     1.8
c 10 86        76509   2     48985   3     26173   2     98741   0     57861   0      4844   0     3.0
c 11 126       23827   1     13417   1     10044   1     30114   0     15729   0      1649   0     1.9
c 12 230        1031   0       373   0       566   0      1254   0       550   0        57   0     0.1
c 13 534          22   0        10   0         9   0        30   0        15   0         5   0     0.0
c 
c avg                  3.5           4.1           3.7           0.2           0.5           0.5
c std                  2.5           2.3           2.2           0.8           1.4           1.4
c 
c   36.893   4% decide
c   11.471   1% bump
c    3.288   0% elim
c 
c    7.413 < 1% rest (below)
c 
c    2.492   0% cce
c    2.427   0% sweep
c    1.858   0% quatres
c    0.833   0% gauss
c    0.735   0% probe
c    0.395   0% block
c    0.330   0% ternres
c    0.327   0% rescore
c    0.227   0% unhide
c    0.157   0% card
c    0.102   0% bca
c    0.022   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.748   0% preprocessing     5%
c   13.465   1% inprocessing     95%
c ==================================
c   14.213   1% simplifying
c  985.763  99% search
c ==================================
c  999.976 100% all
c 
c       3430813 conflicts,        3430.9 confs/sec
c         10704 ternaries,         320.5 confs/ternary
c            85 binaries,        40362.5 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            49 reductions,          0.0 redus/sec,  70016.6 confs/reduction
c         33889 restarts,           33.9 rests/sec,    101.2 confs/restart
c      34134395 decisions,       34135.2 decis/sec,      9.9 decis/conflict
c     627861519 propagations,   627876.5 props/sec,     18.4 props/decision
c 
c 1000.0 seconds, 100.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
