# HG changeset patch
# User blanchet
# Date 1308559262 -7200
# Node ID 12ff5c017cf952a58e0a4ecffdfc9fdfc2fbddd2
# Parent  f205e841402aeaed7ad25b11330039e3902fe71b
slightly better setup for SPASS and Vampire as more results have come in

diff -r f205e841402a -r 12ff5c017cf9 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -253,8 +253,8 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (300, ["mangled_preds?"], sosN))),
-      (0.333, (false, (100, ["mangled_tags"], sosN))),
+     [(0.333, (false, (100, ["mangled_tags"], sosN))),
+      (0.333, (false, (500, ["mangled_preds?"], sosN))),
       (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
      |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
@@ -294,9 +294,9 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (200, ["mangled_tags_heavy?"], sosN))),
-      (0.333, (false, (200, ["poly_preds"], sosN))),
-      (0.334, (true, (50, ["mangled_preds?"], no_sosN)))]
+     [(0.333, (false, (50, ["mangled_preds_heavy"], sosN))),
+      (0.333, (false, (500, ["mangled_tags_heavy?"], sosN))),
+      (0.334, (true, (100, ["mangled_preds?"], no_sosN)))]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}