A certified basis of 1 identity

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

Identifier sb-6205a9618f023946 in the data of the bases-min seal.

Certified for

[6, 13172] [6, 13173] [6, 13197] [6, 13198] [6, 13778] [6, 14270] [6, 14537]

The identities

xy ≈ xyx