A certified basis of 3 identities

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

Identifier sb-de9f06d522aed5f4 in the data of the bases-min seal.

Certified for

[6, 1222] [6, 1264] [6, 1267] [6, 1302] [6, 1303] [6, 1358] [6, 1363] [6, 1366] [6, 1399] [6, 1402] [6, 2907] [6, 3063] [6, 3068] [6, 3070] [6, 3094] [6, 3096] [6, 3099] [6, 3100] [6, 3101] [6, 3102] [6, 3121] [6, 3125] [6, 3128] [6, 3129] [6, 3130] [6, 3132] [6, 3156] [6, 3158] [6, 3161] [6, 3163] [6, 3166] [6, 4011] [6, 4015] [6, 4104] [6, 4114] [6, 4116] [6, 4119] [6, 4123] [6, 4211] [6, 4221] [6, 4223] [6, 5769] [6, 5771] [6, 5820] [6, 5822] [6, 5826] [6, 5827] [6, 5832] [6, 5834] [6, 5836] [6, 5838] [6, 5840] [6, 5843] [6, 5922] [6, 5927] [6, 5931] [6, 6614] [6, 6735] [6, 6754] [6, 6760] [6, 6761] [6, 6764] [6, 6765] [6, 6768] [6, 6776] [6, 6777] [6, 6779] [6, 6781] [6, 6824] [6, 6825] [6, 6830] [6, 6832] [6, 6846] [6, 6848] [6, 6866] [6, 6876] [6, 6881] [6, 6890] [6, 6892] [6, 6899] [6, 6900] [6, 6906] [6, 6907] [6, 6909] [6, 6910] [6, 6911] [6, 6912] [6, 6914] [6, 6922] [6, 6923] [6, 6925] [6, 6927] [6, 6967] [6, 6968] [6, 6973] [6, 6975] [6, 6989] [6, 6991] [6, 7009] [6, 7019] [6, 7024] [6, 7033] [6, 7042] [6, 7049] [6, 7050] [6, 7053] [6, 7054] [6, 8799] [6, 8801] [6, 8807] [6, 8813] [6, 8816] [6, 8885] [6, 8887] [6, 8900] [6, 8902] [6, 8914] [6, 8925] [6, 8927] [6, 8933] [6, 8937] [6, 8941] [6, 8943] [6, 9809] [6, 9819] [6, 9835] [6, 9838] [6, 9843] [6, 9846] [6, 9949] [6, 9950] [6, 9956] [6, 9957] [6, 9958] [6, 9960] [6, 9961] [6, 10172] [6, 10175] [6, 10186] [6, 10188] [6, 10196] [6, 10205] [6, 10207] [6, 10213] [6, 10219] [6, 10226] [6, 10228] [6, 11617] [6, 11620] [6, 11622] [6, 11712] [6, 11714] [6, 11742] [6, 11758] [6, 11761] [6, 11785] [6, 11786] [6, 11792] [6, 11795] [6, 11800] [6, 11801] [6, 11803] [6, 11804] [6, 11805] [6, 11807] [6, 11809] [6, 11810] [6, 11812] [6, 11813] [6, 11815] [6, 11827] [6, 11829] [6, 11841] [6, 11842] [6, 11844] [6, 11850] [6, 11852]

The identities

x² ≈ x⁴
xy ≈ yx
x³y ≈ xy