A certified basis of 2 identities

This list of identities is a basis, proved in Lean, of 8 semigroups of order six, all of which generate the variety V[12182]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.

Identifier sb-30d8875f85b1610a in the data of the bases-min seal.

Certified for

[6, 12182] [6, 12295] [6, 12389] [6, 12441] [6, 14057] [6, 14208] [6, 14209] [6, 14215]

The identities

x²y ≈ xy
xyzy ≈ xzy²