src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

   type term_order = ATP_Problem.term_order
   type atp_format = ATP_Problem.atp_format
   type atp_formula_role = ATP_Problem.atp_formula_role
   type atp_failure = ATP_Proof.atp_failure
 
-  type atp_slice = (int * string) * atp_format * string * string * bool * string
+  type base_slice = int * string
+  type atp_slice = atp_format * string * string * bool * string
   type atp_config =
     {exec : string list * string list,
      arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
        term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
      proof_delims : (string * string) list,
      known_failures : (atp_failure * string) list,
      prem_role : atp_formula_role,
-     best_slices : Proof.context -> atp_slice list,
-     best_max_mono_iters : int,
-     best_max_new_mono_instances : int}
+     good_slices : Proof.context -> (base_slice * atp_slice) list,
+     good_max_mono_iters : int,
+     good_max_new_mono_instances : int}
 
   val default_max_mono_iters : int
   val default_max_new_mono_instances : int
   val term_order : string Config.T
   val e_smartN : string

   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
   val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
-    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice) ->
+    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) ->
     string * (unit -> atp_config)
   val add_atp : string * (unit -> atp_config) -> theory -> theory
   val get_atp : theory -> string -> (unit -> atp_config)
   val supported_atps : theory -> string list
   val is_atp_installed : theory -> string -> bool

 val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice)
 
 val default_max_mono_iters = 3 (* FUDGE *)
 val default_max_new_mono_instances = 100 (* FUDGE *)
 
-type atp_slice = (int * string) * atp_format * string * string * bool * string
+type base_slice = int * string
+type atp_slice = atp_format * string * string * bool * string
 
 type atp_config =
   {exec : string list * string list,
    arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
      term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list,
    proof_delims : (string * string) list,
    known_failures : (atp_failure * string) list,
    prem_role : atp_formula_role,
-   best_slices : Proof.context -> atp_slice list,
-   best_max_mono_iters : int,
-   best_max_new_mono_instances : int}
-
-(* "best_slices" must be found empirically, taking a holistic approach since the
+   good_slices : Proof.context -> (base_slice * atp_slice) list,
+   good_max_mono_iters : int,
+   good_max_new_mono_instances : int}
+
+(* "good_slices" must be found empirically, taking a holistic approach since the
    ATPs are run in parallel. Each slice has the format
 
      (time_frac, ((max_facts, fact_filter), format, type_enc,
                   lam_trans, uncurried_aliases), extra)
 

    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
      ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")],
-   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val agsyhol = (agsyholN, fn () => agsyhol_config)
 
 
 (* Alt-Ergo *)

    known_failures =
      [(ProofMissing, ": Valid"),
       (TimedOut, ": Timeout"),
       (GaveUp, ": Unknown")],
    prem_role = Hypothesis,
-   best_slices = fn _ =>
+   good_slices =
      (* FUDGE *)
-     [((100, meshN), TF1, "poly_native", liftingN, false, "")],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((100, meshN), (TF1, "poly_native", liftingN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
 
 
 (* E *)

    known_failures =
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded")] @
      known_szs_status_failures,
    prem_role = Conjecture,
-   best_slices = fn ctxt =>
+   good_slices = fn ctxt =>
      let
        val heuristic = Config.get ctxt e_selection_heuristic
        val (format, enc, main_lam_trans) =
          if string_ord (getenv "E_VERSION", "2.7") <> LESS then
            (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)

          else
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
      in
        (* FUDGE *)
        if heuristic = e_smartN then
-         [((128, meshN), format, enc, main_lam_trans, false, e_fun_weightN),
-          ((128, mashN), format, enc, main_lam_trans, false, e_sym_offset_weightN),
-          ((91, mepoN), format, enc, main_lam_trans, false, e_autoN),
-          ((1000, meshN), format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN),
-          ((256, mepoN), format, enc, liftingN, false, e_fun_weightN),
-          ((64, mashN), format, enc, combsN, false, e_fun_weightN)]
+         [((128, meshN), (format, enc, main_lam_trans, false, e_fun_weightN)),
+          ((128, mashN), (format, enc, main_lam_trans, false, e_sym_offset_weightN)),
+          ((91, mepoN), (format, enc, main_lam_trans, false, e_autoN)),
+          ((1000, meshN), (format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN)),
+          ((256, mepoN), (format, enc, liftingN, false, e_fun_weightN)),
+          ((64, mashN), (format, enc, combsN, false, e_fun_weightN))]
        else
-         [((500, meshN), format, enc, combsN, false, heuristic)]
+         [((500, meshN), (format, enc, combsN, false, heuristic))]
      end,
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val e = (eN, fn () => e_config)
 
 
 (* iProver *)

    proof_delims = tstp_proof_delims,
    known_failures =
      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((150, meshN), FOF, "mono_guards??", liftingN, false, "")],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((150, meshN), (FOF, "mono_guards??", liftingN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val iprover = (iproverN, fn () => iprover_config)
 
 
 (* LEO-II *)

    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")],
-   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val leo2 = (leo2N, fn () => leo2_config)
 
 
 (* Leo-III *)

       \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
       (if full_proofs then "--nleq --naeq " else "")],
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((512, meshN), TH1, "mono_native_higher", keep_lamsN, false, "")],
-   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((512, meshN), (TH1, "mono_native_higher", keep_lamsN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val leo3 = (leo3N, fn () => leo3_config)
 
 
 (* Satallax *)

       "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem],
    proof_delims =
      [("% SZS output start Proof", "% SZS output end Proof")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((150, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")],
-   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances}
+     K [((150, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val satallax = (satallaxN, fn () => satallax_config)
 
 
 (* SPASS *)

         (MalformedInput, "Undefined symbol"),
         (MalformedInput, "Free Variable"),
         (Unprovable, "No formulae and clauses found in input file"),
         (InternalError, "Please report this error")],
      prem_role = Conjecture,
-     best_slices = fn _ =>
+     good_slices =
        (* FUDGE *)
-       [((150, meshN), format, "mono_native", combsN, true, ""),
-        ((500, meshN), format, "mono_native", liftingN, true, spass_H2SOS),
-        ((50, meshN), format,  "mono_native", liftingN, true, spass_H2LR0LT0),
-        ((250, meshN), format, "mono_native", combsN, true, spass_H2NuVS0),
-        ((1000, mepoN), format, "mono_native", liftingN, true, spass_H1SOS),
-        ((150, meshN), format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2),
-        ((300, meshN), format, "mono_native", combsN, true, spass_H2SOS),
-        ((100, meshN), format, "mono_native", combs_and_liftingN, true, spass_H2)],
-     best_max_mono_iters = default_max_mono_iters,
-     best_max_new_mono_instances = default_max_new_mono_instances}
+       K [((150, meshN), (format, "mono_native", combsN, true, "")),
+        ((500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)),
+        ((50, meshN), (format,  "mono_native", liftingN, true, spass_H2LR0LT0)),
+        ((250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)),
+        ((1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)),
+        ((150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
+        ((300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)),
+        ((100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))],
+     good_max_mono_iters = default_max_mono_iters,
+     good_max_new_mono_instances = default_max_new_mono_instances}
   end
 
 val spass = (spassN, fn () => spass_config)
 
 

       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (Interrupted, "Aborted by signal SIGINT")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices = fn ctxt =>
+   good_slices =
      (* FUDGE *)
-     [((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, sosN),
-      ((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false, sosN),
-      ((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+     K [((500, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, sosN)),
+      ((150, meshN), (TX1, "poly_native_fool", combs_or_liftingN, false, sosN)),
+      ((50, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN))],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
 val vampire = (vampireN, fn () => vampire_config)
 
 
 (* Z3 with TPTP syntax (half experimental, half legacy) *)

    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
      ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
    proof_delims = [("SZS status Theorem", "")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
-   best_slices =
+   good_slices =
      (* FUDGE *)
-     K [((250, meshN), TF0, "mono_native", combsN, false, ""),
-        ((125, mepoN), TF0, "mono_native", combsN, false, ""),
-        ((62, mashN), TF0, "mono_native", combsN, false, ""),
-        ((31, meshN), TF0, "mono_native", combsN, false, "")],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+     K [((250, meshN), (TF0, "mono_native", combsN, false, "")),
+      ((125, mepoN), (TF0, "mono_native", combsN, false, "")),
+      ((62, mashN), (TF0, "mono_native", combsN, false, "")),
+      ((31, meshN), (TF0, "mono_native", combsN, false, ""))],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
 
 
 (* Zipperposition *)

      proof_delims = tstp_proof_delims,
      known_failures =
        [(TimedOut, "SZS status ResourceOut")] @   (* odd way of timing out *)
        known_szs_status_failures,
      prem_role = Hypothesis,
-     best_slices = fn _ =>
-       [((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1"),
-        ((256, mashN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1"),
-        ((128, mepoN), format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj"),
-        ((1024, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1"),
-        ((64, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15"),
-        ((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true")],
-     best_max_mono_iters = default_max_mono_iters,
-     best_max_new_mono_instances = default_max_new_mono_instances}
+     good_slices =
+       K [((512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")),
+        ((256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")),
+        ((128, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")),
+        ((1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")),
+        ((64, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")),
+        ((512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true"))],
+     good_max_mono_iters = default_max_mono_iters,
+     good_max_new_mono_instances = default_max_new_mono_instances}
   end
 
 val zipperposition = (zipperpositionN, fn () => zipperposition_config)
 
 

 
 val max_remote_secs = 1000   (* give Geoff Sutcliffe's servers a break *)
 
 val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"])
 
-fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
+fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice =
   {exec = isabelle_scala_function,
    arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ =>
      [the_remote_system system_name system_versions,
       Isabelle_System.absolute_path problem,
       command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)],
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_says_failures,
    prem_role = prem_role,
-   best_slices = fn ctxt => [best_slice ctxt],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances} : atp_config
-
-fun remotify_config system_name system_versions best_slice
+   good_slices = fn ctxt => [good_slice ctxt],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = default_max_new_mono_instances} : atp_config
+
+fun remotify_config system_name system_versions good_slice
     ({proof_delims, known_failures, prem_role, ...} : atp_config) =
-  remote_config system_name system_versions proof_delims known_failures prem_role best_slice
-
-fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice =
+  remote_config system_name system_versions proof_delims known_failures prem_role good_slice
+
+fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice =
   (remote_prefix ^ name, fn () =>
-     remote_config system_name system_versions proof_delims known_failures prem_role best_slice)
-fun remotify_atp (name, config) system_name system_versions best_slice =
-  (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config)
+     remote_config system_name system_versions proof_delims known_failures prem_role good_slice)
+fun remotify_atp (name, config) system_name system_versions good_slice =
+  (remote_prefix ^ name, remotify_config system_name system_versions good_slice o config)
 
 fun gen_remote_waldmeister name type_enc =
   remote_atp name "Waldmeister" ["710"] tstp_proof_delims
     ([(OutOfResources, "Too many function symbols"),
       (Inappropriate, "****  Unexpected end of file."),
       (Crashed, "Unrecoverable Segmentation Fault")]
      @ known_szs_status_failures)
     Hypothesis
-    (K ((50, meshN), CNF_UEQ, type_enc, combsN, false, "") (* FUDGE *))
+    (K ((50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *))
 
 val remote_agsyhol =
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
-    (K ((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *))
+    (K ((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *))
 val remote_alt_ergo =
   remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"]
-    (K ((250, meshN), TF1, "poly_native", keep_lamsN, false, "") (* FUDGE *))
+    (K ((250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
-    (K ((750, meshN), TF0, "mono_native", combsN, false, "") (* FUDGE *))
+    (K ((750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]
-    (K ((150, meshN), FOF, "mono_guards??", liftingN, false, "") (* FUDGE *))
+    (K ((150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
-    (K ((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "") (* FUDGE *))
+    (K ((40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *))
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
-    (K ((150, meshN), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "") (* FUDGE *))
+    (K ((150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 val remote_zipperposition =
   remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"]
-    (K ((512, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *))
+    (K ((512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *))
 
 
 (* Dummy prover *)
 
 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
    arguments = K (K (K (K (K (K []))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = prem_role,
-   best_slices =
-     K [((200, "mepo"), format, type_enc,
-        if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, "")],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+   good_slices =
+     K [((200, "mepo"), (format, type_enc,
+      if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))],
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_fof =
   (dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false)
 
 val dummy_tfx =