A certified basis of 4 identities
This list of identities is a basis, proved in Lean, of 299 semigroups of order six, all of which generate the variety V[1223]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-84128e1dd9c8f4d6 in the data of the bases-min seal.
Certified for
[6, 1223] [6, 1224] [6, 1225] [6, 1226] [6, 1227] [6, 1228] [6, 1268] [6, 1269] [6, 1270] [6, 1271] [6, 1272] [6, 1273] [6, 1274] [6, 1304] [6, 1305] [6, 1306] [6, 1307] [6, 1308] [6, 1309] [6, 1310] [6, 1364] [6, 1368] [6, 1369] [6, 1370] [6, 1371] [6, 1372] [6, 1373] [6, 1400] [6, 2910] [6, 2912] [6, 2914] [6, 2915] [6, 2918] [6, 2920] [6, 2921] [6, 2923] [6, 2924] [6, 3071] [6, 3072] [6, 3073] [6, 3074] [6, 3075] [6, 3076] [6, 3077] [6, 3103] [6, 3104] [6, 3105] [6, 3106] [6, 3107] [6, 3108] [6, 3122] [6, 3133] [6, 3134] [6, 3135] [6, 3136] [6, 3137] [6, 3138] [6, 3139] [6, 4012] [6, 4013] [6, 4014] [6, 4017] [6, 4018] [6, 4019] [6, 4020] [6, 4021] [6, 4023] [6, 4026] [6, 4028] [6, 4031] [6, 4105] [6, 4106] [6, 4107] [6, 4120] [6, 4121] [6, 4122] [6, 4125] [6, 4126] [6, 4127] [6, 4128] [6, 4129] [6, 4131] [6, 4133] [6, 4135] [6, 4137] [6, 4212] [6, 4213] [6, 4214] [6, 4227] [6, 4228] [6, 4229] [6, 4232] [6, 4233] [6, 4234] [6, 4235] [6, 4236] [6, 4238] [6, 4241] [6, 4243] [6, 4246] [6, 4311] [6, 4312] [6, 4313] [6, 5774] [6, 5775] [6, 5777] [6, 5778] [6, 5780] [6, 5781] [6, 5782] [6, 5783] [6, 5828] [6, 5829] [6, 5841] [6, 5923] [6, 5924] [6, 5925] [6, 5928] [6, 5929] [6, 5930] [6, 5952] [6, 5953] [6, 5955] [6, 5956] [6, 5957] [6, 5958] [6, 5977] [6, 5979] [6, 5980] [6, 5981] [6, 5982] [6, 5997] [6, 5999] [6, 6001] [6, 6002] [6, 6003] [6, 6004] [6, 6005] [6, 6006] [6, 6008] [6, 6616] [6, 6618] [6, 6620] [6, 6621] [6, 6736] [6, 6737] [6, 6738] [6, 6766] [6, 6767] [6, 6769] [6, 6771] [6, 6772] [6, 6778] [6, 6780] [6, 6782] [6, 6783] [6, 6784] [6, 6788] [6, 6790] [6, 6791] [6, 6792] [6, 6793] [6, 6794] [6, 6826] [6, 6827] [6, 6831] [6, 6833] [6, 6849] [6, 6850] [6, 6851] [6, 6867] [6, 6868] [6, 6891] [6, 6893] [6, 6913] [6, 6915] [6, 6917] [6, 6918] [6, 6924] [6, 6926] [6, 6928] [6, 6929] [6, 6930] [6, 6934] [6, 6936] [6, 6937] [6, 6938] [6, 6939] [6, 6940] [6, 6969] [6, 6970] [6, 6974] [6, 6976] [6, 6992] [6, 6993] [6, 6994] [6, 7010] [6, 7011] [6, 7034] [6, 7038] [6, 8800] [6, 8803] [6, 8804] [6, 8808] [6, 8809] [6, 8811] [6, 8815] [6, 8818] [6, 8823] [6, 8828] [6, 8830] [6, 8886] [6, 8889] [6, 8890] [6, 8904] [6, 8906] [6, 8917] [6, 8950] [6, 8953] [6, 8954] [6, 8958] [6, 8959] [6, 8961] [6, 8965] [6, 8968] [6, 8973] [6, 8978] [6, 8980] [6, 9028] [6, 9031] [6, 9032] [6, 9045] [6, 9047] [6, 9058] [6, 9811] [6, 9813] [6, 9821] [6, 9824] [6, 9826] [6, 9839] [6, 9840] [6, 9844] [6, 9845] [6, 9848] [6, 9859] [6, 9861] [6, 9869] [6, 9875] [6, 9876] [6, 9951] [6, 9952] [6, 10173] [6, 10177] [6, 10180] [6, 10187] [6, 10189] [6, 10190] [6, 10191] [6, 10198] [6, 10206] [6, 10209] [6, 10210] [6, 10215] [6, 10221] [6, 10359] [6, 10361] [6, 10367] [6, 10368] [6, 10371] [6, 10372] [6, 10377] [6, 10378] [6, 10381] [6, 10382] [6, 10384] [6, 10386] [6, 10390] [6, 10391] [6, 10393] [6, 10395] [6, 10401] [6, 11618] [6, 11621] [6, 11636] [6, 11638] [6, 11639] [6, 11640] [6, 11720] [6, 11722] [6, 11747] [6, 11759] [6, 11763] [6, 11766] [6, 11787] [6, 11788] [6, 11793] [6, 11796] [6, 11828] [6, 11830]
The identities
- x³y ≈ xy
- x²y² ≈ y²x²
- xy³ ≈ yx³
- xyz ≈ yxz