The links below are to PDF files that contain axioms and problems from the Thousands of Problems for Theorem Provers Library (v6.4.0), created by Geoff Sutcliffe and Christian Suttner. The TPTP language is based on Prolog syntax and is not easily readable since all function and relation symbols (except "=") are written in prefix form. Here a Python program was used to translate the TPTP syntax into more readable LaTeX. The axioms and problem files of a topic domain are merged into one PDF, allowing the reader to scan the problems quickly. To avoid huge amounts of output, only axiom and problem files that have <5000 characters have been translated.

The python code and generated latex files are at The translator does not provide error messages and will parse some formulas that do not conform to the TPTP syntax. It displays some binary/ternary relations in functional form (e.g. meet(a,b,c) is shown as a /\ b=c, but spacing is removed around the = sign to distinguish relations from functional notation like a /\ b = c).

Clauses are displayed as implications (if they contain some negative disjuncts), and most formulas are displayed on one line (in some cases making them less readable or longer than the width of the page). Variable names are converted to lowercase and trailing digits are shown as subscripts.

1AgentsAGT.pdf 43K
2General algebraALG.pdf 175K
3AnalysisANA.pdf 233K
4ArithmeticARI.pdf 182K
5BiologyBIO.pdf 23K
6Boolean algebraBOO.pdf 90K
7Category theoryCAT.pdf 77K
8Combinatory logicCOL.pdf 264K
9Computing theoryCOM.pdf 100K
10Commonsense ReasoningCSR.pdf 507K
11Data StructuresDAT.pdf 121K
12FieldsFLD.pdf 194K
13GeographyGEG.pdf 50K
14GeometryGEO.pdf 374K
15Graph theoryGRA.pdf 82K
16GroupsGRP.pdf 768K
17Homological algebraHAL.pdf 35K
18Henkin modelsHEN.pdf 69K
19Hardware creationHWC.pdf 35K
20Hardware verificationHWV.pdf 107K
21Kleene algebraKLE.pdf 108K
22Knowledge representationKRS.pdf 194K
23LatticesLAT.pdf 296K
24Logic calculiLCL.pdf 580K
25Left distributiveLDA.pdf 60K
26ManagementMGT.pdf 34K
27MedicineMED.pdf 201K
28Miscellaneous MSC.pdf 71K
29Natural Language ProcessingNLP.pdf 120K
30Number theoryNUM.pdf 503K, NUN.pdf 33K
31PhilosophyPHI.pdf 44K
32PlanningPLA.pdf 57K
33ProductsPRD.pdf 25K
34PuzzlesPUZ.pdf 294K
35QuantalesQUA.pdf 35K
36Relation algebraREL.pdf 96K
37RingsRNG.pdf 117K
38Robbins algebraROB.pdf 47K
39Social Choice TheorySCT.pdf 32K
40Set theorySET.pdf 959K, SEU.pdf 733K, SEV.pdf 295K
41Semantic WebSWB.pdf 274K
42Software creationSWC.pdf 767K
43Software verificationSWV.pdf 1000K, SWW.pdf 93K
44SyntacticSYN.pdf 509K, SYO.pdf 310K
45TopologyTOP.pdf 56K

Certainly some of the output can be improved further. If you notice errors or have suggestions, please email jipsen AT

Peter Jipsen --- Chapman University --- September 2016