# HG changeset patch
# User desharna
# Date 1740489805 -3600
# Node ID 62c039ce397c4d2dad787f205065deee4a264d72
# Parent  2ea9efde917cb9163db6b97f372cfc8d34d72b74
tuned options given to modern E

Testing 500 goals of the HOL-Library session with a timeout of 30 s resulted in the following results.

- No option: 9.4 % solved
- Option "--auto": 45 % solved
- Option "--auto-schedule": 46.8 % solved

diff -r 2ea9efde917c -r 62c039ce397c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Feb 21 18:46:59 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 25 14:23:25 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