If anyone would like to see and use Stickel's representation, it appears
as problems PUZ015-2 and PUZ016-2 of the forthcoming release of the
TPTP problem library. The release will be v1.2.0, and will be out soon.
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
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