TPTP Documents File: OverallSynopsis
Overall Statistics
------------------ THF FOF CNF
Domains 41 : 14 (34%) + 31 (75%) + 31 (75%)
Abstract problems 10076 : 2129 (21%) + 4297 (42%) + 5047 (50%)
Problems 16512 : 2729 (16%) + 6983 (42%) + 6800 (41%)
Problems with equality 11968 (72%) : 2009 (73%) + 5334 (76%) + 4625 (68%)
Pure equality problems 2114 (12%) : 0 ( 0%) + 364 ( 5%) + 1750 (25%)
Theorem/Unsatisfiable 13083 (79%) : 2098 (76%) + 6045 (86%) + 4940 (72%)
CounterSat/Satisfiable 2082 (12%) : 317 (11%) + 801 (11%) + 964 (14%)
The TPTP Domain Structure
-------------------------
The domain structure of the TPTP is depicted below, with counts of the numbers
of problems and versions in each domain. The prefixes name subdirectories in
the Problems directory, and prefix the problem names in that directory.
Domain # Problems
Field Subfield Prefix Abst / Vers
-----------------------------------------------------------------------
|-- Logic --------|-- Combinatory Logic COL 121 / 239
| |-- Logic Calculi LCL 735 / 1079
| |-- Henkin Models HEN 13 / 67
|
|-- Mathematics --|-- Set Theory SET 967 / 1395
| |-- Set Theory Continued SEU 978 / 1766
| |-- Set Theory Continued SEV 420 / 420
| |-- Graph Theory GRA 74 / 126
| |-- Algebra --|-- Relation Algebra REL 52 / 218
| | |-- Boolean Algebra BOO 105 / 140
| | |-- Robbins Algebra ROB 31 / 40
| | |-- Left Distributive LDA 14 / 23
| | |-- Lattices LAT 392 / 727
| | |-- Kleene Algebra KLE 168 / 225
| | |-- Groups GRP 763 / 1073
| | |-- Rings RNG 126 / 261
| | |-- Fields FLD 99 / 279
| | |-- Homological Alg HAL 6 / 9
| | |-- General Algebra ALG 298 / 392
| |-- Number Theory NUM 824 / 1091
| |-- Topology TOP 48 / 131
| |-- Analysis ANA 42 / 91
| |-- Geometry GEO 268 / 589
| |-- Category Theory CAT 37 / 130
|
|-- Computer -----|-- Computing Theory COM 24 / 46
| Science |-- Knowledge Representation KRS 271 / 271
| |-- Natural Language Processing NLP 262 / 520
| |-- Planning PLA 31 / 46
| |-- Agents AGT 26 / 52
| |-- Commonsense Reasoning CSR 116 / 756
| |-- Software Creation SWC 423 / 846
| |-- Software Verification SWV 570 / 962
|
|-- Science and --|-- Hardware Creation HWC 4 / 6
| Engineering |-- Hardware Verification HWV 38 / 83
| |-- Medicine MED 11 / 11
| |-- Processes PRO 18 / 72
|
|-- Social -------|-- Management MGT 66 / 156
| Sciences |-- Geography GEG 1 / 1
|
|-- Other --------|-- Syntactic SYN 986 / 1291
|-- Syntactic Continued SYO 498 / 666
|-- Puzzles PUZ 129 / 183
|-- Miscellaneous MSC 21 / 33