# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 97f8c6c88134ec3a99dc2f0182b7b4f6c5642641
# Parent  7b5846065c1be739343b04a91a420cf15d0306db
tweak slices, based on eval by Daniel Wand

diff -r 7b5846065c1b -r 97f8c6c88134 src/HOL/Tools/ATP/atp_systems.ML
--- 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)