Overall Statistics
------------------                        THF           TFF
                                          FOF           CNF
Domains                     53       :     33 (62%) +    19 (35%) +
                                           41 (77%) +    40 (75%)
Abstract problems        14705       :   2991 (20%) +  1877 (12%) +
                                         5648 (38%) +  6224 (42%)
Problems                 22686       :   3854 (16%) +  2084 ( 9%) +
                                         8630 (38%) +  8118 (35%)
Problems with equality   17535 (77%) :   3136 (81%) +  1737 (83%) +
                                         6811 (78%) +  5851 (72%)
Pure equality problems    2670 (11%) :      0 ( 0%) +   339 (16%) +
                                          372 ( 4%) +  1959 (24%)
Theorem/Unsatisfiable    18091 (79%) :   3262 (84%) +  1667 (79%) +
                                         7094 (82%) +  6068 (74%)
CounterSat/Satisfiable   2807 (12%) :     398 (10%) +   118 ( 5%) +
                                         1061 (12%) +  1230 (15%)

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 /  240
 |                 |-- Logic Calculi                    LCL   918 / 1412
 |                 |-- Henkin Models                    HEN    13 /   68
 |
 |-- Mathematics --|-- Set Theory                       SET   967 / 1413
 |                 |-- Set Theory Continued             SEU   970 / 1754
 |                 |-- Set Theory Continued             SEV   496 /  503
 |                 |-- Graph Theory                     GRA    75 /  127
 |                 |-- Algebra --|-- Relation Algebra   REL    53 /  221
 |                 |             |-- Boolean Algebra    BOO   105 /  143
 |                 |             |-- Robbins Algebra    ROB    34 /   46
 |                 |             |-- Left Distributive  LDA    41 /   50
 |                 |             |-- Lattices           LAT   396 /  738
 |                 |             |-- Quantales          QUA    21 /   21
 |                 |             |-- Kleene Algebra     KLE   182 /  250
 |                 |             |-- Groups             GRP   781 / 1094
 |                 |             |-- Rings              RNG   128 /  266
 |                 |             |-- Fields             FLD   101 /  281
 |                 |             |-- Linear Algebra     LIN    15 /   15
 |                 |             |-- Homological Alg    HAL     7 /   10
 |                 |             |-- Real Algebra       RAL    70 /   70
 |                 |             |-- General Algebra    ALG   444 /  549
 |                 |-- Number Theory                    NUM   953 / 1572
 |                 |-- Number Theory Continued          NUN    92 /  135
 |                 |-- Topology                         TOP    48 /  131
 |                 |-- Analysis                         ANA   129 /  180
 |                 |-- Geometry                         GEO   538 /  860
 |                 |-- Category Theory                  CAT    38 /  135
 |
 |-- Computer -----|-- Computing Theory                 COM   211 /  238
 |   Science       |-- Knowledge Representation         KRS   291 /  305
 |                 |-- Natural Language Processing      NLP   263 /  550
 |                 |-- Planning                         PLA    52 /   89
 |                 |-- Agents                           AGT    42 /   77
 |                 |-- Commonsense Reasoning            CSR   306 / 1030
 |                 |-- Semantic Web                     SWB   108 /  217
 |                 |-- Data Structures                  DAT   330 /  332
 |                 |-- Software Creation                SWC   424 /  847
 |                 |-- Software Verification            SWV   998 / 1452
 |                 |-- Software Verification Continued  SWW   880 /  988
 |
 |-- Science and --|-- Biology                          BIO     4 /    4
 |   Engineering   |-- Hardware Creation                HWC     4 /    6
 |                 |-- Hardware Verification            HWV   134 /  511
 |                 |-- Medicine                         MED    12 /   12
 |                 |-- Processes                        PRO    28 /   82
 |                 |-- Products                         PRD     3 /    3
 |
 |-- Social -------|-- Social Choice Theory             SCT   265 /  300
 |   Sciences      |-- Management                       MGT    67 /  157
 |                 |-- Geography                        GEG    24 /   24
 |
 |-- Arts and -----|-- Philosophy                       PHI    15 /   24
 |   Humanities
 |
 |-- Other --------|-- Arithmetic                       ARI   681 /  693
                   |-- Syntactic                        SYN   986 / 1313
                   |-- Syntactic Continued              SYO   661 /  881
                   |-- Puzzles                          PUZ   147 /  216
                   |-- Miscellaneous                    MSC    33 /   51