A 2-base for inverse semigroups

An open problem in the theory of inverse semigroups was whether the variety of such semigroups, when viewed as algebras with a binary operation and a unary operation, is 2-based, that is, has a base for its identities consisting of 2 independent axioms. In this note, we announce the affirmative solution to this problem: the identities $$x(x^{\mathrm{\prime }}x)=xx(x^{\mathrm{\prime }}(y(y^{\mathrm{\prime }}((zu{)}^{\mathrm{\prime }}{w}^{\mathrm{\prime }}{)}^{\mathrm{\prime }})))=y(y^{\mathrm{\prime }}(x(x^{\mathrm{\prime }}((wz)u))))$$ form a base for inverse semigroups where ${}^{\mathrm{\prime }}$ turns out to be the natural inverse operation. We recount here the history of the problem including our previous efforts to find a 2-base using automated deduction and the method that finally worked. We describe our efforts to simplify the proof using $\text{textsc}Prover9$, present the simplified proof itself and conclude with some open problems.