A certified basis of 4 identities
This list of identities is a basis, proved in Lean, of 264 semigroups of order six, all of which generate the variety V[3191]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-3d171aded53eb431 in the data of the bases-min seal.
Certified for
[6, 3191] [6, 3193] [6, 3202] [6, 3204] [6, 3206] [6, 3213] [6, 3215] [6, 3220] [6, 3222] [6, 3226] [6, 3229] [6, 3231] [6, 3233] [6, 3237] [6, 3239] [6, 5937] [6, 5940] [6, 5961] [6, 5964] [6, 5967] [6, 5985] [6, 5988] [6, 6014] [6, 6015] [6, 6018] [6, 6019] [6, 6022] [6, 6023] [6, 6027] [6, 6028] [6, 6029] [6, 7067] [6, 7069] [6, 7074] [6, 7076] [6, 7078] [6, 7081] [6, 7083] [6, 7093] [6, 7098] [6, 7102] [6, 7107] [6, 7109] [6, 7111] [6, 7134] [6, 7136] [6, 7138] [6, 7142] [6, 7147] [6, 7149] [6, 7152] [6, 7170] [6, 7172] [6, 7175] [6, 7176] [6, 7178] [6, 7180] [6, 7181] [6, 7187] [6, 7190] [6, 7194] [6, 7195] [6, 7198] [6, 7219] [6, 7220] [6, 7221] [6, 7223] [6, 7224] [6, 7226] [6, 7230] [6, 7232] [6, 7234] [6, 7238] [6, 7239] [6, 7241] [6, 7243] [6, 7260] [6, 7261] [6, 7262] [6, 7264] [6, 7268] [6, 7270] [6, 7273] [6, 8577] [6, 8579] [6, 8584] [6, 8586] [6, 8588] [6, 8591] [6, 8593] [6, 8700] [6, 8704] [6, 8708] [6, 9855] [6, 9857] [6, 9862] [6, 9988] [6, 9990] [6, 9994] [6, 9996] [6, 10013] [6, 10017] [6, 10021] [6, 10024] [6, 10026] [6, 10069] [6, 10072] [6, 10078] [6, 10080] [6, 10082] [6, 10084] [6, 10088] [6, 10237] [6, 10239] [6, 10242] [6, 10243] [6, 10247] [6, 10250] [6, 10252] [6, 10254] [6, 10267] [6, 10269] [6, 10273] [6, 10275] [6, 10279] [6, 10281] [6, 10284] [6, 10285] [6, 10316] [6, 10317] [6, 10330] [6, 10334] [6, 10431] [6, 10432] [6, 10436] [6, 10437] [6, 10443] [6, 10444] [6, 10469] [6, 10470] [6, 10471] [6, 10472] [6, 10477] [6, 10478] [6, 10479] [6, 10481] [6, 10655] [6, 10666] [6, 10667] [6, 11626] [6, 11629] [6, 11646] [6, 11647] [6, 11717] [6, 11944] [6, 11946] [6, 11954] [6, 11959] [6, 11974] [6, 11977] [6, 11989] [6, 11990] [6, 11991] [6, 11993] [6, 11997] [6, 11999] [6, 12002] [6, 12026] [6, 12032] [6, 12039] [6, 12053] [6, 12055] [6, 12056] [6, 12057] [6, 12060] [6, 12061] [6, 12062] [6, 12065] [6, 12078] [6, 12088] [6, 12113] [6, 12116] [6, 12118] [6, 12121] [6, 12124] [6, 12127] [6, 12132] [6, 12138] [6, 12151] [6, 12156] [6, 12157] [6, 12158] [6, 12210] [6, 12212] [6, 12214] [6, 12222] [6, 12225] [6, 12239] [6, 12242] [6, 12252] [6, 12255] [6, 12256] [6, 12258] [6, 12264] [6, 12266] [6, 12269] [6, 12354] [6, 12355] [6, 12356] [6, 12357] [6, 12360] [6, 12361] [6, 12363] [6, 12365] [6, 12369] [6, 12374] [6, 12376] [6, 12377] [6, 12378] [6, 12387] [6, 12403] [6, 12405] [6, 12408] [6, 12409] [6, 12411] [6, 12413] [6, 12414] [6, 12418] [6, 12420] [6, 12423] [6, 12431] [6, 13813] [6, 13815] [6, 13823] [6, 13828] [6, 13843] [6, 13846] [6, 13858] [6, 13859] [6, 13860] [6, 13862] [6, 13866] [6, 13868] [6, 13871] [6, 14018] [6, 14037] [6, 14054] [6, 14055] [6, 14058] [6, 14059] [6, 14062] [6, 14065] [6, 14066] [6, 14069] [6, 14205] [6, 14213] [6, 14301] [6, 14303] [6, 14306] [6, 14307] [6, 14310] [6, 14313] [6, 14394] [6, 14398]
The identities
- x²y ≈ xy
- x²yz ≈ xyxz
- xyzy ≈ xzy²
- xyz² ≈ xzy²