# HG changeset patch
# User blanchet
# Date 1314292179 -7200
# Node ID a4cbf5668a549034f470549df9f18969297d5a61
# Parent  b20309fa102b9280ad6996c54a9e5acf5ad922dc
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation

diff -r b20309fa102b -r a4cbf5668a54 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:05:40 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:09:39 2011 +0200
@@ -366,8 +366,8 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, TFF, "simple", ""))),
-        (0.25, (false, (125, TFF, "simple", ""))),
+     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
+        (0.25, (false, (125, FOF, "mono_guards?", ""))),
         (0.125, (false, (62, TFF, "simple", ""))),
         (0.125, (false, (31, TFF, "simple", "")))]}