1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 21 17:17:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jun 21 17:17:39 2011 +0200
     1.3 @@ -215,10 +215,10 @@
     1.4         (* FUDGE *)
     1.5         if method = e_smartN then
     1.6           [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
     1.7 -          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN))),
     1.8 -          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN)))]
     1.9 +          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
    1.10 +          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
    1.11         else
    1.12 -         [(1.0, (true, (300, ["mangled_tags?"], method)))]
    1.13 +         [(1.0, (true, (500, ["mangled_tags?"], method)))]
    1.14       end}
    1.15  
    1.16  val e = (eN, e_config)
    1.17 @@ -253,8 +253,8 @@
    1.18     formats = [FOF],
    1.19     best_slices = fn ctxt =>
    1.20       (* FUDGE *)
    1.21 -     [(0.333, (false, (100, ["mangled_tags"], sosN))),
    1.22 -      (0.333, (false, (500, ["mangled_preds?"], sosN))),
    1.23 +     [(0.333, (false, (150, ["mangled_tags"], sosN))),
    1.24 +      (0.333, (false, (300, ["poly_tags?"], sosN))),
    1.25        (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
    1.26       |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
    1.27           else I)}
    1.28 @@ -294,9 +294,9 @@
    1.29     formats = [FOF],
    1.30     best_slices = fn ctxt =>
    1.31       (* FUDGE *)
    1.32 -     [(0.333, (false, (50, ["mangled_preds_heavy"], sosN))),
    1.33 -      (0.333, (false, (500, ["mangled_tags_heavy?"], sosN))),
    1.34 -      (0.334, (true, (100, ["mangled_preds?"], no_sosN)))]
    1.35 +     [(0.333, (false, (150, ["poly_preds"], sosN))),
    1.36 +      (0.334, (true, (50, ["mangled_preds?"], no_sosN))),
    1.37 +      (0.333, (false, (500, ["mangled_tags?"], sosN)))]
    1.38       |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
    1.39           else I)}
    1.40