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 \[ \quad x(x'x) = x \qquad \quad x (x' (y (y' ((z u)'
w')'))) = y (y' (x (x' ((w z) u)))) \] form a base for inverse semigroups where
${}'$ 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 \textsc{Prover9}, present the simplified proof
itself and conclude with some open problems.