src/HOL/Tools/ATP/atp_systems.ML

       (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
       (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
 
 val spass_new_H1SOS = "-Heuristic=1 -SOS"
-val spass_new_H2 = "-Heuristic=2"
+val spass_new_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
 val spass_new_H2SOS = "-Heuristic=2 -SOS"
 val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
 val spass_new_H2NuVS0Red2 =
   "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
 

    prem_kind = #prem_kind spass_old_config,
    best_slices = fn _ =>
      (* FUDGE *)
      [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
       (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
-      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
+      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2LR0LT0))),
       (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
       (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
       (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
       (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
       (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}