# HG changeset patch
# User wenzelm
# Date 1740771527 -3600
# Node ID bb2ea9e80c33148665344285792d4d7612e9add6
# Parent  8e770d3cc85cf0e1a5e5e47fd01131048e91671e
clone of 62c039ce397c for Isabelle2025 release;

diff -r 8e770d3cc85c -r bb2ea9e80c33 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Feb 23 22:37:36 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Feb 28 20:38:47 2025 +0100
@@ -223,27 +223,32 @@
 
 val new_e_config : atp_config =
   (* FUDGE: this solved 950/1500 (63.33 %) using MePo when testing *)
-  make_e_config 128
-    [(((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false,  512, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false,   64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,   32, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false,   16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false,   64, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false,  128, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, "")))]
+  let
+    val extra_options = "--auto-schedule"
+    val good_slices =
+      [(((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false,   64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,   32, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false,   16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false,   64, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options)))]
+    in
+      make_e_config 128 good_slices
+    end
 
 in