Overall TPTP Statistics
-----------------------
Number of domains                     25
Number of abstract problems         2044
Number of generic problems            85
Number of problems                  2752       : 2710 NP (98%) +   42 Pr ( 2%)
Number of non-Horn problems         1486 (54%) : 1456 NP (53%) +   30 Pr ( 1%)
Number of range rest. problems       105 ( 4%) :   63 NP ( 2%) +   42 Pr ( 2%)
Number of problems with equality    1920 (70%)
Number of pure equality problems     493 (18%)
Number of satisfiable problems >=     59 ( 2%) :   53 NP ( 2%) +    6 Pr ( 0%)
Number of standard problems         1898 (69%) : 1893 NP (69%) +    5 Pr ( 0%)
Total number of clauses           323074
Total number of literals          743104


Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of clauses              2    504   118    54       3     82    24    18
% of non-Horn clauses         0%    99%    5%    4%      0%    81%   25%   25%
  in non-Horn problems        2%    99%    9%    5%      8%    81%   35%   33%
% of unit clauses             0%   100%   34%   22%      0%   100%   19%   13%
% of range rest. clauses      0%   100%   60%   63%
Number of literals             2   1512   273   129       4    232    64    40
% of equality literals        0%   100%   43%   46%
  in equality problems       19%   100%   61%   47%
Av literals per clause       1.0    8.0   2.0   2.1     1.0    5.0   2.4   2.4 
Maximal clause size            1     25     4     5       1     11     3     3
Number of predicate symbols    1     48     9     3       2     63    13    11
% of propositions             0%    67%    0%    0%
Minimal predicate arities      0      5     1     1
Maximal predicate arities      1     10     2     3
Number of functors             1     93    23     9
% of constants                0%   100%   50%   50%
Minimal functor arities        0      2     0     0
Maximal functor arities        0      8     2     2
Number of variables            0   1094   269   130
% of singletons               0%   100%    8%    7%
Maximal term depth             1     14     4     4


The TPTP Domain Structure
-------------------------
The domain structure of the TPTP is depicted below,  with counts of the numbers
of problems  and versions in each domain.  The prefixes name  subdirectories in
the Problems directory, and prefix the problem names in that directory.

                                                    Domain    # of Problems
     Field             Subfield                     Prefix  Abst / Vers / Gen
 ----------------------------------------------------------------------------

 |-- Logic --------|-- Combinatory Logic               COL    81 /  141 /   0
 |                 |-- Logic Calculi                   LCL   256 /  278 /   0
 |                 |-- Henkin Models                   HEN    12 /   64 /   0
 |
 |-- Mathematics --|-- Set Theory                      SET   562 /  695 /   0
 |                 |
 |                 |-- Graph Theory                    GRA     1 /    1 /   0
 |                 |
 |                 |-- Algebra --|-- Boolean Algebra   BOO    19 /   52 /   0
 |                 |             |-- Robbins           ROB    27 /   36 /   0
 |                 |             |-- Left Distributive LDA    14 /   23 /   0
 |                 |             |-- Lattices          LAT     5 /   10 /   0
 |                 |             |-- Groups            GRP   193 /  313 /  50
 |                 |             |-- Rings             RNG    40 /  100 /   0
 |                 |             |-- General Algebra   ALG     2 /    4 /   0
 |                 |
 |                 |-- Number Theory                   NUM   285 /  309 /   2
 |                 |
 |                 |-- Topology                        TOP    19 /   24 /   0
 |                 |
 |                 |-- Analysis                        ANA     5 /   19 /   0
 |                 |
 |                 |-- Geometry                        GEO    78 /  165 /   0
 |                 |
 |                 |-- Category Theory                 CAT    19 /   58 /   0
 |
 |-- Computer -----|-- Computing Theory                COM     4 /    6 /   0
 |   Science       |-- Planning                        PLA    23 /   30 /   0
 |                 |-- Program Verification            PRV     9 /    9 /   0
 |
 |-- Engineering --|-- Circuit Design                  CID     3 /    4 /   0
 |                 |-- Circuit Verification            CIV     4 /    4 /   0
 |
 |-- Other --------|-- Syntactic                       SYN   340 /  350 /  27
                   |-- Puzzles                         PUZ    34 /   45 /   3
                   |-- Miscellaneous                   MSC     9 /   12 /   3
