Errors in McCune's Papers

W. McCune and L. Wos. A case study in automated theorem proving: Searching for sages in combinatory logic. J. Automated Reasoning, 3(1):91--107, 1987.

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, Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 310, pages 714--729, Berlin, 1988. Springer-Verlag.

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. Automated Deduction in Equational Logic and Cubic Curves, Springer-Verlag LNAI #1095, 1996.

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.