Posted on the Web March 6, 2002. Last updated on September 11, 2005 by Bob Veroff.

# HBCK

The following problem is posed as an open question in .
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

```   (((x * y) * y) * x) * x = (((y * x) * x) * y) * y
```
can be derived from HBCK. Blok and Ferreirim (see ) indicate that such a proof can be found, but the result relies on a model-theoretic argument.

Using the method of proof sketches , we have been able to find a proof with Otter . Our proof makes use of the definition

```   g(x,y) = (((x * y) * y) * x) * x
```
and can be found here.

### References

 McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

 McCune, W., and Padmanabhan, R., Automated deduction in equational logic and cubic curves, Lecture Notes in Artificial Intelligene 1095, Springer-Verlag, Berlin (1996).

 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)