TPTP Documents File: CNFSynopsis
Overall CNF Statistics
----------------------
Domains 31
Abstract problems 5047
Problems 6800
Problems with equality 4625 (68%)
Pure equality problems 1750 (25%)
Theorem/Unsatisfiable 4940 (72%)
CounterSat/Satisfiable 964 (14%)
Non-Horn problems 4076 (24%)
Range rest. problems 702 ( 4%)
Unit equality problems 1038 ( 6%)
Problem-by-problem Min Max Avg Med
------------------ ------------------------------
Number of clauses 1 3240 177 32
% of unit clauses 0% 100% 48% 34%
% of non-Horn clauses 0% 99% 12% 7%
in non-Horn problems 0% 99% 20% 10%
% of range rest. clauses 0% 100% 67% 75%
Number of literals 1 127126 787 79
% of equality literals 0% 100% 34% 17%
in problems with equality 0% 100% 50% 23%
Maximal clause size 1 901 8 5
Average clause size 1 40 2 1
Number of predicate symbols 1 1817 22 4
% of propositions 0% 100% 2% 0%
Maximal predicate arity 0 56 3 2
Number of functors 0 903 32 11
% of constants 0% 100% 51% 50%
Maximal functor arity 0 18 2 2
Number of variables 0 120428 667 50
Maximal term depth 0 721 4 4
Average term depth 0 163 1 2
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 121 / 239
| |-- Logic Calculi LCL 444 / 566
| |-- Henkin Models HEN 13 / 67
|
|-- Mathematics --|-- Set Theory SET 615 / 800
| |-- Set Theory Continued SEU 0 / 0
| |-- Set Theory Continued SEV 0 / 0
| |-- Graph Theory GRA 1 / 1
| |-- Algebra --|-- Relation Algebra REL 50 / 108
| | |-- Boolean Algebra BOO 104 / 139
| | |-- Robbins Algebra ROB 31 / 40
| | |-- Left Distributive LDA 14 / 23
| | |-- Lattices LAT 284 / 314
| | |-- Kleene Algebra KLE 0 / 0
| | |-- Groups GRP 691 / 877
| | |-- Rings RNG 42 / 104
| | |-- Fields FLD 99 / 279
| | |-- Homological Alg HAL 0 / 0
| | |-- General Algebra ALG 25 / 27
| |-- Number Theory NUM 290 / 321
| |-- Topology TOP 19 / 24
| |-- Analysis ANA 42 / 91
| |-- Geometry GEO 162 / 253
| |-- Category Theory CAT 20 / 62
|
|-- Computer -----|-- Computing Theory COM 9 / 14
| Science |-- Knowledge Representation KRS 17 / 17
| |-- Natural Language Processing NLP 258 / 258
| |-- Planning PLA 26 / 40
| |-- Agents AGT 0 / 0
| |-- Commonsense Reasoning CSR 0 / 0
| |-- Software Creation SWC 423 / 423
| |-- Software Verification SWV 232 / 579
|
|-- Science and --|-- Hardware Creation HWC 4 / 6
| Engineering |-- Hardware Verification HWV 38 / 83
| |-- Medicine MED 0 / 0
| |-- Processes PRO 0 / 0
|
|-- Social -------|-- Management MGT 66 / 78
| Sciences |-- Geography GEG 0 / 0
|
|-- Other --------|-- Syntactic SYN 830 / 844
|-- Syntactic Continued SYO 0 / 0
|-- Puzzles PUZ 67 / 102
|-- Miscellaneous MSC 10 / 21