c launch: /data/cnf/sc2014/app/MD5-28-1.cnf.bz2
c host: atom01
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 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-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/MD5-28-1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-28-1.cnf.bz2
c no embedded options
c found 'p cnf 8282 62558' header
c read 8282 variables, 62558 clauses, 243772 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 --queuesort=1
c --queuesortjwh=0
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 --score=6
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 8273 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 [score-type] AVG (--score=6)
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    8273    62345         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 26 variables
c [simpleprobe-1] all 8256 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 10 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 10 variables, found 324 hbrs, 3 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 63 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8246 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 2587 variables 31% in round 1 in 9051057 steps
c [elim-1-1] backward subsumption/strengthening limit 9051000
c [elim-1-1-1] backward checking 5586 touched variables 68%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 83 and strengthened 169 clauses in 1212499 steps
c [elim-1-1] rescheduled 228 variables 3% by backward subsumption
c [elim-1-2] eliminated 40 variables 0% in round 2 in 582886 steps
c [elim-1-2] backward subsumption/strengthening limit 582800
c [elim-1-2-1] backward checking 223 touched variables 3%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 38 and strengthened 189 clauses in 295427 steps
c [elim-1-2] rescheduled 182 variables 2% by backward subsumption
c [elim-1-3] eliminated 1 variables 0% in round 3 in 520015 steps
c [elim-1-3] backward subsumption/strengthening limit 520000
c [elim-1-3-1] backward checking 85 touched variables 1%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 0 and strengthened 0 clauses in 163501 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2628 = 32% variables out of 8246 scheduled
c [phase-count-1] 57653 negative 99.1% of 58176 except 523 0.9%
c [phase-count-1] 55956 positive 96.2% of 58176 except 2220 3.8%
c [phase-count-1] less non-negative clauses 523 than limit 5800 (10.0%)
c [phase-count-1] non-pos/non-neg = 2220/523 = 4.24 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 5618 negative 100%
c [sort-queue-1] sorted 5618 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5618 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 2655 variables 32.1% (5618 remain 68%)
c [simplification-1] removed 4169 irredundant clauses 6.7% (58176 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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 5618 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2396 variables remain 43% (3222 retained 57%)
c [simpleprobe-2] removed 0 variables, found 20 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 11236 literals 100%
c [treelook-1] scheduling used 279185 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300112 steps
c [treelook-1] 8142 literals remain 72%
c [treelook-1] 4239 variables remain to probed next time 75%
c [treelook-1] removed 0 variables, found 38 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 609 sched 11%, 0 failed, 0 lifted, 30 hbrs
c [basicprobe-1-1] 628 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 629 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 31 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5618 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 178 blocked clauses
c [block-1] 178 < 1/100 * 58176 = 581 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 124 clauses out of 906 (14%) of length 6
c [cce-1-1] eliminated 7383 clauses out of 22618 (33%) of length 5
c [cce-1-1] eliminated 327 clauses out of 19625 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7834 large clauses in 9395882 steps
c [cce-1-1] allowing another 4697941 steps for small clauses
c [cce-1-1] scheduling 864 clauses = 460 binary + 404 ternary
c [cce-1-1] tried to eliminate 864 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 1%
c [cce-1-1] eliminated 76 ternary clauses 19%
c [cce-1-1] eliminated 80 small clauses 9%
c [cce-1-1] eliminated 80 small clauses in 4795567 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7914 covered clauses in round 1
c [cce-1-2] eliminated 2 clauses out of 782 (0%) of length 6
c [cce-1-2] eliminated 44 clauses out of 15235 (0%) of length 5
c [cce-1-2] eliminated 54 clauses out of 19298 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 100 large clauses in 8355053 steps
c [cce-1-2] allowing another 4177526 steps for small clauses
c [cce-1-2] scheduling 784 clauses = 456 binary + 328 ternary
c [cce-1-2] tried to eliminate 784 small clauses 100%
c [cce-1-2] eliminated 1 ternary clauses 0%
c [cce-1-2] eliminated 1 small clauses 0%
c [cce-1-2] eliminated 1 small clauses in 4273639 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 101 covered clauses in round 2
c [cce-1-3] eliminated 20 clauses out of 15191 (0%) of length 5
c [cce-1-3] eliminated 30 clauses out of 19244 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 50 large clauses in 9448940 steps
c [cce-1-3] allowing another 4724470 steps for small clauses
c [cce-1-3] scheduling 783 clauses = 456 binary + 327 ternary
c [cce-1-3] tried to eliminate 783 small clauses 100%
c [cce-1-3] eliminated 4 ternary clauses 1%
c [cce-1-3] eliminated 4 small clauses 1%
c [cce-1-3] eliminated 4 small clauses in 4827862 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 54 covered clauses in round 3
c [cce-1] eliminated 8069 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5604 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 127 variables 2% in round 1 in 12296509 steps
c [elim-2-1] backward subsumption/strengthening limit 7703491
c [elim-2-1-1] backward checking 458 touched variables 8%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 15 clauses in 130152 steps
c [elim-2-1] rescheduled 39 variables 1% by backward subsumption
c [elim-2-2] eliminated 4 variables 0% in round 2 in 65280 steps
c [elim-2-2] backward subsumption/strengthening limit 65200
c [elim-2-2-1] backward checking 30 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 2 and strengthened 4 clauses in 51998 steps
c [elim-2-2] rescheduled 4 variables 0% by backward subsumption
c [elim-2-3] no variable eliminated in round 3 in 13024 steps
c [elim-2] fully completed in 3 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 131 = 2% variables out of 5604 scheduled
c [bca-1] limit of 10000000 steps and 98594 added (scaled 2)
c [bca-1] 9196 out of 10948 literals actually usable 84%
c [bca-1] added 0 blocked clauses in 36720 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2082 pos 38.0% + 3391 neg 62.0% = 5473 sched 100.0% ret 0
c [sweep-1-1] 852905 steps 1072 queries 287.14 avg class size
c [sweep-1-1] 9394 decisions 1072 SAT calls 15.11 avg env size
c [sweep-1-1] fully completed sweeping round
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-1-2] 2082 pos 38.0% + 3391 neg 62.0% = 5473 sched 100.0% ret 0
c [sweep-1-2] 148245 steps 149 queries 1239.49 avg class size
c [sweep-1-2] 1397 decisions 149 SAT calls 16.48 avg env size
c [sweep-1-2] 4864 variables remain 89% (609 retained 11%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] removed 0 vars in TOTAL (2 rounds, 1219 queries)
c [sort-queue-2] sorted 2406 enqueued variables after 1000 conflicts
c [score-dist-2] active 3067 (56%), one 0 (0%), zero 2406 (44%)
c [score-dist-2] max exp 512, different 10 (2%)
c [score-dist-2] median active exp 511, avg 510.3
c [simplification-2] removed 145 variables 2.6% (5473 remain 66%)
c [simplification-2] removed 9129 irredundant clauses 15.7% (49047 remain 79%)
c [simplification-2] maximum reduction of 16% = max (3%, 16%)
c [simplification-2] large reduction 16% >= 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 19703 quaternary clauses 53% in total
c [quatres-1-2] added 289 single-self-subsuming ternary resolvents
c [quatres-1-2] added 440 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 5473 free variables schedulable
c [ternres-1] 3973 ternary resolvents (83 bin, 3890 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3 at-most-one constraints of average size 3.0
c [card-2] found 22 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 25 out of 25 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 0 used 0%
c [card-2] exported 0 binary clauses, 0.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 14166 xors of average arity 3.6
c [gauss-1] connected 50736 occurrences of 4161 variables (average 12.2)
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, 227 tauts, 0 hbrs, 101 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 18 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 663 (0%) of length 6
c [cce-2-1] eliminated 32 clauses out of 14930 (0%) of length 5
c [cce-2-1] eliminated 89 clauses out of 19105 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 122 large clauses in 7756359 steps
c [cce-2-1] allowing another 3878179 steps for small clauses
c [cce-2-1] scheduling 12807 clauses = 475 binary + 12332 ternary
c [cce-2-1] tried to eliminate 12807 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 1%
c [cce-2-1] eliminated 191 ternary clauses 2%
c [cce-2-1] eliminated 194 small clauses 2%
c [cce-2-1] eliminated 194 small clauses in 5613111 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 316 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 3864575 steps for small clauses
c [cce-2-2] scheduling 12613 clauses = 472 binary + 12141 ternary
c [cce-2-2] tried to eliminate 12613 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 316 covered clauses in TOTAL during 2 rounds
c [cce-2] 316 < 1/100 * 49044 = 490 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5473 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 184 variables 3% in round 1 in 11801688 steps
c [elim-3-1] backward subsumption/strengthening limit 8198312
c [elim-3-1-1] backward checking 392 touched variables 7%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 28 clauses in 119421 steps
c [elim-3-1] rescheduled 57 variables 1% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 134164 steps
c [elim-3-2] backward subsumption/strengthening limit 134100
c [elim-3-2-1] backward checking 18 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 0 and strengthened 2 clauses in 49543 steps
c [elim-3-2] rescheduled 4 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 3366 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 187 = 3% variables out of 5473 scheduled
c [sort-queue-3] sorted 1453 enqueued variables after 3000 conflicts
c [score-dist-3] active 3833 (73%), one 0 (0%), zero 1453 (27%)
c [score-dist-3] max exp 513, different 11 (2%)
c [score-dist-3] median active exp 513, avg 512.1
c [simplification-3] removed 187 variables 3.4% (5286 remain 64%)
c [simplification-3] removed 2064 irredundant clauses 4.2% (46983 remain 75%)
c [simplification-3] maximum reduction of 4% = max (3%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 17000 (soft 7000 + delta 10000)
c [simplification-3] new conflict limit 7000 (hard 17000)
c 
c [simplification-4] limit 7000 conflicts (hard 17000) hit after 7001 conflicts
c [quatres-2] found 19773 quaternary clauses 53% in total
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 292 single-self-subsuming ternary resolvents
c [quatres-2-2] added 605 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5286 free variables schedulable
c [ternres-2] 581 ternary resolvents (7 bin, 574 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5096 literals 48%
c [treelook-2] scheduling used 150044 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150061 steps
c [treelook-2] 3527 literals remain 33%
c [treelook-2] 2507 variables remain to probed next time 47%
c [treelook-2] removed 0 variables, found 18 hbrs
c [transred-2] limit 236110 with penalty 0 = 0 + 0
c [transred-2] removed 20 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5286 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 703 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5185 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 79 variables 2% in round 1 in 11361221 steps
c [elim-4-1] backward subsumption/strengthening limit 11361200
c [elim-4-1-1] backward checking 187 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 26 clauses in 75002 steps
c [elim-4-1] rescheduled 48 variables 1% by backward subsumption
c [elim-4-2] eliminated 7 variables 0% in round 2 in 106909 steps
c [elim-4-2] backward subsumption/strengthening limit 106900
c [elim-4-2-1] backward checking 7 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 39854 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 86 = 2% variables out of 5185 scheduled
c [bca-2] limit of 10000000 steps and 91286 added (scaled 2)
c [bca-2] 3623 out of 10200 literals actually usable 36%
c [bca-2] added 0 blocked clauses in 19150 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 2172 pos 47.8% + 2372 neg 52.2% = 4544 sched 89.1% ret 555
c [sweep-2-1] 501589 steps 437 queries 350.64 avg class size
c [sweep-2-1] 6878 decisions 436 SAT calls 24.13 avg env size
c [sweep-2-1] 1361 variables remain 27% (3738 retained 73%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 436 queries)
c [sort-queue-4] sorted 814 enqueued variables after 7001 conflicts
c [score-dist-4] active 4285 (84%), one 0 (0%), zero 814 (16%)
c [score-dist-4] max exp 514, different 11 (2%)
c [score-dist-4] median active exp 514, avg 513.4
c [simplification-4] removed 187 variables 3.5% (5099 remain 62%)
c [simplification-4] removed 1590 irredundant clauses 3.4% (45393 remain 73%)
c [simplification-4] maximum reduction of 4% = max (4%, 3%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 8000
c [simplification-4] penalized conflict interval 8000 = 1 * 8000
c [simplification-4] hard conflict limit 25001 (soft 15001 + delta 10000)
c [simplification-4] new conflict limit 15001 (hard 25001)
c 
c [simplification-5] limit 15001 conflicts (hard 25001) hit after 15003 conflicts
c [quatres-3] found 20536 quaternary clauses 51% in total
c [quatres-3-1] added 6 double-self-subsuming ternary resolvents
c [quatres-3-2] added 370 single-self-subsuming ternary resolvents
c [quatres-3-2] added 768 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5099 free variables schedulable
c [ternres-3] 549 ternary resolvents (13 bin, 536 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5366 xors of average arity 3.0
c [gauss-2] connected 16098 occurrences of 1349 variables (average 11.9)
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 564626 with penalty 0 = 0 + 0
c [transred-3] removed 6 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5099 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 449 blocked clauses
c [block-3] 449 < 1/100 * 45393 = 453 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 26 clauses out of 13785 (0%) of length 5
c [cce-3-1] eliminated 82 clauses out of 17617 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 108 large clauses in 8690962 steps
c [cce-3-1] allowing another 4345481 steps for small clauses
c [cce-3-1] scheduling 11459 clauses = 464 binary + 10995 ternary
c [cce-3-1] tried to eliminate 11459 small clauses 100%
c [cce-3-1] eliminated 1 ternary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 1 small clauses in 6125407 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 109 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 4324354 steps for small clauses
c [cce-3-2] scheduling 11458 clauses = 464 binary + 10994 ternary
c [cce-3-2] tried to eliminate 11458 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 109 covered clauses in TOTAL during 2 rounds
c [cce-3] 109 < 1/100 * 44944 = 449 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5037 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 11128308 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 5037 scheduled
c [sort-queue-5] sorted 601 enqueued variables after 15003 conflicts
c [score-dist-5] active 4436 (88%), one 0 (0%), zero 601 (12%)
c [score-dist-5] max exp 515, different 11 (2%)
c [score-dist-5] median active exp 515, avg 514.6
c [simplification-5] removed 62 variables 1.2% (5037 remain 61%)
c [simplification-5] removed 558 irredundant clauses 1.2% (44835 remain 72%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 18000
c [simplification-5] penalized conflict interval 18000 = 1 * 18000
c [simplification-5] hard conflict limit 43003 (soft 33003 + delta 10000)
c [simplification-5] new conflict limit 33003 (hard 43003)
c 
c [simplification-6] limit 33003 conflicts (hard 43003) hit after 33003 conflicts
c [quatres-4] found 22397 quaternary clauses 48% in total
c [quatres-4-1] added 13 double-self-subsuming ternary resolvents
c [quatres-4-2] added 542 single-self-subsuming ternary resolvents
c [quatres-4-2] added 842 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5037 free variables schedulable
c [ternres-4] 624 ternary resolvents (10 bin, 614 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 8 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 11 out of 11 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 3713976 penalty 1 = 1 + 0
c [basicprobe-2-0] 846 sched 17%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-2-1] 863 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 863 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-3] 863 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-3] fully completed probing
c [basicprobe-2-3] removed 0 variables, found 28 hbrs
c [unhide-3] limit 74279 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 3 tauts, 0 hbrs, 531 literals
c [transred-4] limit 1485590 with penalty 0 = 0 + 0
c [transred-4] removed 7 transitive binary clauses
c [sort-queue-6] sorted 502 enqueued variables after 33003 conflicts
c [score-dist-6] active 4535 (90%), one 0 (0%), zero 502 (10%)
c [score-dist-6] max exp 516, different 12 (2%)
c [score-dist-6] median active exp 516, avg 515.7
c [simplification-6] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-6] removed 0 irredundant clauses 0.0% (44835 remain 72%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 38000
c [simplification-6] penalized conflict interval 38000 = 1 * 38000
c [simplification-6] hard conflict limit 90003 (soft 71003 + delta 19000)
c [simplification-6] new conflict limit 71003 (hard 90003)
c 
c [simplification-7] limit 71003 conflicts (hard 90003) hit after 71003 conflicts
c [quatres-5] found 25249 quaternary clauses 44% in total
c [quatres-5-1] added 20 double-self-subsuming ternary resolvents
c [quatres-5-2] added 620 single-self-subsuming ternary resolvents
c [quatres-5-2] added 801 quaternary resolvents
c [ternres-5] limit 4164396 with penalty 0 = 0 + 0
c [ternres-5] all 5037 free variables schedulable
c [ternres-5] 401 ternary resolvents (9 bin, 392 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 7 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5037 variables 100%
c [block-4] limit of 25000000 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5037 variables 100%
c [elim-6] limit of 41643963 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 11070037 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 5037 scheduled
c [bca-3] limit of 10000000 steps and 90014 added (scaled 2)
c [bca-3] 1291 out of 10076 literals actually usable 13%
c [bca-3] added 0 blocked clauses in 69470 steps
c [sweep-3] limit 312329 penalty 2 = 2 + 0
c [sweep-3-1] 664 pos 49.2% + 686 neg 50.8% = 1350 sched 26.8% ret 3687
c [sweep-3-1] 312342 steps 73 queries 181.11 avg class size
c [sweep-3-1] 4380 decisions 72 SAT calls 134.71 avg env size
c [sweep-3-1] 853 variables remain 17% (4184 retained 83%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 72 queries)
c [sort-queue-7] sorted 391 enqueued variables after 71003 conflicts
c [score-dist-7] active 4646 (92%), one 0 (0%), zero 391 (8%)
c [score-dist-7] max exp 518, different 14 (3%)
c [score-dist-7] median active exp 518, avg 517.6
c [simplification-7] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-7] removed 78 irredundant clauses 0.2% (44757 remain 72%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 38000
c [simplification-7] new conflict interval 76000
c [simplification-7] penalized conflict interval 76000 = 1 * 76000
c [simplification-7] hard conflict limit 185003 (soft 147003 + delta 38000)
c [simplification-7] new conflict limit 147003 (hard 185003)
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 -   24.5    5037    44757     84759   30054  11704   440   11   377   11   3%    739  121   11    6  164%
c 
c [simplification-8] limit 147003 conflicts (hard 185003) hit after 147003 conflicts
c [quatres-6] found 28576 quaternary clauses 39% in total
c [quatres-6-1] added 7 double-self-subsuming ternary resolvents
c [quatres-6-2] added 500 single-self-subsuming ternary resolvents
c [quatres-6-2] added 680 quaternary resolvents
c [ternres-6] limit 10608442 with penalty 0 = 0 + 0
c [ternres-6] all 5037 free variables schedulable
c [ternres-6] 267 ternary resolvents (8 bin, 259 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 530422 penalty 2 = 2 + 0
c [gauss-3] extracted 1816 xors of average arity 3.0
c [gauss-3] connected 5448 occurrences of 1314 variables (average 4.1)
c [gauss-3] limit 530422 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2122 schedulable variables 42%
c [simpleprobe-3] limit 21216885 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 29 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 27 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 132605535 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 30 clauses out of 13577 (0%) of length 5
c [cce-4-1] eliminated 236 clauses out of 17527 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 266 large clauses in 7059709 steps
c [cce-4-1] allowing another 3529854 steps for small clauses
c [cce-4-1] scheduling 11529 clauses = 465 binary + 11064 ternary
c [cce-4-1] tried to eliminate 11529 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 5085243 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 268 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 3483760 steps for small clauses
c [cce-4-2] scheduling 11527 clauses = 465 binary + 11062 ternary
c [cce-4-2] tried to eliminate 11527 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 268 covered clauses in TOTAL during 2 rounds
c [cce-4] 268 < 1/100 * 44757 = 447 considered unsuccessful
c [sort-queue-8] sorted 357 enqueued variables after 147003 conflicts
c [score-dist-8] active 4680 (93%), one 0 (0%), zero 357 (7%)
c [score-dist-8] max exp 519, different 13 (2%)
c [score-dist-8] median active exp 519, avg 518.7
c [simplification-8] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-8] removed 268 irredundant clauses 0.6% (44489 remain 71%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 38000 = 76000 / 2
c [simplification-8] new conflict interval 114000
c [simplification-8] penalized conflict interval 114000 = 1 * 114000
c [simplification-8] hard conflict limit 318003 (soft 261003 + delta 57000)
c [simplification-8] new conflict limit 261003 (hard 318003)
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 -   43.2    5037    44489    148648   41342  13345   462   12   377   12   3%    916   46   13    9  134%
c -   60.9    5037    44489    213008   56344  13796   466   13   395   13   3%    984   28   15   11  131%
c 
c [simplification-9] limit 261003 conflicts (hard 318003) hit after 261003 conflicts
c [quatres-7] found 31421 quaternary clauses 34% in total
c [quatres-7-1] removed 6 duplicate quaternary clauses
c [quatres-7-1] added 10 double-self-subsuming ternary resolvents
c [quatres-7-2] added 352 single-self-subsuming ternary resolvents
c [quatres-7-2] added 607 quaternary resolvents
c [ternres-7] limit 19129021 with penalty 0 = 0 + 0
c [ternres-7] all 5037 free variables schedulable
c [ternres-7] 255 ternary resolvents (14 bin, 241 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 16 transitive binary clauses
c [sort-queue-9] sorted 329 enqueued variables after 261003 conflicts
c [score-dist-9] active 4708 (93%), one 0 (0%), zero 329 (7%)
c [score-dist-9] max exp 519, different 13 (2%)
c [score-dist-9] median active exp 519, avg 518.8
c [simplification-9] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-9] removed 0 irredundant clauses 0.0% (44489 remain 71%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 114000
c [simplification-9] new conflict interval 228000
c [simplification-9] penalized conflict interval 228000 = 1 * 228000
c [simplification-9] hard conflict limit 603003 (soft 489003 + delta 114000)
c [simplification-9] new conflict limit 489003 (hard 603003)
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 -   76.3    5037    44489    271794   63160  14708   468   14   401   14   4%   1008   16   15   13  115%
c -   90.8    5037    44489    333471   74119  14925   470   16   406   15   4%   1018    8   15   14  104%
c -  104.2    5037    44489    392910   82629  15146   473   17   416   24   4%   1021    9   17   16  111%
c -  117.2    5037    44489    451844   91142  15335   476   18   423   16   4%   1023    9   20   17  116%
c 
c [simplification-10] limit 489003 conflicts (hard 603003) hit after 489003 conflicts
c [quatres-8] found 35114 quaternary clauses 29% in total
c [quatres-8-1] removed 22 duplicate quaternary clauses
c [quatres-8-1] added 9 double-self-subsuming ternary resolvents
c [quatres-8-2] added 348 single-self-subsuming ternary resolvents
c [quatres-8-2] added 627 quaternary resolvents
c [ternres-8] limit 33011155 with penalty 0 = 0 + 0
c [ternres-8] all 5037 free variables schedulable
c [ternres-8] 219 ternary resolvents (16 bin, 203 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2063197 penalty 3 = 3 + 0
c [card-4] found 4 at-most-one constraints of average size 3.0
c [card-4] found 23 at-most-two constraints of average size 4.0
c [card-4] using previous limit 2063197 for elimination
c [card-4] 26 out of 27 constraints (96%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 825278 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 905 tauts, 0 hbrs, 16977 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 11 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5037 variables 100%
c [block-5] limit of 82527888 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1 blocked clauses
c [block-5] 1 < 1/100 * 44489 = 444 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5037 variables 100%
c [elim-7] limit of 165055777 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 10868299 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 5037 scheduled
c [sort-queue-10] sorted 197 enqueued variables after 489003 conflicts
c [score-dist-10] active 4840 (96%), one 0 (0%), zero 197 (4%)
c [score-dist-10] max exp 520, different 13 (2%)
c [score-dist-10] median active exp 520, avg 519.9
c [simplification-10] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-10] removed 43 irredundant clauses 0.1% (44446 remain 71%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 228000
c [simplification-10] new conflict interval 456000
c [simplification-10] penalized conflict interval 456000 = 1 * 456000
c [simplification-10] hard conflict limit 1173003 (soft 945003 + delta 228000)
c [simplification-10] new conflict limit 945003 (hard 1173003)
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 -  130.9    5037    44446    509860   99397  15362   489   19   425   26   5%   1024    5   21   18  117%
c -  143.5    5037    44446    566677  106979  15471   489   21   422   17   5%   1024   -1   21   19  112%
c -  155.5    5037    44446    622744  114380  15580   490   21   428   18   5%   1024    2   21   20  103%
c -  167.5    5037    44446    677876  121097  15692   490   21   432   18   5%   1024    5   23   21  110%
c -  179.6    5037    44446    732853  127109  15847   492   21   435   19   5%   1024    3   21   21   99%
c -  191.7    5037    44446    788078  132780  15960   493   23   433   19   5%   1024    2   24   22  110%
c -  204.1    5037    44446    843885  138884  16075   495   23   436   20   5%   1024    3   26   22  117%
c -  216.6    5037    44446    899462  144066  16159   496   24   433   20   5%   1024   -3   26   23  115%
c 
c [simplification-11] limit 945003 conflicts (hard 1173003) hit after 945003 conflicts
c [quatres-9] found 39514 quaternary clauses 24% in total
c [quatres-9-1] removed 34 duplicate quaternary clauses
c [quatres-9-1] added 4 double-self-subsuming ternary resolvents
c [quatres-9-2] added 415 single-self-subsuming ternary resolvents
c [quatres-9-2] added 709 quaternary resolvents
c [ternres-9] limit 62136649 with penalty 0 = 0 + 0
c [ternres-9] all 5037 free variables schedulable
c [ternres-9] 384 ternary resolvents (7 bin, 377 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 1553416 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5016 literals 50%
c [treelook-3] scheduling used 738081 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1553416 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 532652 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 12 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 13 transitive binary clauses
c [bca-4] limit of 10000000 steps and 89392 added (scaled 2)
c [bca-4] 463 out of 10076 literals actually usable 5%
c [bca-4] added 0 blocked clauses in 191360 steps
c [sweep-4] limit 2330124 penalty 3 = 3 + 0
c [sweep-4-1] 404 pos 47.4% + 449 neg 52.6% = 853 sched 16.9% ret 4184
c [sweep-4-1] 1111785 steps 179 queries 46.01 avg class size
c [sweep-4-1] 10602 decisions 178 SAT calls 240.78 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4-2] 2445 pos 48.5% + 2592 neg 51.5% = 5037 sched 100.0% ret 0
c [sweep-4-2] 1223768 steps 107 queries 213.46 avg class size
c [sweep-4-2] 9477 decisions 106 SAT calls 534.20 avg env size
c [sweep-4-2] 1204 variables remain 24% (3833 retained 76%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 284 queries)
c [sort-queue-11] sorted 64 enqueued variables after 945003 conflicts
c [score-dist-11] active 4973 (99%), one 0 (0%), zero 64 (1%)
c [score-dist-11] max exp 521, different 7 (1%)
c [score-dist-11] median active exp 521, avg 521.0
c [simplification-11] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-11] removed 0 irredundant clauses 0.0% (44446 remain 71%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 456000
c [simplification-11] new conflict interval 912000
c [simplification-11] penalized conflict interval 912000 = 1 * 912000
c [simplification-11] hard conflict limit 2313003 (soft 1857003 + delta 456000)
c [simplification-11] new conflict limit 1857003 (hard 2313003)
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 -  230.7    5037    44446    955517  149714  17051   507   24   430   20   6%   1024   -6   27   23  115%
c -  243.8    5037    44446   1012156  155414  17104   508   24   439   21   5%   1024    5   27   23  115%
c -  256.9    5037    44446   1068621  160307  17171   508   24   448   21   5%   1024   11   21   24   89%
c -  270.7    5037    44446   1125759  165499  17225   509   25   432   22   6%   1024   -1   29   24  117%
c -  284.4    5037    44446   1183281  170704  17303   511   25   430   22   6%   1024   -6   26   24  106%
c -  298.3    5037    44446   1241003  175264  17355   512   25   432   23   6%   1024   -3   29   25  118%
c -  312.8    5037    44446   1299736  180314  17386   516   24   437   23   6%   1024    1   24   25   97%
c -  327.8    5037    44446   1358963  184951  17452   519   24   422   23   6%   1024  -11   22   25   86%
c -  343.0    5037    44446   1418882  189891  17531   519   25   422   24   6%   1024  -12   29   25  117%
c -  358.7    5037    44446   1479373  194370  17598   519   25   431   24   6%   1024   -0   24   25   95%
c -  375.1    5037    44446   1540569  199599  17641   520   26   437   25   6%   1024    2   29   26  111%
c -  391.7    5037    44446   1601840  203895  17692   521   25   444   25   6%   1024    9   23   26   87%
c -  408.5    5037    44446   1664308  208940  17743   522   26   457   26   6%   1024   20   28   26  109%
c -  425.8    5037    44446   1726961  213946  17784   522   27   431   26   6%   1024   -6   29   26  109%
c -  443.6    5037    44446   1789745  217985  17853   523   27   451   26   6%   1024   13   23   26   89%
c -  461.8    5037    44446   1853837  222546  17906   525   27   436   27   6%   1024   -1   32   27  119%
c 
c [simplification-12] limit 1857003 conflicts (hard 2313003) hit after 1857849 conflicts
c [quatres-10] found 44509 quaternary clauses 19% in total
c [quatres-10-1] removed 54 duplicate quaternary clauses
c [quatres-10-1] added 4 double-self-subsuming ternary resolvents
c [quatres-10-2] added 365 single-self-subsuming ternary resolvents
c [quatres-10-2] added 825 quaternary resolvents
c [ternres-10] limit 134432637 with penalty 0 = 0 + 0
c [ternres-10] all 5037 free variables schedulable
c [ternres-10] 195 ternary resolvents (9 bin, 186 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 3360815 penalty 3 = 3 + 0
c [gauss-4] extracted 15428 xors of average arity 3.6
c [gauss-4] connected 56156 occurrences of 4479 variables (average 12.5)
c [gauss-4] limit 3360815 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 10 transitive binary clauses
c [cce-5] limit of 84020398 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 20 clauses out of 13456 (0%) of length 5
c [cce-5-1] eliminated 145 clauses out of 17248 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 165 large clauses in 8315772 steps
c [cce-5-1] allowing another 4157886 steps for small clauses
c [cce-5-1] scheduling 843 clauses = 467 binary + 376 ternary
c [cce-5-1] tried to eliminate 843 small clauses 100%
c [cce-5-1] eliminated 2 binary clauses 0%
c [cce-5-1] eliminated 12 ternary clauses 3%
c [cce-5-1] eliminated 14 small clauses 2%
c [cce-5-1] eliminated 14 small clauses in 4264702 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 179 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 4114415 steps for small clauses
c [cce-5-2] scheduling 829 clauses = 465 binary + 364 ternary
c [cce-5-2] tried to eliminate 829 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 179 covered clauses in TOTAL during 2 rounds
c [cce-5] 179 < 1/100 * 44446 = 444 considered unsuccessful
c [sort-queue-12] sorted 1 enqueued variables after 1857849 conflicts
c [score-dist-12] active 5036 (100%), one 0 (0%), zero 1 (0%)
c [score-dist-12] max exp 522, different 3 (1%)
c [score-dist-12] median active exp 522, avg 522.0
c [simplification-12] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-12] removed 179 irredundant clauses 0.4% (44267 remain 71%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 912000
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] hard conflict limit 3357849 (soft 2857849 + delta 500000)
c [simplification-12] new conflict limit 2857849 (hard 3357849)
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 -  482.1    5037    44267   1918630  227738  18493   526   28   439   27   6%   1024    5   26   27   95%
c -  501.6    5037    44267   1983771  232194  18531   526   29   439   28   7%   1024    4   35   27  128%
c -  521.3    5037    44267   2049792  236658  18562   526   26   433   28   6%   1024   -2   27   27   98%
c -  541.5    5037    44267   2116555  241414  18593   527   27   429   28   6%   1024   -6   27   27   99%
c -  562.8    5037    44267   2183890  245832  18622   527   27   428   29   6%   1024   -6   33   28  119%
c -  584.0    5037    44267   2251895  250128  18654   528   28   433   29   6%   1024   -2   24   28   86%
c -  606.3    5037    44267   2320967  254212  18690   528   28   437   30   6%   1024   -1   30   28  107%
c -  628.6    5037    44267   2391230  259321  18718   528   30   450   30   7%   1024   14   38   28  137%
c -  651.4    5037    44267   2461539  263941  18746   528   28   437   30   6%   1024   -0   24   28   86%
c -  674.9    5037    44267   2532394  267971  18781   528   29   431   31   7%   1024   -3   29   28  103%
c -  699.0    5037    44267   2604353  272722  18806   528   29   429   31   7%   1024   -7   25   28   88%
c -  723.1    5037    44267   2677093  277151  18852   529   27   446   31   6%   1024   10   31   28  110%
c -  748.6    5037    44267   2750414  281725  18883   530   28   431   32   7%   1024   -7   31   28  109%
c -  773.5    5037    44267   2824363  286953  18915   531   28   430   32   7%   1024   -6   30   28  106%
c 
c [simplification-13] limit 2857849 conflicts (hard 3357849) hit after 2872888 conflicts
c [quatres-11] found 48342 quaternary clauses 16% in total
c [quatres-11-1] removed 46 duplicate quaternary clauses
c [quatres-11-1] added 4 double-self-subsuming ternary resolvents
c [quatres-11-2] added 236 single-self-subsuming ternary resolvents
c [quatres-11-2] added 678 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 5037 free variables schedulable
c [ternres-11] 110 ternary resolvents (13 bin, 97 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 9 transitive binary clauses
c [score-dist-13] active 5037 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 523, different 1 (0%)
c [score-dist-13] median active exp 523, avg 523.0
c [simplification-13] removed 0 variables 0.0% (5037 remain 61%)
c [simplification-13] removed 0 irredundant clauses 0.0% (44267 remain 71%)
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] hard conflict limit 5872888 (soft 4872888 + delta 1000000)
c [simplification-13] new conflict limit 4872888 (hard 5872888)
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 -  799.5    5037    44267   2898281  291987  19272   535   29   437   32   7%   1024   -0   28   29   97%
c -  825.6    5037    44267   2972736  296317  19292   536   30   434   33   7%   1024   -0   30   29  103%
c -  851.5    5037    44267   3047802  300745  19318   536   29   437   33   7%   1024    1   27   29   94%
c -  878.0    5037    44267   3123739  305346  19350   536   28   436   34   6%   1024   -2   26   29   91%
c -  905.7    5037    44267   3200165  309554  19376   536   28   432   34   7%   1024   -7   33   29  113%
c -  933.4    5037    44267   3277528  313838  19398   536   29   434   35   7%   1024   -2   29   29  101%
c -  961.2    5037    44267   3355790  318967  19426   536   30   436   35   7%   1024    1   32   29  109%
c -  990.3    5037    44267   3433905  322826  19453   536   30   444   35   7%   1024    8   33   29  111%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (60 skipped), 316700 steps
c bkwd: tried 20340 clauses, 40318 lits, 1.98 lits/clause
c bkwd: checked 666585 occs, 32.77 occs/clause, 16.53 occs/lit
c bkwd: subsumed 0 binary, 20 ternary, 105 large
c bkwd: strengthened 0 binary, 15 ternary (100% self), 418 large (0% self)
c blkd: 5 bces, 1331 removed, 2100291 resolutions, 4467046 steps
c blkd: 425 blocking literals 3%, 177 pure
c bump: 3446436 bumped seen, 251707989 lits 73.0 on average
c card: 4 count, 2 units, 0 am1, 5399566 steps
c card: 67 rescheduled, 261 eliminated, 29051 resolved, 1597 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: 173 at-most-two constraints found, average size 4.00
c card: 172 at-most-two constraints used 99%, average size 4.00
c cces: 5 cces, 8941 eliminated, 8784 ate 98%, 157 abce 2%
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: 306330 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 30 decompositions, 22 equivalent 0%
c deco: 2410 decision-only clauses 0%, 42% reduction
c decs: 32677881 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 3209 eliminated 39%, 6 pure 0%
c elms: 16 rounds, 2.3 rounds/bve
c elms: 3026 small 94%, 0 large 0%
c elms: 24743 tried small, 3026 succeeded 12%, 21717 failed 88%
c elms: 951 subsumed, 1049 strengthened, 0 blocked
c elms: 1975651 copies, 3657206 resolutions, 2373892 ipos
c elms: 60791 subchks, 54709 strchks
c gaus: 4 extractions, 36776 extracted, 3.5 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13783046 steps, 6891523 extr 50%, 6047744 elim 44%
c glue: 24.6 orig avg, 24.6 real avg, 3.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 513 = 373 simple 73% + 130 trn 25% + 10 lrg 2%, 7 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3446436 clauses, 49.9 length
c lrnd: 172137610 lits = 181947943 orig - 9810333 removed 5%
c lrnd: 1632777 uips 47%, 1284357 flips 37%
c mins: 3193388 mins 93%, 23 bin 0%, 245983 size 7%
c mins: 147194323 poisoned searches, 11494167 hits, 8% hit rate
c mins: 288900565 used twice searches, 53378495 hits, 18% hit rate
c move: moved 972, 14 bin 1%, 958 trn 99%
c otfs: 16751 driving 44%, 21424 restarting 56%
c otfs: str 38175, 37781 red 99%, 394 irr 1%
c otfs: str 38175, 0 bin 0%, 244 trn 1%, 37931 lrg 99%
c otfs: sub 541, 541 red 100%, 0 irr 0%
c otfs: sub 541, 0 bin 0%, 76 trn 14%, 465 lrg 86%
c phas: 1 computed, 5618 set, 0 pos (0%), 5618 neg (100%)
c prbs: 2 basic, 10602 probed, 0 failed, 0 lifted
c prbs: 3 simple, 30151 probed, 3 failed, 20 eqs
c prbs: 3 treelook, 9679 probed, 0 failed, 0 lifted
c prom: 469933 locked 27% out of 1709848 tried
c prps: 653779732 props, 20 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 7582 quat, 4329 self1, 80 self2, 162 dup
c queu: 12 sorted, 32677881 next (101871 steps 0.00)
c queu: 251729004 enq (7352685532 steps 29.21), 251707989 deq 100%
c redc: 2770 clauses 0%, 605516 tried 17%, 0 sat 0%
c redc: 2836 lits 0%, 5002592 tried 3%, 0 sat 0%
c redc: 76 times jump level reduced, 16.4 levels on average
c reds: 53 count, 65328.7 conflicts per reduce
c reds: 0 memlim 0%, 53 arith 100%
c reds: 1992578 collected 65%, 1078913 retired 35%
c rmbd: 59 removed, 59 red 100%
c rsts: 32899 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3446436 count (4393636 tried 1.3), 16084 sub out of 3438499 (0.5%)
c swps: 4 count, 6 rounds, 2011 queries (335.2/round)
c swps: 2013 sat calls, 2 unsat (0.4% success rate)
c swps: 42128 decisions 20.9, 765 conflicts 0.4
c swps; 343.1 avg class size, 68.7 avg environment size
c swps: 0 failed, 5 impls, 0 equivs
c swp0: 669 type 0 queries, 6 unsat (0.9%), 669 sat (100.0%)
c swp1: 1342 type 1 queries, 26 unsat (1.9%), 1342 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: 72248895 calls to obtain time
c tops: 14 fixed 0%, 0 its, 0.00 confs/it
c trds: 11 transitive reductions, 144 removed, 0 failed
c trds: 112042 nodes, 9913 edges, 14741 steps
c trim: 125773 words, 0.5 MB
c trnr: 11 count, 189 bin, 7369 trn, 40698330 steps
c unhd: 4 count, 4 rounds, 1492665 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: 1219 tauts, 0 bin 0%, 1037 trn 85%, 173 lrg 14%
c unhd: 1219 tauts, 9 stamp 1%, 1177 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 17672 str, 0 bin 0%, 119 trn 1%, 17553 lrg 99%, 17578 red 99%
c vars: 5037 remaining 61% and 3245 removed 39% out of 8282
c vars: 14 fixed 0%, 3209 eliminated 39%, 22 equivalent 0%
c vsts: 30124845614 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 46.1 search visits per propagation, 8699.5 per conflict
c wchs: 8046326726 pushed, 11664484 enlarged, 886 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3446081       1992578       1078913     200230554      31012277       1702296
c 
c  0 0        304436   9       549   0         0   0 178519282  89< 25295328  82   1356880  80     9.4
c  1 5        226751   7    116603   6     90706   8  11763643   6   2056157   7<   123245   7<    0.7
c  2 6        644145  19    383720  19    243515  23   5437924   3   1363409   4     81250   5     1.0
c  3 9        641667  19    398417  20    234105  22   1742715   1    755802   2     40764   2     1.1
c  4 14       466593  14<   304706  15<   155506  14<   985961   0    502874   2     28379   2     1.3
c  5 21       329114  10    219419  11    104892  10    584544   0    323322   1     19359   1     1.5
c  6 30       238123   7    161538   8     73150   7    375443   0    217702   1     13785   1     1.7
c  7 41       176552   5    121390   6     52601   5    256809   0    153358   0     10241   1     1.9
c  8 54       133097   4     92971   5     38018   4    184338   0    113359   0      8018   0     2.0
c  9 69        98212   3     68761   3     27668   3    132183   0     82138   0      6172   0     1.9
c 10 86       122750   4     85060   4     35336   3    163401   0    101309   0      8987   1     3.8
c 11 126       60243   2     37777   2     21263   2     78552   0     44936   0      5011   0     3.2
c 12 230        4398   0      1667   0      2153   0      5759   0      2583   0       205   0     0.4
c 
c avg                  3.9           4.4           4.1           0.2           0.5           0.6
c std                  2.7           2.5           2.5           0.9           1.5           1.7
c 
c  119.799  12% bump
c   22.004   2% decide
c    3.177   0% elim
c 
c    4.711 < 1% rest (below)
c 
c    1.953   0% cce
c    1.571   0% quatres
c    0.715   0% sweep
c    0.680   0% probe
c    0.580   0% gauss
c    0.388   0% block
c    0.288   0% ternres
c    0.171   0% bca
c    0.163   0% unhide
c    0.132   0% card
c    0.023   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.703   0% preprocessing     6%
c   10.426   1% inprocessing     94%
c ==================================
c   11.128   1% simplifying
c  988.854  99% search
c ==================================
c  999.982 100% all
c 
c       3462422 conflicts,        3462.5 confs/sec
c          7745 ternaries,         447.1 confs/ternary
c            40 binaries,        86560.6 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            53 reductions,          0.1 redus/sec,  65328.7 confs/reduction
c         32899 restarts,           32.9 rests/sec,    105.2 confs/restart
c      32677881 decisions,       32678.5 decis/sec,      9.4 decis/conflict
c     653779732 propagations,   653791.4 props/sec,     20.0 props/decision
c 
c 1000.0 seconds, 90.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
