A Common Lisp version of our theorem-prover is now available.  The
system runs well in three Common Lisps:  KCL, Symbolics, and Lucid.
There are no operating system or dialect conditionals, so the code may
well run in other implementations of Common Lisp.

Included as sample input is the work of Hunt on the FM8501
microprocessor and of Shankar on Goedel's incompleteness theorem and
the Church-Rosser theorem.

To get a copy follow these instructions:

1.   ftp to Internet host cli.com.
     (cli.com currently has Internet number
     192.31.85.1)
2.   log in as ftp, your name as password 
3.   get the file /pub/nqthm/README
4.   read the file README and follow the directions it gives.

Inquiries concerning tapes may be sent to:

    Computational Logic, Inc., Suite 290
    1717 W. 6th St.
    Austin, Texas 78703

A comprehensive manual is available.  For information on obtaining a
copy, write to the address above.

Bob Boyer         J Moore
boyer@cli.com     moore@cli.com