Overall FOF Statistics
----------------------
Domains                     36
Abstract problems         4865
Problems                  7807
Problems with equality    6064 (77%)
Pure equality problems     368 ( 4%)
Theorem/Unsatisfiable     6799 (87%)
CounterSat/Satisfiable     877 (11%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1  3341984    31485       61
% of unit formulae                  0%     100%      30%      22%
Number of atoms                      1  5328211    61584      261
% of equality atoms                 0%     100%      19%      11%
  in problems with equality         0%     100%      24%      17%
Avg atoms per formula              1.0  12812.0     51.2      3.2
Number of predicate symbols          0   204678     2211       13
% of propositions                   0%     100%    -nan%       0%
Maximal predicate arity              0       81        3        2
Number of functors                   0  1050014    10371       13
% of constants                      0%     100%      40%      27%
Maximal functor arity                0      220        3        2
Number of variables                  0   972236    15654      123
          !                          0   972235     6940      110
          ?                          0     9512      395        8
Number of connectives                0  2065419    32831      193
Maximal formula depth                1     4213       41       16
Average formula depth                1     4209       14        5
Maximal term depth                   0       40        4        4
Average term depth                   0        8        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   190 /  407
 |                 |-- Henkin Models                    HEN     0 /    0
 |
 |-- Mathematics --|-- Set Theory                       SET   447 /  468
 |                 |-- Set Theory Continued             SEU   433 /  906
 |                 |-- Set Theory Continued             SEV     0 /    0
 |                 |-- Graph Theory                     GRA    25 /   32
 |                 |-- Algebra --|-- Relation Algebra   REL    52 /  110
 |                 |             |-- Boolean Algebra    BOO     1 /    1
 |                 |             |-- Robbins Algebra    ROB     0 /    0
 |                 |             |-- Left Distributive  LDA     0 /    0
 |                 |             |-- Lattices           LAT   108 /  413
 |                 |             |-- Quantales          QUA     0 /    0
 |                 |             |-- Kleene Algebra     KLE   170 /  229
 |                 |             |-- Groups             GRP    86 /  202
 |                 |             |-- Rings              RNG    84 /  157
 |                 |             |-- Fields             FLD     0 /    0
 |                 |             |-- Homological Alg    HAL     6 /    9
 |                 |             |-- General Algebra    ALG   221 /  285
 |                 |-- Number Theory                    NUM   361 /  641
 |                 |-- Topology                         TOP    29 /  107
 |                 |-- Analysis                         ANA     0 /    0
 |                 |-- Geometry                         GEO   265 /  418
 |                 |-- Category Theory                  CAT    17 /   68
 |
 |-- Computer -----|-- Computing Theory                 COM    15 /   31
 |   Science       |-- Knowledge Representation         KRS   254 /  254
 |                 |-- Natural Language Processing      NLP   262 /  262
 |                 |-- Planning                         PLA     6 /    6
 |                 |-- Agents                           AGT    26 /   52
 |                 |-- Commonsense Reasoning            CSR   119 /  784
 |                 |-- Semantic Web                     SWB   108 /  204
 |                 |-- Data Structures                  DAT     0 /    0
 |                 |-- Software Creation                SWC   423 /  423
 |                 |-- Software Verification            SWV   328 /  346
 |                 |-- Software Verification Continued  SWW   245 /  291
 |
 |-- Science and --|-- Hardware Creation                HWC     0 /    0
 |   Engineering   |-- Hardware Verification            HWV    13 /   26
 |                 |-- Medicine                         MED    11 /   11
 |                 |-- Processes                        PRO    18 /   72
 |
 |-- Social -------|-- Social Choice Theory             SCT    70 /   85
 |   Sciences      |-- Management                       MGT    66 /   78
 |                 |-- Geography                        GEG     1 /    1
 |
 |-- Other --------|-- Arithmetic                       ARI     0 /    0
                   |-- Syntactic                        SYN   365 /  375
                   |-- Syntactic Continued              SYO     2 /    7
                   |-- Puzzles                          PUZ    28 /   36
                   |-- Miscellaneous                    MSC    10 /   10
