A certified basis of 8 identities
This list of identities is a basis, proved in Lean, of 162 semigroups of order six, all of which generate the variety V[2593]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-ea8a692f1bc136f8 in the data of the bases-min seal.
Certified for
[6, 2593] [6, 2599] [6, 2601] [6, 2629] [6, 2631] [6, 2645] [6, 2647] [6, 2649] [6, 2651] [6, 2656] [6, 2658] [6, 2662] [6, 2692] [6, 2695] [6, 2700] [6, 2711] [6, 2713] [6, 2718] [6, 2720] [6, 2817] [6, 2818] [6, 2819] [6, 2822] [6, 2823] [6, 2825] [6, 2826] [6, 2827] [6, 2828] [6, 2829] [6, 2830] [6, 2831] [6, 2833] [6, 2834] [6, 2835] [6, 2837] [6, 2838] [6, 2840] [6, 2841] [6, 5125] [6, 5131] [6, 5133] [6, 5135] [6, 5142] [6, 5144] [6, 5146] [6, 5150] [6, 5152] [6, 5154] [6, 5169] [6, 5176] [6, 5178] [6, 5180] [6, 5182] [6, 5184] [6, 5186] [6, 5188] [6, 5190] [6, 5202] [6, 5272] [6, 5273] [6, 5274] [6, 5275] [6, 5277] [6, 5278] [6, 5279] [6, 5281] [6, 5282] [6, 5283] [6, 5285] [6, 5287] [6, 5288] [6, 5289] [6, 5290] [6, 5291] [6, 5292] [6, 5293] [6, 5294] [6, 5296] [6, 5339] [6, 5363] [6, 5373] [6, 5374] [6, 5375] [6, 5376] [6, 5387] [6, 5394] [6, 5395] [6, 5396] [6, 5397] [6, 5400] [6, 5401] [6, 5402] [6, 5403] [6, 5406] [6, 5410] [6, 5411] [6, 5412] [6, 5413] [6, 5415] [6, 5416] [6, 5417] [6, 5418] [6, 5431] [6, 5432] [6, 5433] [6, 5438] [6, 5444] [6, 5474] [6, 5536] [6, 5538] [6, 5697] [6, 5718] [6, 5727] [6, 5846] [6, 5867] [6, 9269] [6, 9271] [6, 9275] [6, 9277] [6, 9280] [6, 9282] [6, 9287] [6, 9289] [6, 9292] [6, 9323] [6, 9324] [6, 9326] [6, 9327] [6, 9328] [6, 9329] [6, 9331] [6, 9332] [6, 9333] [6, 9340] [6, 9341] [6, 9345] [6, 9346] [6, 9348] [6, 9349] [6, 9350] [6, 9351] [6, 9354] [6, 9355] [6, 9356] [6, 9360] [6, 9361] [6, 9363] [6, 9366] [6, 9367] [6, 9371] [6, 9372] [6, 9390] [6, 9416] [6, 9418] [6, 9475] [6, 9486] [6, 9492] [6, 9509] [6, 9517] [6, 9523] [6, 9528] [6, 9606]
The identities
- x³ ≈ x⁴
- x²y ≈ xyx
- x²y ≈ xy²
- x²y ≈ yx²
- x³y ≈ x²y
- xyz ≈ xzy
- xyz ≈ yxz
- x²yz ≈ xyz