added refute mode to Sledgehammer to find 'counterexamples'

--- a/NEWS	Tue Feb 14 09:36:35 2023 +0100
+++ b/NEWS	Wed Feb 15 10:56:23 2023 +0100
@@ -228,6 +228,12 @@
 
 * Metis:
   - Made clausifier more robust in the face of nested lambdas.
+    Minor INCOMPATIBILITY.
+
+* Sledgehammer:
+  - Added refutational mode to find likely unprovable conectures. It is
+    enabled by default in addition to the usual proving mode and can be
+    enabled or disabled using the 'refute' option.
 
 
 *** ML ***

--- a/src/Doc/Sledgehammer/document/root.tex	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Feb 15 10:56:23 2023 +0100
@@ -99,9 +99,10 @@
 \label{introduction}
 
 Sledgehammer is a tool that applies automatic theorem provers (ATPs)
-and satisfiability-modulo-theories (SMT) solvers on the current goal.%
-\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
-historical.}
+and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
+to find proofs but also to find inconsistencies.%
+\footnote{The distinction between ATPs and SMT solvers is mostly
+historical but convenient.}
 %
 The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
 \cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III
@@ -113,9 +114,9 @@
 \cite{bouton-et-al-2009}, and Z3 \cite{de-moura-2008}. These are always run
 locally.
 
-The problem passed to the external provers (or solvers) consists of your current
-goal together with a heuristic selection of hundreds of facts (theorems) from the
-current theory context, filtered by relevance.
+The problem passed to the automatic provers (or solvers) consists of your
+current goal together with a heuristic selection of hundreds of facts (theorems)
+from the current theory context, filtered by relevance.
 
 The result of a successful proof search is some source text that typically
 reconstructs the proof within Isabelle. For ATPs, the reconstructed proof
@@ -123,6 +124,10 @@
 integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
 the kernel. Thus its results are correct by construction.
 
+Sometimes the automatic provers might detect that the goal is inconsistent with
+the background facts---or even that the background facts are inconsistent
+regardless of of the goal.
+
 For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be
 enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options >
 Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
@@ -162,9 +167,9 @@
 already include properly set up executables for CVC4, cvc5, E, SPASS, Vampire,
 veriT, Z3, and Zipperposition ready to use.
 
-\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
-SPASS, Vampire, veriT, Z3, and Zipperposition binary packages from \download.
-Extract the archives, then add a line to your
+\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4,
+cvc5, E, SPASS, Vampire, veriT, Z3, and Zipperposition binary packages from
+\download. Extract the archives, then add a line to your
 \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
 startup. Its value can be retrieved by executing \texttt{isabelle}
@@ -225,8 +230,8 @@
 \postw
 
 Instead of issuing the \textbf{sledgehammer} command, you can also use the
-Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like
-the following output after a few seconds:
+Sledgehammer panel in Isabelle/jEdit. Either way, Sledgehammer will produce
+something like the following output after a few seconds:
 
 \prew
 \slshape
@@ -238,7 +243,7 @@
 cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\
 z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\
 vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
-QED
+Done
 \postw
 
 Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel.
@@ -260,6 +265,23 @@
 readable and also faster than \textit{metis} or \textit{smt} one-line
 proofs. This feature is experimental.
 
+For goals that are inconsistent with the background theory (and hence unprovable
+unless the theory is itself inconsistent), such as
+
+\prew
+\textbf{lemma} ``$\mathit{length}\; (\mathit{zip}\; \mathit{xs}\; \mathit{ys}) = \mathit{length}\; \mathit{xs}$'' \\
+\textbf{sledgehammer}
+\postw
+
+Sledgehammer's output might look as follows:
+
+\prew
+\slshape
+vampire found an inconsistency\ldots \\
+vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
+Done
+\postw
+
 
 \section{Hints}
 \label{hints}
@@ -791,6 +813,16 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
+\opsmart{check\_consistent}{dont\_check\_consistent}
+Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
+default, it looks for both proofs and inconsistencies.
+
+An inconsistency indicates that the goal, taken as an axiom, would be
+inconsistent with some specific background facts if it were added as a lemma,
+indicating a likely issue with the goal. Sometimes the inconsistency involves
+only the background theory; this might happen, for example, if an axiom is used
+or if a lemma was introduced with \textbf{sorry}.
+
 \optrue{minimize}{dont\_minimize}
 Specifies whether the proof minimization tool should be invoked automatically
 after proof search.

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -21,7 +21,7 @@
      command: unit -> string list,
      options: Proof.context -> string list,
      smt_options: (string * string) list,
-     good_slices: ((int * int * string) * string list) list,
+     good_slices: ((int * bool * bool * int * string) * string list) list,
      outcome: string -> string list -> outcome * string list,
      parse_proof: (Proof.context -> SMT_Translate.replay_data ->
        ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -30,7 +30,8 @@
 
   (*registry*)
   val add_solver: solver_config -> theory -> theory
-  val good_slices: Proof.context -> string -> ((int * int * string) * string list) list
+  val good_slices: Proof.context -> string ->
+    ((int * bool * bool * int * string) * string list) list
 
   (*filter*)
   val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list ->
@@ -155,7 +156,7 @@
    command: unit -> string list,
    options: Proof.context -> string list,
    smt_options: (string * string) list,
-   good_slices: ((int * int * string) * string list) list,
+   good_slices: ((int * bool * bool * int * string) * string list) list,
    outcome: string -> string list -> outcome * string list,
    parse_proof: (Proof.context -> SMT_Translate.replay_data ->
      ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -180,7 +181,7 @@
 type solver_info = {
   command: unit -> string list,
   smt_options: (string * string) list,
-  good_slices: ((int * int * string) * string list) list,
+  good_slices: ((int * bool * bool * int * string) * string list) list,
   parse_proof: Proof.context -> SMT_Translate.replay_data ->
     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
     parsed_proof,

--- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -104,13 +104,13 @@
   smt_options = [(":produce-unsat-cores", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+    [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = NONE }
@@ -124,13 +124,13 @@
   smt_options = [(":produce-unsat-cores", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+    [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = NONE }
@@ -169,12 +169,12 @@
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, 1024, meshN), []),
-     ((2, 512, mashN), []),
-     ((2, 64, meshN), []),
-     ((2, 128, meshN), []),
-     ((2, 256, mepoN), []),
-     ((2, 32, meshN), [])],
+    [((2, false, false, 1024, meshN), []),
+     ((2, false, false, 512, mashN), []),
+     ((2, false, true, 128, meshN), []),
+     ((2, false, false, 64, meshN), []),
+     ((2, false, false, 256, mepoN), []),
+     ((2, false, false, 32, meshN), [])],
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
   parse_proof = SOME (K Lethe_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
@@ -210,12 +210,12 @@
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, 1024, meshN), []),
-     ((2, 512, mepoN), []),
-     ((2, 64, meshN), []),
-     ((2, 256, meshN), []),
-     ((2, 128, mashN), []),
-     ((2, 32, meshN), [])],
+    [((2, false, false, 1024, meshN), []),
+     ((2, false, false, 512, mepoN), []),
+     ((2, false, false, 64, meshN), []),
+     ((2, false, true, 256, meshN), []),
+     ((2, false, false, 128, mashN), []),
+     ((2, false, false, 32, meshN), [])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }
@@ -250,7 +250,7 @@
   Theory.setup
     (Method.setup \<^binding>\<open>smt\<close>
       (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method))
-      "Call to the SMT solvers veriT or z3")
+      "Call to the SMT solver veriT or z3")
 
 (* overall setup *)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -70,6 +70,12 @@
   | alternative _ NONE (y as SOME _) = y
   | alternative _ NONE NONE = NONE
 
+fun varify_nonfixed_terms_global nonfixeds tm = tm
+  |> Same.commit (Term_Subst.map_aterms_same
+    (fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME
+      | Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm])
+      | _ => raise Same.SAME))
+
 fun max_outcome outcomes =
   let
     val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
@@ -148,17 +154,20 @@
 
 fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
     (problem as {state, subgoal, factss, ...} : prover_problem)
-    (slice as ((slice_size, num_facts, fact_filter), _)) name =
+    (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name =
   let
     val ctxt = Proof.context_of state
 
-    val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
+    val _ = spying spy (fn () => (state, subgoal, name,
+      "Launched" ^ (if abduce then " (abduce)" else "") ^
+      (if check_consistent then " (check_consistent)" else "")))
 
     val _ =
       if verbose then
         writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
           plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
-          "...")
+          (if abduce then " (abduce)" else "") ^
+          (if check_consistent then " (check_consistent)" else "") ^ "...")
       else
         ()
 
@@ -168,7 +177,8 @@
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
-      |> prefix ("Facts in " ^ name ^ " proof: ")
+      |> prefix ("Facts in " ^ name ^ " " ^
+        (if check_consistent then "inconsistency" else "proof") ^ ": ")
       |> writeln
 
     fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -196,8 +206,8 @@
             |> AList.group (op =)
             |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
         in
-          "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
-          plural_s num_used_facts ^
+          "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^
+          string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^
           (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
         end
       | spying_str_of_res {outcome = SOME failure, ...} =
@@ -233,6 +243,21 @@
     (output, output_message)
   end
 
+fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) =
+  if outcome = SOME ATP_Proof.TimedOut then
+    (SH_Timeout, K "")
+  else if is_some outcome then
+    (SH_None, K "")
+  else
+    (SH_Some (result, []), fn () =>
+       (if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then
+          (case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of
+            [] => "The goal is inconsistent"
+          | facts => "The goal is inconsistent with these facts: " ^ commas facts)
+        else
+          "The following facts are inconsistent: " ^
+          commas (map fst used_facts)))
+
 fun check_expected_outcome ctxt prover_name expect outcome =
   let
     val outcome_code = short_string_of_sledgehammer_outcome outcome
@@ -248,22 +273,48 @@
           if exists (fn (_, (Played _, _)) => true | _ => false) preplay_results then
             ()
           else
-            error ("Unexpected outcome: the external prover found a some proof but preplay failed")
+            error ("Unexpected outcome: the external prover found a proof but preplay failed")
       | ("unknown", SH_Unknown) => ()
       | ("timeout", SH_Timeout) => ()
       | ("none", SH_None) => ()
       | _ => error ("Unexpected outcome: " ^ quote outcome_code))
   end
 
-fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn
-    (problem as {state, subgoal, ...}) slice prover_name =
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode found_something
+    writeln_result learn (problem as {state, subgoal, ...})
+    (slice as ((_, _, check_consistent, _, _), _)) prover_name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = Time.scale 5.0 timeout
 
+    fun flip_problem {comment, state, goal, subgoal, factss = factss, ...} =
+      let
+        val thy = Proof_Context.theory_of ctxt
+        val assms = Assumption.all_assms_of ctxt
+        val assm_ts = map Thm.term_of assms
+        val subgoal_t = Logic.get_goal (Thm.prop_of goal) subgoal
+        val polymorphic_subgoal_t = (Logic.list_implies (assm_ts, subgoal_t))
+          |> Logic.varify_global
+        val nonfixeds =
+          subtract (op =) (fold Term.add_free_names assm_ts []) (Term.add_free_names subgoal_t [])
+        val monomorphic_subgoal_t = subgoal_t
+          |> varify_nonfixed_terms_global nonfixeds
+        val subgoal_thms = map (Skip_Proof.make_thm thy)
+          [polymorphic_subgoal_t, monomorphic_subgoal_t]
+        val new_facts =
+          map (fn thm => (((sledgehammer_goal_as_fact, (Assum, General)), thm))) subgoal_thms
+      in
+        {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1,
+         subgoal_count = 1, factss = map (apsnd (append new_facts)) factss,
+         found_something = found_something "an inconsistency"}
+      end
+
+    val problem = problem |> check_consistent ? flip_problem
+
     fun really_go () =
       launch_prover params mode learn problem slice prover_name
-      |> preplay_prover_result params state subgoal
+      |> (if check_consistent then analyze_prover_result_for_consistency else
+        preplay_prover_result params state subgoal)
 
     fun go () =
       if debug then
@@ -330,13 +381,15 @@
   end
 
 fun prover_slices_of_schedule ctxt factss
-    ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule =
+    ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
+      ...} : params)
+    schedule =
   let
     fun triplicate_slices original =
       let
         val shift =
-          map (apfst (fn (slice_size, num_facts, fact_filter) =>
-            (slice_size, num_facts,
+          map (apfst (fn (slice_size, abduce, check_consistent, num_facts, fact_filter) =>
+            (slice_size, abduce, check_consistent, num_facts,
              if fact_filter = mashN then mepoN
              else if fact_filter = mepoN then meshN
              else mashN)))
@@ -353,14 +406,17 @@
           the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
       | adjust_extra (extra as SMT_Slice _) = extra
 
-    fun adjust_slice max_slice_size ((slice_size0, num_facts0, fact_filter0), extra) =
+    fun adjust_slice max_slice_size
+        ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) =
       let
         val slice_size = Int.min (max_slice_size, slice_size0)
+        val abduce = abduce |> the_default abduce0
+        val check_consistent = check_consistent |> the_default check_consistent0
         val fact_filter = fact_filter |> the_default fact_filter0
         val max_facts = max_facts |> the_default num_facts0
         val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
       in
-        ((slice_size, num_facts, fact_filter), adjust_extra extra)
+        ((slice_size, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra)
       end
 
     val provers = distinct (op =) schedule
@@ -378,7 +434,7 @@
           SOME (slice0 :: slices) =>
           let
             val prover_slices' = AList.update (op =) (prover, slices) prover_slices
-            val slice as ((slice_size, _, _), _) =
+            val slice as ((slice_size, _, _, _, _), _) =
               adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0
           in
             (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule
@@ -389,8 +445,8 @@
     |> distinct (op =)
   end
 
-fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,
-      slices, ...})
+fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules,
+      max_facts, max_proofs, slices, ...})
     mode writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
@@ -402,12 +458,13 @@
         val _ = Proof.assert_backward state
         val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
 
-        val found_proofs = Synchronized.var "found_proofs" 0
+        val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0
 
-        fun found_proof prover_name =
+        fun found_something a_proof_or_inconsistency prover_name =
           if mode = Normal then
-            (Synchronized.change found_proofs (fn n => n + 1);
-             (the_default writeln writeln_result) (prover_name ^ " found a proof..."))
+            (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1);
+             (the_default writeln writeln_result) (prover_name ^ " found " ^
+             a_proof_or_inconsistency ^ "..."))
           else
             ()
 
@@ -437,7 +494,8 @@
                 SOME n => n
               | NONE =>
                 fold (fn prover =>
-                    fold (fn ((_, n, _), _) => Integer.max n) (get_slices ctxt prover))
+                      fold (fn ((_, _, _, max_facts, _), _) => Integer.max max_facts)
+                    (get_slices ctxt prover))
                   provers 0)
               * 51 div 50  (* some slack to account for filtering of induction facts below *)
 
@@ -463,9 +521,9 @@
             val factss = get_factss provers
             val problem =
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-               factss = factss, found_proof = found_proof}
+               factss = factss, found_something = found_something "a proof"}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
-            val launch = launch_prover_and_preplay params mode writeln_result learn
+            val launch = launch_prover_and_preplay params mode found_something writeln_result learn
 
             val schedule =
               if mode = Auto_Try then provers
@@ -487,7 +545,7 @@
             else
               (learn chained_thms;
                Par_List.map (fn (prover, slice) =>
-                   if Synchronized.value found_proofs < max_proofs then
+                   if Synchronized.value found_proofs_and_inconsistencies < max_proofs then
                      launch problem slice prover
                    else
                      (SH_None, ""))
@@ -499,11 +557,19 @@
          handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
         |> `(fn (outcome, message) =>
           (case outcome of
-            SH_Some _ => (the_default writeln writeln_result "QED"; true)
+            SH_Some _ => (the_default writeln writeln_result "Done"; true)
           | SH_Unknown => (the_default writeln writeln_result message; false)
-          | SH_Timeout => (the_default writeln writeln_result "No proof found"; false)
+          | SH_Timeout =>
+            (the_default writeln writeln_result
+               ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
+                " found");
+             false)
           | SH_None => (the_default writeln writeln_result
-                (if message = "" then "No proof found" else "Warning: " ^ message);
+                (if message = "" then
+                   "No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
+                   " found"
+                 else
+                   "Warning: " ^ message);
               false)))
       end)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -11,7 +11,7 @@
   type atp_formula_role = ATP_Problem.atp_formula_role
   type atp_failure = ATP_Proof.atp_failure
 
-  type base_slice = int * int * string
+  type base_slice = int * bool * bool * int * string
   type atp_slice = atp_format * string * string * bool * string
   type atp_config =
     {exec : string list * string list,
@@ -67,8 +67,8 @@
 val default_max_mono_iters = 3 (* FUDGE *)
 val default_max_new_mono_instances = 100 (* FUDGE *)
 
-(* desired slice size, desired number of facts, fact filter *)
-type base_slice = int * int * string
+(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *)
+type base_slice = int * bool * bool * int * string
 
 (* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
    prover-specific extra information *)
@@ -142,7 +142,7 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((2, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((2, false, false, 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}
 
@@ -165,7 +165,7 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))],
+     K [((1000 (* infinity *), false, false, 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}
 
@@ -200,12 +200,12 @@
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")
      in
        (* FUDGE *)
-       K [((1000 (* infinity *), 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), 128, mepoN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
-         ((1000 (* infinity *), 256, mepoN), (format, type_enc, liftingN, false, extra_options)),
-         ((1000 (* infinity *), 64, mashN), (format, type_enc, combsN, false, extra_options))]
+       K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+         ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
+         ((1000 (* infinity *), false, false, 128, mepoN), (format, type_enc, lam_trans, false, extra_options)),
+         ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
+         ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options)),
+         ((1000 (* infinity *), false, false, 64, mashN), (format, type_enc, combsN, false, extra_options))]
      end,
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}
@@ -229,11 +229,11 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((2, 32, meshN), (TF0, "mono_native", liftingN, false, "")),
-       ((2, 512, meshN), (TX0, "mono_native", liftingN, false, "")),
-       ((2, 128, mashN), (TF0, "mono_native", combsN, false, "")),
-       ((2, 1024, meshN), (TF0, "mono_native", liftingN, false, "")),
-       ((2, 256, mepoN), (TF0, "mono_native", combsN, false, ""))],
+     K [((2, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, "")),
+       ((2, false, false, 512, meshN), (TX0, "mono_native", liftingN, false, "")),
+       ((2, false, false, 128, mashN), (TF0, "mono_native", combsN, false, "")),
+       ((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, "")),
+       ((2, false, true, 256, mepoN), (TF0, "mono_native", combsN, false, ""))],
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -259,7 +259,7 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((2, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((2, false, false, 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}
 
@@ -281,8 +281,8 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((6, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")),
-       ((6, 512, meshN), (TF0, "mono_native", liftingN, false, ""))],
+     K [((6, false, false, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")),
+       ((6, false, false, 512, meshN), (TF0, "mono_native", liftingN, false, ""))],
    good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -306,7 +306,7 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((12, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((12, false, false, 256, 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}
 
@@ -341,14 +341,14 @@
    generate_isabelle_info = true,
    good_slices =
      (* FUDGE *)
-     K [((2, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")),
-      ((2, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)),
-      ((2, 50, meshN), (DFG Monomorphic,  "mono_native", liftingN, true, spass_H2LR0LT0)),
-      ((2, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)),
-      ((2, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)),
-      ((2, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
-      ((2, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)),
-      ((2, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))],
+     K [((2, false, false, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")),
+      ((2, false, false, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)),
+      ((2, false, false, 50, meshN), (DFG Monomorphic,  "mono_native", liftingN, true, spass_H2LR0LT0)),
+      ((2, false, false, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)),
+      ((2, false, false, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)),
+      ((2, false, true, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
+      ((2, false, false,  300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)),
+      ((2, false, false, 100, meshN), (DFG Monomorphic, "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}
 
@@ -387,14 +387,14 @@
    generate_isabelle_info = false,
    good_slices =
      (* FUDGE *)
-     K [((2, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
-      ((2, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)),
-      ((2, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((2, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
-      ((2, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((2, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)),
-      ((2, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)),
-      ((2, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))],
+     K [((2, false, false, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
+      ((2, false, false, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)),
+      ((2, false, false, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
+      ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
+      ((2, false, false, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
+      ((2, false, false, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)),
+      ((2, false, false, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)),
+      ((2, false, false, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))],
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
@@ -419,21 +419,21 @@
      prem_role = Hypothesis,
      generate_isabelle_info = true,
      good_slices =
-       K [((1, 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")),  (* sh5_sh1.sh *)
-          ((1, 1024, meshN), (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")),  (* sh8_shallow_sine.sh *)
-          ((1, 256, 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")),  (* sh10_new_c.s3.sh *)
-          ((1, 512, mepoN), (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")),  (* sh10_c_ic.sh *)
-          ((1, 512, 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=lift --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")),  (* sh8_b.comb.sh (modified) *)
-          ((1, 1024, mashN), (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 --avatar=eager --split-only-ground=true")),  (* sh5_add_var_l_av.sh *)
-          ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --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=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")),  (* sh10_e_lift.sh *)
-          ((1, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -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 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")),  (* sh5_shallow_sine.sh *)
-          ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")),  (* sh5_e_short1.sh *)
-          ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")),  (* sh5_32.sh *)
-          ((1, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")),  (* sh5_sh4.sh *)
-          ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")),  (* sh5_lifting2.sh *)
-          ((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")),  (* sh5_noforms.sh *)
-          ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")),  (* sh8_old_zip1.sh *)
-          ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))],  (* sh5_sh.eqenc.sh *)
+       K [((1, false, false, 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")),  (* sh5_sh1.sh *)
+          ((1, false, false, 512, mepoN), (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")),  (* sh10_c_ic.sh *)
+          ((1, false, false, 1024, meshN), (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")),  (* sh8_shallow_sine.sh *)
+          ((1, false, false, 256, 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")),  (* sh10_new_c.s3.sh *)
+          ((1, false, true, 512, 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=lift --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")),  (* sh8_b.comb.sh (modified) *)
+          ((1, false, false, 1024, mashN), (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 --avatar=eager --split-only-ground=true")),  (* sh5_add_var_l_av.sh *)
+          ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --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=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")),  (* sh10_e_lift.sh *)
+          ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -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 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")),  (* sh5_shallow_sine.sh *)
+          ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")),  (* sh5_e_short1.sh *)
+          ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")),  (* sh5_32.sh *)
+          ((1, false, false, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")),  (* sh5_sh4.sh *)
+          ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")),  (* sh5_lifting2.sh *)
+          ((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")),  (* sh5_noforms.sh *)
+          ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")),  (* sh8_old_zip1.sh *)
+          ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))],  (* sh5_sh.eqenc.sh *)
      good_max_mono_iters = default_max_mono_iters,
      good_max_new_mono_instances = default_max_new_mono_instances}
   end
@@ -515,30 +515,30 @@
       (Crashed, "Unrecoverable Segmentation Fault")]
      @ known_szs_status_failures)
     Hypothesis false
-    (K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *))
 
 val remote_agsyhol =
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
-    (K ((1000 (* infinity *), 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
-    (K ((1000 (* infinity *), 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]
-    (K ((1000 (* infinity *), 150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), 150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 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 ((1000 (* infinity *), 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *))
+    (K ((1000 (* infinity *), false, false, 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *))
 
 
 (* Dummy prover *)
@@ -551,7 +551,7 @@
    prem_role = prem_role,
    generate_isabelle_info = false,
    good_slices =
-     K [((2, 256, "mepo"), (format, type_enc,
+     K [((2, false, false, 256, "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}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -53,6 +53,8 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("spy", "false"),
+   ("abduce", "smart"),
+   ("check_consistent", "smart"),
    ("type_enc", "smart"),
    ("strict", "false"),
    ("lam_trans", "smart"),
@@ -84,6 +86,8 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("dont_spy", "spy"),
+   ("dont_abduce", "abduce"),
+   ("dont_check_consistent", "check_consistent"),
    ("non_strict", "strict"),
    ("no_uncurried_aliases", "uncurried_aliases"),
    ("dont_learn", "learn"),
@@ -228,6 +232,16 @@
     val overlord = lookup_bool "overlord"
     val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
+    val check_consistent =
+      if mode = Auto_Try then
+        SOME false
+      else
+        lookup_option lookup_bool "check_consistent"
+    val abduce =
+      if mode = Auto_Try then
+        SOME false
+      else
+        lookup_option lookup_bool "abduce"
     val type_enc =
       if mode = Auto_Try then
         NONE
@@ -261,13 +275,14 @@
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
-     type_enc = type_enc, strict = strict, lam_trans = lam_trans,
-     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
-     induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
-     max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-     max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0,
-     smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout,
-     preplay_timeout = preplay_timeout, expect = expect}
+     abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict,
+     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
+     fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
+     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
+     max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs,
+     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+     minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -18,6 +18,7 @@
      del : (Facts.ref * Token.src list) list,
      only : bool}
 
+  val sledgehammer_goal_as_fact : string
   val no_fact_override : fact_override
 
   val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
@@ -64,6 +65,8 @@
 val max_facts_for_complex_check = 25000
 val max_simps_for_clasimpset = 10000
 
+val sledgehammer_goal_as_fact = "Sledgehammer.goal_as_fact"
+
 val no_fact_override = {add = [], del = [], only = false}
 
 fun needs_quoting keywords s =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -868,7 +868,7 @@
   let
     val problem =
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
-       subgoal_count = 1, factss = [("", facts)], found_proof = K ()}
+       subgoal_count = 1, factss = [("", facts)], found_something = K ()}
     val slice = hd (get_slices ctxt prover)
   in
     get_minimizing_prover ctxt MaSh (K ()) prover params problem slice

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -29,6 +29,8 @@
      overlord : bool,
      spy : bool,
      provers : string list,
+     abduce : bool option,
+     check_consistent : bool option,
      type_enc : string option,
      strict : bool,
      lam_trans : string option,
@@ -61,7 +63,7 @@
      subgoal : int,
      subgoal_count : int,
      factss : (string * fact list) list,
-     found_proof : string -> unit}
+     found_something : string -> unit}
 
   datatype prover_slice_extra =
     ATP_Slice of atp_slice
@@ -134,6 +136,8 @@
    overlord : bool,
    spy : bool,
    provers : string list,
+   abduce : bool option,
+   check_consistent : bool option,
    type_enc : string option,
    strict : bool,
    lam_trans : string option,
@@ -160,8 +164,8 @@
   YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
 
 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
-    induction_rules = Exclude ?
-      filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
+  induction_rules = Exclude ?
+    filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
 
 fun slice_timeout slice_size slices timeout =
   let
@@ -178,7 +182,7 @@
    subgoal : int,
    subgoal_count : int,
    factss : (string * fact list) list,
-   found_proof : string -> unit}
+   found_something : string -> unit}
 
 datatype prover_slice_extra =
   ATP_Slice of atp_slice
@@ -234,9 +238,14 @@
     SOME facts => facts
   | NONE => snd (hd factss))
 
-fun facts_of_basic_slice (_, num_facts, fact_filter) factss =
-  facts_of_filter fact_filter factss
-  |> take num_facts
+fun facts_of_basic_slice (_, _, _, num_facts, fact_filter) factss =
+  let
+    val facts = facts_of_filter fact_filter factss
+    val (goal_facts, nongoal_facts) =
+      List.partition (equal sledgehammer_goal_as_fact o fst o fst) facts
+  in
+    goal_facts @ take num_facts nongoal_facts
+  end
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -104,10 +104,10 @@
 fun run_atp mode name
     ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs,
       compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params)
-    ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
+    ({comment, state, goal, subgoal, subgoal_count, factss, found_something} : prover_problem)
     slice =
   let
-    val (basic_slice as (slice_size, _, _),
+    val (basic_slice as (slice_size, _, _, _, _),
         ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) =
       slice
     val facts = facts_of_basic_slice basic_slice factss
@@ -247,7 +247,7 @@
               in
                 if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
               end
-            | NONE => (found_proof name; NONE))
+            | NONE => (found_something name; NONE))
           | _ => outcome)
       in
         (atp_problem_data,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -83,7 +83,8 @@
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, induction_rules, ...} : params)
-    slice silent (prover : prover) timeout i n state goal facts =
+    (slice as ((_, abduce, check_consistent, _, _), _)) silent (prover : prover) timeout i n state
+    goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
       (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -91,9 +92,9 @@
     val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
-       type_enc = type_enc, strict = strict, lam_trans = lam_trans,
-       uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
-       induction_rules = induction_rules, max_facts = SOME (length facts),
+       type_enc = type_enc, abduce = SOME abduce, check_consistent = SOME check_consistent,
+       strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
+       fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
        isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
@@ -101,7 +102,7 @@
        expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)], found_proof = K ()}
+       factss = [("", facts)], found_something = K ()}
     val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
         message} =
       prover params problem slice
@@ -117,7 +118,7 @@
       (case outcome of
         SOME failure => string_of_atp_failure failure
       | NONE =>
-        "Found proof" ^
+        "Found " ^ (if check_consistent then "inconsistency" else "proof") ^
          (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
          " (" ^ string_of_time run_time ^ ")"));
     result

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -120,10 +120,10 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0,
       smt_proofs, minimize, preplay_timeout, ...})
-    ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
+    ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem)
     slice =
   let
-    val (basic_slice as (slice_size, _, _), SMT_Slice options) = slice
+    val (basic_slice as (slice_size, _, _, _, _), SMT_Slice options) = slice
     val facts = facts_of_basic_slice basic_slice factss
     val ctxt = Proof.context_of state
 
@@ -139,7 +139,7 @@
       (case outcome of
         NONE =>
         let
-          val _ = found_proof name;
+          val _ = found_something name;
           val preferred =
             if smt_proofs then
               SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -33,7 +33,7 @@
     val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params
     val name = hd provers
     val prover = get_prover ctxt mode name
-    val default_max_facts = #2 (fst (hd (get_slices ctxt name)))
+    val default_max_facts = #4 (fst (hd (get_slices ctxt name)))
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val keywords = Thy_Header.get_keywords' ctxt
     val css_table = clasimpset_rule_table_of ctxt
@@ -45,7 +45,7 @@
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)], found_proof = K ()}
+       factss = [("", facts)], found_something = K ()}
     val slice = hd (get_slices ctxt name)
   in
     (case prover params problem slice of