What https://szs.tptp.org says about the SZS values and the BNF does not: their mnemonics and their descriptions.
This module is written by hand and maintained by hand. Tptp.Szs.Ontology is
generated from the vendored SZSOntology.bnf, which is the TPTP World's source
of truth for the values and the isa hierarchy among them, and delegates to this
module for everything else. The page publishes the mnemonics and descriptions in
prose only, so they are transcribed here and edited when the page changes; the
test suite checks that every generated value has both, so a value added to the
BNF fails the build until its entry is transcribed.
Each value's describe/1 text is quoted from the page. NOTICE carries the
attribution the TPTP's terms require for it.
Case sensitivity
SAT is Satisfiable and Sat is Saturation, so from_mnemonic/1 is case
sensitive. The lower-case three-letter form occurring inside a TPTP
status(...) annotation has a separate entry point, from_status_value/1,
which searches the success ontology alone, that being the only source
<inference_status_value> draws from, as the test suite verifies against the BNF.
Ass and ASS are a second such pair: Ass is Assurance in the data
ontology and ASS is Assumed in the no-success ontology.
Arguments of Assumed
Every mnemonic on the page is three letters except one. Assumed is
ASS(U,S): the success value S was assumed because the actual result is
unknown for the no-success reason U, where U is drawn from the subontology
beneath Unknown. The BNF states the same as
<Assumed> ::= Assumed(<Unknown>,<Success>), and
Tptp.Szs.Ontology.arguments/1 reports the two domains. mnemonic(:assumed)
returns "ASS" and from_mnemonic/1 accepts "ASS" alone, since a pair of
arguments is not a member of a closed set of atoms.
A consumer reading such a status line must decompose it: take the text
preceding the first (, resolve it here, and resolve the two arguments, which
are themselves mnemonics, with further calls. The page does not state how the
form is written in a % SZS status line, and the TPTP BNF cannot express it:
<status_value> is a list of plain words, so status(ass(...)) has no
derivation. Treat ASS(...) as a form to recognise rather than to emit.
Summary
Functions
What the page says a status value means, in its own words.
Turn a three-letter mnemonic into an atom. Case sensitive, because case is
meaningful: SAT is Satisfiable and Sat is Saturation.
Turn the lower-case mnemonic inside a TPTP status(...) annotation into an atom.
The three-letter mnemonic for a status value.
The page these mnemonics and descriptions are transcribed from.
Functions
@spec describe(Tptp.Szs.Ontology.t()) :: binary()
What the page says a status value means, in its own words.
iex> Tptp.Szs.Page.describe(:theorem)
"All models of Ax are models of C."@spec from_mnemonic(binary()) :: {:ok, Tptp.Szs.Ontology.t()} | {:ambiguous, [Tptp.Szs.Ontology.t()]} | :error
Turn a three-letter mnemonic into an atom. Case sensitive, because case is
meaningful: SAT is Satisfiable and Sat is Saturation.
A mnemonic the page reuses answers {:ambiguous, values} rather than picking
one — IIn is both InfiniteInterpretation and IncompleteInterpretation.
iex> Tptp.Szs.Page.from_mnemonic("THM")
{:ok, :theorem}
iex> Tptp.Szs.Page.from_mnemonic("IIn")
{:ambiguous, [:infinite_interpretation, :incomplete_interpretation]}
iex> Tptp.Szs.Page.from_mnemonic("thm")
:error@spec from_status_value(binary()) :: {:ok, Tptp.Szs.Ontology.t()} | :error
Turn the lower-case mnemonic inside a TPTP status(...) annotation into an atom.
<inference_status_value> in the SZS BNF is the success ontology's mnemonic,
lower-cased, and the test suite checks that all of them are present here.
iex> Tptp.Szs.Page.from_status_value("thm")
{:ok, :theorem}
iex> Tptp.Szs.Page.from_status_value("prf")
:error@spec mnemonic(Tptp.Szs.Ontology.t()) :: binary()
The three-letter mnemonic for a status value.
iex> Tptp.Szs.Page.mnemonic(:theorem)
"THM"@spec source() :: binary()
The page these mnemonics and descriptions are transcribed from.
The page carries no version number, so there is nothing finer to report. The transcription was last checked against it on 2026-09-10.