  With the inclusion of an effective methodology, this article answers in
detail a question that, for a quarter of a century, remained open despite
intense study by various researchers. Is the formula XCB =
e(x,e(e(e(x,y),e(z,y)),z)) a single axiom for the classical equivalential
calculus when the rules of inference consist of detachment (modus ponens) and
substitution? Where the function e represents equivalence, this calculus can be
axiomatized quite naturally with the formulas e(x,x), e(e(x,y),e(y,x)), and
e(e(x,y),e(e(y,z),e(x,z))), which correspond to reflexivity, symmetry, and
transitivity, respectively. (We note that e(x,x) is dependent on the other two
axioms.) Heretofore, thirteen shortest single axioms for classical equivalence
of length eleven had been discovered, and XCB was the only remaining formula of
that length whose status was undetermined. To show that XCB is indeed such a
single axiom, we focus on the rule of condensed detachment, a rule that
captures detachment together with an appropriately general, but restricted,
form of substitution. The proof we present in this paper consists of
twenty-five applications of condensed detachment, completing with the deduction
of transitivity followed by a deduction of symmetry. We also discuss some
factors that may explain in part why XCB resisted relinquishing its treasure
for so long. Our approach relied on diverse strategies applied by the automated
reasoning program OTTER. Thus ends the search for shortest single axioms for
the equivalential calculus.
