--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 27 16:59:13 2012 +0300
@@ -406,6 +406,7 @@
val spass_old = (spass_oldN, spass_old_config)
+val spass_new_H1SOS = "-Heuristic=1 -SOS"
val spass_new_H2 = "-Heuristic=2"
val spass_new_H2SOS = "-Heuristic=2 -SOS"
val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
@@ -429,9 +430,9 @@
(0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
(0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
(0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
- (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
+ (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, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]}
+ (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]}
val spass_new = (spass_newN, spass_new_config)