WRT ...
> The TPTP problem library can be accessed through the URLs:
> http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
> http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
Gustav Meglicki suggests ...
> What about an ftp location of the whole package?
1. Obtaining the TPTP by FTP
prompt> cd <the directory where you want the TPTP to reside>
prompt> ftp -i coral.cs.jcu.edu.au # or: ftp -i 137.219.17.4
# or use
ftp -i flop.informatik.tu-muenchen.de # or: ftp -i 131.159.8.35
Name (coral.cs.jcu.edu.au:<your login-name>): ftp
331 Guest login ok, send your complete e-mail address as password.
Password:<your full login-name>
ftp> cd pub/research/tptp-library # on coral.cs.jcu.edu.au
cd pub/tptp-library # on flop.informatik.tu-muenchen.de
ftp> binary
ftp> mget *.gz
ftp> quit
Or use the World Wide Web (WWW) with either of the following URLs :
http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/TPTP.HTML
http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html
2. Installing the TPTP
prompt> gunzip -c TPTP-v1.2.0.tar.gz | tar xvf -
prompt> TPTP-v1.2.0/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. BinProlog
is freely available by anonymous ftp from clement.info.umoncton.ca:BinProlog
3. Converting all the TPTP problems to the syntax of other ATP systems
prompt> TPTP-v1.2.0/TPTP2X/tptp2X -f<Syntax>
where <Syntax> is one of kif, leantap, tap, meteor, mgtp, otter, pttp,
setheo, sprfn, or tptp.
The tptp option simply expands include directives, producing files in the
TPTP Prolog-style syntax. tptp2X offers MUCH more than this. See the TPTP
technical report for a detailed description of the utility, including
information on how to produce output in your own syntax.
Cheers,
Geoff
Geoff Sutcliffe
Department of Computer Science Email : geoff@cs.jcu.edu.au
James Cook University Phone : +61 77 815085/814622
Townsville, Australia, 4811. FAX : +61 77 814029