Inside the TPTP

Scope.
Release v2.7.0 of the TPTP contains 4880 abstract problems, which result in 7267 ATP problems (due to alternative presentations, see Sections Problem Versions and Problem Generators). There are 1678 abstract FOF problems, which result in 1745 FOF ATP problems, and 4363 abstract CNF problems, which result in 5522 CNF ATP problems. The TPTP documents OverallSynopsis, FOFSynopsis, and CNFSynopsis provide some overall statistics about the TPTP.

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, and others. The domains are presented and discussed in Section The TPTP Domain Structure.

Sources
The problems have been collected from various sources. The two principal sources have been 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; smaller numbers of problems have been provided by a number of further contributors (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 v<Version>.<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.

The TPTP Domain Structure

This section provides the structure according to which the problems are grouped into domains. Some information about the domains is also given.

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. Five main fields are defined: logic, mathematics, computer science, engineering, 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 (see Section  Problem and Axiomatization Naming). 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

Logic Combinatory logic COL
Logic calculi LCL
Henkin models HEN
Mathematics Set theory SET
Graph theory GRA
Algebra Boolean algebra BOO
Robbins algebra ROB
Left distributive LDA
Lattices LAT
Groups GRP
Rings RNG
Homological algebra HAL
General algebra ALG
Number theory NUM
Topology TOP
Analysis ANA
Geometry GEO
Field theory FLD
Category theory CAT
Computer science Computing theory COM
Knowledge representation KRS
Natural Language Processing NLP
Planning PLA
Agents AGT
Software creation SWC
Software verification SWV
Engineering Hardware creation HWC
Hardware verification HWV
Social sciences Management MGT
Other Syntactic SYN
Puzzles PUZ
Miscellaneous MSC
The Domain Structure of the TPTP.

A brief description of the domains, with a non-ATP reference for a general introduction and a generic ATP reference, is given below. For each domain, appropriate DDC and MSC numbers are also given:

Problem Versions and Standard Axiomatizations

There are often many ways to formulate a problem for presentation to an ATP system. Thus, in the TPTP, there are often alternative presentations of a problem. The alternative presentations are called versions of the underlying abstract problem. As the problem versions are the objects that ATP systems must deal with, they are referred to simply as problems, and the abstract problems are referred to explicitly as such. Each problem is stored in a separate physical file. In the TPTP the most coarse grain differentiation between problem versions is whether the problem is presented in FOF or CNF. Within a given presentation, the primary reason for different versions of an abstract problem is the use of different axiomatizations. This issue is discussed below. A secondary reason is different formulations of the theorem to be proved, e.g., different clausal forms of a FOF problem.

Different Axiomatizations
Commonly, many different axiomatizations of a theory exist. By using different axiomatizations of a particular theory, different versions of a problem can be formed.

In the TPTP an axiomatization is standard if it is a complete axiomatization of an established theory, no lemmas have been added, and it is not designed specifically to be suited or ill-suited to any ATP system, calculus, or control strategy. A problem version is standard if it uses a standard axiomatization. (Note: A standard axiomatization may be redundant, because some axioms are dependent on others. In general, it is not known whether or not an axiomatization is minimal, and thus the possibility of redundancy in standard axiomatizations must be tolerated.) In the TPTP, standard axiomatizations are kept in separate axiom files, and are included in problems as appropriate. Sets of specialization axioms may be used to extend or constrain an axiomatization. Specialization axioms are also kept in separate axiom files.

Within the ATP community, some problems have been created with non-standard axiomatizations. A non-standard axiomatization may be formed by modifying a standard axiomatization: the standard axiomatization may be reduced (i.e., axioms are removed) and the result is an incomplete axiomatization, or it may be augmented (i.e., lemmas are added) and the result is a redundant axiomatization. Incomplete and redundant axiomatizations are typically used to find a proof of a conjecture (based on the axiomatization) using a particular ATP system. An axiomatization may also be non-standard because it is biased, i.e., designed specifically to be suited or ill-suited to some ATP system, calculus, or control strategy. A problem version is incomplete, redundant, or biased if its axiomatization is. In the TPTP, for each incomplete, redundant, and biased problem, a new version of the problem with a standard axiomatization is usually created. Finally, an axiomatization may be non-standard because it does not capture any established theory. i.e., a standard axiomatization does not exist, but the axioms are not biased. A problem version with such an axiomatization is especial. Typically, the axioms in an especial problem are specific to that problem, and are not used in any other problem.

In any 'real' application of an ATP system, a standard or especial problem version would typically be used, at least initially. The use of standard axiomatizations is particularly desirable.

Equality Axiomatization
In the TPTP equality is represented using the equal/2 predicate, written in prefix notation like all other predicates. The equal/2 predicate is used if the equality axiomatization in the problem is complete, i.e., including the required axioms of reflexivity, symmetry, transitivity, function substitution for all functors, and predicate substitution for all predicate symbols. Such a complete equality axiomatization may be either explicit - the axioms are provided, or implicit - the axioms can be derived. If the equality axiomatization is not complete, but the 'intention' is to represent equality, the equalish/2 predicate is used.

If a standard axiomatization uses equality, the required axioms of substitution are kept separate from the theory specific axioms. The equality axioms of reflexivity, symmetry, and transitivity are also kept in a separate file.

Many ATP systems have built in mechanisms, e.g., paramodulation, that make some or all of the equality and substitution axioms unnecessary. If any of these axioms are removed when the problems are submitted to an ATP system, then the removal must be explicitly noted in reported results (see Section Using the TPTP). The tptp2X utility (see Section The tptp2X Utility) can be used to remove equality axioms.

Problem Generators

Some abstract problems have a generic nature, and particular instances of the abstract problem are formed according to some size parameter(s). An example of a generic problem is the N-queens problem: place N queens on a N by N chess board such that no queen attacks another. The formulae for any size of this problem can be generated automatically, for any size of N >= 2. Note that satisfiability may depend on the problem size.

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 may 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, and a full description of their use is given in Section The tptp2X Utility.

For convenience, the TPTP still contains, where they exist, a theorem and a non-theorem size instance of each generic problem. The TPTP sizes chosen are non-trivial, unless the problem remains easy up to sizes that have very large files. In the latter situation the TPTP size is that used in TPTP v1.2.0. The statistics in the TPTP documents Overall synopsis, FOF synopsis, and CNF synopsis take into account these instances of generic problems.

Problem, Generator, and Axiomatization Naming

Providing unambiguous names for all problems is necessary in a problem library. A naming scheme has been developed for the TPTP, to provide unique, stable names for abstract problems, problems, axiomatizations, and generators. Files are assigned names according to the schemes depicted in Sections Problem Naming and Axiom Naming. The DDDNNN combination provides an unambiguous name for an abstract problem or axiomatization. The DDDNNNFV[.SSS] combination provides an unambiguous name for a problem or generator, and the DDDNNNFE combination provides an unambiguous name for a set of axioms. The complete file names are unique within the TPTP. For example, the file GRP135-1.002.p contains the group theory problem number 135, version number 1, generated size 2. Similarly, the file CAT001-0.ax contains the basic category theory axiomatization number 1.

DDD NNN F V .SSS .T
DDD - Domain name abbreviation. The domain names and their abbreviations are listed in Section  The Domain Structure of the TPTP.
NNN - Abstract problem number. It is unique within the domain.
F - Form. - for CNF and + for FOF.
V - Version number. It differentiates between different versions of the abstract problem, as discussed in Section  Problem Versions.
SSS - Size parameter(s). These only occur for generated problems, and give the size parameter(s).
T - File name extension. p for problem files, g for generator files.

Problem file naming scheme.

The abstract problem numbers within each domain are not always successive. This is because some numbers have already been allocated to problems that will be part of a future TPTP release (see Section The Present).

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.

DDD NNN F V .TT
DDD - Domain name abbreviation. The domain names and their abbreviations are listed in Section  The Domain Structure of the TPTP.
NNN - Axiomatization number. It is unique within the domain.
F - Form. - for CNF and + for FOF.
V - Specialization number. It identifies sets of axioms that are used to specialize an axiomatization. Axiomatizations of basic theories are allocated the number 0, and specialization axiom sets are numbered from 1 onwards.
T - File name extension. An extension ax denotes a file containing axioms specific to a theory. An extension eq denotes a file containing equality substitution axioms for the corresponding theory specific axioms.

Axiom file naming scheme.

If a file is ever removed from or renamed in the TPTP, then the 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.

Problem Presentation

The physical presentation of the TPTP problem library is such that ATP researchers can easily use the problems. The TPTP file format, for problem files and axiom files, has three main sections. The first section is a header section that contains information for the user. This information is not for use by ATP systems (see Section Using the TPTP). The second section contains include instructions for axiom files. The last section contains the formulae that are specific to the problem or axiomatization. TPTP generator files have three sections, different from the problem and axiom files. The header section of generator files is similar to that of problem and axiom files, but with place-holders for information that is filled in based on the size of problem and the formulae generated. Following that comes Prolog source code to generate the formulae, and finally data describing the permissible sizes and the chosen TPTP size for the problem. More details are given in Section  Writing your own Problem Generators.

The syntax of all files is that of Prolog. This conformance makes it trivial to manipulate the files using Prolog. All information in the files that is not for use by ATP systems is formatted as Prolog comments, with a leading %. The formulae are formatted as Prolog facts. The tptp2X utility can be used to convert TPTP files to other known ATP system formats (see Section The tptp2X Utility). A description of the information contained in TPTP files is given below.

The Header Section

This section contains information about the problem, for the user. It is divided into four parts separated by blank lines. The first part identifies and describes the problem. The second part provides information about occurrences of the problem in the literature and elsewhere. The third part gives the problem's ATP status and a table of syntactic measurements made on the problem. The last part contains general information about the problem. Examples of TPTP headers, extracted from the problem files GRP194+1.p and GRP039-7.p, are shown in Figures Example FOF header and Example CNF header. 

%--------------------------------------------------------------------------
% File     : GRP194+1 : TPTP v2.2.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.00 v2.1.0
% Syntax   : Number of formulae    :   19 (   3 unit)
%            Number of atoms       :   47 (  22 equality)
%            Maximal formula depth :    6 (   3 average)
%            Number of connectives :   28 (   0 ~  ;   0  |;  11  &)
%                                         (   1 <=>;  16 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    3 (   0 propositional; 2-2 arity)
%            Number of functors    :    5 (   3 constant; 0-3 arity)
%            Number of variables   :   47 (   0 singleton;  46 !;   1 ?)
%            Maximal term depth    :    3 (   1 average)


% Comments : 
%--------------------------------------------------------------------------
Example of a FOF problem file header (GRP194+1.p). 

%--------------------------------------------------------------------------
% File     : GRP039-7 : TPTP v2.2.0. Bugfixed v1.0.1.
% Domain   : Group Theory (Subgroups)
% Problem  : Subgroups of index 2 are normal
% Version  : [MOW76] (equality) axioms : Augmented.
% English  : If O is a subgroup of G and there are exactly 2 cosets
%            in G/O, then O is normal [that is, for all x in G and
%            y in O, x*y*inverse(x) is back in O].


% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% Source   : [MOW76]
% Names    : GP2 [MOW76]


% Status   : unsatisfiable
% Rating   : 0.60 v2.2.0, 0.67 v2.1.0, 0.89 v2.0.0
% Syntax   : Number of clauses    :   25 (   2 non-Horn;  13 unit;  12 RR)
%            Number of literals   :   43 (  28 equality)
%            Maximal clause size  :    4 (   1 average)
%            Number of predicates :    2 (   0 propositional; 1-2 arity)
%            Number of functors   :    8 (   5 constant; 0-2 arity)
%            Number of variables  :   38 (   0 singleton)
%            Maximal term depth   :    3 (   1 average)


% Comments : Used to define a subgroup of index two is a theorem which
%            says that {for all x, for all y, there exists a z such that
... some lines removed here for brevity
% Bugfixes : v1.0.1 - Duplicate axioms multiply_inverse_left and 
%            multiply_inverse_right removed.
%--------------------------------------------------------------------------
Example of a CNF problem file header (GRP039-7.p).

The % File field.
This field contains three items of information. The first item is the problem's name. The current TPTP release number is given next, followed by the TPTP release in which the problem was released or last bugfixed (i.e., the formulae were changed). The problem name in Figure Example CNF header is GRP039-7. The TPTP release is v2.2.0, and the problem clauses were last bugfixed in release v1.0.1.

The % Domain field.
The domain field identifies the domain, and possibly a subdomain, from which the problem is drawn (see Section  The TPTP Domain Structure). The domain corresponds to the first three letters of the problem name. The domain of the problem of Figure Example CNF header is Group Theory, and the subdomain is Subgroups.

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. Thus, the problem of Figure Example CNF header proves that Subgroups of index 2 are normal.

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. In the problem of Figure Example CNF header the axiomatization used is that of [MOW76]. If the axiomatization is a pure equality axiomatization (uses only the equal/2 predicate) then this is noted too, as is the case in Figure Example CNF header.

The second possible differentiation is the status of the axiomatization, as discussed in Section Problem Versions. There are 12 possiblities:

In the problem of Figure Example CNF header an existing standard axiomatization has been Augmented, and has become non-standard due to redundancy.

The third possible differentiation between problem versions is in the theorem formulation. Variations in the theorem formulation are noted in a Theorem formulation entry, e.g.,

% 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.
The problems in the TPTP have been (physically) obtained from a variety of sources, both hardcopy and electronic. In this field the source of the problem is acknowledged, 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:

The problem of Figure Example CNF header was taken from [MOW76].

The % Names field.
Problems which have appeared in other problem collections or the literature, often have names which are known in the ATP community. This field lists all such names known to us for the problem, along with the source of the name. If the source is an existing problem collection then the collection name is cited, as in the % Source field. If the source of a name is a paper then a citation is given. If a problem is not given a name in a paper then ``-'' is used as the known name and a citation is given. Problems which first appeared in the TPTP have source TPTP, and no other name. In generator files all known names for instances of the abstract problem are listed, with the instance size given before the source. A reverse index, from known names to TPTP names, is distributed with the TPTP (see Section Physical Organization). The problem of Figure Example CNF header is called GP2 in [MOW76].

The % Status field.
This field gives the ATP status of the problem. For FOF problems it is one of:

For CNF problems it is one of: In Figure Example CNF header the status is unsatisfiable.

The % Rating field.
This field gives the difficulty of the problem, measured relative to state-of-the-art ATP systems. The rating is a real number in the range 0.0 to 1.0, where 0.0 means that all state-of-the-art ATP systems can solve the problem (i.e., the problem is easy), and 1.0 means no state-of-the-art ATP system can solve the problem (i.e., the problem is hard). The rating is followed by a TPTP release number, indicating in which release the rating was assigned. If no rating has been assigned, a ? is given. In Figure Example CNF header the rating is 0.60, assigned in release v2.2.0.

The % Syntax field.
This field lists various syntactic measures of the problem's clauses. The measures for CNF problems are: the number of clauses, the number of non-Horn clauses, the number of unit clauses, the number of range restricted clauses, the number of literals, the number of equality literals, the maximal and average clause size (measured by number of literals), the number of distinct predicate symbols, the number of distinct propositional symbols, the minimal and maximal predicate symbol arities, the number of distinct function symbols, the number of distinct constants, the minimal and maximal functor arities, the number of distinct variables, the number of singleton variables (variables that appear only once in a clause), and the maximal and average term depth (with constants and variables having depth 1). The measures for FOF problems are: the number of formulae, the number if unit formulae, the number of atoms, the number of equality atoms, the maximal and average formula depth, the number of connectives, the numbers of each type of connective, the number of distinct propositional symbols, the minimal and maximal predicate symbol arities, the number of distinct function symbols, the number of distinct constants, the minimal and maximal functor arities, the number of distinct variables, the number of singleton variables, the numbers of universally and existentially quantified variables, and the maximal and average term depth. See Section Inside the TPTP for a summary of this information over the entire TPTP.

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 (see Section 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. In the problem of Figure Example CNF header a bugfix was made in release v1.0.1, by removing duplicate multiply_inverse_left and multiply_inverse_right clauses.

The Include Section

The include section contains include instructions for TPTP axiom files. An example is shown in Figure Example include section, extracted from the problem file GRP194+1.p. 

%--------------------------------------------------------------------------
%----Include reflexivity from the axioms of equality
include('Axioms/EQU001+0.ax',[reflexivity]).
%----Include Semigroup axioms
include('Axioms/GRP007+0.ax').
%----Include Substitution axioms for semigroup axioms
include('Axioms/GRP007+0.eq').
%--------------------------------------------------------------------------
Example of a problem file include section (GRP194+1.p).

Each of the include instructions indicates that the formulae in the named axiom file should be included at that point. If the include instruction has a second argument, it may be a formula name or []ed list of formulae names, in which case only the named formulae are included from the file. If there is no second argument, or the second argument is all, then all the formulae in the file are included. In Figure Example include section only reflexivity is included from Axioms/EQU001+0.ax. Full versions of TPTP problems (without include instructions) can be created by using the tptp2X utility (see Section The tptp2X Utility).

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.

The Formulae Section for FOF Problems

The atoms that appear in a formula are presented in the form of Prolog terms. The connectives used to build non-atomic formulae are prefix ~ for negation, 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), and infix ~& for negated conjunction (NAND). Negation has higher precedence than the binary connectives, but no precedence between binary connectives is assumed; brackets are used to ensure the correct association. The binary connectives are right associative. The universal quantifier is ! and the existential quantifier is ?. Quantified formulae are written in the form <Quantifier> [<Variables>] : <Formula>. FOF formulae can be read as Prolog terms using appropriate operator definitions.

Each formula has a name, in the form of a Prolog atom. Each formula also has a type, one of axiom, hypothesis, or conjecture. There can be at most one conjecture formula, in which case the problem is to determine if the conjecture is a theorem of the axiom and hypothesis formulae. If there is no conjecture then the problem is to determine if the formulae are satisfiable. The name, type, and formula are bundled as the three arguments of a Prolog fact, whose predicate symbol is input_formula. These facts are in the formulae section of the problem file.

An example of a formula section, extracted from the problem file GRP194+1.p, is shown in Figure  Example FOF formulae. 

%--------------------------------------------------------------------------
input_formula(phi_substitution_1,axiom,(
    ! [A,B] :
      ( equal(A,B)
     => equal(phi(A),phi(B)) )   )).

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

... some formulae omitted here for brevity

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

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

input_formula(prove_left_zero_h,conjecture,(
    left_zero(h,phi(f_left_zero))   )).
%--------------------------------------------------------------------------
Example of a FOF problem file formulae section (GRP194+1.p).

The Clauses Section for CNF Problems

The literals that make up a clause are presented as a Prolog list of terms (i.e., in [ ]). Each literal is a unary term whose functor is either ++ or --, indicating a positive or negative literal respectively. The argument of the term is the atom of the literal, in the form of a Prolog term. Thus predicate symbols and functors start with lower case alphanumeric, and variables start with upper case alphabetic. Variables may not start with an _. All symbols contain only alphanumerics and _. If a symbol starts with a numeric, it contains only numerics (i.e., it is a number). FOF formulae can be read as Prolog terms using appropriate operator definitions for ++ and --.

Each clause has a name, in the form of a Prolog atom. Each clause also has a type, one of axiom, hypothesis, or conjecture. Clauses of type conjecture are derived from the negation of the underlying FOF conjecture. If there are conjecture clauses then the problem is to determine if the clause set is unsatisfiable, corresponding to the underlying conjecture being a theorem of the underlying axioms and hypotheses. If there are no conjecture clauses then the problem is to determine if the clauses are satisfiable. Formulae are of type hypothesis only if they can clearly be determined as such; otherwise they are of type conjecture. The name, type, and literal list of each clause are bundled as the three arguments of a Prolog fact, whose predicate symbol is input_clause. These facts are in the clauses section of the problem file.

An example of a clause section, extracted from the problem file GRP039-7.p, is shown in Firgure  Example CNF clauses. 

%--------------------------------------------------------------------------
%----Redundant two axioms
input_clause(right_identity,axiom,
    [++equal(multiply(X,identity),X)]).

input_clause(right_inverse,axiom,
    [++equal(multiply(X,inverse(X)),identity)]).

... some clauses omitted here for brevity

%----Denial of theorem
input_clause(b_in_O2,hypothesis,
    [++subgroup_member(b)]).

input_clause(b_times_a_inverse_is_c,hypothesis,
    [++equal(multiply(b,inverse(a)),c)]).

input_clause(a_times_c_is_d,hypothesis,
    [++equal(multiply(a,c),d)]).

input_clause(prove_d_in_O2,conjecture,
    [--subgroup_member(d)]).
%--------------------------------------------------------------------------
Example of a CNF problem file clause section (GRP039-7.p).

Physical Organization

The TPTP is physically organized into six subdirectories, as follows: