Synopsis

Overall Statistics
------------------                         THF           TFF
                                           FOF           CNF
Domains                     55       :     36 (65%) +    29 (52%) +
                                           43 (78%) +    42 (76%)
Abstract problems        15888       :   3549 (22%) +  2439 (15%) +
                                         6033 (37%) +  6312 (39%)
Problems                 25775       :   5042 (19%) +  3297 (12%) +
                                         9091 (35%) +  8345 (32%)
Problems with equality   20172 (78%) :   4310 (85%) +  2670 (80%) +
                                         7122 (78%) +  6070 (72%)
Non-classical problems     147 ( 0%) :     15 ( 0%) +   132 ( 4%) +
                                            0 ( 0%) +     0 ( 0%)
Theorem/Unsat/ContraAx   20891 (81%) :   4338 (86%) +  2575 (78%) +
                                         7709 (84%) +  6269 (75%)
CounterSat/Satisfiable    3275 (12%) :    444 ( 8%) +   290 ( 8%) +
                                         1239 (13%) +  1302 (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   132 /  254
 |                 |-- Logic Calculi                    LCL   958 / 1516
 |                 |-- Henkin Models                    HEN    13 /   68
 |
 |-- Mathematics --|-- Set Theory                       SET   967 / 1429
 |                 |-- Set Theory Continued             SEU   970 / 1770
 |                 |-- Set Theory Continued             SEV   506 /  513
 |                 |-- Graph Theory                     GRA   116 /  175
 |                 |-- Algebra --|-- Relation Algebra   REL    53 /  223
 |                 |             |-- MV Algebras        MVA    15 /   15
 |                 |             |-- Boolean Algebra    BOO   105 /  150
 |                 |             |-- Robbins Algebra    ROB    34 /   48
 |                 |             |-- Left Distributive  LDA    41 /   50
 |                 |             |-- Lattices           LAT   401 /  758
 |                 |             |-- Quantales          QUA    21 /   21
 |                 |             |-- Kleene Algebra     KLE   182 /  257
 |                 |             |-- Groups             GRP   821 / 1207
 |                 |             |-- Rings              RNG   128 /  268
 |                 |             |-- Fields             FLD   101 /  281
 |                 |             |-- Linear Algebra     LIN    15 /   15
 |                 |             |-- Homological Alg    HAL     7 /   10
 |                 |             |-- Real Algebra       RAL    70 /   70
 |                 |             |-- General Algebra    ALG   444 /  551
 |                 |-- Number Theory                    NUM   953 / 1633
 |                 |-- Number Theory Continued          NUN   135 /  178
 |                 |-- Topology                         TOP    53 /  136
 |                 |-- Analysis                         ANA   140 /  209
 |                 |-- Geometry                         GEO   659 /  982
 |                 |-- Category Theory                  CAT    38 /  136
 |
 |-- Computer -----|-- Computing Theory                 COM   211 /  242
 |   Science       |-- Knowledge Representation         KRS   291 /  306
 |                 |-- Natural Language Processing      NLP   266 /  601
 |                 |-- Planning                         PLA    59 /  112
 |                 |-- Agents                           AGT    42 /   77
 |                 |-- Commonsense Reasoning            CSR   306 / 1054
 |                 |-- Semantic Web                     SWB   109 /  233
 |                 |-- Interactive Theorem Proving      ITP   414 / 1601
 |                 |-- Data Structures                  DAT   333 /  348
 |                 |-- Software Creation                SWC   534 /  957
 |                 |-- Software Verification            SWV   998 / 1457
 |                 |-- Software Verification Continued  SWW   904 / 1041
 |
 |-- Science and --|-- Biology                          BIO     6 /    6
 |   Engineering   |-- Hardware Creation                HWC     4 /    6
 |                 |-- Hardware Verification            HWV   134 /  548
 |                 |-- Medicine                         MED    12 /   12
 |                 |-- Processes                        PRO    33 /   87
 |                 |-- Products                         PRD     3 /    3
 |
 |-- Social -------|-- Social Choice Theory             SCT   265 /  309
 |   Sciences      |-- Management                       MGT    67 /  158
 |                 |-- Geography                        GEG    24 /   24
 |
 |-- Arts and -----|-- Philosophy                       PHI    45 /   62
 |   Humanities
 |
 |-- Other --------|-- Arithmetic                       ARI   681 /  693
                   |-- Syntactic                        SYN   986 / 1332
                   |-- Syntactic Continued              SYO   901 / 1293
                   |-- Puzzles                          PUZ   149 /  237
                   |-- Miscellaneous                    MSC    33 /   53