A certified basis of 57 identities

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

Identifier sb-6da0c641429cb63e in the data of the bases-min seal.

Certified for

The identities

1. x³ ≈ x⁴
2. x³ ≈ x⁴
3. x³ ≈ x⁴
4. x²y² ≈ xyxy
5. x²y² ≈ xyxy
6. x²y² ≈ xyxy
7. xyxy ≈ xy²x
8. xyxy ≈ yx²y
9. x³yx ≈ x²yx
10. x³yx ≈ x²yx
11. x²yx ≈ x²yx²
12. x²yx² ≈ xyx²
13. xyx² ≈ xyx³
14. xyx² ≈ xyx³
15. x²yzy ≈ x²zy²
16. x²yzy ≈ xyxzy
17. x²yzy ≈ xyzxy
18. x²yz² ≈ xyxz²
19. x²yz² ≈ xyzxz
20. x²yz² ≈ xzxyz
21. x²yz² ≈ xzyxz
22. xyxzx ≈ xzxyx
23. xyxzy ≈ xy²zx
24. xyxzy ≈ yx²zy
25. xyxz² ≈ xyzxz
26. xyxz² ≈ xzyxz
27. xy²zx ≈ xyzyx
28. xyzxy ≈ xyzyx
29. xyzxy ≈ yxzxy
30. xyzxz ≈ xyz²x
31. xyzxz ≈ zyx²z
32. xyzyx ≈ xzy²x
33. x²yxzx ≈ xyxzx
34. xyx²zx ≈ xyxzx
35. xyxzx ≈ xyxzx²
36. x²yztz ≈ x²tzyz
37. x²yztz ≈ xyxztz
38. x²yztz ≈ xyztxz
39. x²yztz ≈ xzyxtz
40. xyxztz ≈ xyxtz²
41. xyxztz ≈ xyzxtz
42. xyxzt² ≈ xytzxt
43. xyxzt² ≈ xzxyt²
44. xyxzt² ≈ xtyxzt
45. xyzxty ≈ xyzytx
46. xyzxty ≈ yxzxty
47. xyzxtz ≈ xyz²tx
48. xyzxtz ≈ zyx²tz
49. xyzytx ≈ xzy²tx
50. xyz²tx ≈ xyztzx
51. xyztxz ≈ xyztzx
52. xyztxz ≈ zyxtxz
53. xyxztut ≈ xyxutzt
54. xyxztut ≈ xytzxut
55. xyxztut ≈ xzxytut
56. xyztxuz ≈ xyztzux
57. xyztxuz ≈ zyxtxuz