StrArgsDepsSymsPremsProverThm%CoS%UniqST⌀STΣThmCoSMaybeEmptyErrFound
hhjournalnb_t_nts_ad2orig0154epar24.6660.11130.05524.434432135101796
hhjournalnb_t_nts_ad2orig092vam23.9980.05650.05724.7243111341231796
hhjournalnb_t_nts_ad2orig0128epar23.7190.11100.04318.564262136801796
defaultdefault00512epar22.4390.00010.0187.064030139301796
seqd2_div_s010128epar22.3830.00000.0135.314020139311796
defaultdefault00128epar22.3270.00000.0135.254010139501796
seqd2_div_s020128epar22.1050.00000.0124.933970139451796
pgranku_div_s010128epar22.0490.00000.0135.1739601339611796
seqd2_div_s010512epar22.0490.00000.0155.773960140001796
maxcutdefault01128epar21.9930.00000.0145.433950139651796
pgrankdu_div_s020128epar21.8820.00000.0145.5639301355481796
seqd_u_div_s2010128epar21.8260.00000.0124.753920139681796
pgrankdu_div_s010128epar21.7710.00000.0135.2339101386191796
epcldefault010128epar21.7150.00000.0135.053900139971796
seqd2_div_s020512epar21.7150.00000.0155.753900140421796
seqd_u_div_exps020128epar21.6590.00000.0135.2338901387201796
seqd_u_div_exps010128epar21.5480.00000.0134.873870140181796
seqd_u_div_s010128epar21.5480.00000.0135.083870140361796
seqd_u_div_exps010512epar21.4370.00000.0134.873850140471796
seqd_u_div_s2020128epar21.4370.00000.0135.0338501396151796
pgranku_div_s020128epar21.3810.00010.0176.43384013071051796
pgranku_div_s010512epar21.3250.00000.0145.2338301355581796
maxcutdefault05512epar21.2140.00000.0145.1638101391241796
pgrankdu010128epar21.2140.00000.0124.503810140961796
epcldefault020128epar21.1580.00000.0124.5538001404121796
maxcutdefault010512epar21.1020.00000.0155.7237901377401796
seqd_u_div_s020128epar21.0470.00000.0134.8937801402161796
pgrankdu_div_s010512epar20.9350.00000.0145.1837601403171796
pgrankdu_div_s020512epar20.9350.00010.0186.8537601376441796
maxcutdefault01512epar22.3680.00000.0134.843740129261672
pgranku010128epar20.8240.00000.0114.203740141571796
epcldefault010512epar20.7680.00000.0134.713730141581796
pgrankdu010512epar20.7130.00000.0134.673720141951796
seqd_u_div_exps020512epar20.7130.00010.0155.5737201407171796
seqd_u_div_s2010512epar20.7130.00000.0124.533720141771796
hhjournalnb_t_nts_ad2orig01024epar20.6010.11160.05721.043702142401796
maxcutdefault05128epar20.6010.00000.0124.5737001392341796
seqd2_div_s060128epar20.6010.00000.0124.2737001361651796
seqd_u_div_s010512epar20.6010.00000.0124.573700142061796
pgranku010512epar20.4900.00000.0134.873680142171796
pgranku_div_s020512epar20.4900.00000.0145.0636801331971796
pgrankd_div_s020128epar20.4340.00000.0155.64367013101191796
pgrankdu020128epar20.3790.00000.0124.2436601420101796
pgrankdu020512epar20.3790.00000.0155.483660142371796
seqd_u_div_s2020512epar20.3230.00000.0124.4736501418131796
pgrankd010128epar20.2670.00000.0134.8036401369631796
seqd2_div_s060512epar20.2670.00000.0144.9836401378541796
seqd_u_div_s020512epar20.2670.00000.0134.6536401419131796
hhjournalnb_0_hdorig0512epar20.2120.00030.04416.093630143301796
pgrankd_div_s010128epar20.1560.00000.0134.7036201363711796
pgranku020128epar20.1560.00010.0155.3036201417171796
seqd_u_div_s2060128epar20.1560.00000.0134.63362013211131796
epcldefault020512epar20.1000.00000.0124.4836101424111796
pgranku020512epar20.1000.00000.0155.4536101423121796
maxcutdefault010128epar19.9330.00000.0134.6535801391471796
seqd_u_div_s2060512epar19.8780.00000.0124.3135701348911796
pgrankd020128epar19.8220.00000.0124.3435601354861796
epcldefault060128epar19.5430.00000.0134.6735101409361796
pgranku060128epar19.5430.00010.0155.1435101400451796
sequ2_div_s010128epar19.5430.00000.0113.9635101422231796
pgrankdu_div_s060128epar19.4880.00000.0165.54350012991471796
seqd_u_div_exps060128epar19.3760.00000.0144.76348012901581796
sequ2_div_s020128epar19.3760.00000.0134.3934801409391796
pgrankdu060128epar19.1540.00000.0124.2434401416361796
pgrankd060128epar18.9310.00000.0113.89340013431131796
pgranku_div_s060128epar18.8200.00000.0154.97338012572011796
sequ2_div_s060128epar18.5970.00000.0113.8333401374881796
seqd_u_div_s060512epar18.5410.00000.0134.2533301388751796
pgrankd_div_s060128epar18.3740.00000.0154.80330012362301796
seqd_u_div_exps060512epar18.3740.00000.0124.05330013251411796
pgrankdu_div_s060512epar18.2630.00000.0144.54328013351331796
seqd_u_div_s060128epar18.2070.00000.0134.0932701373961796
pgrankdu060512epar18.1510.00000.0113.6932601437331796
epcldefault060512epar18.0400.00000.0113.6732401444281796
pgrankd010512epar17.7620.00000.0123.9131901427501796
pgranku_div_s060512epar17.7620.00000.0144.37319012981791796
pgrankd_div_s010512epar17.6500.00000.0123.9531701416631796
hhjournalnb_vd1orig0128epar17.0380.00000.03510.633060149001796
pgrankd_div_s020512epar16.3700.00000.0164.59294013931091796
sequ2_div_s010512epar15.8130.00000.0113.2228401495171796
pgrankd020512epar15.6460.00000.0112.9728101435801796
hhjournalnb_o_hdorig0128vam15.5900.00020.04512.542800151511796
pgranku060512epar15.3120.00000.0113.1327501493281796
seqd2_div_s01032z3_415.1450.00000.0112.952720015241796
defaultdefault0032z3_415.0890.00000.0112.922710015251796
hhjournalkn40_t_nts_ad1orig032epar15.0895.62410.03011.16271101142401796
seqd2_div_s02032z3_415.0890.00000.0133.512710015251796
pgranku06032z3_414.9780.00040.0379.872690015271796
epcldefault01032z3_414.9220.00000.0123.142680015281796
pgrankd060512epar14.8110.00000.0102.6826601442881796
seqd2_div_s06032z3_414.7550.00060.0379.702650015311796
sequ2_div_s020512epar14.7550.00000.0102.5926501498331796
epcldefault02032z3_414.6440.00000.0133.302630015331796
pgranku_div_s01032z3_414.7030.00000.0123.202620015201782
seqd_u_div_exps01032z3_414.5880.00000.0123.022620015341796
pgranku01032z3_414.4770.00000.0133.262600015361796
sequ2_div_s060512epar14.4770.00000.0102.6326001467691796
maxcutdefault0132z3_414.4210.00000.0112.752590015371796
seqd_u_div_s06032z3_414.4210.00040.04110.612590015371796
pgranku_div_s02032z3_414.4300.00000.0143.742580015301788
seqd_u_div_s02032z3_414.3100.00010.0194.952570015391796
seqd_u_div_s201032z3_414.3100.00000.0112.792570015391796
epcldefault06032z3_414.2540.00000.0184.612560015401796
seqd_u_div_s01032z3_414.1980.00000.0123.002550015411796
maxcutdefault01032z3_414.1430.00000.0112.922540015421796
pgrankdu_div_s02032z3_414.1430.00000.0122.952540015421796
pgrankdu_div_s01032z3_414.0870.00000.0102.572530015431796
seqd_u_div_exps02032z3_414.0870.00000.0112.892530015431796
hhjournalnb_t_nts_ad1orig032z3_413.9760.00040.05213.142510015451796
maxcutdefault0532z3_413.9830.00000.0112.782510015441795
pgrankdu01032z3_413.9760.00000.0102.632510015451796
pgrankdu06032z3_413.9760.00010.0204.962510015451796
sequ2_div_s06032z3_413.8080.00050.04110.082480015481796
alldefault0all128epar13.7530.00000.0163.86247012742751796
hhjournalnb_t_nts_vd1orig0128z3_413.6410.00000.0399.552450015511796
pgranku_div_s06032z3_413.6410.00010.0307.262450015511796
sequ2_div_s02032z3_413.5860.00000.0194.692440015521796
pgrankdu02032z3_413.5300.00000.0092.312430015531796
seqd2_div_s01092vam13.4740.00000.0092.122420155311796
seqd_u_div_s206032z3_413.4740.00030.0296.952420015541796
pgrankd_div_s060512epar13.4190.00010.0184.36241013641911796
pgranku_div_s01092vam13.4190.00000.0102.4524101505501796
seqd_u_div_exps06032z3_413.4190.00000.0194.662410015551796
pgranku02032z3_414.0600.00000.0245.772400014671707
seqd2_div_s02092vam13.3630.00000.0092.102400155601796
defaultdefault0092vam13.5560.00000.0092.052390152401763
maxcutdefault0192vam13.3070.00000.0092.082390155251796
seqd_u_div_exps01092vam13.2520.00000.0092.072380155081796
sequ2_div_s01032z3_413.5000.00000.0194.642380015251763
pgrankdu01092vam13.1960.00000.0081.942370155451796
pgrankd_div_s02032z3_413.1240.00000.0174.012340015491783
pgrankdu_div_s01092vam13.0290.00000.0081.9623401547151796
seqd_u_div_exps02092vam13.0290.00000.0092.0823401546161796
epcldefault02092vam13.0530.00000.0092.0023301537151785
pgrankd02032z3_413.0530.00030.0296.822330015521785
pgrankd_div_s01032z3_412.9730.00000.0153.432330015631796
alldefault0all32z3_412.9180.000230.15335.382320015641796
epcldefault01092vam12.9180.00000.0081.912320156131796
seqd_u_div_s01092vam13.0530.00000.0092.002300152661762
seqd_u_div_s201092vam12.8060.00000.0081.902300155971796
pgrankdu02092vam12.7510.00000.0092.0522901552151796
pgrankdu_div_s06032z3_412.6950.00000.0153.392280015681796
seqd2_div_s06092vam12.6950.00000.0092.1322801535331796
pgrankdu_div_s02092vam12.6390.00000.0081.9322701522471796
seqd_u_div_s02092vam12.5840.00000.0081.9122601559111796
seqd_u_div_s202092vam12.8340.00000.0081.8922601525101761
seqd_u_div_s202032z3_414.4230.00000.0132.962250013351560
pgrankd06032z3_412.4720.00010.0204.522240015721796
pgrankd01032z3_412.5560.00000.0102.342230015531776
pgranku01092vam12.4160.00000.0091.992230156581796
pgrankd01092vam12.3610.00000.0091.9822201529451796
pgranku_div_s02092vam12.2490.00000.0092.0822001492841796
pgranku06092vam12.1380.00000.0102.1521801554241796
maxcutdefault0592vam12.0820.00000.0091.8821701528511796
pgrankd_div_s01092vam12.0820.00000.0091.9021701518611796
seqd_u_div_s206092vam11.9710.00000.0091.8521501502791796
epcldefault06092vam11.9150.00000.0081.7021401548341796
seqd_u_div_exps06092vam11.8600.00000.0122.54213014521311796
pgrankd_div_s06032z3_411.7480.00010.0193.922110015851796
hhjournalkn160_t_nts_ad1orig0512z3_411.6930.00030.05912.312100015861796
pgranku02092vam11.6930.00000.0091.802100158061796
pgrankd02092vam11.5810.00000.0091.8020801523651796
pgrankd_div_s02092vam11.5810.00000.0091.80208014841041796
pgrankdu06092vam11.5260.00000.0091.8920701566231796
sequ2_div_s01092vam11.4700.00000.0081.6520601573171796
maxcutdefault01092vam11.4400.00000.0081.6920501522651792
sequ2_div_s06092vam11.3030.00000.0091.8320301546471796
pgranku_div_s06092vam11.1920.00000.0112.15201014521431796
sequ2_div_s02092vam11.1360.00000.0081.5619501532241751
pgrankdu_div_s06092vam10.6900.00000.0091.78192014821221796
pgrankd06092vam10.6260.00000.0091.7219001502961788
seqd_u_div_s06092vam10.5790.00000.0081.5219001522841796
pgrankd_div_s06092vam10.3290.00000.0112.13185014291771791
hhjournalwin_t_nts_hdorig0128epar9.9670.05620.0376.601791161601796
alldefault0all92vam9.0200.00000.0142.24162014342001796
alldefault0all512epar8.5190.00000.0101.48153014891541796
hhjournalnb_t_nts_hdorig032z3_47.9060.00000.0284.031420016541796
hhjournalwin_t_nts_hdorig032z3_43.7860.00000.0271.84680017281796
any47.8845.7918601041796

Greedy sequence

ProverSum%SumG+2G1+2G-1+2G+2MAlt
hhjournal-nb_t_nts_ad2-orig-0-154-epar24.666443
maxcut-default-0-1-128-epar31.180560= pgrank-d_div_s-0-20-128-epar
all-default-0-all-32-z3_434.855626
hhjournal-nb_t_nts_ad2-orig-0-1024-epar36.693659= seq-d_u_div_s-0-60-32-z3_4
seq-d_u_div_s-0-60-32-z3_438.474691
hhjournal-nb_t_nts_ad2-orig-0-92-vam40.033719
default-default-0-0-512-epar40.980736
seq-u2_div_s-0-60-32-z3_441.759750
hhjournal-kn160_t_nts_ad1-orig-0-512-z3_442.316760
seq-d2_div_s-0-60-32-z3_442.762768= pgrank-du_div_s-0-20-512-epar = pgrank-du_div_s-0-60-128-epar = pgrank-d_div_s-0-20-128-epar
pgrank-du_div_s-0-20-512-epar43.207776= pgrank-du_div_s-0-60-128-epar = pgrank-d_div_s-0-20-128-epar
hhjournal-nb_0_hd-orig-0-512-epar43.541782= pgrank-d-0-20-32-z3_4 = pgrank-u_div_s-0-20-128-epar = hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = ... (5)
pgrank-d-0-20-32-z3_443.875788= pgrank-u_div_s-0-20-128-epar = hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = epcl-default-0-60-32-z3_4 = ... (4)
pgrank-u_div_s-0-20-128-epar44.209794= hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4
hhjournal-nb_t_nts_ad1-orig-0-32-z3_444.543800= seq-d_u_div_s-0-20-32-z3_4
seq-d_u_div_s-0-20-32-z3_444.878806
pgrank-u_div_s-0-60-32-z3_445.156811= pgrank-u-0-60-32-z3_4
hhjournal-kn40_t_nts_ad1-orig-0-32-epar45.379815= hhjournal-win_t_nts_hd-orig-0-128-epar = pgrank-du_div_s-0-60-128-epar = pgrank-u-0-60-32-z3_4
pgrank-du_div_s-0-60-128-epar45.601819= pgrank-u-0-60-32-z3_4
pgrank-u-0-60-32-z3_445.824823
pgrank-d_div_s-0-10-92-vam45.991826= seq-d_u_div_exps-0-10-92-vam = pgrank-d_div_s-0-20-32-z3_4 = hhjournal-win_t_nts_hd-orig-0-128-epar = ... (13)
pgrank-d_div_s-0-20-32-z3_446.158829= seq-d_u_div_s2-0-60-32-z3_4
seq-d_u_div_s2-0-60-32-z3_446.325832
seq-d_u_div_s-0-60-512-epar46.437834= pgrank-d-0-10-128-epar = hhjournal-win_t_nts_hd-orig-0-128-epar = epcl-default-0-20-32-z3_4 = ... (7)
pgrank-d-0-10-128-epar46.548836= hhjournal-win_t_nts_hd-orig-0-128-epar = epcl-default-0-20-32-z3_4 = seq-d_u_div_exps-0-60-32-z3_4 = ... (5)
hhjournal-win_t_nts_hd-orig-0-128-epar46.659838= epcl-default-0-20-32-z3_4 = seq-d_u_div_exps-0-60-32-z3_4 = hhjournal-nb_o_hd-orig-0-128-vam
epcl-default-0-20-32-z3_446.771840= seq-d_u_div_exps-0-60-32-z3_4 = hhjournal-nb_o_hd-orig-0-128-vam
seq-d_u_div_exps-0-60-32-z3_446.882842= hhjournal-nb_o_hd-orig-0-128-vam
hhjournal-nb_o_hd-orig-0-128-vam46.993844
pgrank-u-0-60-128-epar47.049845= pgrank-u_div_s-0-60-512-epar = pgrank-d_div_s-0-60-32-z3_4 = pgrank-d_div_s-0-20-512-epar = ... (26)
pgrank-u_div_s-0-60-512-epar47.105846= pgrank-d_div_s-0-60-32-z3_4 = pgrank-d_div_s-0-20-512-epar = seq-d_u_div_s-0-20-128-epar = ... (25)
pgrank-d_div_s-0-60-32-z3_447.160847= pgrank-d_div_s-0-20-512-epar = seq-d_u_div_s-0-20-128-epar = pgrank-u-0-20-512-epar = ... (23)
pgrank-d_div_s-0-20-512-epar47.216848= seq-d_u_div_s-0-20-128-epar = pgrank-u-0-20-512-epar = seq-u2_div_s-0-10-32-z3_4 = ... (22)
seq-d_u_div_s-0-20-128-epar47.272849= seq-u2_div_s-0-10-32-z3_4 = pgrank-d_div_s-0-60-512-epar = all-default-0-all-92-vam = ... (19)
seq-u2_div_s-0-10-32-z3_447.327850= pgrank-d_div_s-0-60-512-epar = all-default-0-all-92-vam = all-default-0-all-128-epar = ... (17)
pgrank-d_div_s-0-60-512-epar47.383851= all-default-0-all-92-vam = all-default-0-all-128-epar = seq-d_u_div_s-0-10-128-epar = ... (15)
all-default-0-all-92-vam47.439852= all-default-0-all-128-epar = seq-d_u_div_s-0-10-128-epar = pgrank-du_div_s-0-10-128-epar = ... (14)
seq-d_u_div_s-0-10-128-epar47.494853= pgrank-du_div_s-0-10-128-epar = seq-d_u_div_exps-0-20-512-epar = pgrank-d_div_s-0-10-32-z3_4 = ... (11)
seq-d_u_div_exps-0-20-512-epar47.550854= pgrank-d_div_s-0-10-32-z3_4 = pgrank-d-0-60-32-z3_4 = pgrank-du-0-60-32-z3_4 = ... (9)
pgrank-d_div_s-0-10-32-z3_447.606855= pgrank-d-0-60-32-z3_4 = pgrank-du-0-60-32-z3_4 = pgrank-u-0-20-32-z3_4 = ... (8)
pgrank-d-0-60-32-z3_447.661856= pgrank-du-0-60-32-z3_4 = pgrank-u-0-20-32-z3_4 = pgrank-d_div_s-0-20-128-epar = ... (6)
pgrank-du-0-60-32-z3_447.717857= pgrank-u-0-20-32-z3_4 = pgrank-d_div_s-0-20-128-epar = epcl-default-0-60-128-epar = ... (5)
pgrank-u-0-20-32-z3_447.773858= pgrank-d_div_s-0-20-128-epar = epcl-default-0-60-128-epar = pgrank-u-0-20-128-epar = ... (4)
pgrank-d_div_s-0-20-128-epar47.829859= epcl-default-0-60-128-epar = pgrank-u-0-20-128-epar
pgrank-u-0-20-128-epar47.884860