--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 16:14:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 16:37:23 2011 +0200
@@ -334,12 +334,13 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
(if is_old_vampire_version () then
- [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+ [(0.333, (false, (150, FOF, "poly_guards", sosN))),
+ (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
(0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
else
- [(0.334, (true, (50, TFF, "simple", no_sosN))),
+ [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+ (0.334, (true, (50, TFF, "simple", no_sosN))),
(0.333, (false, (500, TFF, "simple", sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}