make sure that if slicing is disabled, a non-SOS slice is chosen
authorblanchet
Thu, 25 Aug 2011 23:55:21 +0200
changeset 44503 97ec9abd3253
parent 44502 c537d5e5a365
child 44504 6f29df8d2007
make sure that if slicing is disabled, a non-SOS slice is chosen
src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 23:54:57 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 23:55:21 2011 +0200
@@ -335,12 +335,12 @@
      (* FUDGE *)
      (if is_old_vampire_version () then
         [(0.333, (false, (150, FOF, "poly_guards", sosN))),
-         (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
-         (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
+         (0.333, (false, (500, FOF, "mono_tags?", sosN))),
+         (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
       else
         [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
-         (0.334, (true, (50, TFF Implicit, "simple", no_sosN))),
-         (0.333, (false, (500, TFF Implicit, "simple", sosN)))])
+         (0.333, (false, (500, TFF Implicit, "simple", sosN))),
+         (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}