Overall THF Statistics
----------------------
Domains                     14
Abstract problems         2129
Problems                  2729
Problems with equality    2009 (73%)
Theorem/Unsatisfiable     2098 (76%)
CounterSat/Satisfiable     317 (11%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1      749       65        8
% of unit formulae                  0%      99%      24%      25%
Number of atoms                      2     7624      641       87
% of equality atoms                 0%      33%       5%       6%
  in problems with equality         1%      33%       7%       7%
% of variable atoms                 0%      84%      34%      33%
Avg atoms per formula              1.5    998.0     32.5      8.1
Number of symbols                    1      390       37        8
Number of variables                  0     1189      100       16
          ^                          0      175       17        2
          !                          0     1067       76        8
          ?                          0       64        6        2
Number of connectives                0     4591      348       44
Number of type connectives           0      477       53       10
Maximal formula depth                2      359       38       11
Average formula depth                2      350       11        6

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   107 /  107
 |                 |-- Henkin Models                    HEN     0 /    0
 |
 |-- Mathematics --|-- Set Theory                       SET   111 /  127
 |                 |-- Set Theory Continued             SEU   545 /  860
 |                 |-- Graph Theory                     GRA    48 /   93
 |                 |-- Algebra --|-- Relation Algebra   REL     0 /    0
 |                 |             |-- Boolean Algebra    BOO     0 /    0
 |                 |             |-- Robbins Algebra    ROB     0 /    0
 |                 |             |-- Left Distributive  LDA     0 /    0
 |                 |             |-- Lattices           LAT     0 /    0
 |                 |             |-- Kleene Algebra     KLE     0 /    0
 |                 |             |-- Groups             GRP     1 /    1
 |                 |             |-- Rings              RNG     0 /    0
 |                 |             |-- Fields             FLD     0 /    0
 |                 |             |-- Homological Alg    HAL     0 /    0
 |                 |             |-- General Algebra    ALG    53 /   80
 |                 |-- Number Theory                    NUM   208 /  212
 |                 |-- Topology                         TOP     0 /    0
 |                 |-- Analysis                         ANA     0 /    0
 |                 |-- Geometry                         GEO     0 /    0
 |                 |-- Category Theory                  CAT     0 /    0
 |
 |-- Computer -----|-- Computing Theory                 COM     1 /    1
 |   Science       |-- Knowledge Representation         KRS     0 /    0
 |                 |-- Natural Language Processing      NLP     0 /    0
 |                 |-- Planning                         PLA     0 /    0
 |                 |-- Agents                           AGT     0 /    0
 |                 |-- Commonsense Reasoning            CSR     0 /    0
 |                 |-- Software Creation                SWC     0 /    0
 |                 |-- Software Verification            SWV    23 /   37
 |
 |-- Science and --|-- Hardware Creation                HWC     0 /    0
 |   Engineering   |-- Hardware Verification            HWV     0 /    0
 |                 |-- Medicine                         MED     0 /    0
 |                 |-- Processes                        PRO     0 /    0
 |
 |-- Social -------|-- Management                       MGT     0 /    0
 |   Sciences      |-- Geography                        GEG     0 /    0
 |
 |-- Other --------|-- Syntactic                        SYN    63 /   72
                   |-- Syntactic Continued              SYO   498 /  666
                   |-- Puzzles                          PUZ    49 /   51
                   |-- Miscellaneous                    MSC     2 /    2

