A certified basis of 13 identities

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

Identifier sb-2699b275605820b1 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. xyx ≈ xyx³
8. x²y³ ≈ xy³x
9. x²yz ≈ xyxz
10. xyzx ≈ xzyx
11. xyzy ≈ xzy²
12. x²yzy ≈ xy²zx
13. xyzt ≈ xzyt