A certified basis of 3 identities

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

Identifier sb-9fcf92f0a235cdcb in the data of the bases-min seal.

Certified for

[6, 1117] [6, 1169] [6, 1175] [6, 1186] [6, 1194] [6, 1196] [6, 1197] [6, 1198] [6, 1199] [6, 1200] [6, 1204] [6, 1205] [6, 1206] [6, 3050] [6, 3830] [6, 3831] [6, 3949] [6, 3997] [6, 6359]

The identities

x² ≈ x³
x²y ≈ xyx
xyx ≈ yx²