src/HOL/Tools/ATP/atp_systems.ML
changeset 58495 aefcb244423f
parent 58478 999adf103930
child 59070 c67c0a729c2d
equal deleted inserted replaced
58494:ed380b9594b5 58495:aefcb244423f
   534      known_szs_status_failures,
   534      known_szs_status_failures,
   535    prem_role = Conjecture,
   535    prem_role = Conjecture,
   536    best_slices = fn ctxt =>
   536    best_slices = fn ctxt =>
   537      (* FUDGE *)
   537      (* FUDGE *)
   538      (if is_vampire_beyond_1_8 () then
   538      (if is_vampire_beyond_1_8 () then
   539         [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
   539         [(0.333, (((500, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
   540          (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
   540          (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
   541          (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
   541          (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
   542       else
   542       else
   543         [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
   543         [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
   544          (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
   544          (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),