IS H(BCK) FINITELY BASED?

A BCK-algebra is an algebra ⟨A; ∗, 0⟩ of type ⟨2, 0⟩ satisfying the following collection of identities and quasi-identities:

((x ∗ y) ∗ (x ∗ z)) ∗ (z ∗ y) ≈ 0
x ∗ 0 ≈ x
0 ∗ x ≈ 0

x ∗ y ≈ 0 & y ∗ x ≈ 0 ⊃ x ≈ y.

By a result of Wroński, the class BCK of all BCK-algebras is not a variety. The varietal closure of BCK is H(BCK), the class of all homomorphic images of members of BCK.

Problem: Is H(BCK) finitely based? If H(BCK) is finitely based, provide a finite axiomatisation.

From the perspective of AR, any solution to this problem will likely involve a mixture of AR and higher-order mathematics.

J. Raftery has stated that this problem appears to be very difficult.