A certified basis of 187 identities

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

Identifier sb-8472381e49aaedb7 in the data of the bases-min seal.

Certified for

The identities

1. x²y ≈ xyx
2. x²y ≈ yx²
3. xyx ≈ yx²
4. x³y ≈ x²yx
5. x³y ≈ x²y²
6. x³y ≈ xyx²
7. x³y ≈ xyxy
8. x³y ≈ xy²x
9. x³y ≈ xy³
10. x³y ≈ yx³
11. x³y ≈ yx²y
12. x³y ≈ yxyx
13. x³y ≈ yxy²
14. x³y ≈ y²x²
15. x³y ≈ y²xy
16. x³y ≈ y³x
17. x²yx ≈ x²y²
18. x²yx ≈ xyx²
19. x²yx ≈ xyxy
20. x²yx ≈ xy²x
21. x²yx ≈ xy³
22. x²yx ≈ yx³
23. x²yx ≈ yx²y
24. x²yx ≈ yxyx
25. x²yx ≈ yxy²
26. x²yx ≈ y²x²
27. x²yx ≈ y²xy
28. x²y² ≈ xyx²
29. x²y² ≈ xyxy
30. x²y² ≈ xy²x
31. x²y² ≈ xy³
32. x²y² ≈ yx³
33. x²y² ≈ yx²y
34. x²y² ≈ yxyx
35. x²y² ≈ yxy²
36. x²y² ≈ y²x²
37. xyx² ≈ xyxy
38. xyx² ≈ xy²x
39. xyx² ≈ xy³
40. xyx² ≈ yx³
41. xyx² ≈ yx²y
42. xyx² ≈ yxyx
43. xyx² ≈ yxy²
44. xyxy ≈ xy²x
45. xyxy ≈ xy³
46. xyxy ≈ yx³
47. xyxy ≈ yx²y
48. xyxy ≈ yxyx
49. xy²x ≈ xy³
50. xy²x ≈ yx³
51. xy²x ≈ yx²y
52. xy³ ≈ yx³
53. xyz ≈ xzy
54. xyz ≈ yxz
55. xyz ≈ yzx
56. xyz ≈ zyx
57. x²yz ≈ x²zy
58. x²yz ≈ xyxz
59. x²yz ≈ xy²z
60. x²yz ≈ xyzx
61. x²yz ≈ xyzy
62. x²yz ≈ xyz²
63. x²yz ≈ xzxy
64. x²yz ≈ xzyx
65. x²yz ≈ xzy²
66. x²yz ≈ xzyz
67. x²yz ≈ xz²y
68. x²yz ≈ yx²z
69. x²yz ≈ yxyz
70. x²yz ≈ yxzx
71. x²yz ≈ yxzy
72. x²yz ≈ yxz²
73. x²yz ≈ y²xz
74. x²yz ≈ y²zx
75. x²yz ≈ yzx²
76. x²yz ≈ yzxy
77. x²yz ≈ yzxz
78. x²yz ≈ yzyx
79. x²yz ≈ yz²x
80. x²yz ≈ zx²y
81. x²yz ≈ zxyx
82. x²yz ≈ zxy²
83. x²yz ≈ zxyz
84. x²yz ≈ zxzy
85. x²yz ≈ zyx²
86. x²yz ≈ zyxy
87. x²yz ≈ zyxz
88. x²yz ≈ zy²x
89. x²yz ≈ zyzx
90. x²yz ≈ z²yx
91. xyxz ≈ xy²z
92. xyxz ≈ xyzx
93. xyxz ≈ xyzy
94. xyxz ≈ xyz²
95. xyxz ≈ xzxy
96. xyxz ≈ xzyx
97. xyxz ≈ xzy²
98. xyxz ≈ xzyz
99. xyxz ≈ xz²y
100. xyxz ≈ yx²z
101. xyxz ≈ yxyz
102. xyxz ≈ yxzx
103. xyxz ≈ yxzy
104. xyxz ≈ yxz²
105. xyxz ≈ yzx²
106. xyxz ≈ yzxy
107. xyxz ≈ yzxz
108. xyxz ≈ yzyx
109. xyxz ≈ yz²x
110. xyxz ≈ zx²y
111. xyxz ≈ zxyx
112. xyxz ≈ zxy²
113. xyxz ≈ zxyz
114. xyxz ≈ zyx²
115. xyxz ≈ zyxy
116. xyxz ≈ zyxz
117. xyxz ≈ zy²x
118. xyxz ≈ zyzx
119. xy²z ≈ xyzx
120. xy²z ≈ xyzy
121. xy²z ≈ xyz²
122. xy²z ≈ xzyx
123. xy²z ≈ xzy²
124. xy²z ≈ xzyz
125. xy²z ≈ xz²y
126. xy²z ≈ yx²z
127. xy²z ≈ yxzx
128. xy²z ≈ yxzy
129. xy²z ≈ yxz²
130. xy²z ≈ yzx²
131. xy²z ≈ yzxy
132. xy²z ≈ yzxz
133. xy²z ≈ yz²x
134. xy²z ≈ zxyx
135. xy²z ≈ zxy²
136. xy²z ≈ zxyz
137. xy²z ≈ zyx²
138. xy²z ≈ zyxy
139. xy²z ≈ zyxz
140. xy²z ≈ zy²x
141. xyzx ≈ xyzy
142. xyzx ≈ xyz²
143. xyzx ≈ xzyx
144. xyzx ≈ xzy²
145. xyzx ≈ xzyz
146. xyzx ≈ yxzx
147. xyzx ≈ yxzy
148. xyzx ≈ yxz²
149. xyzx ≈ yzx²
150. xyzx ≈ yzxy
151. xyzx ≈ yzxz
152. xyzx ≈ zxyx
153. xyzx ≈ zxy²
154. xyzx ≈ zyx²
155. xyzx ≈ zyxy
156. xyzx ≈ zyxz
157. xyzy ≈ xyz²
158. xyzy ≈ xzy²
159. xyzy ≈ xzyz
160. xyzy ≈ yxzx
161. xyzy ≈ yxz²
162. xyzy ≈ yzx²
163. xyzy ≈ yzxz
164. xyzy ≈ zxy²
165. xyzy ≈ zyx²
166. xyzy ≈ zyxy
167. xyz² ≈ xzy²
168. xyz² ≈ yxz²
169. xyz² ≈ yzx²
170. xyz² ≈ zyx²
171. xyzt ≈ xytz
172. xyzt ≈ xzyt
173. xyzt ≈ xzty
174. xyzt ≈ xtzy
175. xyzt ≈ yxzt
176. xyzt ≈ yxtz
177. xyzt ≈ yzxt
178. xyzt ≈ yztx
179. xyzt ≈ ytxz
180. xyzt ≈ ytzx
181. xyzt ≈ zyxt
182. xyzt ≈ zytx
183. xyzt ≈ ztxy
184. xyzt ≈ ztyx
185. xyzt ≈ tyzx
186. xyzt ≈ tzyx
187. xyztu ≈ vwsrp