W. McCune and L. Wos. A case study in automated theorem proving: Searching for sages in combinatory logic.

In Section 7, the extensionality is written incorrectly as [all x all y all z] (xy)=(zy) -> x=z. It should be [all x all z] ([all y] (xy)=(zy)) -> x=z. The clause form of extensionality (clause 4) should be s(x,g(x,z)) != s(z,g(x,z)) | x=z, and clauses 6 and 7 should have the Skolem term g(J,K). Otherwise, the proof is correct.

L. Wos and W. McCune. Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs. In E. Lusk and R. Overbeek, editors,

Section 2.4, Problem 4. The example S (S (K S) K) (S (K (S (S (S K K) (S K K)))) K) of a U combinator is incorrect. We switched the variables when constructing the combinator: in fact, it behaves like a combinator U', where U'xy = x(yyx).

W. McCune and R Padmanabhan.

Page 164, 6 lines from the bottom of the page. The equation for collapsing a pair of absorption equations should be p(u,g(x),x) = p(u,h(y),y).

*Please let me know if you find any substantial errors not listed here.*