Overall CNF Statistics
----------------------
Number of domains                     30
Number of abstract problems         4362
Number of generic problems            86
Number of problems                  5521       : 5478 NP (99%) +   43 Pr ( 0%)
Number of non-Horn problems         3354 (60%) : 3323 NP (60%) +   31 Pr ( 0%)
Number of range rest. problems       580 ( 10%) :  537 NP ( 9%) +   43 Pr ( 0%)
Number of problems with equality    3590 (65%)
Number of pure equality problems    1136 (20%)
Number of unit equality problems     777 (14%)
Number of satisfiable problems >=   773 ( 14%) :  766 NP (13%) +    7 Pr ( 0%)
Number of standard problems         3494 (63%) : 3492 NP (63%) +    2 Pr ( 0%)
 
 
Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of clauses              1   3240    94    34       3    204    35    19
% of non-Horn clauses         0%    99%   13%    7%      0%    81%   25%   21%
  in non-Horn problems        1%    99%   22%   13%      4%    81%   34%   33%
% of unit clauses             0%   100%   44%   34%      0%   100%   19%    6%
% of range rest. clauses      0%   100%   68%   75%
Number of literals             1 127126   728    84       4    448    90    49
% of equality literals        0%   100%   30%   17%
  in equality problems        0%   100%   45%   22%
Maximal clause size            1     60     6     5       1     11     3     3
Average clause size            1     40     2     2       1      5     1     2
Number of predicate symbols    1   1817    22     4       2     63    16    12
% of propositions             0%    97%    2%    0%
Minimal predicate arity        0     54     1     1
Maximal predicate arity        1     56     3     2
Number of functors             0    244    21    10
% of constants                0%   100%   49%   50%
Minimal functor arity          0      2     0     0
Maximal functor arity          0      8     2     2
Number of variables            0 120428   620    71
% of singletons               0%   100%    9%    6%
Maximal term depth             1     85     4     4
Average term depth             1      8     1     2
 

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    # of Problems
     Field             Subfield                      Prefix  Abst / Vers / Gen
 -----------------------------------------------------------------------------

 |-- Logic --------|-- Combinatory Logic                COL    97 /  193 /   0
 |                 |-- Logic Calculi                    LCL   425 /  527 /   0
 |                 |-- Henkin Models                    HEN    13 /   67 /   0
 |
 |-- Mathematics --|-- Set Theory                       SET   568 /  706 /   0
 |                 |-- Graph Theory                     GRA     1 /    1 /   0
 |                 |-- Algebra --|-- Boolean Algebra    BOO   104 /  139 /   0
 |                 |             |-- Robbins Algebra    ROB    28 /   37 /   0
 |                 |             |-- Left Distributive  LDA    14 /   23 /   0
 |                 |             |-- Lattices           LAT    97 /  104 /   0
 |                 |             |-- Groups             GRP   614 /  791 /  50
 |                 |             |-- Rings              RNG    42 /  104 /   0
 |                 |             |-- Fields             FLD    99 /  279 /   0
 |                 |             |-- General Algebra    ALG    13 /   15 /   0
 |                 |             |-- Homological Alg    HAL     0 /    0 /   0
 |                 |-- Number Theory                    NUM   289 /  315 /   2
 |                 |-- Topology                         TOP    19 /   24 /   0
 |                 |-- Analysis                         ANA     6 /   21 /   0
 |                 |-- Geometry                         GEO   162 /  253 /   0
 |                 |-- Category Theory                  CAT    20 /   62 /   0
 |
 |-- Computer -----|-- Computing Theory                 COM     6 /    8 /   0
 |   Science       |-- Agents                           AGT     0 /    0 /   0
 |                 |-- Knowledge Representation Schemes KRS    17 /   17 /   0
 |                 |-- Natural Language Processing      NLP   258 /  258 /   0
 |                 |-- Planning                         PLA    25 /   32 /   0
 |                 |-- Software Creation                SWC   423 /  423 /   0
 |                 |-- Software Verification            SWV    21 /   21 /   0
 |
 |-- Engineering --|-- Hardware Creation                HWC     4 /    6 /   0
 |                 |-- Hardware Verification            HWV    38 /   83 /   0
 |
 |-- Social -------|-- Management                       MGT    66 /   78 /   0
 |   Sciences
 |
 |-- Other --------|-- Syntactic                        SYN   826 /  839 /  27
                   |-- Puzzles                          PUZ    58 /   82 /   4
                   |-- Miscellaneous                    MSC     9 /   13 /   3
