The shortest single axioms for groups of exponent 4

We study equations of the form (α = x), which are single axioms for groups of exponent 4, where α is a term in product only. Every such α must have at least nine variable occurrences, and there are exactly three such α of this size, up to variable renaming and mirroring. These terms were found by an exhaustive search through all terms of this form. Automated techniques were used in two ways: to eliminate many α by verifying that (α = x) is ture in some nongroup, and to verify that the group axioms do indeed follow from the successful (α = x). We also present an improvement on Neumannʹs scheme for single axioms for varieties of groups.