J. A. Robinson's Lisp code for his resolution theorem prover

Here are the pages - from Chapter 13 of "Logic: Form and Function" - where J. A. Robinson documents and describes his hyper-resolution theorem prover in Lisp. You will find the Lisp interestingly archaic.

My apologies for the poor quality - it was done in a rush. Nevertheless, the material is quite readable. It's published as the PDF link below.

PDF