Overall CNF Statistics
----------------------
Domains                     34
Abstract problems         5963
Problems                  7753
Problems with equality    5572 (71%)
Pure equality problems    1816 (23%)
Theorem/Unsatisfiable     5788 (74%)
CounterSat/Satisfiable    1090 (14%)
Non-Horn problems         4955 (63%)
Range rest. problems       708 ( 9%)
Unit equality problems    1090 (14%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of clauses                    1     5233      232       41
% of unit clauses                   0%     100%      47%      34%
% of non-Horn clauses               0%      99%      12%       7%
  in non-Horn problems              0%      99%      19%      11%
% of range rest. clauses            0%     100%      67%      71%
Number of literals                   1   127126      875       91
% of equality literals              0%     100%      34%      21%
  in problems with equality         0%     100%      47%      23%
Maximal clause size                  1      901        8        5
Average clause size                  1       40        1        1
Number of predicate symbols          1     1817       23        4
% of propositions                   0%     100%       2%       0%
Maximal predicate arity              0       56        3        2
Number of functors                   0      903       34       12
% of constants                      0%     100%      49%      48%
Maximal functor arity                0       32        2        2
Number of variables                  0   120428      814       71
Maximal term depth                   0      721        5        5
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   560 /  682
 |                 |-- 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    34 /   45
 |                 |             |-- Left Distributive  LDA    40 /   49
 |                 |             |-- Lattices           LAT   286 /  318
 |                 |             |-- Quantales          QUA     0 /    0
 |                 |             |-- Kleene Algebra     KLE     0 /    0
 |                 |             |-- Groups             GRP   702 /  888
 |                 |             |-- Rings              RNG    44 /  106
 |                 |             |-- Fields             FLD    99 /  279
 |                 |             |-- Homological Alg    HAL     0 /    0
 |                 |             |-- General Algebra    ALG   169 /  171
 |                 |-- 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 /   45
 |                 |-- Agents                           AGT     0 /    0
 |                 |-- Commonsense Reasoning            CSR     0 /    0
 |                 |-- Semantic Web                     SWB     0 /    0
 |                 |-- Data Structures                  DAT     0 /    0
 |                 |-- Software Creation                SWC   423 /  423
 |                 |-- Software Verification            SWV   656 / 1003
 |                 |-- Software Verification Continued  SWW    72 /   72
 |
 |-- Science and --|-- Hardware Creation                HWC     4 /    6
 |   Engineering   |-- Hardware Verification            HWV    52 /  121
 |                 |-- Medicine                         MED     0 /    0
 |                 |-- Processes                        PRO     0 /    0
 |
 |-- Social -------|-- Social Choice Theory             SCT   101 /  101
 |   Sciences      |-- Management                       MGT    66 /   78
 |                 |-- Geography                        GEG     0 /    0
 |
 |-- Other --------|-- Arithmetic                       ARI     0 /    0
                   |-- Syntactic                        SYN   830 /  844
                   |-- Syntactic Continued              SYO     1 /    5
                   |-- Puzzles                          PUZ    67 /  102
                   |-- Miscellaneous                    MSC    10 /   21

