Skip to main content

A library for handling TPTP related input and systems

Project description

A TPTP python package


  • install python >= 3.5
  • clone this repository


Run locally:

List all solvers

python3 -m tptp local list-solvers

Run Leo III.

$ python3 -m tptp local run --solver-name leo3 --problem problems/SYN001+1.p --timeout 60

Run cvc4

$ python3 -m tptp local run --solver-name cvc4 --problem problems/SYN001+1.p --timeout 60

Run System-on-TPTP:

List all solvers

$ python3 -m tptp system-on-tptp list-solvers

Run Leo III.

$ python3 -m tptp system-on-tptp request --solver-name "Leo-III---1.4" --solver-command "run_Leo-III %s %d" --problem "problems/SYN001+1.p" 

Test the competition mode

$ python3 -m tptp competition competition-test/

Run with more output. Good for error tracking.

$ python3 -m tptp competition competition-test/ --verbose

Making a solver TPTP ready

SZS Status, SZS Ontology

A solver can be used by this libary if it supports the SZS Ontology as its result on the stdout.

The solution status should be reported exactly once, in a line starting % SZS status" (the leading '%' makes the line into a TPTP language comment).

For instance, a SAT-solver started for problem SYN001+1 should output the line

% SZS status Satisfiable for SYN001+1

as part of its output if it proves the problem is satisfiable.


  • if your solver proves the problem is unsatisfiable, the line % SZS status Unsatisfiable for SYN001+1.
  • if your solver gaves up the prove, the line % SZS status GaveUp for SYN001+1.
  • a full list of possible values for the SZS Status can be found at the SZS Ontology definition.

Any prove or prove-model should additionally be printed on the stdout in the following form.

% SZS output start CNFRefutation for SYN001+1
% SZS output end CNFRefutation for SYN001+1

Test your solver

To test your solve add it to our test competition, which can be found at


Here you add your solver to the SOLVERS constant

        'type': 'local',
        'name': 'my-solver',
        'pretty-name': 'MySolver'
        'command': 'my-solver-binary-or-shell-script %s -t %d',

This will ensure that your solver

  • is called my-solver and is pretty printed MySolver
  • when invoked to solve the problem absolute/path/SYN001+1.p within a timeout of 60 seconds the program/shellscript my-solver-binary-or-shell-script "absolute/path/SYN001+1.p" -t 60 is called
  • your problem should output an SZS Status from the SZS Ontology (see above)

Running our test competition should now list your solver.

$ python3 -m tptp competition competition-test/
% Satisfiable for Sat1.cnf expecting Satisfiable with MySolver -t 60s which is correct

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

tptp-0.0.3.dev2.tar.gz (31.3 kB view hashes)

Uploaded source

Built Distribution

tptp-0.0.3.dev2-py3-none-any.whl (45.2 kB view hashes)

Uploaded py3

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page