TPTP Documents File: FOFSynopsis
Overall FOF Statistics
----------------------
Domains 31
Abstract problems 4297
Problems 6983
Problems with equality 5334 (76%)
Pure equality problems 364 ( 5%)
Theorem/Unsatisfiable 6045 (86%)
CounterSat/Satisfiable 801 (11%)
Problem-by-problem Min Max Avg Med
------------------ ------------------------------
Number of formulae 1 3341990 34176 49
% of unit formulae 0% 100% 29% 20%
Number of atoms 1 5328217 66501 218
% of equality atoms 0% 100% 18% 11%
in problems with equality 0% 100% 24% 17%
Avg atoms per formula 1.0 12812.0 56.8 3.3
Number of predicate symbols 0 204678 2470 13
% of propositions 0% 100% nan% 0%
Maximal predicate arity 0 81 3 2
Number of functors 0 1050014 11070 10
% of constants 0% 100% 39% 25%
Maximal functor arity 0 220 2 2
Number of variables 0 972236 16427 112
! 0 972235 6774 88
? 0 9512 352 5
Number of connectives 0 2065419 35307 170
Maximal formula depth 1 4213 42 15
Average formula depth 1 4209 16 5
Maximal term depth 0 40 4 4
Average term depth 0 4 1 1
The TPTP Domain Structure
-------------------------
The domain structure of the TPTP is depicted below, with counts of the numbers
of FOF 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 0 / 0
| |-- Logic Calculi LCL 189 / 406
| |-- Henkin Models HEN 0 / 0
|
|-- Mathematics --|-- Set Theory SET 447 / 468
| |-- Set Theory Continued SEU 433 / 906
| |-- Set Theory Continued SEV 0 / 0
| |-- Graph Theory GRA 25 / 32
| |-- Algebra --|-- Relation Algebra REL 52 / 110
| | |-- Boolean Algebra BOO 1 / 1
| | |-- Robbins Algebra ROB 0 / 0
| | |-- Left Distributive LDA 0 / 0
| | |-- Lattices LAT 108 / 413
| | |-- Kleene Algebra KLE 168 / 225
| | |-- Groups GRP 79 / 195
| | |-- Rings RNG 84 / 157
| | |-- Fields FLD 0 / 0
| | |-- Homological Alg HAL 6 / 9
| | |-- General Algebra ALG 221 / 285
| |-- Number Theory NUM 329 / 558
| |-- Topology TOP 29 / 107
| |-- Analysis ANA 0 / 0
| |-- Geometry GEO 183 / 336
| |-- Category Theory CAT 17 / 68
|
|-- Computer -----|-- Computing Theory COM 15 / 31
| Science |-- Knowledge Representation KRS 254 / 254
| |-- Natural Language Processing NLP 262 / 262
| |-- Planning PLA 6 / 6
| |-- Agents AGT 26 / 52
| |-- Commonsense Reasoning CSR 116 / 756
| |-- Software Creation SWC 423 / 423
| |-- Software Verification SWV 328 / 346
|
|-- Science and --|-- Hardware Creation HWC 0 / 0
| Engineering |-- Hardware Verification HWV 0 / 0
| |-- Medicine MED 11 / 11
| |-- Processes PRO 18 / 72
|
|-- Social -------|-- Management MGT 66 / 78
| Sciences |-- Geography GEG 1 / 1
|
|-- Other --------|-- Syntactic SYN 365 / 375
|-- Syntactic Continued SYO 0 / 0
|-- Puzzles PUZ 25 / 30
|-- Miscellaneous MSC 10 / 10