Overall FOF Statistics
----------------------
Number of domains                      21
Number of abstract problems          2244
Number of generic problems             1
Number of problems                   2324       :  2299 NP (98%) +   25 Pr ( 1%)
Number of problems with equality     1729 (74%)
Number of pure equality problems      185 ( 7%)
Number of non-theorem problems >=     182 (7%) :   182 NP (7%) +    0 Pr ( 0%)
Number of standard problems          1039 (44%) :  1039 NP (44%) +    0 Pr ( 0%)
 
 
Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of formulae             1    923    71    29       1      4     1     1
% of unit formulae            0%   100%   19%    7%      0%   100%    8%    0%
Number of atoms                2   7269   279   186       1     28     5     4
% of equality atoms           0%   100%   20%   16%
  in equality problems        0%   100%   27%   19%
Av atoms per formula         1.0 1736.0  49.4   4.2     1.0   28.0   4.9   4.0 
Maximal formula depth          2    324    28    19       1     28     4     4
Average formula depth          1    150    13     6       1     28     4     4
Number of connectives          0   7890   246   124       0     27     4     4
          ~                    0    931    38     6       0      5     0     0
          |                    0   3569    51     4       0      4     0     0
          &                    0   3642    84    43       0      2     0     0
          <=>                  0    202     9     5       0     27     1     1
          =>                   0    765    62    19       0      3     0     0
          <=                   0      2     0     0       0      0     0     0
          <~>                  0      4     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    209    14    11       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    290    26     5
% of constants                0%   100%   37%   20%
Minimal functor arity          0      3     0     0
Maximal functor arity          0      5     1     2
Number of variables            0   1414    94    80
% of singletons               0%    17%    0%    0%
          !                    0   1414    87    74
          ?                    0    148     7     2
Maximal term depth             1     40     3     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   303 /  324 /   0
 |                 |-- Graph Theory                     GRA    11 /   18 /   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     5 /    5 /   0
 |                 |             |-- Rings              RNG     0 /    0 /   0
 |                 |             |-- Fields             FLD     0 /    0 /   0
 |                 |             |-- General Algebra    ALG   198 /  199 /   0
 |                 |             |-- Homological Alg    HAL     6 /    9 /   0
 |                 |-- Number Theory                    NUM    84 /   84 /   0
 |                 |-- Topology                         TOP     3 /    3 /   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       |-- Knowledge Representation Schemes KRS   158 /  158 /   0
 |                 |-- Natural Language Processing      NLP   258 /  258 /   0
 |                 |-- Planning                         PLA     6 /    6 /   0
 |                 |-- Agents                           AGT    26 /   52 /   0
 |                 |-- Commonsense Reasoning            CSR    24 /   29 /   0
 |                 |-- Software Creation                SWC   423 /  423 /   0
 |                 |-- Software Verification            SWV   220 /  220 /   0
 |
 |-- Engineering --|-- Hardware Creation                HWC     0 /    0 /   0
 |                 |-- Hardware Verification            HWV     0 /    0 /   0
 |
 |-- Social -------|-- Management                       MGT    66 /   78 /   0
 |   Sciences
 |
 |-- Other --------|-- Syntactic                        SYN   363 /  366 /   1
                   |-- Puzzles                          PUZ     6 /    6 /   0
                   |-- Miscellaneous                    MSC     2 /    2 /   0
