--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Jun 17 11:27:21 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Jun 17 12:57:22 2021 +0200
@@ -552,7 +552,7 @@
val zipperposition_config : atp_config =
let
- val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
+ val format = THF (With_FOOL, Polymorphic, THF_Without_Choice)
in
{exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -563,9 +563,9 @@
prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
- (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
- (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
+ [(0.333, (((128, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_blsimp)),
+ (0.333, (((32, "meshN"), format, "poly_native_higher_fool", keep_lamsN, false), zipperposition_s6)),
+ (0.334, (((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_cdots))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
end