use native encoding with Vampire -- modern versions handle types better than the old ones
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 30 14:18:07 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 30 14:18:07 2014 +0200
@@ -536,7 +536,7 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_vampire_beyond_1_8 () then
- [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+ [(0.333, (((500, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
(0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
(0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
else