Overall FOF Statistics
----------------------
Domains                     26
Abstract problems         3481
Problems                  5051
Problems with equality    4096 (81%)
Pure equality problems     211 ( 4%)
Theorem/Unsatisfiable     4394 (86%)
CounterSat/Satisfiable     512 (10%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1  3341990    43641       67
% of unit formulae                  0%     100%      25%      19%
Number of atoms                      1  5328217    87760      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     3393       17
% of propositions                   0%     100%       7%       0%
Maximal predicate arity              0       81        3        2
Number of functors                   0  1050014    14004       10
% of constants                      0%     100%      34%      20%
Maximal functor arity                0       10        3        2
Number of variables                  0   972236    22390      122
          !                          0   972235     9081      108
          ?                          0     9512      451        8
Number of connectives                0  2065419    48135      177
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   364 /  368
                   |-- Syntactic Continued              SYO     0 /    0
                   |-- Puzzles                          PUZ    22 /   24
                   |-- Miscellaneous                    MSC     7 /    7
