--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 01 08:00:51 2023 +0100
@@ -64,6 +64,7 @@
val tptp_cnf : string
val tptp_fof : string
+ val tptp_tcf : string
val tptp_tff : string
val tptp_thf : string
val tptp_has_type : string
@@ -222,6 +223,7 @@
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
+val tptp_tcf = "tcf" (* sometimes appears in E's output *)
val tptp_tff = "tff"
val tptp_thf = "thf"
val tptp_has_type = ":"
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Mar 01 08:00:51 2023 +0100
@@ -572,7 +572,8 @@
end)
fun parse_tstp_fol_line full problem =
- ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
+ ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tcf
+ || Scan.this_string tptp_tff) -- $$ "(")
|-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
-- (if full then parse_fol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
-- parse_tstp_extra_arguments --| $$ ")" --| $$ "."