diff --git a/src/HOL/Tools/ATP/atp_proof.ML b/src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML
+++ b/src/HOL/Tools/ATP/atp_proof.ML
@@ -1,721 +1,720 @@
 (*  Title:      HOL/Tools/ATP/atp_proof.ML
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Mathias Fleury, ENS Rennes
 
 Abstract representation of ATP proofs and TSTP/SPASS syntax.
 *)
 
 signature ATP_PROOF =
 sig
   type 'a atp_type = 'a ATP_Problem.atp_type
   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
   type atp_formula_role = ATP_Problem.atp_formula_role
   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
   type 'a atp_problem = 'a ATP_Problem.atp_problem
 
   exception UNRECOGNIZED_ATP_PROOF of unit
 
   datatype atp_failure =
     MaybeUnprovable |
     Unprovable |
     GaveUp |
     ProofMissing |
     ProofIncomplete |
     ProofUnparsable |
     UnsoundProof of bool * string list |
     TimedOut |
     Inappropriate |
     OutOfResources |
     MalformedInput |
     MalformedOutput |
     Interrupted |
     Crashed |
     InternalError |
     UnknownError of string
 
   type atp_step_name = string * string list
   type ('a, 'b) atp_step =
     atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
   type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
 
   val agsyholN : string
   val alt_ergoN : string
   val eN : string
   val iproverN : string
   val leo2N : string
   val leo3N : string
   val satallaxN : string
   val spassN : string
   val vampireN : string
   val waldmeisterN : string
   val z3_tptpN : string
   val zipperpositionN : string
   val remote_prefix : string
   val dummy_fofN : string
   val dummy_tfxN : string
   val dummy_thfN : string
 
   val agsyhol_core_rule : string
   val spass_input_rule : string
   val spass_pre_skolemize_rule : string
   val spass_skolemize_rule : string
   val z3_tptp_core_rule : string
 
   val short_output : bool -> string -> string
   val string_of_atp_failure : atp_failure -> string
   val extract_important_message : string -> string
   val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option
   val extract_tstplike_proof_and_outcome :
     bool -> (string * string) list -> (atp_failure * string) list -> string
     -> string * atp_failure option
   val is_same_atp_step : atp_step_name -> atp_step_name -> bool
   val scan_general_id : string list -> string * string list
   val parse_fol_formula : string list ->
     (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
   val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
   val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
   val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
 
   val skip_term : string list -> string * string list
   val parse_hol_formula : string list ->
     ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula *
     string list
   val dummy_atype : string ATP_Problem.atp_type
   val role_of_tptp_string : string -> ATP_Problem.atp_formula_role
   val parse_line : string -> ('a * string ATP_Problem.atp_problem_line list) list ->
     string list -> ((string * string list) * ATP_Problem.atp_formula_role *
     (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
       'c) ATP_Problem.atp_formula
     * string * (string * 'd list) list) list * string list
   val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
     ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
   val vampire_step_name_ord : (string * 'a) ord
   val core_of_agsyhol_proof :  string -> string list option
   val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string
 
   val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof
 end;
 
 structure ATP_Proof : ATP_PROOF =
 struct
 
 open ATP_Util
 open ATP_Problem
 
 val agsyholN = "agsyhol"
 val alt_ergoN = "alt_ergo"
 val eN = "e"
 val iproverN = "iprover"
 val leo2N = "leo2"
 val leo3N = "leo3"
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
 val waldmeisterN = "waldmeister"
 val z3_tptpN = "z3_tptp"
 val zipperpositionN = "zipperposition"
 val remote_prefix = "remote_"
 val dummy_fofN = "dummy_fof"
 val dummy_tfxN = "dummy_tfx"
 val dummy_thfN = "dummy_thf"
 
 val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
 val spass_input_rule = "Inp"
 val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
 val spass_skolemize_rule = "__Sko" (* arbitrary *)
 val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
 
 exception UNRECOGNIZED_ATP_PROOF of unit
 
 datatype atp_failure =
   MaybeUnprovable |
   Unprovable |
   GaveUp |
   ProofMissing |
   ProofIncomplete |
   ProofUnparsable |
   UnsoundProof of bool * string list |
   TimedOut |
   Inappropriate |
   OutOfResources |
   MalformedInput |
   MalformedOutput |
   Interrupted |
   Crashed |
   InternalError |
   UnknownError of string
 
 fun short_output verbose output =
   if verbose then
     if output = "" then "No details available" else elide_string 1000 output
   else
     ""
 
 fun from_lemmas [] = ""
   | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
-fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
-  | string_of_atp_failure Unprovable = "The generated problem is unprovable"
-  | string_of_atp_failure GaveUp = "The prover gave up"
+fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
+  | string_of_atp_failure Unprovable = "Unprovable problem"
+  | string_of_atp_failure GaveUp = "Gave up"
   | string_of_atp_failure ProofMissing =
-    "The prover claims the conjecture is a theorem but did not provide a proof"
+    "Claims the conjecture is a theorem but did not provide a proof"
   | string_of_atp_failure ProofIncomplete =
-    "The prover claims the conjecture is a theorem but provided an incomplete proof"
+    "Claims the conjecture is a theorem but provided an incomplete proof"
   | string_of_atp_failure ProofUnparsable =
-    "The prover claims the conjecture is a theorem but provided an unparsable proof"
+    "Claims the conjecture is a theorem but provided an unparsable proof"
   | string_of_atp_failure (UnsoundProof (false, ss)) =
-    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
-    "; specify a sound type encoding or omit the \"type_enc\" option"
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
+    ", probably due to the use of an unsound type encoding"
   | string_of_atp_failure (UnsoundProof (true, ss)) =
-    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
     ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
   | string_of_atp_failure TimedOut = "Timed out"
-  | string_of_atp_failure Inappropriate =
-    "The generated problem lies outside the prover's scope"
-  | string_of_atp_failure OutOfResources = "The prover ran out of resources"
-  | string_of_atp_failure MalformedInput = "The generated problem is malformed"
-  | string_of_atp_failure MalformedOutput = "The prover output is malformed"
-  | string_of_atp_failure Interrupted = "The prover was interrupted"
-  | string_of_atp_failure Crashed = "The prover crashed"
-  | string_of_atp_failure InternalError = "An internal prover error occurred"
+  | string_of_atp_failure Inappropriate = "Problem outside the prover's scope"
+  | string_of_atp_failure OutOfResources = "Ran out of resources"
+  | string_of_atp_failure MalformedInput = "Malformed problem"
+  | string_of_atp_failure MalformedOutput = "Malformed output"
+  | string_of_atp_failure Interrupted = "Interrupted"
+  | string_of_atp_failure Crashed = "Crashed"
+  | string_of_atp_failure InternalError = "Internal prover error"
   | string_of_atp_failure (UnknownError s) =
-    "A prover error occurred" ^
+    "Prover error" ^
     (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s)
 
 fun extract_delimited (begin_delim, end_delim) output =
   (case first_field begin_delim output of
     SOME (_, tail) =>
     (case first_field "\n" tail of
       SOME (_, tail') =>
       if end_delim = "" then
         tail'
       else
         (case first_field end_delim tail' of
           SOME (body, _) => body
         | NONE => "")
     | NONE => "")
   | NONE => "")
 
 val tstp_important_message_delims =
   ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
 
 fun extract_important_message output =
   (case extract_delimited tstp_important_message_delims output of
     "" => ""
   | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
            |> map (perhaps (try (unprefix "%")))
            |> map (perhaps (try (unprefix " ")))
            |> space_implode "\n " |> quote)
 
 (* Splits by the first possible of a list of delimiters. *)
 fun extract_tstplike_proof delims output =
   (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
     (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output
   | _ => "")
 
 fun extract_known_atp_failure known_failures output =
   known_failures
   |> find_first (fn (_, pattern) => String.isSubstring pattern output)
   |> Option.map fst
 
 fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output =
   let
     val known_atp_failure = extract_known_atp_failure known_failures output
     val tstplike_proof = extract_tstplike_proof proof_delims output
   in
     (case (tstplike_proof, known_atp_failure) of
       (_, SOME ProofIncomplete) => ("", NONE)
     | (_, SOME ProofUnparsable) => ("", NONE)
     | ("", SOME ProofMissing) => ("", NONE)
     | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
     | res as ("", _) => res
     | (tstplike_proof, _) => (tstplike_proof, NONE))
   end
 
 type atp_step_name = string * string list
 
 fun is_same_atp_step (s1, _) (s2, _) = s1 = s2
 
 val vampire_fact_prefix = "f"
 
 fun vampire_step_name_ord p =
   let val q = apply2 fst p in
     (* The "unprefix" part is to cope with Vampire's output. *)
     (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of
       (SOME i, SOME j) => int_ord (i, j)
     | _ => raise Fail "not Vampire")
   end
 
 type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
 type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
 
 (**** PARSING OF TSTP FORMAT ****)
 
 (* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting
    with "$" and possibly with "!" in them (for "z3_tptp"). *)
 val scan_general_id =
   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode))
     -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) ""
     >> op ^
 
 fun skip_term x =
   let
     fun skip _ accum [] = (accum, [])
       | skip n accum (ss as s :: ss') =
         if (s = "," orelse s = ".") andalso n = 0 then
           (accum, ss)
         else if member (op =) [")", "]"] s then
           if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
         else if member (op =) ["(", "["] s then
           skip (n + 1) (s :: accum) ss'
         else
           skip n (s :: accum) ss'
   in
     (skip 0 [] #>> (rev #> implode)) x
   end
 and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
 
 datatype source =
   File_Source of string * string option |
   Inference_Source of string * string list |
   Introduced_Source of string
 
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_atype = AType (("", []), [])
 
 (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
 fun parse_dependency x =
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
 and parse_dependencies x =
   (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency)
    >> (filter_out (curry (op =) "theory"))) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id
      --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x
 and parse_inference_source x =
   (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
    --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
    -- parse_dependencies --| $$ "]" --| $$ ")") x
 and parse_introduced_source x =
   (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id
    --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x
 and parse_source x =
   (parse_file_source >> File_Source >> SOME
    || parse_inference_source >> Inference_Source >> SOME
    || parse_introduced_source >> Introduced_Source >> SOME
    || scan_general_id >> (fn s => SOME (Inference_Source ("", [s]))) (* for E *)
    || skip_term >> K NONE) x
 
 fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
 
 fun parse_class x = scan_general_id x
 and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x
 
 fun parse_type x =
   (($$ "(" |-- parse_type --| $$ ")"
     || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type
        >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *))
     || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
         -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
        >> AType)
    -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
   >> (fn (a, NONE) => a
        | (a, SOME (bin_op, b)) =>
          if bin_op = tptp_app then
            (case a of
              AType (s_clss, tys) => AType (s_clss, tys @ [b])
            | _ => raise UNRECOGNIZED_ATP_PROOF ())
          else if bin_op = tptp_fun_type then
            AFun (a, b)
          else if bin_op = tptp_product_type then
            AType ((tptp_product_type, []), [a, b])
          else
            raise Fail "impossible case")) x
 and parse_types x =
   (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
 
 (* We currently half ignore types. *)
 fun parse_fol_optional_type_signature x =
   (Scan.option ($$ tptp_has_type |-- parse_type)
    >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some
         | res => res)) x
 and parse_fol_arg x =
   ($$ "(" |-- parse_fol_term --| $$ ")" --| parse_fol_optional_type_signature
    || scan_general_id -- parse_fol_optional_type_signature
        -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
        -- Scan.optional ($$ "(" |-- parse_fol_terms --| $$ ")") []
      >> (fn (((s, ty_opt), tyargs), args) =>
        if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then
          ATerm ((s, the_list ty_opt), [])
        else
          ATerm ((s, tyargs), args))) x
 and parse_fol_term x =
   (parse_fol_arg -- Scan.repeat ($$ tptp_app |-- parse_fol_arg)
    --| parse_fol_optional_type_signature >> list_app) x
 and parse_fol_terms x = (parse_fol_term ::: Scan.repeat ($$ "," |-- parse_fol_term)) x
 
 fun parse_fol_atom x =
   (parse_fol_term --
     Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_fol_term)
    >> (fn (u1, NONE) => AAtom u1
         | (u1, SOME (neg, u2)) =>
           AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
 
 (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *)
 fun parse_fol_literal x =
   ((Scan.repeat ($$ tptp_not) >> length)
       -- ($$ "(" |-- parse_fol_formula --| $$ ")"
           || parse_fol_quantified_formula
           || parse_fol_atom)
       >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
 and parse_fol_formula x =
   (parse_fol_literal
    -- Scan.option ((Scan.this_string tptp_implies
                     || Scan.this_string tptp_iff
                     || Scan.this_string tptp_not_iff
                     || Scan.this_string tptp_if
                     || $$ tptp_or
                     || $$ tptp_and) -- parse_fol_formula)
    >> (fn (phi1, NONE) => phi1
         | (phi1, SOME (c, phi2)) =>
           if c = tptp_implies then mk_aconn AImplies phi1 phi2
           else if c = tptp_iff then mk_aconn AIff phi1 phi2
           else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2)
           else if c = tptp_if then mk_aconn AImplies phi2 phi1
           else if c = tptp_or then mk_aconn AOr phi1 phi2
           else if c = tptp_and then mk_aconn AAnd phi1 phi2
           else raise Fail ("impossible connective " ^ quote c))) x
 and parse_fol_quantified_formula x =
   (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
    --| $$ "[" -- parse_fol_terms --| $$ "]" --| $$ ":" -- parse_fol_literal
    >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) NONE
 
 val waldmeister_conjecture_name = "conjecture_1"
 
 fun is_same_term subst tm1 tm2 =
   let
     fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2))
           (SOME subst) =
         if typ1 <> typ2 andalso length args1 = length args2 then NONE
         else
           let val ls = length subst in
             SOME ((var1, var2) :: subst)
             |> do_term_pair body1 body2
             |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst)
                  | NONE => NONE)
             |> (if length args1 = length args2
               then fold2 do_term_pair args1 args2
               else K NONE)
           end
       | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) =
         (case apply2 is_tptp_variable (s1, s2) of
           (true, true) =>
           (case AList.lookup (op =) subst s1 of
             SOME s2' => if s2' = s2 then SOME subst else NONE
           | NONE =>
             if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst)
             else NONE)
         | (false, false) =>
           if s1 = s2 then
             SOME subst
           else
             NONE
         | _ => NONE) |> (if length args1 = length args2
                        then fold2 do_term_pair args1 args2
                        else K NONE)
       | do_term_pair _ _ _ = NONE
   in
     SOME subst |> do_term_pair tm1 tm2 |> is_some
   end
 
 fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
     q1 = q2 andalso length xs1 = length xs2 andalso
     is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
   | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
     c1 = c2 andalso length phis1 = length phis2 andalso
     forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
   | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst tm1 tm2 orelse
     (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2)
   | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
   | is_same_formula _ _ _ _ = false
 
 fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) =
     if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
   | matching_formula_line_identifier _ _ = NONE
 
 fun find_formula_in_problem phi =
   maps snd
   #> map_filter (matching_formula_line_identifier phi)
   #> try (single o hd)
   #> the_default []
 
 fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms))
   | commute_eq _ = raise Fail "expected equation"
 
 fun role_of_tptp_string "axiom" = Axiom
   | role_of_tptp_string "definition" = Definition
   | role_of_tptp_string "lemma" = Lemma
   | role_of_tptp_string "hypothesis" = Hypothesis
   | role_of_tptp_string "conjecture" = Conjecture
   | role_of_tptp_string "negated_conjecture" = Negated_Conjecture
   | role_of_tptp_string "plain" = Plain
   | role_of_tptp_string "type" = Type_Role
   | role_of_tptp_string _ = Unknown
 
 val tptp_binary_ops =
   [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and,
    tptp_not_or, tptp_not_iff, tptp_app]
 
 fun parse_one_in_list xs =
   foldl1 (op ||) (map Scan.this_string xs)
 
 fun parse_binary_op x =
   (parse_one_in_list tptp_binary_ops
    >> (fn c => if c = tptp_equal then "equal" else c)) x
 
 val parse_fol_quantifier =
    parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the]
 
 val parse_hol_quantifier =
    parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the]
 
 fun mk_ho_of_fo_quant q =
   if q = tptp_forall then tptp_ho_forall
   else if q = tptp_exists then tptp_ho_exists
   else if q = tptp_hilbert_choice then tptp_hilbert_choice
   else if q = tptp_hilbert_the then tptp_hilbert_the
   else raise Fail ("unrecognized quantification: " ^ q)
 
 fun remove_hol_app (ATerm ((s, ty), arg)) =
     if s = tptp_app then
       (case arg of
         ATerm ((s, ty), arg) :: t => remove_hol_app (ATerm ((s, ty), map remove_hol_app arg @ t))
       | [AAbs ((var, tvar), phi), t] =>
         remove_hol_app (AAbs ((var, tvar), map remove_hol_app phi @ [t])))
     else
       ATerm ((s, ty), map remove_hol_app arg)
   | remove_hol_app (AAbs (((s, ty), arg), t)) = AAbs (((s, ty), remove_hol_app arg), t)
 
 fun parse_hol_typed_var x =
   (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
      --| Scan.option (Scan.this_string ","))
    || $$ "(" |-- parse_hol_typed_var --| $$ ")") x
 
 fun parse_simple_hol_term x =
   (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term
       >> (fn ((q, ys), t) =>
           fold_rev
             (fn (var, ty) => fn r =>
                 AAbs (((var, the_default dummy_atype ty), r), [])
                 |> (if tptp_lambda <> q then
                       mk_app (q |> mk_ho_of_fo_quant
                                 |> mk_simple_aterm)
                     else I))
             ys t)
   || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not)
   || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
     >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
   || parse_hol_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_hol_term --| $$ ")"
   || parse_binary_op >> mk_simple_aterm) x
 and parse_hol_term x =
   (parse_simple_hol_term -- Scan.repeat (parse_binary_op -- parse_simple_hol_term)
     >> (fn (t1, c_ti_s) =>
         fold (fn (c, ti) => fn left =>
             if c = tptp_app then mk_app left ti else mk_apps (mk_simple_aterm c) [left, ti])
           c_ti_s t1)) x
 
 fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x
 
 fun parse_tstp_hol_line problem =
   (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ ","
   -- Symbol.scan_ascii_id --| $$ "," -- (parse_hol_formula || skip_term >> K dummy_phi)
      -- parse_tstp_extra_arguments --| $$ ")"
   --| $$ "."
   >> (fn (((num, role), phi), src) =>
       let
         val role' = role_of_tptp_string role
         val ((name, phi), rule, deps) =
           (case src of
             SOME (File_Source (_, SOME s)) =>
             if role' = Definition then
               (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
             else
               (((num, [s]), phi), "", [])
           | SOME (Inference_Source (rule, deps)) => (((num, []), phi), rule, deps)
           | SOME (Introduced_Source rule) => (((num, []), phi), rule, [])
           | _ => (((num, [num]), phi), "", []))
       in
         [(name, role', phi, rule, map (rpair []) deps)]
       end)
 
 fun parse_tstp_fol_line problem =
   ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
     |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
     -- (parse_fol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
     --| $$ ")" --| $$ "."
    >> (fn (((num, role0), phi), src) =>
           let
             val role = role_of_tptp_string role0
             val ((name, phi), role', rule, deps) =
               (* Waldmeister isn't exactly helping. *)
               (case src of
                 SOME (File_Source (_, SOME s)) =>
                 (if s = waldmeister_conjecture_name then
                    (case find_formula_in_problem (mk_anot phi) problem of
                      (* Waldmeister hack: Get the original orientation of the equation to avoid
                         confusing Isar. *)
                      [(s, phi')] =>
                      ((num, [s]),
                       phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)
                    | _ => ((num, []), phi))
                  else
                    ((num, [s]), phi),
                  role, "", [])
               | SOME (File_Source _) =>
                 (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
               | SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps)
               | SOME (Introduced_Source rule) => (((num, []), phi), Lemma, rule, [])
               | _ => (((num, [num]), phi), role, "", []))
 
             fun mk_step () = (name, role', phi, rule, map (rpair []) deps)
           in
             [(case role' of
                Definition =>
                (case phi of
                  AAtom (ATerm (("equal", _), _)) =>
                   (* Vampire's equality proxy axiom *)
                   (name, Definition, phi, rule, map (rpair []) deps)
                | _ => mk_step ())
              | _ => mk_step ())]
           end)
 
 fun parse_tstp_line problem = parse_tstp_fol_line problem || parse_tstp_hol_line problem
 
 (**** PARSING OF SPASS OUTPUT ****)
 
 (* SPASS returns clause references of the form "x.y". We ignore "y". *)
 val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
 
 val parse_spass_annotations =
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
 
 (* We ignore the stars and the pluses that follow literals. *)
 fun parse_decorated_atom x =
   (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
 
 fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
   | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits)
 
 fun parse_horn_clause x =
   (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
      -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
      -- Scan.repeat parse_decorated_atom
    >> (mk_horn o apfst (op @))) x
 
 val parse_spass_debug =
   Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")")
 
 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms> .
            derived from formulae <ident>* *)
 fun parse_spass_line x =
   (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":"
      -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
    >> (fn ((((num, rule), deps), u), names) =>
           [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
 
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
 (* Syntax: SZS core <name> ... <name> *)
 fun parse_z3_tptp_core_line x =
   (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
    >> map (core_inference z3_tptp_core_rule)) x
 
 fun parse_line local_name problem =
   (* Satallax is handled separately, in "atp_satallax.ML". *)
   if local_name = spassN then parse_spass_line
   else if local_name = z3_tptpN then parse_z3_tptp_core_line
   else parse_tstp_line problem
 
 fun core_of_agsyhol_proof s =
   (case split_lines s of
     "The transformed problem consists of the following conjectures:" :: conj ::
     _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
   | _ => NONE)
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
     (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
     clean_up_dependencies (name :: seen) steps
 
 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
 
 fun map_term_names_in_atp_proof f =
   let
     fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys)
       | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
       | map_type (APi (ss, ty)) = APi (map f ss, map_type ty)
 
     fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts)
       | map_term (AAbs (((s, ty), tm), args)) =
         AAbs (((f s, map_type ty), map_term tm), map map_term args)
 
     fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi)
       | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis)
       | map_formula (AAtom t) = AAtom (map_term t)
 
     fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps)
   in
     map map_step
   end
 
 fun nasty_name pool s = Symtab.lookup pool s |> the_default s
 
 fun nasty_atp_proof pool =
   not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
 
 fun string_of_list f xs = enclose "[" "]" (commas (map f xs))
 
 fun string_of_atp_step_name (s, ss) = "(" ^ s ^ ", " ^ string_of_list I ss ^ ")"
 
 fun string_of_atp_step f g (name, role, x, y, names) =
   let
     val name' = string_of_atp_step_name name
     val role' = ATP_Problem.tptp_string_of_role role
     val x' = f x
     val y' = g y
     val names' = string_of_list string_of_atp_step_name names
   in
     "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")"
   end
 
 fun parse_proof local_name problem =
   strip_spaces_except_between_idents
   #> raw_explode
   #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
        (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem))))
   #> fst
 
 fun atp_proof_of_tstplike_proof _ _ "" = []
   | atp_proof_of_tstplike_proof local_prover problem tstp =
     (case core_of_agsyhol_proof tstp of
       SOME facts => facts |> map (core_inference agsyhol_core_rule)
     | NONE =>
       tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
       |> parse_proof local_prover problem
       |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))))
 
 end;
diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
@@ -1,737 +1,739 @@
 (*  Title:      HOL/Tools/ATP/atp_systems.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Setup for supported ATPs.
 *)
 
 signature SLEDGEHAMMER_ATP_SYSTEMS =
 sig
   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 slice_spec = (int * string) * atp_format * string * string * bool
   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 -> (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
   val force_sos : bool Config.T
   val term_order : string Config.T
   val e_smartN : string
   val e_autoN : string
   val e_fun_weightN : string
   val e_sym_offset_weightN : string
   val e_selection_heuristic : string Config.T
   val e_default_fun_weight : real Config.T
   val e_fun_weight_base : real Config.T
   val e_fun_weight_span : real Config.T
   val e_default_sym_offs_weight : real Config.T
   val e_sym_offs_weight_base : real Config.T
   val e_sym_offs_weight_span : real Config.T
   val spass_H1SOS : string
   val spass_H2 : string
   val spass_H2LR0LT0 : string
   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
   val is_vampire_noncommercial_license_accepted : unit -> bool option
   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 -> slice_spec * string) ->
     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 refresh_systems_on_tptp : unit -> unit
   val effective_term_order : Proof.context -> string -> term_order
 end;
 
 structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS =
 struct
 
 open ATP_Problem
 open ATP_Proof
 open ATP_Problem_Generate
 
 
 (* ATP configuration *)
 
 val default_max_mono_iters = 3 (* FUDGE *)
 val default_max_new_mono_instances = 100 (* FUDGE *)
 
 type slice_spec = (int * string) * atp_format * string * string * bool
 
 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 -> (real * (slice_spec * string)) list,
    best_max_mono_iters : int,
    best_max_new_mono_instances : int}
 
 (* "best_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)
 
    where
 
      time_frac = faction of the time available given to the slice (which should
        add up to 1.0)
 
      extra = 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). *)
 
 val mepoN = "mepo"
 val mashN = "mash"
 val meshN = "mesh"
 
 val tstp_proof_delims =
   [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"),
    ("% SZS output start Refutation", "% SZS output end Refutation"),
    ("% SZS output start Proof", "% SZS output end Proof")]
 
 fun known_szs_failures wrap =
   [(Unprovable, wrap "CounterSatisfiable"),
    (Unprovable, wrap "Satisfiable"),
    (GaveUp, wrap "GaveUp"),
    (GaveUp, wrap "Unknown"),
    (GaveUp, wrap "Incomplete"),
    (ProofMissing, wrap "Theorem"),
    (ProofMissing, wrap "Unsatisfiable"),
    (TimedOut, wrap "Timeout"),
    (Inappropriate, wrap "Inappropriate"),
    (OutOfResources, wrap "ResourceOut"),
    (OutOfResources, wrap "MemoryOut"),
    (Interrupted, wrap "Forced"),
    (Interrupted, wrap "User")]
 
 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
 val known_says_failures = known_szs_failures (prefix " says ")
 
 structure Data = Theory_Data
 (
   type T = ((unit -> atp_config) * stamp) Symtab.table
   val empty = Symtab.empty
   val extend = I
   fun merge data : T =
     Symtab.merge (eq_snd (op =)) data
     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
 )
 
 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
 
 val sosN = "sos"
 val no_sosN = "no_sos"
 
 val force_sos = Attrib.setup_config_bool \<^binding>\<open>atp_force_sos\<close> (K false)
 
 val smartN = "smart"
 (* val kboN = "kbo" *)
 val lpoN = "lpo"
 val xweightsN = "_weights"
 val xprecN = "_prec"
 val xsimpN = "_simp" (* SPASS-specific *)
 
 (* Possible values for "atp_term_order":
    "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
 val term_order =
   Attrib.setup_config_string \<^binding>\<open>atp_term_order\<close> (K smartN)
 
 
 (* agsyHOL *)
 
 val agsyhol_config : atp_config =
   {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
    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 =
      (* FUDGE *)
      K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, 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}
 
 val agsyhol = (agsyholN, fn () => agsyhol_config)
 
 
 (* Alt-Ergo *)
 
 val alt_ergo_config : atp_config =
   {exec = (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
      ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
       " " ^ File.bash_path problem],
    proof_delims = [],
    known_failures =
      [(ProofMissing, ": Valid"),
       (TimedOut, ": Timeout"),
       (GaveUp, ": Unknown")],
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
      [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "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)
 
 
 (* E *)
 
 val e_smartN = "smart"
 val e_autoN = "auto"
 val e_fun_weightN = "fun_weight"
 val e_sym_offset_weightN = "sym_offset_weight"
 
 val e_selection_heuristic =
   Attrib.setup_config_string \<^binding>\<open>atp_e_selection_heuristic\<close> (K e_smartN)
 (* FUDGE *)
 val e_default_fun_weight =
   Attrib.setup_config_real \<^binding>\<open>atp_e_default_fun_weight\<close> (K 20.0)
 val e_fun_weight_base =
   Attrib.setup_config_real \<^binding>\<open>atp_e_fun_weight_base\<close> (K 0.0)
 val e_fun_weight_span =
   Attrib.setup_config_real \<^binding>\<open>atp_e_fun_weight_span\<close> (K 40.0)
 val e_default_sym_offs_weight =
   Attrib.setup_config_real \<^binding>\<open>atp_e_default_sym_offs_weight\<close> (K 1.0)
 val e_sym_offs_weight_base =
   Attrib.setup_config_real \<^binding>\<open>atp_e_sym_offs_weight_base\<close> (K ~20.0)
 val e_sym_offs_weight_span =
   Attrib.setup_config_real \<^binding>\<open>atp_e_sym_offs_weight_span\<close> (K 60.0)
 
 fun e_selection_heuristic_case heuristic fw sow =
   if heuristic = e_fun_weightN then fw
   else if heuristic = e_sym_offset_weightN then sow
   else raise Fail ("unexpected " ^ quote heuristic)
 
 fun scaled_e_selection_weight ctxt heuristic w =
   w * Config.get ctxt (e_selection_heuristic_case heuristic
                            e_fun_weight_span e_sym_offs_weight_span)
   + Config.get ctxt (e_selection_heuristic_case heuristic
                          e_fun_weight_base e_sym_offs_weight_base)
   |> Real.ceil |> signed_string_of_int
 
 fun e_selection_weight_arguments ctxt heuristic sel_weights =
   if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
     (* supplied by Stephan Schulz *)
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
     \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
     e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
     "(SimulateSOS," ^
     (e_selection_heuristic_case heuristic
          e_default_fun_weight e_default_sym_offs_weight
      |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
     ",20,1.5,1.5,1" ^
     (sel_weights ()
      |> map (fn (s, w) => "," ^ s ^ ":" ^
                           scaled_e_selection_weight ctxt heuristic w)
      |> implode) ^
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))' "
   else
     "-xAuto "
 
 val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
 fun e_ord_precedence [_] = ""
   | e_ord_precedence info = info |> map fst |> space_implode "<"
 
 fun e_term_order_info_arguments false false _ = ""
   | e_term_order_info_arguments gen_weights gen_prec ord_info =
     let val ord_info = ord_info () in
       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
     end
 
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        ["--auto-schedule --tstp-in --tstp-out --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^
         e_term_order_info_arguments gen_weights gen_prec ord_info ^
         "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
         " --proof-object=1 " ^
         File.bash_path problem],
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
    known_failures =
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded")] @
      known_szs_status_failures,
    prem_role = Conjecture,
    best_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 (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool", keep_lamsN)
          else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
            (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
          else
            (THF (Without_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher", combsN)
      in
        (* FUDGE *)
        if heuristic = e_smartN then
          [(0.15, (((128, meshN), format, enc, main_lam_trans, false), e_fun_weightN)),
           (0.15, (((128, mashN), format, enc, main_lam_trans, false), e_sym_offset_weightN)),
           (0.15, (((91, mepoN), format, enc, main_lam_trans, false), e_autoN)),
           (0.15, (((1000, meshN), format, "poly_guards??", main_lam_trans, false), e_sym_offset_weightN)),
           (0.15, (((256, mepoN), format, enc, liftingN, false), e_fun_weightN)),
           (0.25, (((64, mashN), format, enc, combsN, false), e_fun_weightN))]
        else
          [(1.0, (((500, ""), format, enc, 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)
 
 
 (* iProver *)
 
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
      ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
       "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
      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)
 
 
 (* LEO-II *)
 
 val leo2_config : atp_config =
   {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
      ["--foatp e --atp e=\"$E_HOME\"/eprover \
       \--atp epclextract=\"$E_HOME\"/epclextract \
       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
       (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
       File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")] @
      known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
      K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, 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}
 
 val leo2 = (leo2N, fn () => leo2_config)
 
 
 (* Leo-III *)
 
 (* Include choice? Disabled now since it's disabled for Satallax as well. *)
 val leo3_config : atp_config =
   {exec = (["LEO3_HOME"], ["leo3"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ =>
      [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
       \-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 =
      (* FUDGE *)
      K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, 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}
 
 val leo3 = (leo3N, fn () => leo3_config)
 
 
 (* Satallax *)
 
 (* Choice is disabled until there is proper reconstruction for it. *)
 val satallax_config : atp_config =
   {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
      [(case getenv "E_HOME" of
         "" => ""
       | home => "-E " ^ home ^ "/eprover ") ^
       "-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 =
      (* FUDGE *)
      K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, 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}
 
 val satallax = (satallaxN, fn () => satallax_config)
 
 
 (* SPASS *)
 
 val spass_H1SOS = "-Heuristic=1 -SOS"
 val spass_H2 = "-Heuristic=2"
 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
 val spass_H2SOS = "-Heuristic=2 -SOS"
 
 val spass_config : atp_config =
   let
     val format = DFG Monomorphic
   in
     {exec = (["SPASS_HOME"], ["SPASS"]),
      arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ =>
        ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
         "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
         |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = [("Here is a proof", "Formulae used in the proof")],
      known_failures =
        [(GaveUp, "SPASS beiseite: Completion found"),
         (TimedOut, "SPASS beiseite: Ran out of time"),
         (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
         (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 _ =>
        (* FUDGE *)
        [(0.1667, (((150, meshN), format, "mono_native", combsN, true), "")),
         (0.1667, (((500, meshN), format, "mono_native", liftingN, true), spass_H2SOS)),
         (0.1666, (((50, meshN), format,  "mono_native", liftingN, true), spass_H2LR0LT0)),
         (0.1000, (((250, meshN), format, "mono_native", combsN, true), spass_H2NuVS0)),
         (0.1000, (((1000, mepoN), format, "mono_native", liftingN, true), spass_H1SOS)),
         (0.1000, (((150, meshN), format, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
         (0.1000, (((300, meshN), format, "mono_native", combsN, true), spass_H2SOS)),
         (0.1000, (((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}
   end
 
 val spass = (spassN, fn () => spass_config)
 
 
 (* Vampire *)
 
 fun is_vampire_noncommercial_license_accepted () =
   let
     val flag = Options.default_string \<^system_option>\<open>vampire_noncommercial\<close>
       |> String.map Char.toLower
   in
     if flag = "yes" then
       SOME true
     else if flag = "no" then
       SOME false
     else
       NONE
   end
 
 fun check_vampire_noncommercial () =
   (case is_vampire_noncommercial_license_accepted () of
     SOME true => ()
   | SOME false =>
     error (Pretty.string_of (Pretty.para
       "The Vampire prover may be used only for noncommercial applications"))
   | NONE =>
     error (Pretty.string_of (Pretty.para
       "The Vampire prover is not activated; to activate it, set the Isabelle system option \
       \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \
       \/ Isabelle / General)")))
 
 val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
 
 val vampire_full_proof_options =
   " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
 val vampire_config : atp_config =
   let
     val format = TFF (Without_FOOL, Monomorphic)
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
        (check_vampire_noncommercial ();
         [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
          " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
          |> sos = sosN ? prefix "--sos on "]),
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @
        tstp_proof_delims,
      known_failures =
        [(GaveUp, "UNPROVABLE"),
         (GaveUp, "CANNOT PROVE"),
         (Unprovable, "Satisfiability detected"),
         (Unprovable, "Termination reason: Satisfiable"),
         (Interrupted, "Aborted by signal SIGINT")] @
        known_szs_status_failures,
      prem_role = Hypothesis,
      best_slices = fn ctxt =>
        (* FUDGE *)
        [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)),
         (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)),
         (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))]
        |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   end
 
 val vampire = (vampireN, fn () => vampire_config)
 
 
 (* Z3 with TPTP syntax (half experimental, half legacy) *)
 
 val z3_tptp_config : atp_config =
   let
     val format = TFF (Without_FOOL, Monomorphic)
   in
     {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
      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 =
        (* FUDGE *)
        K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")),
           (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")),
           (0.125, (((62, mashN), format, "mono_native", combsN, false), "")),
           (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))],
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   end
 
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
 
 
 (* Zipperposition *)
 
 val zipperposition_blsimp = "--mode ho-pragmatic --max-inferences 3 --ho-max-app-projections 0 --ho-max-elims 0 --ho-max-rigid-imitations 2 --ho-max-identifications 0 --ho-unif-max-depth 2 --boolean-reasoning no-cases --ext-rules ext-family --ext-rules-max-depth 1 --kbo-weight-fun invdocc --ho-prim-enum tf --ho-prim-enum-early-bird true --tptp-def-as-rewrite --ho-unif-level pragmatic-framework -q '1|const|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)' -q '1|prefer-sos|staggered(1)' -q '2|prefer-fo|default' -q '1|prefer-neg-unit|orient-lmax(2,1,2,1,1)' -q '2|prefer-easy-ho|conjecture-relative-struct(1.5,3.5,2,3)' --ho-elim-leibniz 2 --ho-fixpoint-decider true --ho-pattern-decider false --ho-solid-decider true --ho-max-solidification 12  --select e-selection11 --solve-formulas true --sup-at-vars false --sup-at-var-headed false --lazy-cnf true --lazy-cnf-kind simp --lazy-cnf-renaming-threshold 4 --sine 50 --sine-tolerance 1.7 --sine-depth-max 3 --sine-depth-min 1 --sine-trim-implications true --ho-selection-restriction none --sup-from-var-headed false --sine-trim-implications true"
 val zipperposition_s6 = "--tptp-def-as-rewrite --rewrite-before-cnf true --mode ho-competitive --boolean-reasoning no-cases --ext-rules off --ho-prim-enum none --recognize-injectivity true --ho-elim-leibniz off --ho-unif-level full-framework --no-max-vars -q '3|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-ho-steps|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|fifo' -q '3|by-app-var-num|pnrefined(2,1,1,1,2,2,2)' --select ho-selection5 --prec-gen-fun unary_first --solid-subsumption false --ignore-orphans false --ho-solid-decider true --ho-fixpoint-decider true --ho-pattern-decider true --sup-at-vars false --sup-at-var-headed false --sup-from-var-headed false --ho-neg-ext-simpl true"
 val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -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 --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank"
 
 val zipperposition_config : atp_config =
   let
     val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
        ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
         |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = tstp_proof_delims,
-     known_failures = known_szs_status_failures,
+     known_failures =
+       [(TimedOut, "SZS status ResourceOut")] @   (* odd way of timing out *)
+       known_szs_status_failures,
      prem_role = Hypothesis,
      best_slices = fn _ =>
        (* FUDGE *)
        [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
         (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
         (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = default_max_new_mono_instances}
   end
 
 val zipperposition = (zipperpositionN, fn () => zipperposition_config)
 
 
 (* Remote ATP invocation via SystemOnTPTP *)
 
 val no_remote_systems = {url = "", systems = [] : string list}
 val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems
 
 fun get_remote_systems () =
   Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems ()
     handle ERROR msg => (warning msg; no_remote_systems)
       | Timeout.TIMEOUT _ => no_remote_systems
 
 fun find_remote_system name [] systems =
     find_first (String.isPrefix (name ^ "---")) systems
   | find_remote_system name (version :: versions) systems =
     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
       NONE => find_remote_system name versions systems
     | res => res
 
 fun get_remote_system name versions =
   Synchronized.change_result remote_systems (fn remote =>
     (if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote)
       then get_remote_systems () else remote) |> ` #systems)
   |> `(find_remote_system name versions)
 
 fun the_remote_system name versions =
   (case get_remote_system name versions of
     (SOME sys, _) => sys
   | (NONE, []) => error "SystemOnTPTP is currently not available"
   | (NONE, syss) =>
     (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
       [] => error "SystemOnTPTP is currently not available"
     | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg)
     | syss =>
       error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
         commas_quote syss ^ ".)")))
 
 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 =
   {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 => [(1.0, 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
     ({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_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)
 
 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, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *))
 
 val remote_agsyhol =
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
     (K (((60, ""), THF (Without_FOOL, Monomorphic, 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, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
     (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]
     (K (((150, ""), 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, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), THF (Without_FOOL, Polymorphic, 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.0"]
     (K (((512, ""), THF (Without_FOOL, Monomorphic, 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 [(1.0, (((200, ""), 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}
 
 
 val dummy_fof_format = FOF
 val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
 val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
 
 val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
 val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
 val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
 
 val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice)
 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "mono_native_higher_fool" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
 
 
 (* Setup *)
 
 fun add_atp (name, config) thy =
   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
 
 fun get_atp thy name =
   fst (the (Symtab.lookup (Data.get thy) name))
   handle Option.Option => error ("Unknown ATP: " ^ name)
 
 val supported_atps = Symtab.keys o Data.get
 
 fun is_atp_installed thy name =
   let val {exec, ...} = get_atp thy name () in
     exists (fn var => getenv var <> "") (fst exec)
   end
 
 fun refresh_systems_on_tptp () =
   Synchronized.change remote_systems (fn _ => get_remote_systems ())
 
 fun effective_term_order ctxt atp =
   let val ord = Config.get ctxt term_order in
     if ord = smartN then
       {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
        gen_simp = false}
     else
       let val is_lpo = String.isSubstring lpoN ord in
         {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
          gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
       end
   end
 
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
    remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf]
 
 val _ = Theory.setup (fold add_atp atps)
 
 end;