Searching for shortest single axioms for groups of exponent 6
In this note, we study shortest (with respect to the number of variable occurrences on the left-hand side) possible single axioms for groups of exponent 6 of the form T = x, where T is a term in product only. These investigations were carried out with the automated theorem provers OTTER and Prover9 and the finite first-order model finder Mace4.
single axiom group exponent automated theorem-proving