online-atps: OnlineATPs is a client for TPTP World and its ATPs

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


This package provides an interface to use the automatic theorem provers (ATPs) of TPTP World.

[Skip to ReadMe]


Change logNone available
Dependenciesaeson (>= && <1.2), base (>= && <4.10), bytestring (>= && <0.11), directory (>= && <1.4), filepath (>= && <1.5), HTTP (>=4000 && <5000), http-client (>=0.5.1 && <1.0), mtl (>=2.2.1 && <2.3), network (>=2.6.0 && <3.0), pretty (>= && < || >=1.1.2 && <1.2), split (>=0.2 && <1.0), tagsoup (>=0.14 && <1.0), text (>= && <1.3), unordered-containers (==0.2.*), yaml (>=0.8.17 && <0.9) [details]
AuthorJonathan Prieto-Cubides
MaintainerJonathan Prieto-Cubides <>
CategoryLogic, Theorem Provers
Home page
Bug tracker
Source repositoryhead: git clone git://
UploadedTue Jan 24 23:04:17 UTC 2017 by jonaprieto



when develop takes places.


Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainers' corner

For package maintainers and hackage trustees

Readme for online-atps-

[back to package description]

OnlineATPs Build Status

OnlineATPs is a client for SystemOnTPTP that allows us to take advantage of using ATPs without install any of them.


$ cabal update
$ cabal install cabal-install


$ git clone
$ cd online-atps
$ cabal install

Also, yo may interested in checking the Makefile and execute make install-bin.


The work flow using OnlineATPs consists mainly in provide a problem in TSTP format, and ATP name and then wait over a second while the request takes place in TPTP world and returns with a response. Let's see.

$ online-atps --list-atps
$ online-atps --help
Usage: online-atps [OPTIONS] FILE

    --atp=NAME          Set the ATP (online-e, online-vampire, online-z3, ...)
    --fof               Only use ATP for FOF
    --help              Show this help
    --list-atps         Consult all ATPs available in TPTP World
    --only-check        Only checks the output looking for a theorem.
    --time=NUM          Set timeout for the ATPs in seconds (default: 300)
    --version           Show version number
    --version-atp=NAME  Show version of the atp NAME
$ cat basic.tptp
fof(a1, axiom, a).
fof(a2, axiom, b).
fof(a3, axiom, (a & b) => z).
fof(a4, conjecture, z).

Prove the conjecture with the help of ATPs. You could use one from the list (--list-atps option) or with all ATPs available. For instance, let's try with Vampire:

$ online-atps basic.tptp --atp=vampire
% SZS start RequiredInformation
% Congratulations - you have become a registered power user of SystemOnTPTP,
at IP address
% Please consider donating to the TPTP project - see for
% When you donate this message will disappear.
% If you do not donate a random delay might be added to your processing time.
% SZS end RequiredInformation
Vampire---4.1   system information being retrieved
Vampire---4.1's non-default parameters being retrieved
    -t none
    -f tptp:raw
    -x vampire --mode casc -m 90000 -t %d %s
Vampire---4.1   being checked for execution
Vampire---4.1   checking time limit 240
Vampire---4.1   checking problem name /tmp/SystemOnTPTPFormReply38743/
% ------------------------------
% Version: Vampire 4.1 for CASC J8 Entry
% Termination reason: Refutation

% Memory used [KB]: 511
% Time elapsed: 0.043 s
% ------------------------------
% ------------------------------
% Success in time 0.045 s

RESULT: SOT_Xry401 - Vampire---4.1 says Theorem - CPU = 0.00 WC = 0.04
OUTPUT: SOT_Xry401 - Vampire---4.1 says Refutation - CPU = 0.00 WC = 0.04


Check the issues. Thanks.