--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 16:59:27 2012 +0200
@@ -392,7 +392,7 @@
|> (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 =
@@ -411,7 +411,7 @@
(* 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))),