The TPTP Problem Library

Abstract

• the motivations for building the library;
• a discussion of the inadequacies of previous problem collections, and how these have been resolved in the TPTP;
• a description of the library structure, including overview information;
• descriptions of supplementary utility programs;
• guidelines for obtaining and using the library.

Table of Contents

• Introduction
• Inside the TPTP
  • The Domain Structure
  • Problem Versions and Standard Axiomatizations
  • Problem Generators
  • Problem and Axiomatization Naming
  • Problem Presentation
    • Header Section
    • Include Section
    • Formulae Section
  • The Arithmetic System
  • The Non-classical Logics
  • Physical Organization
• Utilities
  • TPTP2X
  • TPTP4X
  • TPTP2T
• Getting and Using the TPTP
• Conclusion

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.

Current Limitations of the TPTP.
The TPTP library currently limited to problems expressed in classical logic.

• 15888 abstract problems, which result in 25775 ATP problems (due to alternative presentations and Problem Generators).
• 25628 problems in classical logic, and 147 problems in non-classical logic
• 20172 problems with equality
• 3549 THF abstract problems, which result in 5042 THF ATP problems
• 2439 TFF abstract problems, which result in 3297 TFF ATP problems, of which 436 are TXF problems
• 6033 FOF abstract problems, which result in 9091 FOF ATP problems
• 6312 CNF abstract problems, which result in 8345 CNF ATP problems

The problems in the TPTP are syntactically diverse, as is indicated by the ranges of the values in the tables. The problems in the TPTP are also semantically diverse, as is indicated by the range of domains that are covered. The problems are grouped into domains, covering topics in the fields of logic, mathematics, computer science, engineering, social sciences, arts and humanities, and others.

Sources
The problems have been collected from various sources. Early sources were existing electronic problem collections and the ATP literature. Other sources include logic programming, mathematics, puzzles, and correspondence with ATP researchers. Many people and organizations have contributed towards the TPTP: the foundations of the TPTP were laid with David Plaisted's SPRFN collection; many problems were taken from Argonne National Laboratory's ATP problem library (special thanks to Bill McCune here); Art Quaife provided several hundred problems in set theory and algebra; the Journal of Automated Reasoning, CADE Proceedings, and Association for Automated Reasoning Newsletters have provided a wealth of material; many problems have been provided by ATP users and system developers (see the Acknowledgements).

Releases
The TPTP is managed in the manner of a software product, in the sense that fixed releases are made. Each release of the TPTP is identified by a release number, in the form vVersion.Edition.Patch level. The Version number enumerates major new releases of the TPTP, in which important new features have been added. The Edition number is incremented each time new problems are added to the current version. The Patch level is incremented each time errors, found in the current edition, are corrected. All non-trivial changes are recorded in a history file, as well as in the file for an affected problem.

An attempt has been made to classify the totality of the TPTP problems in a systematic and natural way. The resulting domain scheme reflects the natural hierarchy of scientific domains, as presented in standard subject classification literature. The current classification is based mainly on the Dewey Decimal Classification (DDC) [CB+89] and the Mathematics Subject Classification (MSC) [MSC92] used for the Mathematical Reviews by the American Mathematical Society. Seven fields are defined: logic, mathematics, computer science, engineering, social sciences, arts and humanities, and other. Each field contains further subdivisions, called domains. Each domain is identified by a three-letter mnemonic. These mnemonics are also part of the TPTP problem naming scheme. The TPTP domains constitute the basic units of the classification. The full classification scheme is shown in Figure  The Domain Structure of the TPTP, and the numbers of abstract problems, problems, and generic problems in each domain are shown in the TPTP document OverallSynopsis

• AGT Agents.
  An agent is an autonomous software component of a computer program, typically designed to act intelligently and communicate with other agents.
  Indices: DDC ???; MSC 68T35.
  References: General [RN95]; ATP --.
• ALG Algebra.
  Algebra is a branch of mathematics concerning the study of structure, relation, and quantity. An algebra is a set with a system of operations defined on it.
  Indices: DDC 512; MSC 06XX, 20XX.
  References: General [Bou89, BM65, BB70]; ATP --.
• ARI Arithmetic.
  Arithmetic problems that do arithmetic computations (but do not reason about arithmetic (see the NUM domain).
  Indices: DDC 513; MSC 97FXX.
  References: General [Hig10]; ATP [Sim86].
• ANA Analysis.
  Analysis is a branch of mathematics concerned with functions and limits. The main parts of analysis are differential calculus, integral calculus, and the theory of functions.
  Indices: DDC 515; MSC 26XX.
  References: General [Ros90]; ATP [Ble90].
• BIO Biology.
  Biology is a natural science concerned with the study of life and living organisms, including their structure, function, growth, evolution, distribution, and taxonomy.
  Indices: DDC 570; MSC 92XX.
  References: General [RU+13]; ATP [CC+13, CDI13].
• BOO Boolean Algebra.
  A Boolean algebra is a set of elements with two binary operations that are idempotent, commutative, and associative. These operations are mutually distributive, there exist universal bounds 0, 1, and there is a unary operation of complementation.
  Indices: DDC 511.324, 512.89; MSC 06EXX.
  References: General [Whi61, BM65, BB70]; ATP --.
• CAT Category Theory.
  A category is a mathematical structure together with the morphisms that preserve this structure.
  Indices: DDC 512.55; MSC 18XX.
  References: General [Mac71]; ATP [MOW76].
• COL Combinatory Logic.
  Combinatory logic is about applying one function to another. It can be viewed as an alternative foundation of mathematics (or, due to its Turing-completeness, as a programming language). More formally, it is a system satisfying two combinators and satisfying reflexivity, symmetry, transitivity, and two equality substitution axioms for the function that exists implicitly for applying one combinator to another.
  Indices: DDC 510.101; MSC 03B40.
  References: General [CF58, CHS72, Bar81]; ATP [WM88].
• COM Computing Theory.
  Computing theory is a subfield of computer science dealing with theoretical issues such as decidability (whether or not a given problem admits an algorithmic solution), completeness (does an algorithm always find a solution if one exists?), correctness (are only solutions produced?), and computational complexity (the resource requirements of algorithms).
  Indices: DDC 004-006; MSC 68XX.
  References: General [HU79]; ATP --.
• CSR Commonsense Reasoning.
  Commonsense reasoning is the branch of artificial intelligence concerned with replicating human thinking. There are several components to this problem, including: developing adequately broad and deep commonsense knowledge bases; developing reasoning methods that exhibit the features of human thinking, including the ability to reason with knowledge that is true by default, the ability to reason rapidly across a broad range of domains, and the ability to tolerate uncertainty in your knowledge; developing new kinds of cognitive architectures that support multiple reasoning methods and representations.
  Indices: DDC 121.3; MSC 68TXX.
  References: General [Sha97]; ATP [Lif95, McC59, SME04]
• DAT Data Structures.
  A data structure is a particular way of storing and organizing data in a computer so that it can be used efficiently.
  Indices: DDC 005.73; MSC 68P05.
  References: General [AHU87]; ATP --.
• FLD Field Theory.
  A field is ring (see below) in which the * operation is commutative, and for which there is an identity element in G, and for which each non-identity element of G has an inverse in G.
  Indices: DDC 512.32; MSC 12XX.
  References: General [Ada82]; ATP [Dra93].
• GEG Geography.
  Geography is the study of the Earth and its lands, features, inhabitants, and phenomena.
  Indices: DDC 910; MSC 91C99.
  References: General [NGS99]; ATP --.
• GEO Geometry.
  Geometry is a branch of mathematics that deals with the measurement, properties, and relationships of points, lines, angles, surfaces, and solids.
  Indices: DDC 516; MSC 51.
  References: General [Tar51, Tar59]; ATP [Qua92].
• GRA Graph Theory.
  A graph consists of a finite non-empty set of vertices together with a prescribed set of edges, each edge connecting a pair of vertices.
  Indices: DDC 510.09; MSC 05CXX, 68R10.
  References: General [Har69, BB70]; ATP --.
• GRP Group Theory.
  A group is a set G and a binary operation +:GxG -> G which is associative, and for which there is an identity element in G, and for which each element of G has an inverse in G.
  Indices: DDC 512.2; MSC 20
  References: General [Bou89, BM65]; ATP [MOW76].
• HAL Homological Algebra.
  Homological algebra is an abstract algebra concerned with results valid for many different kinds of spaces. Modules are the basic tools used in homological algebra.
  Indices: DDC 512.55; MSC 18XX.
  References: General [Wei94]; ATP --.
• HEN Henkin Models.
  Henkin models provide a generalized semantics for higher order logics. This leads to a larger class of models and, as a consequence, fewer true sentences. However, in contrast to standard semantics, complete and correct calculi can be found.
  Indices: DDC 160; MSC 03CXX.
  References: General [Hen50, Leb83]; ATP --.
• HWC Hardware Creation.
  Computer hardware is created by inter-connecting logic gates. Hardware creation is used to form a circuit that will transform given input patterns to required output patterns.
  Indices: DDC 621.395; MSC 94CXX.
  References: General [Hay93]; ATP [WW83].
• HWV Hardware Verification.
  Hardware verification is used to ensure that a previously designed circuit performs the desired transformation of input patterns to required output patterns. One approach is to check the performance of the circuit for every possible combination of given inputs. Other techniques are also used.
  Indices: DDC 621.395; MSC 94CXX.
  References: General [Hay93]; ATP [Woj83].
• ITP Interactive Theorem Proving.
  An interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
  Indices:
  References: General [Wie06, Geu09]; ATP [Urb06, BG+19].
• KLE Kleene Algebra.
  A Kleene Algebra is a bounded distributive lattice with an involution satisfying De Morgan's laws, and the inequality x∧−x ≤ y∨−y. Alternatively, a Kleene Algebra is an algebraic structure that generalizes the operations known from regular expressions.
  Indices: DDC 512.74; MSC 06A99
  References: General [Koz90, BMS03]; ATP [HS07].
• KRS Knowledge Representation.
  Knowledge Representation is concerned with writing down descriptions that can be manipulated by a machine.
  Indices: DDC 006.3; MSC 68T30.
  References: General [BL85, CM87]; ATP --.
• LAT Lattice Theory.
  A lattice is a set of elements, with two binary operations which are idempotent, commutative, and associative, and which satisfy the absorption law.
  Indices: DDC 512.865; MSC 06BXX.
  References: General [BM65]; ATP [McC88].
• LCL Logic Calculi.
  A logic calculus defines axioms and rules of inference that can be used to prove theorems. Indices: DDC 511.3; MSC 03XX. References: General [Luk63]; ATP [MW92].
• LDA Left Distributive Algebra.
  LD-algebras are related to large cardinals. Under a very strong large cardinal assumption, the free-monogenic LD-algebra can be represented by an algebra of elementary embeddings. Theorems about this algebra can be proven from a small number of properties, suggesting the definition of an embedding algebra.
  Indices: DDC 512; MSC 20N02, 03E55, 08B20
  References: General --; ATP [Jec93].
• LIN Linear Algebra.
  Linear algebra is the branch of mathematics concerning vector spaces and linear mappings between such spaces. Indices: DDC 512.5; MSC 15Axx.
  References: General [LH+01]; ATP --.
• MVA MV Algebras.
  An MV algebra is an algebraic structure with a binary "plus" operation, a unary "negate" operation, and the constant 0, satisfying certain axioms. Indices: DDC 512; MSC 03G20
  References: General [Mun11, GT75]; ATP --.
• MED Medicine.
  The science of diagnosing and treating illness, disease, and injury.
  Indices: DDC 610; MSC --.
  References: General [LH+01]; ATP [HLB05].
• MGT Management.
  Management is the study of systems, and their use and production of resources.
  Indices: DDC 302-303; MSC 90XX.
  References: General --; ATP [PM94, PB+94].
• MSC Miscellaneous.
  A collection of problems which do not fit well into any other domain.
• NLP Natural Language Processing.
  Natural language processing considers the automated generation and comprehension of languages used by humans.
  Indices: DDC 006.3; MSC 68T50
  References: General [Obe89i, GWS86]; ATP [Bos00].
• NUM Number Theory.
  Number theory is the study of integers and their properties.
  Indices: DDC 512.7; MSC 11YXX.
  References: General [HW92]; ATP [Qua92].
• PHI Philosophy.
  Philosophy is the study of general and fundamental problems, such as those connected with reality, existence, knowledge, values, reason, mind, and language.
  Indices: DDC 100; MSC -
  References: General [TE99]; ATP -.
• PLA Planning.
  Planning is the process of determining the sequence of actions to be performed by an agent, to reach a specified desired state from a specified initial state.
  Indices: DDC 006.3; MSC 68T99.
  References: General [AK+91]; ATP [Pla81, Pla82].
• PRO Processes.
  Process information includes production scheduling, process planning, workflow, business process reengineering, simulation, process realization process modeling, and project management.
  Indices: DDC 670; MSC 93-XX.
  References: General [Sch99]; ATP [Rei01, BG05].
• PRD Products.
  A product is anything that can be offered to a market that might satisfy a want or need.
  Indices: DDC ???; MSC ??.
  References: General [KA+06]; ATP --.
• QUA Quantales.
  Quantales are partially ordered algebraic structures that generalize locales (point free topologies) as well as various lattices of multiplicative ideals from ring theory and functional analysis. Quantales are sometimes referred to as complete residuated semigroups.
  Indices: DDC 512; MSC 06F07.
  References: General [Mul01, Con71]; ATP --.
• PUZ Puzzles.
  Puzzles are designed to test the ingenuity of humans.
  Indices: DDC 510, 793.73; MSC --.
  References: General [Car86, Smu78, Smu85]; ATP --.
• RAL Real Algebra.
  Real algebra is the study of "real" objects such as real rings, real places and real varieties. Indices: DDC 512; MSC 13J30
  References: General [Lam84]; ATP --.
• REL Relation Algebra.
  A relation algebra is a residuated Boolean algebra supporting an involutary unary operation called converse. The motivating example of a relation algebra is the algebra 2^X^2 of all binary relations on a set X, with RoS interpreted as the usual composition of binary relations.
  Indices: DDC 512; MSC 03G15, 06D99
  References: General [SS93, Mad06]; ATP [HS08].
• RNG Ring Theory.
  A ring is a group (see above) in which the binary operation is commutative, with an associative and distributive operation *:GxG -> G for which there is an identity element in G.
  Indices: DDC 200; MSC -.
  References: General [Bou89, BB70]; ATP [MOW76].
• ROB Robbins Algebra.
  The Robbins Algebra domain revolves around the question "Is every Robbins algebra Boolean?". Most of the problems in this domain identify conditions that make a near-Boolean algebra Boolean.
  Indices: DDC 512; MSC 03G15.
  References: General [HMT71]; ATP [Win90].
• SCT Social Choice Theory.
  Social choice theory is a theoretical framework for measuring individual interests, values, or welfares as an aggregate towards collective decision..
  Indices: DDC 330.1; MSC -.
  References: General [Arr63]; ATP [Nip09].
• SET, SEU, and SEV Set Theory.
  Classically, a set is a totality of certain definite, distinguishable objects of our intuition or thought - called the elements of the set. Due to paradoxes that arise from such a naive definition, mathematicians now regard the notion of a set as an undefined, primitive concept [How72].
  Indices: DDC 511.322, 512.817; MSC 03EXX, 04XX.
  References: General [Neu25, Qui69]; ATP [Qua92].
• SWB Semantic Web.
  Semantic Web is a group of methods and technologies to allow machines to understand the meaning – or "semantics" – of information on the World Wide Web.
  Indices: DDC ??.?; MSC --.
  References: General [BHL01]; ATP [HV06].
• SWC Software Creation.
  Software creation is used to form a computer program that meets given specifications.
  Indices: DDC ???.?; MSC 68N30.
  References: General --; ATP --.
• SWV and SWW and SWX Software Verification.
  Software verification formally establishes that a computer program does the task it is designed for.
  Indices: DDC 005.14; MSC 68Q60.
  References: General --; ATP [WO+92, MOW76].
• SYN and SYO Syntactic.
  Syntactic problems have no obvious semantic interpretation.
  Indices: DDC --; MSC --.
  References: General [Chu56]; ATP [Pel86].
• TOP Topology.
  Topology is the study of properties of geometric configurations (e.g., point sets) which are unaltered by elastic deformations (homeomorphisms, i.e., functions that are 1-1 mappings between sets, such that both the function and its inverse are continuous).
  Indices: DDC 514; MSC 46AXX.
  References: General [Kel55, Mun75]; ATP [WM89].

Equality Axiomatization
In the TPTP equality is represented in infix using = and != for equality and inequality. An inequality has the same meaning as a negated equality. If equality is present in a problem, axioms of equality are not provided; it is assumed that equality reasoning is builtin to every ATP system. If equality axioms are required by an ATP system they can be added using the TPTP2X or TPTP4X utility. If any axioms are added when the problems are submitted to an ATP system, then the addition must be explicitly noted in reported results/

Up to TPTP v1.1.3, the TPTP contained problem files for particular sizes of generic problems. This, however, was undesirable. Firstly, only a finite number of different problem sizes could be included, and therefore a desired size might have been missing. Secondly, even a small number of different problem sizes for each generic problem could consume a considerable amount of disk space. To overcome these problems, the TPTP contains generator files. Generator files are used to generate instances of generic problems, according to user supplied size parameters. The generators are used in conjunction with the tptp2X utility.

For convenience, the TPTP still contains, where they exist, interesting size instances of each generic problem. The TPTP sizes were chosen to be non-trivial, The statistics in the TPTP documents take into account these instances of generic problems.

A regular expression for recognizing problem file names is "[A-Z]{3}[0-9]{3}[-+^=_][1-9][0-9]*(\.[0-9]{3})*\.p". A regular expression for recognizing axiom file names is "[A-Z]{3}[0-9]{3}[-+^=_][1-9][0-9]*\.ax".

The version numbers used for each abstract problem do not always start at 1, and are not always successive. This is because the same version number is assigned (wherever possible) to all problems that come from the same source, within each domain.

If a file is ever removed from or renamed in the TPTP, then its extension is changed to .rm. The file is not physically removed, and a comment is added to the file to explain what has happened. This mechanism maintains the unique identification of problems and axiomatizations.

A full BNF specification of the problem and axiom file formats is provided in the Documents directory of the TPTP. The TPTP2X and TPTP4X utilities can be used to convert TPTP files to other known ATP system formats. A description of the information contained in TPTP files is given below.

The problem files SYN000* are contrived to use most features of the TPTP language, and are thus suitable for testing parsers, etc. They are not suitable for evaluating ATP systems' reasoning capabilities.

The Header Section

%--------------------------------------------------------------------------
% File     : GRP194+1 : TPTP v8.0.0. Released v2.0.0.
% Domain   : Group Theory (Semigroups)
% Problem  : In semigroups, a surjective homomorphism maps the zero
% Version  : [Gol93] axioms.
% English  : If (F,*) and (H,+) are two semigroups, phi is a surjective
%            homomorphism from F to H, and id is a left zero for F,
%            then phi(id) is a left zero for H.

% Refs     : [Gol93] Goller (1993), Anwendung des Theorembeweisers SETHEO a
% Source   : [Gol93]
% Names    :

% Status   : Theorem
% Rating   : 0.22 v7.5.0, 0.25 v7.4.0, 0.10 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.36 v6.1.0, 0.47 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.50 v5.3.0, 0.48 v5.2.0, 0.40 v5.1.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0
% Syntax   : Number of formulae    :    8 (   2 unt;   0 def)
%            Number of atoms       :   21 (   4 equ)
%            Maximal formula atoms :    4 (   2 avg)
%            Number of connectives :   13 (   0   ~;   0   |;   6   &)
%                                         (   1 <=>;   6  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   5 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :    3 (   2 usr;   0 prp; 2-2 aty)
%            Number of functors    :    5 (   5 usr;   3 con; 0-3 aty)
%            Number of variables   :   15 (  14   !;   1   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments :
%--------------------------------------------------------------------------

The % Domain field.
The domain field identifies the domain, and possibly a subdomain, from which the problem is drawn. The domain corresponds to the first three letters of the problem name.

The % Problem field.
This field provides a one-line, high-level description of the abstract problem. In axiom files, this field is called % Axioms, and provides a one-line, high-level description of the axiomatization.

The % Version field.
This field gives information that differentiates this version of the problem from other versions of the problem. The first possible differentiation is the axiomatization that is used. If a specific axiomatization is used, a citation is provided. If the axiomatization is a pure equality axiomatization (uses only the equal/2 predicate) then this is noted too.

The second possible differentiation is the status of the axiomatization. There are 12 possiblities:

• empty. Indicates that the axiomatization is standard, i.e., it is complete and has had no lemmas added (it might be redundant).
• Especial. Indicates that the axiomatization does not capture any established theory.
• Biased. Indicates that the axiomatization is designed specifically to be suited or ill-suited to some ATP system, calculus, or control strategy.
• Incomplete. Indicates that the axiomatization is incomplete.
• Reduced > Complete. Indicates that a existing standard axiomatization has had axioms removed, and the result is complete. The existing axiomatization is necessarily redundant.
• Reduced > Incomplete. Indicates that a existing standard axiomatization has had axioms removed, and the result is non-standard due to incompleteness.
• Augmented. Indicates that a existing standard axiomatization has had lemmas added, and the result is non-standard due to redundancy.
• Reduced & Augmented > Complete. Indicates that a existing standard axiomatization has had axioms removed and lemmas added, and the result is complete. (Non-standard) after Complete. >
• Reduced & Augmented > Incomplete. Indicates that a existing standard axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.
• Incomplete > Reduced > Incomplete. Indicates that an existing incomplete axiomatization has had axioms removed, and the result is non-standard due to incompleteness.
• Incomplete > Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms added, and the result is complete.
• Incomplete > Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had lemmas added, and the result is non-standard due to incompleteness.
• Incomplete > Reduced & Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is complete. (Non-standard) after Complete. >
• Incomplete > Reduced & Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.
• Especial > Reduced > Especial. Indicates that an especial axiomatization has had axioms removed, and the result remains especial.
• Especial > Augmented > Especial. Indicates that an especial axiomatization has had axioms added, and the result remains especial.

% Version  : [McCharen, et al., 1976] (equality) axioms.
%            Theorem formulation : Explicit formulation of the commutator.

The % English field.
This field provides a full description of the problem, if the one-line description in the % Problem field is too terse.

The % Refs field.
This field provides a list of abbreviated references for material in which the problem has been presented. Other relevant references are also listed. The reference keys identify BibTeX entries in the Bibliography.bib file supplied with the TPTP.

The % Source field.
This field acknowledges the source of the problem, usually as a citation. If the problem was sourced from an existing problem collection then the collection name is given in [ ] brackets. The problem collections used thus far are:

• ANL - the Argonne National Laboratory library [ANL]
• OTTER - the collection distributed with the Otter ATP system [McC98]
• Quaife - Art Quaife's collection of set theory (based) problems [Qua92]
• ROO - the problems used to test the ROO ATP system [LM92]
• SPRFN - the collection distributed with the SPRFN ATP system [SPRFN]
• TPTP - the problem first ever appeared in the TPTP
• SETHEO - the collection used to test the SETHEO ATP system [LS+92]

The % Status field.
This field gives the ATP status of the problem, according to the SZS ontology. For THF, TFF, and FOF problems it is one of the following values. For THF problems the default semantics is Henkin with extensionality and choice. If the status is different for other semantics, this is noted on lines after the % Status field.

• Theorem - Every model of the axioms (and other non-conjecture formulae, e.g., hypotheses and lemmas), and there are some such models, is a model of all the conjectures.
• ContradictoryAxioms - There are not models of the axioms (and other non-conjecture formulae, e.g., hypotheses and lemmas).
• CounterSatisfiable - Some models of the axioms (and there are some) are models of the negation of at least one of the conjectures.
• Unsatisfiable - There are no conjectures, and no interpretations are models of the axioms.
• Satisfiable - There are no conjectures, and some interpretations are models of the axioms.
• Unknown - The problem has never been solved by an ATP system.
• Open - The abstract problem has never been solved.

• Unsatisfiable - No interpretations are models of the clauses.
• Satisfiable - Some interpretations are models of the clauses.
• Unknown - The problem has never been solved by an ATP system.
• Open - The abstract problem has never been solved.

The % Syntax field.
This field lists various syntactic measures of the problem's formulae. The measures for THF problems are:

• the numbers of formulae, unit formulae, type formulae, definition formulae,
• the numbers of atoms, equality atoms, connective atoms,
• the maximal and average number of atoms in a formula,
• the numbers of logical connectives, each logical connective,
• the maximal and average formula depth, the number of nested formulae,
• the numbers of tuples, if-then-else formulae, and let-in formulae,
• the numbers of arithmetic formulae, terms, numbers, and variables,
• the numbers of types, user types,
• the numbers of type connectives, each type connective,
• the numbers of distinct (non-variable) symbols, user symbols, constant symbols, and the arity range of the symbols,
• the numbers of uses of the Π, Σ, ε, ι, and typed equality constants,
• the numbers of distinct variables, lambda quantifications, universal quantifications, existential quantifications, typed variables, defined variables, Π, Σ, ε, and ι binders.

• the numbers of formulae, unit formulae, type formulae, definition formulae,
• the numbers of atoms, equality atoms,
• the maximal and average number of atoms in a formula,
• the numbers of logical connectives, each logical connective,
• the maximal and average formula depth,
• the maximal and average term depth,
• the numbers of extended terms, nested formulae, boolean variables,
• the numbers of tuples, if-then-else formulae, and let-in formulae,
• the numbers of arithmetic formulae, terms, numbers, and variables,
• the numbers of types, user types,
• the numbers of type connectives, each type connective,
• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates.
• the numbers of distinct function, user functions, constants, and the arity range of the functions,
• the numbers of distinct variables, universal quantifications, existential quantifications, typed variables, defined variables, Π and Σ binders.

• the numbers of formulae, unit formulae, definition formulae,
• the numbers of atoms, equality atoms,
• the maximal and average number of atoms in a formula,
• the numbers of logical connectives, each logical connective,
• the maximal and average formula depth,
• the maximal and average term depth,
• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates.
• the numbers of distinct function, user functions, constants, and the arity range of the functions,
• the numbers of distinct variables, universal quantifications, existential quantifications.

• the numbers of clauses, unit clauses, non-Horn clauses, range restricted clauses,
• the numbers of literals, equality literals, negated literals,
• the maximal and average clause size,
• the maximal and average term depth,
• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates.
• the numbers of distinct function, user functions, constants, and the arity range of the functions,
• the numbers of distinct variables, singletons.

The % SPC field.
This field indicates to which Specialist Problem Class (SPC) the problem belongs. SPCs are sets of problems that have similar syntactic characteristics, so that that the problems are reasonably homogeneous with respect ATP systems' performances on the problems. SPCs are used for caclulating the difficulty rating [SS01], and for recommending systems to use on problems [SS99]. The characteristics used to build the SPCs are:

• The form of the problem: TH1, TH0, TX1, TX0, TF1, TF0, FOF, CNF
• The known or expected logical (SZS) status: THM (theorem), CAX (contradictory axioms), CSA (countersatisfiable), UNS (unsatisfiable), SAT (satisfiable), UNK (unknown), OPN (open)
• The effective order of the logic (for FOF and CNF problems): PRP (propositional), EPR (effectively propositional), RFO (really first-order),
• The amount of equality in the problem: EQU (with equality), SEQ (some, but not only, equality), PEQ (pure equality), UEQ (unit equality) NUE (non-unit pure equality), NEQ (no equality),
• The amount of arithmetic (for TFF problems): ARI (with arithmetic) NAR (no arithmetic),
• Horness (for CNF problems): HRN (Horn), NHN (non-Horn)

The % Comments field.
This field contains free format comments about the problem, e.g., the significance of the problem, or the reason for creating the problem. If the problem was created using the TPTP2X utility then the TPTP2X parameters are given.

The % Bugfixes field.
This field describes any bugfixes that have been done to the formulae of the problem. Each entry gives the release number in which the bugfix was done, and attempts to pinpoint the bugfix accurately.

The Include Section

%--------------------------------------------------------------------------
%----Include simple curve axioms
include('Axioms/GEO004+0.ax').
%----Include axioms of betweenness for simple curves
include('Axioms/GEO004+1.ax').
%----Include oriented curve axioms
include('Axioms/GEO004+2.ax').
%----Include trajectory axioms
include('Axioms/GEO004+3.ax',[connect_defn,symmetry_of_at_the_same_time]).
%--------------------------------------------------------------------------

Full versions of TPTP problems (without include directives) can be created by using the TPTP2X and TPTP4X utilities.

A side effect of separating out the axioms into axiom files is that the formula order in the TPTP presentation of problems is typically different from that of any original presentation. This reordering is acceptable because the performance of a decent ATP system should not be very dependent on a particular formula ordering.

Annotated Formulae

• The axiom-like formulae are those with the roles axiom, hypothesis, definition, assumption, lemma, theorem, and corollary. They are accepted, without proof, as a basis for proving conjectures in THF, TFF, and FOF problems. In CNF problems the axiom-like formulae are accepted as part of the set whose satisfiability has to be established. There is no guarantee that the axiom-like formulae of a problem are consistent.
• hypothesiss are assumed to be true for a particular problem.
• definitions are used to define symbols.
• assumptions must be discharged before a derivation is complete.
• lemmas and theorems have been proven from the other axiom-like formulae, and are thus redundant wrt those axiom-like formulae. theorem is used also as the role of proven conjectures, in output. A problem containing a lemma or theorem that is not redundant wrt the other axiom-like formulae is ill-formed. theorems are more important than lemmas from the user perspective.
• corollarys have been proven from the axioms and a theorem, and are thus redundant wrt the other axiom-like and theorem formulae. A problem containing a corollary that is not redundant wrt the other axiom-like formulae and theorem formulae is ill-formed.
• conjectures occur in only THF, TFF, and FOF problems, and are to all be proven from the axiom-like formulae. A problem is solved only when all conjectures are proven. (TPTP problems never contain more than one conjecture, and the creation of problems with more than one conjecture is currently deprecated, because contemporary ATP systems commonly treat them as a disjunction, and will prove only one of them.)
• negated_conjectures are formed from negation of a conjecture, typically in FOF to CNF conversion.
• plain formulae have no special user semantics, and are typically used in derivation output.
• type formulae define the types of symbols globally.
• interpretation formulae are used for writing interpretations, typically models of satisfiable sets of formulae, in particular the axioms and negated_conjecture of a non-theorem.
• logic formulae are used for defining the logic in non-classical logics.
• unknowns have unknown role, and this is an error situation.

The syntax for atoms is that of Prolog: variables start with upper case letters, atoms and terms are written in prefix notation, uninterpreted predicates and functors either start with lower case and contain alphanumerics and underscore, or are in 'single quotes'. The language also supports interpreted predicates and functors. These come in two varieties: defined predicates and functors, whose interpretation is specified by the TPTP language, and system predicates and functors, whose interpretation is ATP system specific. Interpreted predicates and functors are syntactically distinct from uninterpreted ones - they are = and !=, or start with a $, a ", or a digit. Non-variable symbols can be given a type globally, in the formula with role type. The defined types are $o - the Boolean type, $i - the type of individuals, $real - the type of reals, $rat - the type of rational, and $int - the type of integers. New types are introduced in formulae with the type role, based on $tType - the type of all types. Full details of the THF and TFF type systems are provided in [SS+12,BP13,SB10,KSR16], with the last providing an overview of the first three.

The defined predicates recognized so far are

• $true and $false, with the obvious interpretations. In typed languages they are of type $o.
• = and != for equality and inequality. In typed languages they are ad hoc polymorphic with both sides having the same type.
• $distinct, whose arguments are hence known to be unequal from each other (but not necessarily unequal to any other constants). $distinct maybe overloaded with different arities. $distinct is used in only the typed languages, and is ad hoc polymorphic with all arguments having the same type.
• The arithmetic predicates described below. The arithmetic predicates are used in only the THF and TFF languages.

• "distinct object"s, written in double quotes. All "distinct object"s are unequal to all "different distinct object"s (but not necessarily unequal to any other constants), e.g., "Apple" != "Microsoft". One way of implementing this is to interpret "distinct object" as the domain element in the double quotes. In typed contexts "distinct object"s are of type $i (and as a result, are unequal to all numbers because their interpretation domains are disjoint in the TPTP type systems).
• Numbers (numeric constants). These are used in the THF and TFF languages. Numbers are interpreted as themselves (as domain elements). All different numbers are unequal, e.g., 1 != 2 (but not necessarily unequal to any other constants). All numbers are also unequal to terms of type $i (because their interpretation domains are disjoint in the TPTP type systems). Numbers are not allowed in FOF and CNF, but for many applications an adequate alternative is to write "numbers" as distinct objects, e.g., "27", so that different "numbers" are known to be unequal to each other, but possibly equal to other terms of type $i.
• The arithmetic functions described below. The arithmetic functions are used in only the THF and TFF languages.

System predicates and functors are used for interpreted predicates and functors that are available in particular ATP tools. System predicates and functors start with $$. The names are not controlled by the TPTP language, so they must be used with caution.

The connectives used to build non-atomic formulae are written using intuitive notations. The universal quantifier is !, the existential quantifier is ?, and the lambda binder is ^. Quantified formulae are written in the form Quantifier [Variables] :  Formula. In the THF, TFF, and FOF languages, every variable in a Formula must be bound by a preceding quantification with adequate scope. Typed Variables are given their type by a :type suffix. The binary connectives are infix | for disjunction, infix & for conjunction, infix <=> for equivalence, infix => for implication, infix <= for reverse implication, infix <~> for non-equivalence (XOR), infix ~| for negated disjunction (NOR), infix ~& for negated conjunction (NAND), infix @ for application. The only unary connective is prefix ~ for negation. Negation has higher precedence than quantification, which in turn has higher precedence than the binary connectives. No precedence is specified between the binary connectives; brackets are used to ensure the correct association. The binary connectives are left associative.

The THF and TFF languages have conditional and let expressions.

• Conditional expressions have $ite as the functor. The expressions are parametric polymorphic, taking a boolean expression as the first argument, then two expressions of any one type as the second and third arguments, as the true and false return values respectively, i.e., the return type is the same as that of the second and third arguments. Let expressions have $let as the functor.
• The expressions provide the types of defined symbols, definitions for the symbols, and a formula/term in which the definitions are applied. Each type declaration is the same as a type declaration in an annotated formula with the type role, and multiple type declarations are given in []ed tuples of declarations. Each definition defines the expansion of one of the declared symbols, and multiple definitions are given in []ed tuples of definitions. If variables are used in the lefthand side of a definition, their values are supplied in the defined symbol's use. Such variables do not need to be declared (they are implicitly declared to be of the type defined by the symbol declaration), but must be top-level arguments of the defined symbol and be pairwise distinct.

The useful_info field of an annotated formula is optional, and if it is not used then the source field becomes optional. The source field is used to record where the annotated formula came from, and is most commonly a file record or an inference record. A file record stores the name of the file from which the annotated formula was read, and optionally the name of the annotated formula as it occurs in that file - this might be different from the name of the annotated formula itself, e.g., if an ATP systems reads an annotated formula, renames it, and then prints it out. An inference record stores information about an inferred formula. The useful_info field of an annotated formula is a list of arbitrary useful information formatted as Prolog terms, as required for user applications.

An example of a THF formula section, extracted from the problem file LCL633^1.p, is shown below. An example of a TFF formula section, extracted from the problem file DAT013=1.p, is shown below that. Example THF formulae. An example of a FOF formula section, extracted from the problem file GRP194+1.p, is shown below that. An example of a clause section, extracted from the problem file GRP039-7.p, is shown below that.

%------------------------------------------------------------------------------
%----Signature
thf(a,type,(
    a: $tType )).

thf(p,type,(
    p: ( a > $i > $o ) > $i > $o )).

thf(g,type,(
    g: a > $i > $o )).

thf(e,type,(
    e: ( a > $i > $o ) > a > $i > $o )).

thf(r,type,(
    r: $i > $i > $o )).

%----Axioms
thf(positiveness,axiom,(
    ! [X: a > $i > $o] :
      ( mvalid
      @ ( mimpl @ ( mnot @ ( p @ X ) )
        @ ( p
          @ ^ [Z: a] :
              ( mnot @ ( X @ Z ) ) ) ) ) )).

thf(g,definition,
    ( g
    = ( ^ [Z: a,W: $i] :
        ! [X: a > $i > $o] :
          ( mimpl @ ( p @ X ) @ ( X @ Z ) @ W ) ) )).

thf(e,definition,
    ( e
    = ( ^ [X: a > $i > $o,Z: a,P: $i] :
        ! [Y: a > $i > $o] :
          ( mimpl @ ( Y @ Z )
          @ ( mbox @ r
            @ ^ [Q: $i] :
              ! [W: a] :
                ( mimpl @ ( X @ W ) @ ( Y @ W ) @ Q ) )
          @ P ) ) )).

%----Conjecture
thf(thm,conjecture,
    ( mvalid
    @ ^ [W: $i] :
      ! [Z: a] :
        ( mimpl @ ( g @ Z ) @ ( e @ g @ Z ) @ W ) )).
%------------------------------------------------------------------------------

%------------------------------------------------------------------------------
tff(list_type,type,(
    list: $tType )).

tff(nil_type,type,(
    nil: list )).

tff(mycons_type,type,(
    mycons: ( $int * list ) > list )).

tff(sorted_type,type,(
    fib_sorted: list > $o )).

tff(empty_fib_sorted,axiom,(
    fib_sorted(nil) )).

tff(single_is_fib_sorted,axiom,(
    ! [X: $int] : fib_sorted(mycons(X,nil)) )).

tff(double_is_fib_sorted_if_ordered,axiom,(
    ! [X: $int,Y: $int] :
      ( $less(X,Y)
     => fib_sorted(mycons(X,mycons(Y,nil))) ) )).

tff(recursive_fib_sort,axiom,(
    ! [X: $int,Y: $int,Z: $int,R: list] :
      ( ( $less(X,Y)
        & $greatereq(Z,$sum(X,Y))
        & fib_sorted(mycons(Y,mycons(Z,R))) )
     => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )).

tff(check_list,conjecture,(
    fib_sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )).
%------------------------------------------------------------------------------

%--------------------------------------------------------------------------
%----Definition of a homomorphism
fof(homomorphism1,axiom,
    ( ! [X] :
        ( group_member(X,f)
       => group_member(phi(X),h) ) )).

fof(homomorphism2,axiom,
    ( ! [X,Y] :
        ( ( group_member(X,f)
          & group_member(Y,f) )
       => multiply(h,phi(X),phi(Y)) = phi(multiply(f,X,Y)) ) )).

fof(surjective,axiom,
    ( ! [X] :
        ( group_member(X,h)
       => ? [Y] :
            ( group_member(Y,f)
            & phi(Y) = X ) ) )).

%----Definition of left zero
fof(left_zero,axiom,
    ( ! [G,X] :
        ( left_zero(G,X)
      <=> ( group_member(X,G)
          & ! [Y] :
              ( group_member(Y,G)
             => multiply(G,X,Y) = X ) ) ) )).

%----The conjecture
fof(left_zero_for_f,hypothesis,
    ( left_zero(f,f_left_zero) )).

fof(prove_left_zero_h,conjecture,
    ( left_zero(h,phi(f_left_zero)) )).
%--------------------------------------------------------------------------

%--------------------------------------------------------------------------
%----Redundant two axioms
cnf(right_identity,axiom,
    ( multiply(X,identity) = X )).

cnf(right_inverse,axiom,
    ( multiply(X,inverse(X)) = identity )).

... some clauses omitted here for brevity

cnf(property_of_O2,axiom,
    ( subgroup_member(X)
    | subgroup_member(Y)
    | multiply(X,element_in_O2(X,Y)) = Y )).

%----Denial of theorem
cnf(b_in_O2,negated_conjecture,
    ( subgroup_member(b) )).

cnf(b_times_a_inverse_is_c,negated_conjecture,
    ( multiply(b,inverse(a)) = c )).

cnf(a_times_c_is_d,negated_conjecture,
    ( multiply(a,c) = d )).

cnf(prove_d_in_O2,negated_conjecture,
    ( ~ subgroup_member(d) )).
%--------------------------------------------------------------------------

The following interpreted predicates and interpreted functions are defined. Each symbol is ad-hoc polymorphic over the numeric types exception - $quotient is not defined for $int). All arguments must have the same numeric type. All the functions, except for $quotient of two $ints, and the coercion functions $to_int and $to_rat, have the same range type as their arguments. For example, $sum can be used with the type signatures ($int * $int) > $int, ($rat * $rat) > $rat, and ($real * $real) > $real. The $quotient of two $ints is a $rat. The coercion function $to_int always has a $int result, and the coercion function $to_rat always has a $rat result. All the predicates have a $o result. For example, $less can be used with the type signatures ($int * $int) > $o, ($rat * $rat) > $o, and ($real * $real) > $o.

Symbol	Operation	Comments, examples                                        -
$int	The type of integers	123, -123 <integer> ::- (<signed_integer>|<unsigned_integer>) <signed_integer> ::- <sign><unsigned_integer> <unsigned_integer> ::- <decimal> <decimal> ::- (<zero_numeric>|<positive_decimal>) <positive_decimal> ::- <non_zero_numeric><numeric>* <sign> ::: [+-] <zero_numeric> ::: [0] <non_zero_numeric> ::: [1-9] <numeric> ::: [0-9]
$rat	The type of rationals	123/456, -123/456, +123/456 <rational> ::- (<signed_rational>|<unsigned_rational>) <signed_rational> ::- <sign><unsigned_rational> <unsigned_rational> ::- <decimal><slash><positive_decimal> <slash> ::: [/]
$real	The type of reals	123.456, -123.456, 123.456E789, 123.456e789, -123.456E789, 123.456E-789, -123.456E-789 <real> ::- (<signed_real>|<unsigned_real>) <signed_real> ::- <sign><unsigned_real> <unsigned_real> ::- (<decimal_fraction>|<decimal_exponent>) <decimal_exponent> ::- (<decimal>|<decimal_fraction>)<exponent><decimal> <decimal_fraction> ::- <decimal><dot_decimal> <dot_decimal> ::- <dot><numeric><numeric>* <dot> ::: [.] <exponent> ::: [Ee]
= (infix)	Comparison of two numbers.	The numbers must be the same atomic type (see the type system).
$less/2	Less-than comparison of two numbers.	$less, $lesseq, $greater, and $greatereq are related by   ! [X,Y] : ( $lesseq(X,Y) <=> ( $less(X,Y) | X = Y ) )   ! [X,Y] : ( $greater(X,Y) <=> $less(Y,X) )   ! [X,Y] : ( $greatereq(X,Y) <=> $lesseq(Y,X) ) i.e, only $less and equality need to be implemented to get all four relational operators.
$lesseq/2	Less-than-or-equal-to comparison of two numbers.
$greater/2	Greater-than comparison of two numbers.
$greatereq/2	Greater-than-or-equal-to comparison of two numbers.
$uminus/1	Unary minus of a number.	$uminus, $sum, and $difference are related by   ! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y)) i.e, only $uminus and $sum need to be implemented to get all three additive operators.
$sum/2	Sum of two numbers.
$difference/2	Difference between two numbers.
$product/2	Product of two numbers.
$quotient/2	Exact quotient of two numbers of the same type.	For non-zero divisors, the result can be computed. For zero divisors the result is not specified. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate the $quotient. Users should always guard their use of $quotient using inequality, e.g.,   ! [X: $real] : ( X != 0.0 => p($quotient(5.0,X)) ) For $rat or $real operands the result is the same type. For $int operands the result is $rat; the result might be simplied.
$quotient_e/2, $quotient_t/2, $quotient_f/2	Integral quotient of two numbers.	The three variants use different rounding to an integral result: $quotient_e(N,D) - the Euclidean quotient, which has a non-negative remainder. If D is positive then $quotient_e(N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then $quotient_e(N,D) is the ceiling of N/D. $quotient_t(N,D) - the truncation of the real division N/D. $quotient_f(N,D) - the floor of the real division N/D. For zero divisors the result is not specified.
$remainder_e/2, $remainder_t/2, $remainder_f/2	Remainder after integral division of two numbers.	For τ ∈ {$int,$rat, $real}, ρ ∈ {e, t,f}, $quotient_ρ and $remainder_ρ are related by   ! [N:τ,D:τ] : $sum($product($quotient_ρ(N,D),D),$remainder_ρ(N,D)) = N For zero divisors the result is not specified.
$floor/1	Floor of a number.	The largest integral value (in the type of the argument) not greater than the argument.
$ceiling/1	Ceiling of a number.	The smallest integral value (in the type of the argument) not less than the argument.
$truncate/1	Truncation of a number.	The nearest integral value (in the type of the argument) with magnitude not greater than the absolute value of the argument.
$round/1	Rounding of a number.	The nearest integral value (in the type of the argument) to the argument. If the argument is halfway between two integral values, the nearest even integral value to the argument.
$is_int/1	Test for coincidence with an $int value.
$is_rat/1	Test for coincidence with a $rat value.
$to_int/1	Coercion of a number to $int.	The largest $int not greater than the argument. If applied to an argument of type $int this is the identity function.
$to_rat/1	Coercion of a number to $rat.	This function is not fully specified. If applied to a $int the result is the argument over 1. If applied to a $rat this is the identity function. If applied to a $real that is (known to be) rational the result is the $rat value. For other reals the result is not specified. In practice, if an ATP system does not "know" that the argument is rational, it should simply not evaluate the $to_rat. Users should always guard their use of $to_rat using $is_rat, e.g.,   ! [X: $real] : ( $is_rat(X) => p($to_rat(X)) )
$to_real/1	Coercion of a number to $real.

The extent to which ATP systems are able to work with the arithmetic predicates and functions can vary, from a simple ability to evaluate ground terms, e.g., $sum(2,3) can be evaluated to 5, through an ability to instantiate variables in equations involving such functions, e.g., $product(2,$uminus(X)) = $uminus($sum(X,2)) can instantiate X to 2, to extensive algebraic manipulation capability. The syntax does not axiomatize arithmetic theory, but may be used to write axioms of the theory.

Full specification of the connectives and their use in formulae is in the BNF starting at <nxf_atom> and <thf_defined_atomic>.

Semantics Specification
An annotated formula with the role logic is used to specify the semantics of formulae. The semantic specification typically comes first in a file. A semantic specification consists of the defined name of the logic followed by == and a list of properties value assignments. Each specification is the property name, followed by == and either a value or a tuple of specification details. If the first element of a list of details is a value, that is the default value for all cases that are not specified in the rest of the list. Each detail after the optional default value is the name of a relevant part of the vocabulary of the problem, followed by == and a value for that named part. The BNF grammar is here. The grammar is not very restrictive on purpose, to enable working with other logics as well. It is possible to create a lot of nonsense specifications, and to say the same thing in different meaningful ways. A tool to check the sanity of a specification is available.

A semantic specification changes the meaning of things such as the boolean type $o, universal quantification with !, etc - their existing meaning in classical logic should not be confused with the meaning in the declared logic.

For plain $modal and all the *_modal logics the properties that may be specified are $domains, $designation, $terms, and $modalities.

• $domains
  • $constant - Constant domain semantics has all world's domains fixed the same.
  • $varying - Varying domain semantics has (potentially) different domains for each world.
  • $cumulative - Cumulative domain semantics and varying, and the domain of each world is a superset of the domains of the worlds from which it can be reached.
  • $decreasing - Decreasing domain semantics and varying, and the domain of each world is a subset of the domains of the worlds from which it can be reached.
• $designation
  • $rigid - Rigid designation independent of worlds.
  • $flexible - Flexible designation dependent on worlds.
• $terms
  • $local - Terms are interpreted in the local world
  • $global - Terms are interpreted globally in all the worlds
• $modalities
  • A known system name in the form $modal_system_Sys
    Sys ∈ { K,KB,K4,K5,K45,KB5,D,DB,D4,D5,D45,M,B,S4,S5,S5U }
  • A tuple of known axiom names in the form [ $modal_axiom_Ax₁, $modal_axiom_Ax₂, ... ]
    Ax_i ∈ { K,M,B,D,4,5,CD,BoxM,C4,C }

For $temporal_instant the properties are the $domains, $designation, and $terms of the modal logic, $modalities with different possible values, and another property $time.

• $modalities
  • A tuple of known axiom names in the form [ $modal_axiom_AxTm₁, $modal_axiom_AxTm₂, ... ]
    Ax_i ∈ { K,M,B,D,4,5 }, Tm_i ∈ { +,- },
• $time
  • A tuple of known time properties in the form [ P₁,P₂, ... ]
    P_i ∈ { $reflexivity, $irreflexivity, $transitivity, $asymmetry, $anti_symmetry, $linearity, $forward_linearity, $backward_linearity, $beginning, $end, $no_beginning, $no_end, $density, $forward_discreteness, $backward_discreteness }

The formulae of a problem can be either local (true in the current world) or global (true in all worlds). By default, formulae with the roles hypothesis and conjecture are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., axiom-$local, conjecture-$global.

• Problems - The problem files directory, with subdirectories for each domain. The domain name abbreviations are used as subdirectory names. The subdirectories contain the problem files.
• Axioms - The axiom files directory.
• Generators - The generator files directory.
• TPTP2X - The directory containing the TPTP2X utility.
• Scripts - A directory containing the TPTP4X and TPTP2T utilities (the directory is called "Scripts" because originally it was planned to put shell scripts there, but things changed).
• Documents - A directory containing documents that relate to the TPTP:
  • ReadMe - General information about the TPTP.
  • History - A history of the changes made to the TPTP up to the current release.
  • ProblemList - A list of all the abstract problems in the TPTP, giving their names, number of THF, TFF, FOF, and CNF versions, and one-line descriptions.
  • AxiomList - A list of the axiomatizations in the TPTP, giving their names, number of THF, TFF, FOF, and CNF specializations, and one-line descriptions.
  • GeneratorList - A list of the generic problems in the TPTP, giving their names, number of FOF and CNF versions, and one-line descriptions. For each version the constraints that determine the permissible sizes, and the TPTP sizes, are given.
  • ReverseIndex - An index from existing known names for problems to their TPTP file names.
  • Bibliography.bib - The BibTeX file containing references for all material cited in the TPTP.
  • ProblemAndSolutionStatistics - Lists all the problems in the TPTP, giving statistics about the problems and information about ATP systems' performances on the problems. The fields are listed and explained below.
  • THFSynopsis, TFFSynopsis, FOFSynopsis, and CNFSynopsis - Statistics on the THF, TFF, FOF, and CNF probhlems in the TPTP, and charts showing the structure of the TPTP problem domains.
  • OverallSynopsis - Statistics on the overall TPTP, and a chart showing the structure of the TPTP problem domains.
  • VerySimilarProblemsLists - A directory containing lists of very similar problems. Problems are considered to be be "very similar" if:
    • They have many formulae in common, e.g., when the same axioms are used for very many conjectures.
    • They have every similar characteristics, e.g., when the problems have been created using different parameters in some automated process.
  • SyntaxBNF - BNF of the TPTP syntax
  • Template - A template for submitting new TPTP problems.
  The files in the Documents directory contain comprehensive online information about the TPTP. They summarize much of the information contained in this report, in specific files. Their format provides quick access to the data, using standard system tools (e.g., grep, awk).

  The fields in the problem lines of the ProblemAndSolutionStatistics file are:

  • Problem name
  • Frm - one of THF, TFF, FOF, or CNF.
  • SZS - The SZS status (using the SZS ontology)
  • Rtng - The problem's difficulty rating.
  • SPC - The problem's Specialist Problem Class
  • FmlCls - The number of formulae/clauses
  • UnitF - The number of unit formulae/clauses
  • TypeF - The number of type declarations (THF and TFF)
  • Atoms - The number of atoms
  • EquAts - The number of equality atoms
  • Conns - The number of logical connectives
  • FOOLs - The number of FOOL logic atoms/terms (TXF)
  • Ariths - The number of arithmetic atoms/terms (THF and TFF)
  • Types - The number of Types (THF and TFF)
  • Symbls - The number of distinct non-variable symbols
  • Preds - The number of disinct predicate symbols
  • Arity - The arity range of predicate symbols
  • Funcs - The number of distinct function symbols
  • Arity - The arity range of function symbols
  • Vars - The number of distinct variables
  • ^ - The number of lambda quantified variables (THF)
  • ! - The number of universally quantified variables
  • ? - The number of existentially quantified variables
  • !> - The number of lambda-pi quantified (polymorphic) variables (TH1 and TF1)

  The fields in the solution lines of the ProblemAndSolutionStatistics file are:

  • System name
  • Res - The result established (using the SZS ontology)
  • RsT - The CPU time taken to get the result
  • Out - The output claimed (using the SZS ontology)
  • SZS - The output detected during analysis (it might be difference from what was claimed, e.g., if the output was not in TPTP format)
  • DDpDSz - If the output is some form of derivation then the derivation depth. If the output is a finite domain model then the domain size.
  • Leaves - The number of leaves if the output is a derivation.
  • All other fields as for a problem.

tptp2X [-h][-q<Level>][-i][-s<Size>][-t<Transform>][-f<Format>] [-d<Directory>] -l<NamesFile>|<TPTPFiles>

• -s<Size> : This specifies the required sizes when generating problems. <Size> is either an integer, a <Low>..<High> integer size range, or a : separated list of <Sizes>.
  • An integer directly specifies the required problem size.
  • Each integer in a size range is used to generate a separate set of formulae.
  • A : separated string of <Sizes> is used for generators that require multiple parameters, one <Size> for each size parameter required. For example, -s3..5:2 means the three sizes 3:2, 4:2, and 5:2.
  -s<Size> is ignored for problem (.p) files.
• -t<Transform> : Specifies format in which the output is to be written.
• -d<Directory> : Specifies the top level directory below which the output files are to be placed. If the <Directory> value is -, then all output files are written to standard output, and all informational output is suppressed (even quieter than -q2). If the input file has a TPTP domain name as its first three characters, the output files for that input file are placed in a subdirectory below the <Directory>, named according to the domain. Otherwise the output files are written in the <Directory>. The default <Directory> is a subdirectory below the TPTP Problems directory, named according to the <Format>.
• -l<NamesFile> : Specifies a file containing the names of the input files which are to be processed, one per line. This can be used instead of an explicit list of files, described next.
• <TPTPFiles> : Lists the input files which are to be processed. The TPTP problem name can be given in which case TPTP2X will find it in your TPTP installation. Three letter domain names can be given, which processes all problems in those domains. If no files are specified, the entire TPTP is processed. If the file name - is specified then input is taken from standard input and all output is written to standard output (overriding any <Directory> specification). The default <TPTPFiles> is all TPTP problem files.

  Hint: If your command shell complains about too many arguments as a result of expanding the <TPTPFiles> argument to a too large number of files, e.g., ~/TPTP/Problems/S*/*.p, place the <TPTPFiles> argument in 'single quotes', and TPTP2X will do the expansion internally.

• stdfof, to remove the connectives <=, <~>, ~|, and ~& from FOF problems, by rewriting formulae to use the other connectives. Suffix +stdfof.
• expand:conjectures, to expand a single FOF problem with multiple conjectures into multiple FOF problems with single conjectures. Suffix +xc_<Index>_<conjecture_name>.
• clausify:<Algorithm>, to transform FOF problems to CNF problems. The <Algorithm> is one of:
  • bundy, to use the algorithm presented in [Bun83],
  • otter, to use the algorithm used in Otter [McC98],
  • quaife, to use Art Quaife's algorithm [Qua90],
  • tptp, to use an algorithm combining features of the otter and quaife algorithms.
  Details of these algorithms can found in [SM96]. Note that these transformations do not simplify the resultant clause set; see the next two transformations for this. Suffix +cls_<Algorithm>.
• simplify, to simplify a set of clauses. Details of the simplifications performed can be found in [SM96]. Suffix +simp.
• cnf:<Algorithm>, to do clausify:<Algorithm> followed by simplify. Details of the performance of these transformations can be found in [SM96]. Generally cnf:otter and cnf:bundy produce clause sets with lower symbol counts than the other two. Suffix +cnf_<Algorithm>.
• fofify:obvious, to convert a set of 1st order clauses to a set of first-order formulae, converting negated_conjecture clauses into a correspoding conjecture. The transformation is very naive. Suffix +fof_obvious.
• axiomate, to remove all conjecture formulae. Suffix +axed.
• tff2fof[:<Inequalities>[:<KnownTypes>]], to convert TFF formulae to FOF. The value of :<Inequalities> can be either with or without, to indicate whether or not axioms that specify that terms from different domains are unequal should be generated. The default is with. The value of :<KnownTypes> is a []ed list of domains for which type guards are not needed. The default is [$i,$int,$rat,$real], i.e., assuming that the output will be given to a system that knows about terms and the numeric types. Suffix +tff2fof.
• propify, to convert a set of 1st order clauses to a set of propositional clauses, preserving satisfiability. The transformation is very naive. Suffix +prop.
• lr, to reverse the literal ordering in the clauses of CNF problems. Suffix +lr.
• cr, to reverse the clause ordering in CNF problems. Suffix +cr.
• clr, to do both clausal reversals. Suffix +clr.
• fr, to reverse the formula ordering in FOF problems. Suffix +fr.
• random, to randomly reorder the clauses and literals in CNF problems, or to randomly reorder the formulae in FOF problems. The rearrangement of formulae, clauses, and literals in a problem facilitates testing the sensitivity of an ATP system to the order of presentation. Suffix +ran.
• er, to reverse the arguments of unit equality clauses in CNF problems. Suffix +er.
• ran_er, to reverse the arguments of randomly selected unit equality clauses in CNF problems. Suffix +ran_er.
• add_equality[:<Add>], to add missing equality axioms to problems that contain equality. If the optional :<Add> flags are omitted, then all equality axioms are added. If the optional :<Add> flags are included, then <Add> is a string that indicates which equality axioms to add. The characters that can be in the string are as for the rm_equality transformation. Suffix +add_<Add>.
• rm_equality[:<Remove>], to remove equality axioms. If the optional :<Remove> flags are omitted, then all equality axioms are removed. If the optional :<Remove> flags are included, then <Remove> is a string that indicates which equality axioms to remove. The characters that can be in the string are:
  • r, to remove reflexivity,
  • s, to remove symmetry,
  • t, to remove transitivity,
  • f, to remove function substitution,
  • p, to remove predicate substitution.
  For example, -t rm_equality:stfp would remove symmetry, transitivity, function substitution, and predicate substitution. This transformation works only if the equality axiomatization is complete (i.e., including the axioms of reflexivity, symmetry, transitivity, function substitution for all functors, and predicate substitution for all predicate symbols). Suffix +rm_eq_<Remove>.
• set_equality[:<Set>], to set the equality axioms in problems that contain equality. If the optional :<Set> flags are omitted, then all equality axioms are set. If the optional :<Set> flags are included, then <Set> is a string that indicates which equality axioms to set. The characters that can be in the string are as for the rm_equality transformation. Suffix +set_eq_<Set>.
• to_equality, to convert CNF problems to a pure equality representation. Every non-equality literal is converted to an equality literal with the same sign. The arguments of the new equality literal are the atom of the non-equality literal and the constant true. Suffix +2eq.
• ifof:<Axioms> to convert intuitionistic propositional formulae to FOF. The <Axioms> specify which axiomatic basis to use. The options are:
  • goedel1
  • goedel2
  • mckinsey
  Suffix +ifof_<_<Axioms>.
• mfof:<Logic>:<Axioms> to convert modal propositional formulae to FOF. The <Logic> specifies which modal logic to use. The options are:
  • mm for multi-modal logic
  • k
  • d
  • m
  • b
  • s4
  • s5
  The <Axioms> specify which modal logic axioms to use. The options are:
  • benzmueller
  • k
  • d
  • m
  • b
  • s4
  • s5
  Suffix +mfof_<_<Logic>_<Axioms>.
• magic, to apply Mark Stickel's magic set transformation [Sti94] to CNF problems. Suffix +magic.
• shorten, to replace all the symbols in the problem by short, meaningless symbols. This is useful if you are only interested in the syntax of the problem, and do not want to read through the long, meaningful symbols that are often used in TPTP problems. Note that equality atoms are not affected. Suffix +shorten.
• none, to do nothing (same as omitting the -t parameter, but required for advanced use. No suffix.

• bliksem, to convert CNF problems to the Bliksem format [deN98]. Suffix .blk.
• dedam to convert CNF unit equality problems to the Dedam format [NRV97]. Suffix .dedam.
• dfg, to convert CNF problems to the DFG format [HKW96]. Suffix .dfg.
• dimacs, to convert propositional CNF problems to the DIMACS format [DIM]. Suffix .dimacs.
• eqp to convert CNF unit equality problems to the EQP format [McC00]. Suffix .eqp.
• geo, to convert problems to the Geo format [dNM06]. Suffix .geo.
• leancop, to convert problems to the leanCoP format [OB03]. Suffix .leancop.
• lf to convert problems to the LF format [Pfe89]. Suffix .lf.
• metitarski, to convert problems to the MetiTarski format [AP10]. Suffix .mski.
• otter:<SoS>:'<Otter options>', to convert FOF and CNF problems to the Otter .in format [McC94]. <SoS> specifies the Set-of-Support to use. It can be one of:
  • conjecture, to use the formulae whose type is conjecture
  • not_conjecture, to use the formulae whose type is not conjecture
  • hypothesis, to use the formulae whose type is hypothesis or conjecture
  • axioms, to use the formulae whose type is axiom
  • positive, to use the positive clauses
  • negative, to use the negative clauses
  • unit, to use the unit clauses
  • all, to use all formulae
  • none, to use no formulae (needed fo Otter's auto mode)
  '<Otter options>' is a quoted (to avoid UNIX shell errors), comma separated list of Otter options, which will be output before the formula lists. See the Otter Reference Manual and Guide [McC94] for details of the available options. For example, -f otter:none:'set(auto),assign(max_seconds,5)' would configure Otter to use its auto mode with a time limit of 5 seconds. As the auto mode is commonly used with Otter, the TPTP2X script allows the abbreviation -f otter to specify -f otter:none:'set(auto),set(tptp_eq),clear(print_given)'. If no -t parameter is specified then -f otter also sets -t equality:stfp. Suffix .in.
• prover9:<Options>, to convert problems to the Prover format [McCURL]. The <Options> specifies any Prover9 options. Suffix .in.
• smt2, to convert TFF and FOF problems to the SMT 2.0 format [BST10]. Suffix .smt2.
• tps, to convert THF problems to the TPS format [AB06]. Suffix .tps.
• tptp, to convert FOF and CNF problems to the TPTP format [SZS03]. Suffix .tptp.
• waldmeister, to convert CNF unit equality problems to the Waldmeister format [HBF96]. Suffix .pr.

Examples

~/TPTP/TPTP2X> tptp2X -tfr,random -f prover9 PUZ001+1

~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~tptp/tmp SYN001-1.g

~/TPTP/TPTP2X> tptp2X -tmagic+shorten - < ~tptp/TPTP/Problems/GRP/GRP001-1.p

The TPTP2X Interactive Mode

The parameters are similar to the TPTP2X script command line parameters. A summary, highlighting differences with "(!)", is given here.

• <TPTPFile> is the name of a single TPTP file. If the file name is not absolute, then it is considered to be relative to the directory specified in the tptp_directory/1 fact in the tptp2X.config file (!). If the file name is user (!), then input is taken from standard input.
• <Size> is either an integer, a : separated string of <Size>s, a <Low>..<High> integer size range, or a Prolog list of <Size>s (!). Each <Size> in a Prolog list of <Size>s is used to generate separate sets of formulae.
• <Transform> is either a single transformation specifier, a + separated string of <Transform>s, or a Prolog list (!) of <Transform>s.
• <Format> is an output format or a Prolog list (!) of output formats. An output file is written for each output format specified. For the otter format, the syntax is otter:<SoS>:[<Otter options>] (!), i.e., the Otter options form a Prolog list.
• <Directory> specifies the directory in which the output files are to be placed. If the <Directory> is user (!) then output is sent to standard output.

If you need help, please contact the TPTP developers.

Writing your own Problem Generators

If you need help, please contact the TPTP developers.

The TPTP2T script is written in perl.

Installation

Using TPTP2T

tptp2T [-f FileName] [-q1 or -q2 or -q3] [-pp or -ps or -pps] {[-]Constraint {[and/or] [-]Constraint}}

• The optional -f <ProblemFile> flag specifies the name of a file containing TPTP problem names. tptp2T will select statistics file lines for only those problems whose names appear in the <ProblemFile>. The problem names (without the .p extension) must appear one per line in the <ProblemFile>, and lines that start with # are ignored.
• The optional -q flag sets quietness: 1=continuous update, 2=final count (default), 3=quiet.
• The option -p flag indicates what output is required. -pp prints problem lines, -ps prints solution lines, -pps prints both. (Defaults: Only problem constraints = -pp, only solution constraints = -ps, both types of constraints = -pps)

• An optional - (hyphen) negates the meaning of any constraint.
• or allows for logical or between constraints.
• and allows for logical and between constraints.
• A space between constraints is treated as an and.
• { } allow for grouping of terms.
• For constraints in which an upper and lower bound are required, a - (hyphen) can be used to indicate don't care.

A problem Constraint is selected from:

• Domains ALG ANA ... TOP
  Only the listed problem domains.
• Form ???
  One of THF, TXF, TFF, FOF, CNF, ANY. Default is ANY.
• Status SZSStatus
  One of Theorem, CounterSatisfiable, Unsatisfiable, Satisfiable, Unknown, Open.
• Rating Min Max
  In the range 0.00 (easiest) to 1.00 (hardest)
• Formulae Min Max
  The number of formulae in the problem.
• UnitFormulae Min Max
  The number of unit formulae
• TypeFormulae Min Max
  The number of type formulae
• Atoms Min Max
  The number of atoms.
• EqualityAtoms Min Max
  The number of equality atoms.
• Equality
  Only problems that use equality.
• PureEquality
  Only problems that use only equality.
• UnitEquality
  Only problems with only unit-equality clauses/formulae.
• FOOLs
  Only problems with FOOL logic atoms/terms
• Arithmetic
  Only problems that use arithmetic.
• Types Min Max
  The number of types used
• Symbols Min Max
  The number of distinct symbols
• Predicates Min Max
  The number of predicates
• MinimalPredicateArity Min Max
  The minimal predicate arity
• MaximalPredicateArity Min Max
  The maximal predicate arity in TFF/FOF/CNF problems.
• Propositional
  Only propositional (only preducates of arity 0) problems
• Functions Min Max
  The number of functions
• MinimalFunctionArity Min Max
  The minimal function arity
• MaximalFunctionArity Min Max
  The maximal function arity
• Variables
  Only problems with variables.
• PIVariables
  Only problems with PI variables.

• System Name[---Version]
  ATP system which found a solution (ANY for any system).
• Result SZSStatus (Any SZS value, e.g., THM)
  Solutions with this result, or a result lower in the SZS ontology.
• ResultTime Min Max
  Solutions found in this time range.
• Output SZSDataform (Any SZS value, e.g., Ref)
  Solutions with this output, or an output lower in the SZS ontology.
• SolutionFormulae Min Max
  The number of formulae in the solution.
• SolutionLeaves Min Max
  The number of leaves in the solution (for DAGs).
• SolutionDepth Min Max
  The depth of the solution (for DAGs, from an axiom to a root).
• SolutionAtoms Min Max
  The number of atoms in the soltuion.
• Equality
  Only solutions that use equality.
• Arithmetic
  Only solutions that use arithmetic.
• Selectivity Min Max
  The ratio of solution leaves to problem formulae.
• Girth Min Max
  The ratio of solution leaves to solution depth.

These files are available online.

Installing the TPTP

prompt> tar xzf TPTP-v9.0.0 .tgz

prompt> cd TPTP-v9.0.0

prompt> ./Scripts/tptp2T_install
... the script will then ask for required information

prompt> ./TPTP2X/tptp2X_install
... the script will then ask for required information

If you don't have any Prolog installed, you need to get one first. Both utilities can be installed in a default configuration by appending a -default flag to the install command.

Important: Using the TPTP

Please contact the TPTP developers if ...

• You find any mistakes in the TPTP.
• You are able to provide further information for a TPTP problem.
• You want to contribute a problem to the TPTP. Please use the problem template that comes with the distribution. Fill in header information as far as possible. Any unambiguous representation will do for the formulae.
• You have any suggestions for improving the TPTP library.

Current proposals for extensions to the TPTP are online at http://www.tptp.org. Comments are welcome.

If you'd like to be kept informed of developments, join the TPTP World Google Group.

Acknowledgements