TSTP FOF Proof Benchmark for the Evaluation of Proof Checkers

This dataset contains a collection of First-Order Logic (FOF) refutation proofs sourced from the TSTP solution library (https://tptp.org/TSTP/), used for the evaluation of the Nörgler certificate checker (https://github.com/leoprover/noergler). All proofs were originally proved by Otter or PyRes, and were preprocessed by (i) translation to pure FOF using the tptp-utils library (https://github.com/leoprover/tptp-utils), and (ii) in case of the PyRes proofs, file names in the file records were corrected. For each set of proofs originating from either of the two provers, a corresponding set of intentionally falsified proofs generated via automated mutation (replacing connectives, negating sub-formulas, and atom substitution) to test the error-detection capabilities of verification tools. The archive includes: Otter: original: The preprocessed Otter proofs (1806) falsified: All proofs of the 'original' set that were successfully falsified (1782) PyRes: original: The preprocessed PyRes proofs (170) falsified: All proofs of the 'original' set that were successfully falsified (170) problems: The TPTP problems associated with the sourced proofs (170) These benchmarks are designed to evaluate both the performance (runtime) and the soundness (detection of incorrect entailments) of TSTP proof checkers.