This is Hao Wang's algorithm for theorem proving, written in SNOBOL4.
It may be found in a 1987 diskette containing the text and code of the report Artificial Intelligence Programming in SNOBOL4 written by Michael G. Shafto; and is adapted from the algorithm on pages 183-185 of The SNOBOL4 Programming Language by Griswold, Poage and Polonsky.