The python code and generated latex files are at math.chapman.edu/~jipsen/tptp/tptplatex/. 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.
| 1 | Agents | AGT.pdf 43K |
| 2 | General algebra | ALG.pdf 175K |
| 3 | Analysis | ANA.pdf 233K |
| 4 | Arithmetic | ARI.pdf 182K |
| 5 | Biology | BIO.pdf 23K |
| 6 | Boolean algebra | BOO.pdf 90K |
| 7 | Category theory | CAT.pdf 77K |
| 8 | Combinatory logic | COL.pdf 264K |
| 9 | Computing theory | COM.pdf 100K |
| 10 | Commonsense Reasoning | CSR.pdf 507K |
| 11 | Data Structures | DAT.pdf 121K |
| 12 | Fields | FLD.pdf 194K |
| 13 | Geography | GEG.pdf 50K |
| 14 | Geometry | GEO.pdf 374K |
| 15 | Graph theory | GRA.pdf 82K |
| 16 | Groups | GRP.pdf 768K |
| 17 | Homological algebra | HAL.pdf 35K |
| 18 | Henkin models | HEN.pdf 69K |
| 19 | Hardware creation | HWC.pdf 35K |
| 20 | Hardware verification | HWV.pdf 107K |
| 21 | Kleene algebra | KLE.pdf 108K |
| 22 | Knowledge representation | KRS.pdf 194K |
| 23 | Lattices | LAT.pdf 296K |
| 24 | Logic calculi | LCL.pdf 580K |
| 25 | Left distributive | LDA.pdf 60K |
| 26 | Management | MGT.pdf 34K |
| 27 | Medicine | MED.pdf 201K |
| 28 | Miscellaneous | MSC.pdf 71K |
| 29 | Natural Language Processing | NLP.pdf 120K |
| 30 | Number theory | NUM.pdf 503K, NUN.pdf 33K |
| 31 | Philosophy | PHI.pdf 44K |
| 32 | Planning | PLA.pdf 57K |
| 33 | Products | PRD.pdf 25K |
| 34 | Puzzles | PUZ.pdf 294K |
| 35 | Quantales | QUA.pdf 35K |
| 36 | Relation algebra | REL.pdf 96K |
| 37 | Rings | RNG.pdf 117K |
| 38 | Robbins algebra | ROB.pdf 47K |
| 39 | Social Choice Theory | SCT.pdf 32K |
| 40 | Set theory | SET.pdf 959K, SEU.pdf 733K, SEV.pdf 295K |
| 41 | Semantic Web | SWB.pdf 274K |
| 42 | Software creation | SWC.pdf 767K |
| 43 | Software verification | SWV.pdf 1000K, SWW.pdf 93K |
| 44 | Syntactic | SYN.pdf 509K, SYO.pdf 310K |
| 45 | Topology | TOP.pdf 56K |
Certainly some of the output can be improved further. If you notice errors or have suggestions, please email jipsen AT chapman.edu