Summary

This is not a bug report — it is a minor code-quality observation about error handling in the TPTP parser. Filing it here so it can be discussed, and accompanied by a small PR that the maintainers are welcome to accept, modify, or decline.

The function role_of_string in src/parsers/ast_tptp.ml (line 55) uses failwith as the catch-all for unrecognised TPTP formula roles. This raises an uncaught Failure exception with no source location:

$ zipperposition --input tptp --output tptp role_bug.p
Failure("not a proper TPTP role: corollary")

where role_bug.p contains:

thf(test, corollary, ($true)).

This does not affect any real user path — Sledgehammer and the TPTP problem library do not use corollary, interpretation, or logic roles in practice.

Scope clarification

• This does not affect Sledgehammer users. Sledgehammer only emits the roles axiom, hypothesis, definition, conjecture, negated_conjecture, type, and plain, all of which are already handled correctly.
• This does not affect standard TPTP benchmark users. These roles are rarely used in practice — neither Sledgehammer nor typical TPTP benchmark problems produce them.
• E and Vampire also reject corollary / interpretation / logic. The functional outcome is identical across all three provers — the input is rejected. The only difference is the error-reporting style.

Differential comparison

Input: thf(test, <ROLE>, ($true)).

E and Vampire produce location-bearing error messages and exit through their normal error paths. Zipperposition is the only one whose parser reaches an uncaught OCaml exception on the same inputs.

Root cause

src/parsers/ast_tptp.ml, lines 39–55:

let role_of_string = function
  | "axiom" -> R_axiom
  | "hypothesis" -> R_hypothesis
  (* ... *)
  | "type" -> R_type
  | "unknown" -> R_unknown
  | s -> failwith ("not a proper TPTP role: " ^ s)  (* ← here *)

For reference, the TPTP BNF <formula_role> semantic rule enumerates:
axiom | hypothesis | definition | assumption | lemma | theorem | corollary | conjecture | negated_conjecture | plain | type | fi_domain | fi_functors | fi_predicates | interpretation | logic | unknown. Zipperposition's table covers most of these but not
corollary, interpretation, or logic.

Suggested fix (see PR)

A small change to role_of_string that:

1. Maps corollary to R_axiom — the TPTP standard classifies it as axiom-like, same category as lemma.
2. Maps interpretation and logic to R_plain — semantic/metadata roles that do not affect proof search.
3. Replaces the failwith catch-all with a stderr warning plus R_unknown fallback, so unrecognised roles do not abort the prover.

This is a minimal, local change. If the maintainers prefer to keep the hard failure but with a proper source location, that would also be reasonable — I'd be happy to adapt the PR accordingly.