A certified basis of 13 identities

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

Identifier sb-16697909f03bdbd9 in the data of the bases-min seal.

Certified for

The identities

1. x² ≈ x⁴
2. x³yx ≈ xyx
3. x²yx ≈ xyx²
4. x²yx² ≈ xyx
5. x²y² ≈ xyxy
6. x²y² ≈ xy²x
7. x²y² ≈ yx²y
8. xyx ≈ xyx³
9. x³y² ≈ yx³y
10. xyzy ≈ xzy²
11. x²yzy ≈ yx²zy
12. xyxz² ≈ xyz²x
13. xyxz² ≈ zxyxz