Overall Statistics
------------------                         THF           TFF
                                           FOF           CNF
Domains                     47       :     22 (46%) +    16 (34%) +
                                           36 (76%) +    34 (72%)
Abstract problems        12402       :   2223 (17%) +   825 ( 6%) +
                                         4865 (39%) +  5963 (48%)
Problems                 19459       :   2929 (15%) +   970 ( 4%) +
                                         7807 (40%) +  7753 (39%)
Problems with equality   14526 (74%) :   2215 (75%) +   675 (69%) +
                                         6064 (77%) +  5572 (71%)
Pure equality problems    2468 (12%) :      0 ( 0%) +   284 (29%) +
                                          368 ( 4%) +  1816 (23%)
Theorem/Unsatisfiable    15834 (81%) :   2366 (80%) +   881 (90%) +
                                         6799 (87%) +  5788 (74%)
CounterSat/Satisfiable    2405 (12%) :    349 (11%) +    89 ( 9%) +
                                          877 (11%) +  1090 (14%)

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  # Problems
     Field             Subfield                      Prefix  Abst / Vers
 -----------------------------------------------------------------------

 |-- Logic --------|-- Combinatory Logic                COL   121 /  239
 |                 |-- Logic Calculi                    LCL   871 / 1217
 |                 |-- Henkin Models                    HEN    13 /   67
 |
 |-- Mathematics --|-- Set Theory                       SET   967 / 1396
 |                 |-- Set Theory Continued             SEU   970 / 1753
 |                 |-- Set Theory Continued             SEV   408 /  413
 |                 |-- Graph Theory                     GRA    74 /  126
 |                 |-- Algebra --|-- Relation Algebra   REL    52 /  218
 |                 |             |-- Boolean Algebra    BOO   105 /  140
 |                 |             |-- Robbins Algebra    ROB    34 /   45
 |                 |             |-- Left Distributive  LDA    40 /   49
 |                 |             |-- Lattices           LAT   394 /  731
 |                 |             |-- Quantales          QUA    20 /   20
 |                 |             |-- Kleene Algebra     KLE   170 /  229
 |                 |             |-- Groups             GRP   781 / 1091
 |                 |             |-- Rings              RNG   128 /  263
 |                 |             |-- Fields             FLD    99 /  279
 |                 |             |-- Homological Alg    HAL     6 /    9
 |                 |             |-- General Algebra    ALG   442 /  534
 |                 |-- Number Theory                    NUM   880 / 1237
 |                 |-- Topology                         TOP    48 /  131
 |                 |-- Analysis                         ANA    42 /   91
 |                 |-- Geometry                         GEO   350 /  672
 |                 |-- Category Theory                  CAT    38 /  131
 |
 |-- Computer -----|-- Computing Theory                 COM    24 /   50
 |   Science       |-- Knowledge Representation         KRS   271 /  272
 |                 |-- Natural Language Processing      NLP   262 /  520
 |                 |-- Planning                         PLA    31 /   51
 |                 |-- Agents                           AGT    41 /   75
 |                 |-- Semantic Web                     SWB   108 /  204
 |                 |-- Commonsense Reasoning            CSR   153 /  866
 |                 |-- Data Structures                  DAT    56 /   57
 |                 |-- Software Creation                SWC   423 /  846
 |                 |-- Software Verification            SWV   998 / 1390
 |                 |-- Software Verification Continued  SWW   412 /  514
 |
 |-- Science and --|-- Hardware Creation                HWC     4 /    6
 |   Engineering   |-- Hardware Verification            HWV    52 /   251
 |                 |-- Medicine                         MED    11 /   11
 |                 |-- Processes                        PRO    18 /   72
 |
 |-- Social -------|-- Social Choice Theory             SCT   171 /  204
 |   Sciences      |-- Management                       MGT    66 /  156
 |                 |-- Geography                        GEG    24 /   24
 |
 |-- Other --------|-- Arithmetic                       ARI   545 /  557
                   |-- Syntactic                        SYN   986 / 1294
                   |-- Syntactic Continued              SYO   534 /  722
                   |-- Puzzles                          PUZ   136 /  200
                   |-- Miscellaneous                    MSC    23 /   36

