SemiBase

A certified basis of 2 identities

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

Identifier sb-463b8ce49f8204f9 in the data of the bases-min seal.

Certified for

[6, 3304] [6, 3444] [6, 3507] [6, 3509] [6, 3511] [6, 3656] [6, 3706] [6, 3708] [6, 3710] [6, 3712] [6, 3720] [6, 3769] [6, 3771] [6, 3773] [6, 3775] [6, 3777] [6, 3779] [6, 3838] [6, 3840] [6, 3870] [6, 6033] [6, 6121] [6, 6136] [6, 6139] [6, 6140] [6, 6205] [6, 6330] [6, 6340] [6, 6343] [6, 6344] [6, 6403] [6, 6406] [6, 6409] [6, 6415] [6, 6418] [6, 6419] [6, 6422] [6, 6423] [6, 6426] [6, 6427] [6, 6448] [6, 6449] [6, 6489] [6, 6517] [6, 6522] [6, 6532] [6, 6757] [6, 7313] [6, 7338] [6, 7361] [6, 7378] [6, 7384] [6, 7509] [6, 7516] [6, 7525] [6, 7526] [6, 7527] [6, 7625] [6, 7634] [6, 7641] [6, 7645] [6, 7646] [6, 7649] [6, 7698] [6, 7746] [6, 7762] [6, 7776] [6, 7786] [6, 7791] [6, 7860] [6, 7865] [6, 7873] [6, 7874] [6, 7875] [6, 7895] [6, 7897] [6, 7899] [6, 7913] [6, 7915] [6, 7917] [6, 7925] [6, 7933] [6, 7934] [6, 7935] [6, 7937] [6, 7938] [6, 7939] [6, 8065] [6, 8067] [6, 8069] [6, 8072] [6, 8073] [6, 8074] [6, 8081] [6, 8082] [6, 8083] [6, 8085] [6, 8086] [6, 8087] [6, 8089] [6, 8090] [6, 8091] [6, 8130] [6, 8138] [6, 8143] [6, 8145] [6, 8189] [6, 8191] [6, 8193] [6, 8195] [6, 8196] [6, 8197] [6, 8199] [6, 8201] [6, 8202] [6, 8203] [6, 8214] [6, 8215] [6, 8216] [6, 8259] [6, 8331] [6, 8338] [6, 8344] [6, 8348] [6, 8349] [6, 8352] [6, 8381] [6, 8383] [6, 8385] [6, 8386] [6, 8388] [6, 8390] [6, 8391] [6, 8392] [6, 8397] [6, 8398] [6, 8428] [6, 8430] [6, 8432] [6, 8437] [6, 8438] [6, 8439] [6, 8444] [6, 8446] [6, 8449] [6, 8450] [6, 8451] [6, 8454] [6, 8457] [6, 8459] [6, 8462] [6, 8463] [6, 8464] [6, 8465] [6, 8467] [6, 8470] [6, 8472] [6, 8473] [6, 8475] [6, 8516] [6, 8538] [6, 8554] [6, 8559] [6, 8620] [6, 8651] [6, 8668] [6, 8670] [6, 8672] [6, 8720] [6, 8734] [6, 8742] [6, 8744] [6, 8748] [6, 8765] [6, 8772] [6, 8777] [6, 9837] [6, 9929] [6, 9935] [6, 10042] [6, 10105] [6, 10148] [6, 10494] [6, 10502] [6, 10509] [6, 10511] [6, 10539] [6, 10546] [6, 10569] [6, 10570] [6, 10571] [6, 10585] [6, 10587] [6, 10593] [6, 10601] [6, 10606] [6, 10607] [6, 10610] [6, 10611] [6, 10658] [6, 10695] [6, 10705] [6, 10722] [6, 10739] [6, 10741] [6, 10743] [6, 10757] [6, 10773] [6, 10775] [6, 10792] [6, 10795] [6, 10800] [6, 10804] [6, 10805] [6, 10806] [6, 10994] [6, 10997] [6, 10998] [6, 11004] [6, 11007] [6, 11008] [6, 11010] [6, 11011] [6, 11013] [6, 11014] [6, 11049] [6, 11050] [6, 11051] [6, 11054] [6, 11056] [6, 11057] [6, 11058] [6, 11059] [6, 11065] [6, 11071] [6, 11074] [6, 11075] [6, 11092] [6, 11094] [6, 11095] [6, 11097] [6, 11098] [6, 11099] [6, 11100] [6, 11101] [6, 11109] [6, 11110] [6, 11111] [6, 11114] [6, 11115] [6, 11131] [6, 11136] [6, 11137] [6, 11138] [6, 11144] [6, 11241] [6, 11244] [6, 11245] [6, 11250] [6, 11251] [6, 11253] [6, 11254] [6, 11255] [6, 11257] [6, 11260] [6, 11265] [6, 11268] [6, 11269] [6, 11328] [6, 11334] [6, 11337] [6, 11342] [6, 11343] [6, 11346] [6, 11348] [6, 11350] [6, 11357] [6, 11358] [6, 11424] [6, 11431] [6, 11433] [6, 11435] [6, 11441] [6, 11444] [6, 11445] [6, 11446] [6, 11469] [6, 11476] [6, 11478] [6, 11489] [6, 11491] [6, 11495] [6, 11496] [6, 11503] [6, 11504] [6, 11506] [6, 11507] [6, 11508] [6, 11532] [6, 11538] [6, 11539] [6, 11540] [6, 11561] [6, 11575] [6, 11577] [6, 11589] [6, 11652] [6, 11679] [6, 11682] [6, 11693] [6, 11735] [6, 11755] [6, 12537] [6, 12546] [6, 12552] [6, 12556] [6, 12558] [6, 12588] [6, 12591] [6, 12598] [6, 12599] [6, 12600] [6, 12610] [6, 12618] [6, 12622] [6, 12624] [6, 12650] [6, 12652] [6, 12658] [6, 12659] [6, 12660] [6, 12675] [6, 12678] [6, 12683] [6, 12697] [6, 12718] [6, 12722] [6, 12724] [6, 12726] [6, 12732] [6, 12733] [6, 12734] [6, 12744] [6, 12757] [6, 12758] [6, 12779] [6, 12780] [6, 12788] [6, 12800] [6, 12806] [6, 12814] [6, 12817] [6, 12818] [6, 12820] [6, 12821] [6, 12839] [6, 12841] [6, 12845] [6, 12847] [6, 12850] [6, 12851] [6, 12861] [6, 12863] [6, 12865] [6, 12867] [6, 12870] [6, 12871] [6, 12880] [6, 12882] [6, 12888] [6, 12890] [6, 13068] [6, 13071] [6, 13080] [6, 13081] [6, 13082] [6, 13083] [6, 13084] [6, 13090] [6, 13095] [6, 13096] [6, 13097] [6, 13104] [6, 13109] [6, 13112] [6, 13115] [6, 13119] [6, 13120] [6, 13130] [6, 13131] [6, 13140] [6, 13151] [6, 13152] [6, 13153] [6, 13154] [6, 13155] [6, 13156] [6, 13215] [6, 13220] [6, 13225] [6, 13227] [6, 13228] [6, 13230] [6, 13242] [6, 13244] [6, 13246] [6, 13247] [6, 13249] [6, 13261] [6, 13265] [6, 13269] [6, 13271] [6, 13272] [6, 13282] [6, 13290] [6, 13293] [6, 13294] [6, 13302] [6, 13304] [6, 13305] [6, 13308] [6, 13309] [6, 13313] [6, 13315] [6, 13316] [6, 13319] [6, 13443] [6, 13448] [6, 13453] [6, 13455] [6, 13456] [6, 13458] [6, 13463] [6, 13465] [6, 13466] [6, 13467] [6, 13469] [6, 13473] [6, 13476] [6, 13477] [6, 13479] [6, 13489] [6, 13490] [6, 13491] [6, 13497] [6, 13498] [6, 13507] [6, 13508] [6, 13513] [6, 13519] [6, 13520] [6, 13521] [6, 13523] [6, 13524] [6, 13525] [6, 13528] [6, 13529] [6, 13530] [6, 13531] [6, 13532] [6, 13534] [6, 13535] [6, 13536] [6, 13538] [6, 13539] [6, 13595] [6, 13600] [6, 13607] [6, 13627] [6, 13633] [6, 13640] [6, 13641] [6, 13642] [6, 13644] [6, 13647] [6, 13653] [6, 13655] [6, 13656] [6, 13658] [6, 13672] [6, 13675] [6, 13679] [6, 13680] [6, 13681] [6, 13682] [6, 13690] [6, 13701] [6, 13704] [6, 13706] [6, 13708] [6, 13709] [6, 13710] [6, 13711] [6, 13718] [6, 13719] [6, 13720] [6, 13721] [6, 13723] [6, 13724] [6, 13727] [6, 13728] [6, 13729] [6, 13730] [6, 13733] [6, 13734] [6, 13784] [6, 13789] [6, 13793] [6, 13798] [6, 13800] [6, 13801] [6, 13803] [6, 13897] [6, 13906] [6, 13912] [6, 13916] [6, 13918] [6, 13948] [6, 13951] [6, 13958] [6, 13959] [6, 13960] [6, 13982] [6, 13987] [6, 13992] [6, 13994] [6, 13995] [6, 13997] [6, 14011] [6, 14098] [6, 14101] [6, 14107] [6, 14110] [6, 14138] [6, 14139] [6, 14140] [6, 14141] [6, 14142] [6, 14153] [6, 14164] [6, 14167] [6, 14173] [6, 14177] [6, 14179] [6, 14234] [6, 14236] [6, 14255] [6, 14259] [6, 14260] [6, 14274] [6, 14276] [6, 14360] [6, 14364] [6, 14366] [6, 14369] [6, 14370] [6, 14372] [6, 14374] [6, 14375] [6, 14376] [6, 14377] [6, 14426] [6, 14428] [6, 14432] [6, 14433] [6, 14434] [6, 14436] [6, 14470] [6, 14472] [6, 14473] [6, 14474]

The identities

  1. x² ≈ x³
  2. x²y ≈ xyx