--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Mar 31 09:50:28 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Mar 31 10:15:48 2025 +0200
@@ -384,13 +384,6 @@
local
-val old_vampire_basic_options =
- ["--proof tptp",
- "--output_axiom_names on"] @
- (if ML_System.platform_is_windows
- then [] (*time slicing is not support in the Windows version of Vampire*)
- else ["--mode casc"])
-
val new_vampire_basic_options =
["--input_syntax tptp",
"--proof tptp",
@@ -428,19 +421,7 @@
good_max_mono_iters = default_max_mono_iters,
good_max_new_mono_instances = good_max_new_mono_instances}
-val old_vampire_config : atp_config =
- (* FUDGE *)
- make_vampire_config old_vampire_basic_options (2 * default_max_new_mono_instances)
- [((2, false, false, 512, meshN), (TX1, "mono_native", combsN, false, sosN)),
- ((2, false, false, 1024, meshN), (TX1, "mono_native", liftingN, false, sosN)),
- ((2, false, false, 256, mashN), (TX1, "mono_native", liftingN, false, no_sosN)),
- ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
- ((2, false, false, 16, meshN), (TX1, "mono_native", liftingN, false, no_sosN)),
- ((2, false, false, 32, meshN), (TX1, "mono_native", combsN, false, no_sosN)),
- ((2, false, false, 64, meshN), (TX1, "mono_native", combs_or_liftingN, false, no_sosN)),
- ((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))]
-
-val new_vampire_config : atp_config =
+val vampire_config : atp_config =
(* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
make_vampire_config new_vampire_basic_options 256
[(((2, false, false, 512, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
@@ -465,11 +446,7 @@
in
-val vampire = (vampireN, fn () =>
- if string_ord (getenv "VAMPIRE_VERSION", "4.8") <> LESS then
- new_vampire_config
- else
- old_vampire_config)
+val vampire = (vampireN, fn () => vampire_config)
end