A certified basis of 5 identities

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

Identifier sb-2a7d53331d848a37 in the data of the bases-min seal.

Certified for

[6, 246] [6, 276] [6, 304] [6, 324] [6, 331] [6, 332] [6, 337] [6, 349] [6, 351] [6, 352] [6, 353] [6, 358] [6, 359] [6, 361] [6, 368] [6, 370] [6, 371] [6, 372] [6, 373] [6, 376] [6, 384] [6, 392] [6, 393] [6, 394] [6, 405] [6, 411] [6, 425] [6, 451] [6, 452] [6, 474] [6, 490] [6, 499] [6, 500] [6, 506] [6, 513] [6, 515] [6, 516] [6, 517] [6, 518] [6, 521] [6, 528] [6, 533] [6, 541] [6, 542] [6, 543] [6, 554] [6, 563] [6, 577] [6, 578] [6, 581] [6, 611] [6, 622] [6, 630] [6, 631] [6, 643] [6, 644] [6, 660] [6, 664] [6, 668] [6, 669] [6, 672] [6, 677] [6, 680] [6, 682] [6, 684] [6, 686] [6, 688] [6, 689] [6, 690] [6, 691] [6, 692] [6, 693] [6, 694] [6, 701] [6, 706] [6, 709] [6, 712] [6, 713] [6, 716] [6, 717] [6, 720] [6, 721] [6, 722] [6, 723] [6, 724] [6, 773] [6, 778] [6, 783] [6, 807] [6, 816] [6, 1466] [6, 1467] [6, 1468] [6, 1475] [6, 1476] [6, 1477] [6, 1482] [6, 1483] [6, 1484] [6, 1638] [6, 1639] [6, 1640] [6, 1647] [6, 1648] [6, 1649] [6, 1655] [6, 1656] [6, 1657] [6, 1658] [6, 1659] [6, 1660] [6, 1661] [6, 1662] [6, 1663] [6, 1683] [6, 1684] [6, 1685] [6, 1689] [6, 1690] [6, 1691] [6, 1695] [6, 1696] [6, 1697] [6, 1799] [6, 1800] [6, 1803] [6, 1804] [6, 1975] [6, 1982] [6, 2004] [6, 2005] [6, 2008] [6, 2009] [6, 2306] [6, 2352] [6, 2419] [6, 2466] [6, 2480] [6, 2481] [6, 2486] [6, 2491] [6, 2492] [6, 2493] [6, 2496] [6, 2499] [6, 2500] [6, 2502] [6, 2504] [6, 2506] [6, 4867] [6, 4869] [6, 4875] [6, 4881] [6, 4882] [6, 4887] [6, 4889] [6, 4890] [6, 4898] [6, 4903] [6, 4905] [6, 4906] [6, 4911] [6, 4913] [6, 4914] [6, 4922] [6, 4927] [6, 4929] [6, 4930] [6, 4942] [6, 4957] [6, 4984] [6, 4986] [6, 4992] [6, 4998] [6, 4999] [6, 5004] [6, 5006] [6, 5007] [6, 5015] [6, 5020] [6, 5022] [6, 5023] [6, 5035] [6, 5056] [6, 5058] [6, 5064] [6, 5070] [6, 5071]

The identities

x³ ≈ x²y
x³ ≈ xyx
x³ ≈ yx²
x³ ≈ y²x
x³ ≈ yzx