--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 06 23:43:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 06 23:46:02 2011 +0200
@@ -302,8 +302,8 @@
formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
- (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
+ [(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *),
+ (0.333, (false, (300, ["mangled_tags?"]))) (* SOS *),
(0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
|> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
else I)}