Overall TFF Statistics
----------------------
Domains                    16
Abstract problems         825
Problems                  970
Problems with equality    675 (69%)
Pure equality problems    284 (29%)
Problems with arithmetic  846 (87%)
Theorem/Unsatisfiable     881 (90%)
CounterSat/Satisfiable     89 ( 9%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of formulae                   1     7092      218        1
% of unit formulae                  0%     100%      66%      73%
% of type formulae                  0%      91%      22%       0%
Number of atoms                      1    14794     1017        2
% of equality atoms                 0%     100%      44%      25%
  in problems with equality         3%     100%      63%      81%
Avg atoms per formula              1.0    894.9     71.3      1.6
Number of predicate symbols          1     1799       83        2
% of propositions                   0%     100%      48%      50%
Maximal predicate arity              1        4        1        2
Number of functors                   0     1126       45        4
% of constants                      0%     100%      71%      75%
% of arithmetic                     0%     100%      62%      75%
Maximal functor arity                0        8        1        2
Number of variables                  0    11616      364        2
          !                          0    11339      360        1
          ?                          0      279        3        0
Number of connectives                0    12398     1135        1
Number of type connectives           0     1571       40        0
Maximal formula depth                1      588       72        3
Average formula depth                1       67        8        2
Maximal term depth                   1       21        2        2
Average term depth                   1        3        1        1

The TPTP Domain Structure
-------------------------
The domain structure of the TPTP is depicted below,  with counts of the numbers
of TFF  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     0 /    0
 |                 |-- Henkin Models                    HEN     0 /    0
 |
 |-- Mathematics --|-- Set Theory                       SET     0 /    0
 |                 |-- Set Theory Continued             SEU     0 /    0
 |                 |-- Set Theory Continued             SEV     6 /    6
 |                 |-- Graph Theory                     GRA     0 /    0
 |                 |-- 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     0 /    0
 |                 |             |-- Kleene Algebra     KLE     0 /    0
 |                 |             |-- Groups             GRP     0 /    0
 |                 |             |-- Rings              RNG     0 /    0
 |                 |             |-- Fields             FLD     0 /    0
 |                 |             |-- Homological Alg    HAL     0 /    0
 |                 |             |-- General Algebra    ALG     0 /    0
 |                 |-- Number Theory                    NUM    68 /   80
 |                 |-- Topology                         TOP     0 /    0
 |                 |-- Analysis                         ANA     0 /    0
 |                 |-- Geometry                         GEO     1 /    1
 |                 |-- Category Theory                  CAT     0 /    0
 |
 |-- Computer -----|-- Computing Theory                 COM     3 /    4
 |   Science       |-- Knowledge Representation         KRS     1 /    1
 |                 |-- Natural Language Processing      NLP     0 /    0
 |                 |-- Planning                         PLA     0 /    0
 |                 |-- Agents                           AGT     0 /    0
 |                 |-- Commonsense Reasoning            CSR     0 /    0
 |                 |-- Semantic Web                     SWB     0 /    0
 |                 |-- Data Structures                  DAT    55 /   55
 |                 |-- Software Creation                SWC     0 /    0
 |                 |-- Software Verification            SWV     4 /    4
 |                 |-- Software Verification Continued  SWW   105 /  123
 |
 |-- Science and --|-- Hardware Creation                HWC     0 /    0
 |   Engineering   |-- Hardware Verification            HWV    13 /   104
 |                 |-- Medicine                         MED     0 /    0
 |                 |-- Processes                        PRO     0 /    0
 |
 |-- Social -------|-- Social Choice Theory             SCT     3 /    9
 |   Sciences      |-- Management                       MGT     0 /    0
 |                 |-- Geography                        GEG     5 /    5
 |
 |-- Other --------|-- Arithmetic                       ARI   545 /  557
                   |-- Syntactic                        SYN     1 /    3
                   |-- Syntactic Continued              SYO     6 /    7
                   |-- Puzzles                          PUZ     7 /    9
                   |-- Miscellaneous                    MSC     2 /    2

