A certified basis of 7 identities

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

Identifier sb-d0f08e7466aa5a6b in the data of the bases-min seal.

Certified for

[6, 5614] [6, 5622] [6, 9451] [6, 9582]

The identities

x³ ≈ x⁴
xyxy ≈ xy²x
x³yx ≈ x²yx
x²yz ≈ xyxz
xyzxy ≈ xyzyx
xyzxz ≈ xyz²x
xyztxz ≈ xyztzx