Overall CNF Statistics
----------------------
Domains                     30
Abstract problems         4824
Problems                  6346
Problems with equality    4171 (65%)
Pure equality problems    1304 (20%)
Theorem/Unsatisfiable     4600 (72%)
CounterSat/Satisfiable     824 (12%)
Non-Horn problems         3825 (33%)
Range rest. problems       702 ( 6%)
Unit equality problems     863 ( 7%)

Problem-by-problem                 Min      Max      Avg      Med
------------------                 ------------------------------
Number of clauses                    1     3240      179       34
% of unit clauses                   0%     100%      45%      34%
% of non-Horn clauses               0%      99%      12%       7%
  in non-Horn problems              1%      99%      21%      11%
% of range rest. clauses            0%     100%      69%      75%
Number of literals                   1   127126      833       82
% of equality literals              0%     100%      29%      16%
  in equality problems              0%     100%      45%      22%
Maximal clause size                  1      901        8        5
Average clause size                  1       40        2        2
Number of predicate symbols          1     1817       23        4
% of propositions                   0%     100%       2%       0%
Maximal predicate arity              0       56        3        2
Number of functors                   0      903       31       10
% of constants                      0%     100%      49%      50%
Maximal functor arity                0       18        2        2
Number of variables                  0   120428      713       66
Maximal term depth                   0       85        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   121 /  239
 |                 |-- Logic Calculi                    LCL   444 /  566
 |                 |-- Henkin Models                    HEN    13 /   67
 |
 |-- Mathematics --|-- Set Theory                       SET   615 /  800
 |                 |-- Set Theory Continued             SEU     0 /    0
 |                 |-- Graph Theory                     GRA     1 /    1
 |                 |-- Algebra --|-- Boolean Algebra    BOO   104 /  139
 |                 |             |-- Robbins Algebra    ROB    31 /   40
 |                 |             |-- Left Distributive  LDA    14 /   23
 |                 |             |-- Lattices           LAT   280 /  310
 |                 |             |-- Groups             GRP   615 /  792
 |                 |             |-- Rings              RNG    42 /  104
 |                 |             |-- Fields             FLD    99 /  279
 |                 |             |-- Homological Alg    HAL     0 /    0
 |                 |             |-- General Algebra    ALG    13 /   15
 |                 |-- Number Theory                    NUM   289 /  315
 |                 |-- Topology                         TOP    19 /   24
 |                 |-- Analysis                         ANA    42 /   91
 |                 |-- Geometry                         GEO   162 /  253
 |                 |-- Category Theory                  CAT    20 /   62
 |
 |-- Computer -----|-- Computing Theory                 COM     9 /   14
 |   Science       |-- Knowledge Representation         KRS    17 /   17
 |                 |-- Natural Language Processing      NLP   258 /  258
 |                 |-- Planning                         PLA    26 /   40
 |                 |-- Agents                           AGT     0 /    0
 |                 |-- Commonsense Reasoning            CSR     0 /    0
 |                 |-- Software Creation                SWC   423 /  423
 |                 |-- Software Verification            SWV   153 /  342
 |
 |-- Science and --|-- Hardware Creation                HWC     4 /    6
 |   Engineering   |-- Hardware Verification            HWV    38 /   83
 |                 |-- Medicine                         MED     0 /    0
 |
 |-- Social -------|-- Management                       MGT    66 /   78
 |   Sciences
 |
 |-- Other --------|-- Syntactic                        SYN   829 /  842
                   |-- Puzzles                          PUZ    67 /  102
                   |-- Miscellaneous                    MSC    10 /   21
