Overall FOF Statistics
----------------------
Domains                     26
Abstract problems         3480
Problems                  5049
Problems with equality    4094 (81%)
Pure equality problems     211 ( 4%)
Theorem/Unsatisfiable     4393 (87%)
CounterSat/Satisfiable     511 (10%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1  3341990    43659       67
% of unit formulae                  0%     100%      24%      19%
Number of atoms                      1  5328217    87795      269
% of equality atoms                 0%     100%      15%      11%
  in equality problems              0%     100%      19%      12%
Avg atoms per formula              1.0   1736.0     27.8      3.4
Number of predicate symbols          1   204678     3395       17
% of propositions                   0%     100%       7%       0%
Maximal predicate arity              0       81        3        2
Number of functors                   0  1050014    14010       10
% of constants                      0%     100%      34%      20%
Maximal functor arity                0       10        3        2
Number of variables                  0   972236    22399      122
          !                          0   972235     9085      108
          ?                          0     9512      451        8
Number of connectives                0  2065419    48154      177
          ~                          0    79193     4018       21
          |                          0     6490      257        3
          &                          0   300558    12832       52
          <=>                        0    11671      555        6
          =>                         0  1867380     8394       37
          <=                         0        2        0        0
          <~>                        0        4        0        0
          ~|                         0        0        0        0
          ~&                         0        0        0        0
Maximal formula depth                1     1614       31       16
Average formula depth                1     1614       12        5
Maximal term depth                   0       40        4        4
Average term depth                   0        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  # Problems
     Field             Subfield                      Prefix  Abst / Vers
 -----------------------------------------------------------------------

 |-- Logic --------|-- Combinatory Logic                COL     0 /    0
 |                 |-- Logic Calculi                    LCL   135 /  136
 |                 |-- Henkin Models                    HEN     0 /    0
 |
 |-- Mathematics --|-- Set Theory                       SET   447 /  468
 |                 |-- Set Theory Continued             SEU   433 /  906
 |                 |-- Graph Theory                     GRA    25 /   32
 |                 |-- Algebra --|-- Boolean Algebra    BOO     1 /    1
 |                 |             |-- Robbins Algebra    ROB     0 /    0
 |                 |             |-- Left Distributive  LDA     0 /    0
 |                 |             |-- Lattices           LAT   100 /  397
 |                 |             |-- Groups             GRP    41 /  149
 |                 |             |-- Rings              RNG     0 /    0
 |                 |             |-- Fields             FLD     0 /    0
 |                 |             |-- Homological Alg    HAL     6 /    9
 |                 |             |-- General Algebra    ALG   221 /  285
 |                 |-- Number Theory                    NUM   115 /  136
 |                 |-- Topology                         TOP    29 /  107
 |                 |-- Analysis                         ANA     0 /    0
 |                 |-- Geometry                         GEO   178 /  236
 |                 |-- Category Theory                  CAT    17 /   68
 |
 |-- Computer -----|-- Computing Theory                 COM     3 /    7
 |   Science       |-- Knowledge Representation         KRS   158 /  158
 |                 |-- Natural Language Processing      NLP   258 /  258
 |                 |-- Planning                         PLA     6 /    6
 |                 |-- Agents                           AGT    26 /   52
 |                 |-- Commonsense Reasoning            CSR   111 /  442
 |                 |-- Software Creation                SWC   423 /  423
 |                 |-- Software Verification            SWV   279 /  288
 |
 |-- Science and --|-- Hardware Creation                HWC     0 /    0
 |   Engineering   |-- Hardware Verification            HWV     0 /    0
 |                 |-- Medicine                         MED    10 /   10
 |
 |-- Social -------|-- Management                       MGT    66 /   78
 |   Sciences
 |
 |-- Other --------|-- Syntactic                        SYN   363 /  366
                   |-- Puzzles                          PUZ    22 /   24
                   |-- Miscellaneous                    MSC     7 /    7
