src/HOL/Tools/ATP/atp_systems.ML

        -> term_order * (unit -> (string * int) list)
           * (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
      prem_role : formula_role,
-     best_slices :
-       Proof.context -> (real * (bool * (slice_spec * string))) list,
+     best_slices : Proof.context -> (real * (slice_spec * string)) list,
      best_max_mono_iters : int,
      best_max_new_mono_instances : int}
 
   val default_max_mono_iters : int
   val default_max_new_mono_instances : int

      -> term_order * (unit -> (string * int) list)
         * (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
    prem_role : formula_role,
-   best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list,
+   best_slices : Proof.context -> (real * (slice_spec * string)) list,
    best_max_mono_iters : int,
    best_max_new_mono_instances : int}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" component gives the faction of the
-   time available given to the slice and should add up to 1.0. The first "bool"
-   component indicates whether the slice's strategy is complete; the "int", the
-   preferred number of facts to pass; the first "string", the preferred type
-   system (which should be sound or quasi-sound); the second "string", the
-   preferred lambda translation scheme; the second "bool", whether uncurried
-   aliased should be generated; the third "string", extra information to
-   the prover (e.g., SOS or no SOS).
+   time available given to the slice and should add up to 1.0. The "int"
+   component indicates the preferred number of facts to pass; the first
+   "string", the preferred type system (which should be sound or quasi-sound);
+   the second "string", the preferred lambda translation scheme; the "bool",
+   whether uncurried aliased should be generated; the third "string", extra
+   information to the prover (e.g., SOS or no SOS).
 
    The last slice should be the most "normal" one, because it will get all the
    time available if the other slices fail early and also because it is used if
    slicing is disabled (e.g., by the minimizer). *)
 

       (TimedOut, ": Timeout"),
       (GaveUp, ": Unknown")],
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))],
+     [(1.0, ((100, alt_ergo_tff1, "poly_native", liftingN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
 

    prem_role = Conjecture,
    best_slices = fn ctxt =>
      let val heuristic = effective_e_selection_heuristic ctxt in
        (* FUDGE *)
        if heuristic = e_smartN then
-         [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),
-          (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))),
-          (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
+         [(0.333, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN)),
+          (0.334, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN)),
+          (0.333, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN))]
        else
-         [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))]
+         [(1.0, ((500, FOF, "mono_tags??", combsN, false), heuristic))]
      end,
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val e = (eN, fn () => e_config)

    proof_delims = tstp_proof_delims,
    known_failures = #known_failures e_config,
    prem_role = Conjecture,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((1000, FOF, "mono_tags??", combsN, false), "")))],
+     K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val e_males = (e_malesN, fn () => e_males_config)
 

      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((150, FOF, "mono_guards??", liftingN, false), "")))],
+     K [(1.0, ((150, FOF, "mono_guards??", liftingN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val iprover = (iproverN, fn () => iprover_config)
 

       (GaveUp, "No.of.Axioms")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
+     K [(1.0, ((40, leo2_thf0, "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 div 2 (* FUDGE *)}
 
 val leo2 = (leo2N, fn () => leo2_config)
 

      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
+     K [(1.0, ((60, satallax_thf0, "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 div 2 (* FUDGE *)}
 
 val satallax = (satallaxN, fn () => satallax_config)
 

       (InternalError, "Please report this error")] @
       known_perl_failures,
    prem_role = Conjecture,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.1667, (false, ((150, DFG Monomorphic, "mono_native", combsN, true), ""))),
-      (0.1667, (false, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS))),
-      (0.1666, (false, ((50, DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0))),
-      (0.1000, (false, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0))),
-      (0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))),
-      (0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
-      (0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))),
-      (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), "")))],
+     [(0.1667, ((150, DFG Monomorphic, "mono_native", combsN, true), "")),
+      (0.1667, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
+      (0.1666, ((50, DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0)),
+      (0.1000, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
+      (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
+      (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
+      (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
+      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val spass = (spassN, fn () => spass_config)
 

      known_szs_status_failures,
    prem_role = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
-        [(0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
-         (0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
-         (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]
+        [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
+         (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
+         (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
       else
-        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
-         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
-         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))])
+        [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
+         (0.333, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
+         (0.334, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I),
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 

    proof_delims = [("\ncore(", ").")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
-        (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
-        (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
-        (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))],
+     K [(0.5, ((250, z3_tff0, "mono_native", combsN, false), "")),
+        (0.25, ((125, z3_tff0, "mono_native", combsN, false), "")),
+        (0.125, ((62, z3_tff0, "mono_native", combsN, false), "")),
+        (0.125, ((31, z3_tff0, "mono_native", combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
 

    arguments = K (K (K (K (K "")))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
-     K [(1.0, (false, ((200, format, type_enc,
-                        if is_format_higher_order format then keep_lamsN
-                        else combsN, false), "")))],
+     K [(1.0, ((200, format, type_enc,
+                if is_format_higher_order format then keep_lamsN
+                else combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_thf_format =
   THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)

        "-s " ^ the_system system_name system_versions ^ " " ^
        "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    prem_role = prem_role,
-   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))],
+   best_slices = fn ctxt => [(1.0, best_slice ctxt)],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 fun remotify_config system_name system_versions best_slice
         ({proof_delims, known_failures, prem_role, ...} : atp_config)