Update: It turns out that Tomasz Kowalski had already published a proof by the time the McCune/Padmanabahn monograph came out.T. Kowalski. A syntactic proof of a conjecture of Andrzej Wronski. Rep. Math. Logic, 28:1000-1005, 1994. (pdf)The problem has been an interesting exercise for automated deduction in any case.
The quasivariety HBCK is defined as follows.
(M3) x * 1 = 1 (M4) 1 * x = x (M5) (x * y) * ((z * x) * (z * y)) = 1 (M7) x * y != 1 | y * x != 1 | x = y (M8) x * x = 1 (M9) x * (y * z) = y * (x * z) (H) (x * y) * (x * z) = (y * x) * (y * z)
The challenge is to find a first-order proof that the equation
(J) (((x * y) * y) * x) * x = (((y * x) * x) * y) * ycan be derived from HBCK. Blok and Ferreirim (see [2]) indicate that such a proof can be found, but the result relies on a model-theoretic argument.
Using the method of proof sketches [3], we have been able to find a proof with Otter [1]. Our proof makes use of the definition
g(x,y) = (((x * y) * y) * x) * xand can be found here.
[1] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.
[2] McCune, W., and Padmanabhan, R., Automated deduction in equational logic and cubic curves, Lecture Notes in Artificial Intelligence 1095, Springer-Verlag, Berlin (1996).
[3] Veroff, R., ``Solving open questions and other challenge problems using proof sketches,'' Journal of Automated Reasoning, Vol. 27, no. 2, pp. 157-174 (2001). (postscript)