Synopsis
Overall Statistics
------------------ THF TFF
FOF CNF
Domains 46 : 18 (39%) + 13 (28%) +
31 (67%) + 32 (69%)
Abstract problems 11927 : 2241 (18%) + 810 ( 6%) +
4420 (37%) + 5868 (49%)
Problems 18480 : 2892 (15%) + 817 ( 4%) +
7137 (38%) + 7634 (41%)
Problems with equality 13559 (73%) : 2131 (73%) + 483 (59%) +
5486 (76%) + 5459 (71%)
Pure equality problems 2457 (13%) : 0 ( 0%) + 281 (34%) +
367 ( 5%) + 1809 (23%)
Theorem/Unsatisfiable 14957 (80%) : 2289 (79%) + 759 (92%) +
6204 (86%) + 5705 (74%)
CounterSat/Satisfiable 2249 (12%) : 351 (12%) + 57 ( 6%) +
799 (11%) + 1042 (13%)
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 866 / 1210
| |-- Henkin Models HEN 13 / 67
|
|-- Mathematics --|-- Set Theory SET 967 / 1395
| |-- Set Theory Continued SEU 978 / 1766
| |-- Set Theory Continued SEV 427 / 427
| |-- Graph Theory GRA 74 / 126
| |-- Algebra --|-- Relation Algebra REL 52 / 218
| | |-- Boolean Algebra BOO 105 / 140
| | |-- Robbins Algebra ROB 34 / 45
| | |-- Left Distributive LDA 40 / 49
| | |-- Lattices LAT 392 / 727
| | |-- Quantales QUA 20 / 20
| | |-- Kleene Algebra KLE 168 / 225
| | |-- Groups GRP 780 / 1090
| | |-- Rings RNG 126 / 261
| | |-- Fields FLD 99 / 279
| | |-- Homological Alg HAL 6 / 9
| | |-- General Algebra ALG 439 / 533
| |-- Number Theory NUM 912 / 1207
| |-- Topology TOP 48 / 131
| |-- Analysis ANA 42 / 91
| |-- Geometry GEO 350 / 672
| |-- Category Theory CAT 38 / 131
|
|-- Computer -----|-- Computing Theory COM 24 / 50
| Science |-- Knowledge Representation KRS 271 / 272
| |-- Natural Language Processing NLP 262 / 520
| |-- Planning PLA 31 / 46
| |-- Agents AGT 26 / 52
| |-- Commonsense Reasoning CSR 153 / 838
| |-- Data Structures DAT 55 / 55
| |-- Software Creation SWC 424 / 858
| |-- Software Verification SWV 998 / 1390
| |-- Software Verification Continued SWW 95 / 95
|
|-- Science and --|-- Hardware Creation HWC 4 / 6
| Engineering |-- Hardware Verification HWV 38 / 83
| |-- Medicine MED 11 / 11
| |-- Processes PRO 18 / 72
|
|-- Social -------|-- Social Choice Theory SCT 101 / 101
| Sciences |-- Management MGT 66 / 156
| |-- Geography GEG 20 / 20
|
|-- Other --------|-- Arithmetic ARI 569 / 571
|-- Syntactic SYN 986 / 1294
|-- Syntactic Continued SYO 522 / 701
|-- Puzzles PUZ 133 / 194
|-- Miscellaneous MSC 23 / 37