The online-atps package


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

[Skip to ReadMe]


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


devwhen develop takes places.DisabledManual

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-

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.