Corpus report

Every problem and axiom file of a local TPTP library, read with Tptp.from_string/2 and nothing else — no include resolved, no lint rule run. A file counts as parsed when the result carries no error-severity diagnostic; warnings do not count against it.

A file that did not parse is listed below with the diagnostic code that refused it, because "did not parse" and "is not TPTP" are different claims and only the code says which one this is. Where the answer is known it is written out below the table, once per explanation rather than once per file, and it disappears from the report along with the failures it explains.

Regenerate with mix tptp.corpus; mix tptp.corpus --check fails if the results below have gone stale against the library on this machine. The nightly workflow sweeps a freshly downloaded release and keeps its own report as an artifact, because a count taken from one snapshot of the library says nothing about another.

Against the previous toolchain

The measurement this replaces ran the TH0/TH1 problem set — 5109 problems as it counted them — through the toolchain that preceded this library, and recorded 628 files that exceeded its parse budget and 221 it could not parse. Those are the two numbers the Timed out and Failed columns below are to be read against. The comparison is of coverage, not of speed: the budget, the machine and the TPTP release are not the same.

Results

The TPTP names a problem's form in its file name, and ^ marks a THF problem: 5279 of the 26925 problems swept are named that way. That is a fact about the names rather than about the contents — only Tptp.Query.dialect/1 answers that — and it is here because the TH0/TH1 set is what the comparison above is over.

What did not parse

SYN000+2.p, SYN000-2.p, SYN000^2.p use theory(equality) as an inference parent, which <source> has not derived since v9.3.1.2 replaced <source> ::= <general_term> with a list of alternatives. Fixed upstream on 10/09/26 — see https://tptp.org/TPTP/Distribution/BuggedProblems-v9.3.1.txt — and the three parse once that edit reaches the distributed tarball. They are the same demonstration of the annotated-formula syntax written once per dialect, and all three carry the same two statements.

SYN000_2.p writes introduced(assumption,[from,the,world,[]]), which is introduced(<intro_type>,<useful_info>) where both the BNF and the TPTP language page state introduced(<intro_type>,<useful_info>,<parents>). The bracket belongs one place to the left: the other three dialects' copies of this file write introduced(assumption,[from,the,world],[]). Distinct from, and not covered by, the theory(equality) fix of 10/09/26 — this file carries both, and the second was reachable only once the first was resolved. Reported upstream on 2026-09-11.

This run

Slowest files