src/HOL/Tools/ATP/atp_systems.ML

      known_szs_status_failures,
    prem_role = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
-        [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
-         (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
+        [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+         (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
          (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
       else
         [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
          (0.333, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
          (0.334, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])