Overall TPTP Statistics
-----------------------
Number of domains                     23
Number of abstract problems         1577
Number of problems                  2295       : 111 Pr ( 5%)  + 2184 NP (95%)
Number of non-Horn problems         1449 (63%) :  56 Pr (50%') : 1393 NP (64%")
Number of problems with equality    1805 (79%) :               : 1805 NP (83%")
Total number of clauses           322156       : (' = % of Pr) : (" = % of NP)
Total number of literals          970456


Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of clauses              2   6404   124    68       2   8192   444    36
% of non-Horn clauses         0%    99%    6%    4%      0%    99%   20%    1%
  in non-Horn problems        0%    99%    9%    4%      1%    99%   40%   45%
% of unit clauses             0%   100%   32%   22%      0%   100%   16%    1%
Number of literals             2  18966   276   162       2 106496  3303   132
% of equality literals        0%   100%   47%   47%
  in equality problems        4%   100%   57%   47%
Av literals per clause       1.0    8.0   2.0   2.0     1.0   13.0   3.4   2.7 
Number of predicate symbols    1   4042    12     4       1    840    69    13
Number of function symbols     0     94    27    13
% of constants                0%   100%   46%   33%
Number of variables            0  32000   311   271
% of singletons               0%   100%    6%    7%
Maximal clause size            1     25     4     5       1     21     5     3
Maximal term depth             0     51     4     6


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.

     Field                  Subfields                    Prefix   Probs / Vers
 -----------------------------------------------------------------------------

 |-- logic -------------|-- combinatory logic               COL      66 /  105
 |                      |-- logic calculi                   LCL     168 /  188
 |                      |-- henkin models                   HEN      12 /   64
 |
 |-- mathematics -------|-- set theory                      SET     567 /  700
 |                      |
 |                      |-- graph theory                    GRA       1 /    1
 |                      |
 |                      |-- algebra --|-- boolean algebra   BOO      17 /   36
 |                      |             |-- robbins           ROB      25 /   34
 |                      |             |-- left dist've      LDA      14 /   23
 |                      |             |-- lattices          LAT       5 /    7
 |                      |             |-- groups            GRP     112 /  145
 |                      |             |-- rings             RNG      40 /  100
 |                      |             |-- general algebra   ALG       2 /    4
 |                      |
 |                      |-- number theory                   NUM     284 /  321
 |                      |
 |                      |-- topology                        TOP      19 /   24
 |                      |
 |                      |-- analysis                        ANA       5 /   17
 |                      |
 |                      |-- geometry                        GEO      77 /  161
 |                      |
 |                      |-- category theory                 CAT      19 /   59
 |
 |-- computer science --|-- computing theory                COM       3 /    4
 |                      |-- planning                        PLA       3 /    4
 |                      |-- program verification            PRV       9 /    9
 |
 |-- other -------------|-- syntactic                       SYN      88 /  203
                        |-- puzzles                         PUZ      33 /   44
                        |-- miscellaneous                   MSC       8 /   42

