Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id XAA06530 for qed-out; Thu, 10 Aug 1995 23:54:52 -0500 Received: from coral.cs.jcu.edu.au (geoff@coral.cs.jcu.edu.au [137.219.53.16]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id XAA06525 for ; Thu, 10 Aug 1995 23:54:32 -0500 Received: (from geoff@localhost) by coral.cs.jcu.edu.au (8.6.10/8.6.10) id OAA00879 for qed@antares.mcs.anl.gov; Fri, 11 Aug 1995 14:54:27 +1000 From: Geoff Sutcliffe Message-Id: <199508110454.OAA00879@coral.cs.jcu.edu.au> Subject: Re: about the proof of the CheckerBoard Problem (fwd) To: qed@antares.mcs.anl.gov Date: Fri, 11 Aug 1995 14:54:26 +1000 (+1000) X-Mailer: ELM [version 2.4 PL23] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: owner-qed@mcs.anl.gov Precedence: bulk Hi, 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 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:): ftp 331 Guest login ok, send your complete e-mail address as password. Password: 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 where 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