Theory-Extensible Sequent Calculus (TESC) is a low-level, mechanically checkable proof format for first-order ATPs. Simple independent verifiers can check an input pair of a TPTP problem and a TESC proof, using the latter to verify that the former is unsatisfiable.

You can generate TESC proof files by compiling them from TSTP solution files using the TPTP-TSTP-TESC Processor (T3P) tool. T3P can also verify TESC proofs using one of three backend checkers: a formally verified checker written and verified in Agda, a performance-optimized checker written in Rust, and a debugging/backup checker written in Prolog.

T3P can be compiled using make. The following programs and variables should be available on the path for successful compilation and usage:

• swipl for compiling the main T3P script.
• cargo (with Rust) for compilation of the TPTP parser and optimized TESC verifier.
• agda (with its standard library) for compiling the verified TESC verifier. You may need to use the exact version of the standard library for correct compilation.
• cadical and drat-trim for handling AVATAR steps used in Vampire's TSTP solutions.
• Environment variables $TPTP and $TESC should be set to the TPTP and TESC directory paths, respectively.

Installation and usage was only tested on Linux.

t3p compile [SOLVER] [PROBLEM] [SOLUTION] [PROOF] compiles a TPTP problem [PROBLEM] and its TSTP solution [SOLUTION] to a new TESC proof [PROOF], where [SOLVER] is the ATP used to generate [SOLUTION]. Currently supported options for [SOLVER] are vampire and eprover.

t3p verify [VERIFIER] [PROBLEM] [PROOF] uses the TESC proof [PROOF] to check that the TPTP problem [PROBLEM] is unsatisfiable. Currently supported options for [VERIFIER] are vtv, otv, and dtv for the Agda, Rust, and Prolog verifiers, respectively. [VERIFIER] may be omitted, in which case T3P default otv.