# HG changeset patch
# User blanchet
# Date 1308669459 -7200
# Node ID a5b1d34d8be781e2b312d6d5c26ca6f6c29e2d77
# Parent  92f5a4c78b37aee0622e5df208addd794a7d9773
tweaked E, SPASS, Vampire setup based on latest Judgment Day results

diff -r 92f5a4c78b37 -r a5b1d34d8be7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 21 17:17:39 2011 +0200
@@ -215,10 +215,10 @@
        (* FUDGE *)
        if method = e_smartN then
          [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
-          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN))),
-          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN)))]
+          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
+          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (300, ["mangled_tags?"], method)))]
+         [(1.0, (true, (500, ["mangled_tags?"], method)))]
      end}
 
 val e = (eN, e_config)
@@ -253,8 +253,8 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (100, ["mangled_tags"], sosN))),
-      (0.333, (false, (500, ["mangled_preds?"], sosN))),
+     [(0.333, (false, (150, ["mangled_tags"], sosN))),
+      (0.333, (false, (300, ["poly_tags?"], 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, (50, ["mangled_preds_heavy"], sosN))),
-      (0.333, (false, (500, ["mangled_tags_heavy?"], sosN))),
-      (0.334, (true, (100, ["mangled_preds?"], no_sosN)))]
+     [(0.333, (false, (150, ["poly_preds"], sosN))),
+      (0.334, (true, (50, ["mangled_preds?"], no_sosN))),
+      (0.333, (false, (500, ["mangled_tags?"], sosN)))]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}