Problem HBCK-1. A first-order proof of a theorem in HBCK. The type is ⟨2, 0⟩ with constant 1. The quasivariety HBCK is defined by

\{ \begin{matrix}x · 1 = 1 & (M3) \\ 1 · x = x & (M4) \\ (x · y) · ((z · x) · (z · y)) = 1 & (M5) \\ x · y = 1, y · x = 1 → x = y & (M7) \\ x · x = 1 & (M8) \\ x · (y · z) = y · (x · z) & (M9) \\ (x · y) · (x · z) = (y · x) · (y · z) & (H) \end{matrix} \} .

Theorem (Blok and Ferreirim [?]). HBCK is an equational class of algebras defined by the equations (M3-5,8-9), (H), and (J):

(((x · y) · y) · x) · x = (((y · x) · x) · y) · y. (J)

Find a first-order derivation of (J) from the axioms of HBCK:

{M3,M4,M5,M7,M8,M9,H} → {J}.

The known proof is model theoretic.