Overall FOF Statistics
----------------------
Number of domains                      16
Number of abstract problems          1678
Number of generic problems             1
Number of problems                   1745       :  1726 NP (98%) +   19 Pr ( 1%)
Number of problems with equality     1300 (74%)
Number of pure equality problems      185 ( 10%)
Number of non-theorem problems >=     70 (4%) :   70 NP (4%) +    0 Pr ( 0%)
Number of standard problems          1040 (59%) :  1040 NP (59%) +    0 Pr ( 0%)
 
 
Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of formulae             1    765    55    28       1      4     1     1
% of unit formulae            0%   100%   11%    6%      0%     0%    0%    0%
Number of atoms                2   7269   298   173       2     28     6     4
% of equality atoms           0%   100%   20%   14%
  in equality problems        0%   100%   26%   18%
Av atoms per formula         1.0 1736.0  64.6   4.3     2.0   28.0   5.7   4.0 
Maximal formula depth          2    324    31    19       2     28     5     4
Average formula depth          1    150    16     7       2     28     5     4
Number of connectives          0   7890   291   139       1     27     6     5
          ~                    0    931    48    14       0      5     1     1
          |                    0   3569    65     4       0      4     1     1
          &                    0   3642    92    43       0      2     0     0
          <=>                  0     36    10     4       0     27     2     1
          =>                   0    241    75    18       0      3     1     1
          <=                   0      0     0     0       0      0     0     0
          <~>                  0      2     0     0       0      0     0     0
          ~|                   0      0     0     0       0      0     0     0
          ~&                   0      0     0     0       0      0     0     0
Number of predicate symbols    1    285    17    16       1     14     2     2
% of propositions             0%    95%    6%    0%
Minimal predicate arity        0      5     1     1
Maximal predicate arity        1      6     2     2
Number of functors             0    204    11     5
% of constants                0%   100%   28%   20%
Minimal functor arity          0      3     0     0
Maximal functor arity          0      5     1     2
Number of variables            0    232    93    68
% of singletons               0%    17%    0%    0%
          !                    0    232    84    57
          ?                    0     62     8     6
Maximal term depth             1      7     2     3
Average term depth             1      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    # of Problems
     Field             Subfield                      Prefix  Abst / Vers / Gen
 -----------------------------------------------------------------------------

 |-- Logic --------|-- Combinatory Logic                COL     0 /    0 /   0
 |                 |-- Logic Calculi                    LCL     4 /    4 /   0
 |                 |-- Henkin Models                    HEN     0 /    0 /   0
 |
 |-- Mathematics --|-- Set Theory                       SET   302 /  323 /   0
 |                 |-- Graph Theory                     GRA     0 /    0 /   0
 |                 |-- Algebra --|-- Boolean Algebra    BOO     0 /    0 /   0
 |                 |             |-- Robbins Algebra    ROB     0 /    0 /   0
 |                 |             |-- Left Distributive  LDA     0 /    0 /   0
 |                 |             |-- Lattices           LAT     0 /    0 /   0
 |                 |             |-- Groups             GRP     3 /    3 /   0
 |                 |             |-- Rings              RNG     0 /    0 /   0
 |                 |             |-- Fields             FLD     0 /    0 /   0
 |                 |             |-- General Algebra    ALG   196 /  196 /   0
 |                 |             |-- Homological Alg    HAL     6 /    9 /   0
 |                 |-- Number Theory                    NUM     0 /    0 /   0
 |                 |-- Topology                         TOP     0 /    0 /   0
 |                 |-- Analysis                         ANA     0 /    0 /   0
 |                 |-- Geometry                         GEO    77 /   77 /   0
 |                 |-- Category Theory                  CAT     0 /    0 /   0
 |
 |-- Computer -----|-- Computing Theory                 COM     1 /    3 /   0
 |   Science       |-- Agents                           AGT    26 /   52 /   0
 |                 |-- Knowledge Representation Schemes KRS     0 /    0 /   0
 |                 |-- Natural Language Processing      NLP   258 /  258 /   0
 |                 |-- Planning                         PLA     6 /    6 /   0
 |                 |-- Software Creation                SWC   423 /  423 /   0
 |                 |-- Software Verification            SWV     9 /    9 /   0
 |
 |-- Engineering --|-- Hardware Creation                HWC     0 /    0 /   0
 |                 |-- Hardware Verification            HWV     0 /    0 /   0
 |
 |-- Social -------|-- Management                       MGT    66 /   78 /   0
 |   Sciences
 |
 |-- Other --------|-- Syntactic                        SYN   296 /  299 /   1
                   |-- Puzzles                          PUZ     4 /    4 /   0
                   |-- Miscellaneous                    MSC     1 /    1 /   0
