A certified basis of 2 identities
This list of identities is a basis, proved in Lean, of 345 semigroups of order six, all of which generate the variety V[3200]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-7727b06112661ecd in the data of the bases-min seal.
Certified for
[6, 3200] [6, 3212] [6, 3219] [6, 3228] [6, 3236] [6, 3241] [6, 5951] [6, 5976] [6, 5996] [6, 6013] [6, 6016] [6, 6017] [6, 6020] [6, 6021] [6, 6024] [6, 6025] [6, 7073] [6, 7080] [6, 7085] [6, 7108] [6, 7110] [6, 7112] [6, 7115] [6, 7117] [6, 7119] [6, 7135] [6, 7137] [6, 7139] [6, 7158] [6, 7161] [6, 7164] [6, 7174] [6, 7179] [6, 7182] [6, 7185] [6, 7193] [6, 7196] [6, 7203] [6, 7204] [6, 7208] [6, 7210] [6, 7211] [6, 7217] [6, 7218] [6, 7222] [6, 7225] [6, 7228] [6, 7237] [6, 7240] [6, 7245] [6, 7248] [6, 7249] [6, 7252] [6, 7253] [6, 7254] [6, 7255] [6, 7258] [6, 7259] [6, 7263] [6, 7266] [6, 7272] [6, 7276] [6, 7277] [6, 7278] [6, 7279] [6, 7282] [6, 7283] [6, 8583] [6, 8590] [6, 8595] [6, 8702] [6, 8706] [6, 8710] [6, 8752] [6, 8755] [6, 8758] [6, 9836] [6, 9870] [6, 9993] [6, 9998] [6, 10022] [6, 10025] [6, 10027] [6, 10051] [6, 10054] [6, 10075] [6, 10079] [6, 10081] [6, 10135] [6, 10141] [6, 10145] [6, 10241] [6, 10251] [6, 10253] [6, 10266] [6, 10270] [6, 10278] [6, 10283] [6, 10310] [6, 10315] [6, 10318] [6, 10335] [6, 10336] [6, 10339] [6, 10341] [6, 10346] [6, 10351] [6, 10353] [6, 10356] [6, 10357] [6, 10358] [6, 10430] [6, 10433] [6, 10434] [6, 10442] [6, 10445] [6, 10446] [6, 10450] [6, 10451] [6, 10455] [6, 10456] [6, 10459] [6, 10460] [6, 10461] [6, 10462] [6, 10463] [6, 10464] [6, 10466] [6, 10467] [6, 10473] [6, 10476] [6, 10480] [6, 10483] [6, 10484] [6, 10485] [6, 10486] [6, 10488] [6, 10489] [6, 10650] [6, 10652] [6, 10653] [6, 10668] [6, 11635] [6, 11645] [6, 11648] [6, 11719] [6, 11745] [6, 11948] [6, 11960] [6, 11963] [6, 11975] [6, 11983] [6, 11992] [6, 11995] [6, 12001] [6, 12005] [6, 12006] [6, 12007] [6, 12008] [6, 12011] [6, 12012] [6, 12027] [6, 12040] [6, 12047] [6, 12051] [6, 12054] [6, 12058] [6, 12066] [6, 12069] [6, 12070] [6, 12073] [6, 12074] [6, 12079] [6, 12082] [6, 12089] [6, 12090] [6, 12091] [6, 12096] [6, 12098] [6, 12100] [6, 12104] [6, 12120] [6, 12125] [6, 12133] [6, 12139] [6, 12143] [6, 12146] [6, 12152] [6, 12153] [6, 12154] [6, 12159] [6, 12161] [6, 12162] [6, 12164] [6, 12169] [6, 12170] [6, 12173] [6, 12183] [6, 12186] [6, 12188] [6, 12189] [6, 12194] [6, 12195] [6, 12211] [6, 12223] [6, 12230] [6, 12240] [6, 12248] [6, 12253] [6, 12254] [6, 12257] [6, 12260] [6, 12261] [6, 12268] [6, 12278] [6, 12284] [6, 12288] [6, 12289] [6, 12293] [6, 12296] [6, 12309] [6, 12310] [6, 12312] [6, 12313] [6, 12325] [6, 12326] [6, 12359] [6, 12362] [6, 12364] [6, 12366] [6, 12367] [6, 12368] [6, 12371] [6, 12373] [6, 12375] [6, 12379] [6, 12381] [6, 12382] [6, 12383] [6, 12384] [6, 12386] [6, 12390] [6, 12393] [6, 12394] [6, 12395] [6, 12396] [6, 12400] [6, 12401] [6, 12407] [6, 12412] [6, 12416] [6, 12422] [6, 12426] [6, 12427] [6, 12430] [6, 12434] [6, 12435] [6, 12439] [6, 12442] [6, 12446] [6, 12447] [6, 12449] [6, 12450] [6, 12452] [6, 12453] [6, 12454] [6, 12455] [6, 12457] [6, 12463] [6, 12464] [6, 12465] [6, 12466] [6, 12467] [6, 12468] [6, 12469] [6, 12470] [6, 12472] [6, 12473] [6, 12474] [6, 12476] [6, 12477] [6, 12479] [6, 12480] [6, 12481] [6, 12482] [6, 12487] [6, 12488] [6, 12489] [6, 12490] [6, 12493] [6, 12494] [6, 13817] [6, 13829] [6, 13832] [6, 13844] [6, 13852] [6, 13861] [6, 13864] [6, 13870] [6, 13874] [6, 13875] [6, 13876] [6, 13877] [6, 13880] [6, 13881] [6, 14020] [6, 14027] [6, 14039] [6, 14045] [6, 14060] [6, 14064] [6, 14068] [6, 14070] [6, 14073] [6, 14074] [6, 14077] [6, 14078] [6, 14081] [6, 14185] [6, 14198] [6, 14206] [6, 14211] [6, 14214] [6, 14219] [6, 14220] [6, 14305] [6, 14309] [6, 14311] [6, 14314] [6, 14315] [6, 14317] [6, 14319] [6, 14322] [6, 14323] [6, 14324] [6, 14393] [6, 14395] [6, 14400] [6, 14401] [6, 14402] [6, 14405] [6, 14444] [6, 14446] [6, 14448] [6, 14449]
The identities
- x²y ≈ xy
- xyx ≈ xy²