The sparsness of research into ATP systems for FOF problems meant that no electronic collections of FOF test problems had previously been commonly available. A CNF problem collection in electronic form was made publicly available by Argonne National Laboratories (in Otter format [McC94]) in 1988 [ANL]. This collection was a major source of problems for ATP researchers. Other electronic collections of CNF problems have been available, but not announced officially (e.g., that distributed with the SPRFN ATP system [SPRFN]). Although some of these collections provided significant support to researchers, and formed the early core of the TPTP library, none (with the possible exception of the ANL collection) was specifically designed to serve as a common basis for ATP research. Rather, these collections typically were built in the course of research into a particular ATP system. As a result there are several factors that limited their usefulness as a common basis for research. In particular, previously existing problem collections:

• were often hard to discover and obtain.
  System development and system evaluations typically relied on a small set of test problems, depending on the collections of problems available to the researcher.
• needed to be transformed to the syntax of the ATP system being considered.
  The problem format used in a collection was often inappropriate for the desired purpose, and a comparatively large effort was required just to make the problems locally usable (which in practice often meant that such collections of problems were simply ignored).
• were often limited in scope and size.
  The problems used were often homogeneous, and thus could not be used for broad testing of the capabilities of the ATP system under consideration. If there are too few problems, statistically significant testing is not possible.
• were often be outdated.
  The problems did not sufficiently reflect the current state-of-the-art in ATP research.
• were sometimes designed and tuned (regarding formula selection, formula ordering, and formula structure) for a particular ATP system.
  Using a collection designed and tuned for a particular ATP system leads to biases in results.
• provided no indication of the significance or difficulty of the problems.
  The significance and difficulty of a problem, with respect to the current state-of-the-art in ATP systems, is hard to assess by newcomers to the field. Existing test problems are often not adequate anymore (e.g., Schubert's Steamroller [Sti86]), while others might be solvable only with specialized techniques (e.g., LIM+ [Ble90]), and therefore are much too hard to start with.
• were inconsistent in their presentation of equally named problems.
  Copies and variants of the same "original" problem existed in different collections. This meant that unambiguous identification of problems, and therefore a clear interpretation of performance figures for given problems, was difficult.
• were usually undocumented.
  It was hard to obtain information on problem semantics, the original problem source, and the particular style of axiomatization. This also contributed to the problem of unambiguous problem identification.
• were almost always unserviced.
  Collections did not provide a mechanism for adding new problems or correcting errors in existing problems, and could be not be used to electronically distribute new and corrected problems to the ATP community. This in turn perpetuated the use of old and erroneous problems.
• provided no guidelines for their use.
  Quite often, inadequate system evaluations were performed. As a consequence, results that provided little indication of the system properties were reported.

The problem of meaningfully interpreting results can be even worse than indicated. A few problems might be selected and hand-tuned (formulae arranged in a special way, irrelevant formulae omitted, lemmas added in, etc) specifically for the ATP system being tested. The presentation of a problem can significantly affect the nature of the problem, and changing the formulae clearly makes a different problem altogether. Nevertheless the problem might be referenced under the same name as it was presented elsewhere. As a consequence the experimental results reveal little. Some researchers avoid this ambiguity by listing the formulae explicitly, but obviously this usually cannot be done for a large number of problems or for large individual problems. The only satisfactory solution to these issues is a common and stable library of problems. The TPTP is such a library.

What is Required?

• is easy to discover and obtain.
  Awareness of the TPTP is assured by extensive formal and informal announcements. The TPTP is available online, and is thus easily available to the research community.
• is easy to use.
  Problems are presented in a specifically designed, easy to understand format. Automatic conversion to other known formats is also provided, thus eliminating the necessity for any other transcription.
• spans a diversity of subject matters.
  This reduces biases in the development and testing of ATP systems, which arise from the use of a limited scope of problems. It also provides an overview of the domains in which ATP systems are used.
• is large enough for statistically significant testing.
  In contrast to common practice, an ATP system should be evaluated over a large number of problems, rather than a small set of judiciously selected examples. The large size of the TPTP makes this possible.
• is comprehensive.
  The TPTP contains most problems known to the community. There is no longer a need to look elsewhere.
• is up-to-date.
  As new problems appear in the literature and elsewhere, they are added to the TPTP as soon as possible.
• is independent of any particular ATP system.
  The problems are arranged so as to be modular and human-readable, rather than arranged for a particular ATP system.
• contains problems varying in difficulty, with a difficulty rating for each problem.
  The difficulty of problems in the TPTP ranges from very simple problems through to open problems. This allows all interested researchers, from newcomers to experts, to rely on the same problem library. The difficulty ratings provided with each problem are important for several reasons:
  1. It simplifies problem selection according to the user's intention.
  2. It allows the quality of an ATP system to be judged.
  3. Over the years, changes in the problem ratings will provide an indicator of the advancement in ATP.
• provides statistics for each problem and for the library as a whole.
  This provides information about the syntactic nature of the problems.
• has an unambiguous naming scheme.
  This provides unambiguous problem reference, and makes the comparison of results meaningful.
• is well structured and documented.
  This allows effective and efficient use of the library. Useful background information, such as an overview of ATP application domains, is provided.
• documents each problem.
  This contributes to the unambiguous identification of each problem.
• provides a mechanism for adding new problems.
  The TPTP contains standard axiomatizations that can be used in new problems. This simplifies the collection of new problems. A template is provided for submission of new problems. The TPTP is thus a channel for making new problems available to the community, in a simple and effective way.
• provides a mechanism for correcting errors in existing problems.
  All errors, noticed by the developers or reported by users, are corrected. Patched TPTP releases are made regularly.
• provides guidelines for its use in evaluating ATP systems.
  A standard library of problems together with evaluation guidelines makes reported results meaningful and reproducible by others. This will in turn simplify and improve system comparisons, and allow ATP researchers to accurately gauge their progress.

The development of the TPTP problem library is an ongoing project, with the aim to provide all of the desired properties.