A certified basis of 30 identities

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

Identifier sb-8c24b3a747abbf86 in the data of the bases-min seal.

Certified for

The identities

1. x³ ≈ x²y
2. x³ ≈ xy²
3. x³ ≈ yx²
4. x³ ≈ y²x
5. x³ ≈ y³
6. x²y ≈ xy²
7. x²y ≈ yx²
8. x²y ≈ y²x
9. xyx ≈ yxy
10. xy² ≈ yx²
11. x³ ≈ y²z
12. x³ ≈ yz²
13. x²y ≈ x²z
14. x²y ≈ xz²
15. x²y ≈ y²z
16. x²y ≈ yz²
17. x²y ≈ zx²
18. x²y ≈ zy²
19. x²y ≈ z²y
20. xy² ≈ xz²
21. xy² ≈ yz²
22. xy² ≈ zy²
23. xyz ≈ zyx
24. x²y ≈ z²t
25. x²y ≈ zt²
26. xy² ≈ zt²
27. x³ ≈ yztu
28. x²y ≈ ztuv
29. xy² ≈ ztuv
30. xyzt ≈ uvws