1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
     1.3 @@ -253,9 +253,9 @@
     1.4     formats = [FOF],
     1.5     best_slices = fn ctxt =>
     1.6       (* FUDGE *)
     1.7 -     [(0.333, (false, (150, ["mangled_preds_heavy"], sosN))),
     1.8 -      (0.333, (false, (150, ["mangled_preds?"], sosN))),
     1.9 -      (0.334, (true, (150, ["poly_preds"], no_sosN)))]
    1.10 +     [(0.333, (false, (300, ["mangled_preds?"], sosN))),
    1.11 +      (0.333, (false, (100, ["mangled_tags"], sosN))),
    1.12 +      (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
    1.13       |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
    1.14           else I)}
    1.15  
    1.16 @@ -294,9 +294,9 @@
    1.17     formats = [FOF],
    1.18     best_slices = fn ctxt =>
    1.19       (* FUDGE *)
    1.20 -     [(0.333, (false, (200, ["mangled_preds_heavy"], sosN))),
    1.21 -      (0.333, (false, (300, ["mangled_tags?"], sosN))),
    1.22 -      (0.334, (true, (400, ["poly_preds"], no_sosN)))]
    1.23 +     [(0.333, (false, (200, ["mangled_tags_heavy?"], sosN))),
    1.24 +      (0.333, (false, (200, ["poly_preds"], sosN))),
    1.25 +      (0.334, (true, (50, ["mangled_preds?"], no_sosN)))]
    1.26       |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
    1.27           else I)}
    1.28