1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 11 12:13:08 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 11 13:41:36 2012 +0100
     1.3 @@ -338,9 +338,12 @@
     1.4  val spass = (spassN, spass_config)
     1.5  
     1.6  val spass_new_H2 = "-Heuristic=2"
     1.7 -val spass_new_H2_SOS = "-Heuristic=2 -SOS"
     1.8 +val spass_new_H2SOS = "-Heuristic=2 -SOS"
     1.9  val spass_new_Red2 = "-RFRew=2 -RBRew=2 -RTaut=2"
    1.10  val spass_new_Sorts0 = "-Sorts=0"
    1.11 +val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
    1.12 +val spass_new_H2NuVS0Red2 =
    1.13 +  "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
    1.14  
    1.15  (* Experimental *)
    1.16  val spass_new_config : atp_config =
    1.17 @@ -355,23 +358,14 @@
    1.18     prem_kind = #prem_kind spass_config,
    1.19     best_slices = fn _ =>
    1.20       (* FUDGE *)
    1.21 -(*
    1.22 -     [(0.25, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H1))),
    1.23 -      (0.20, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2_SOS))),
    1.24 -      (0.20, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
    1.25 -      (0.20, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
    1.26 -      (0.15, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2)))]
    1.27 -*)
    1.28 -     [(0.1, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
    1.29 -      (0.1, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_Sorts0))),
    1.30 -      (0.1, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
    1.31 -      (0.1, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2_SOS))),
    1.32 -      (0.1, (true, ((600, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_Red2))),
    1.33 -      (0.1, (true, ((150, DFG DFG_Sorted, "poly_guards??", combsN, false), spass_new_H2))),
    1.34 -      (0.1, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2_SOS))),
    1.35 -      (0.1, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2))),
    1.36 -      (0.1, (true, ((50, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_Sorts0))),
    1.37 -      (0.1, (true, ((100, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_Red2)))]}
    1.38 +     [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
    1.39 +      (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
    1.40 +      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
    1.41 +      (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
    1.42 +      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
    1.43 +      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
    1.44 +      (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
    1.45 +      (0.1000, (false, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]}
    1.46  
    1.47  val spass_new = (spass_newN, spass_new_config)
    1.48