Overall THF Statistics
----------------------
Domains                     22
Abstract problems         2223
Problems                  2929
Problems with equality    2215 (75%)
Theorem/Unsatisfiable     2366 (80%)
CounterSat/Satisfiable     349 (11%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1     5639      102       10
% of unit formulae                  0%     100%      24%      20%
% of type formulae                  0%      99%      52%      53%
% of defn formulae                 36%       0%      19%      22%
Number of atoms                      1    64867      801       80
% of equality atoms                 0%      43%       7%       7%
  in problems with equality         1%      43%       9%       9%
% of variable atoms                 0%     100%      46%      41%
Avg atoms per formula              1.0    811.0     22.6      6.2
Number of symbols                    1     1442       45        9
Number of variables                  0    11290      153       17
          ^                          0      263       18        2
          !                          0    10753      126        9
          ?                          0      496        8        2
Number of connectives                0    51044      558       47
Number of type connectives           0     5404       83       12
Maximal formula depth                2      359       36       11
Average formula depth                2      350       10        6

The TPTP Domain Structure
-------------------------
The domain structure of the TPTP is depicted below,  with counts of the numbers
of THF  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   126 /  128
 |                 |-- Henkin Models                    HEN     0 /    0
 |
 |-- Mathematics --|-- Set Theory                       SET   111 /  128
 |                 |-- Set Theory Continued             SEU   537 /  847
 |                 |-- Set Theory Continued             SEV   402 /  407
 |                 |-- 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
 |                 |             |-- Quantales          QUA    20 /   20
 |                 |             |-- 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 /   78
 |                 |-- Number Theory                    NUM   177 /  195
 |                 |-- Topology                         TOP     0 /    0
 |                 |-- Analysis                         ANA     0 /    0
 |                 |-- Geometry                         GEO     0 /    0
 |                 |-- Category Theory                  CAT     1 /    1
 |
 |-- Computer -----|-- Computing Theory                 COM     1 /    1
 |   Science       |-- Knowledge Representation         KRS     0 /    0
 |                 |-- Natural Language Processing      NLP     0 /    0
 |                 |-- Planning                         PLA     0 /    0
 |                 |-- Agents                           AGT    15 /   23
 |                 |-- Commonsense Reasoning            CSR    34 /   82
 |                 |-- Semantic Web                     SWB     0 /    0
 |                 |-- Data Structures                  DAT     1 /    2
 |                 |-- Software Creation                SWC     0 /    0
 |                 |-- Software Verification            SWV    23 /   37
 |                 |-- Software Verification Continued  SWW    10 /   28
 |
 |-- Science and --|-- Hardware Creation                HWC     0 /    0
 |   Engineering   |-- Hardware Verification            HWV     0 /    0
 |                 |-- Medicine                         MED     0 /    0
 |                 |-- Processes                        PRO     0 /    0
 |
 |-- Social -------|-- Social Choice Theory             SCT     3 /    9
 |   Sciences      |-- Management                       MGT     0 /    0
 |                 |-- Geography                        GEG    18 /   18
 |
 |-- Other --------|-- Arithmetic                       ARI     0 /    0
                   |-- Syntactic                        SYN    62 /   72
                   |-- Syntactic Continued              SYO   527 /  703
                   |-- Puzzles                          PUZ    50 /   53
                   |-- Miscellaneous                    MSC     3 /    3

