# HG changeset patch
# User blanchet
# Date 1337698767 -7200
# Node ID a2a821abab83d7d26f1010e271169b6773c50244
# Parent  aada9fd08b58f846331019574c41c170d13d4b36
added one slice with configurable simplification turned off

diff -r aada9fd08b58 -r a2a821abab83 src/HOL/Tools/ATP/atp_systems.ML
--- 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))),