Moufang quasigroups
It is well known that the following four Moufang identities, M1: \((x(yz))x=(xy)(zx)\) and N1: \(((xy)z)y=x(y(zy))\) and their respective mirrors M2 and N2 (obtained by writing them backwards), are equivalent in loops which are then called Moufang loops. The author now shows that every quasigroup satisfying any one of these four identities is a Moufang loop, so that in fact these identities are equivalent in quasigroups. The proofs have been aided (not produced) by the automated deduction tool OTTER, developed by W. W. McCune.
scientific article; zbMATH DE number 923681