 We can dispense with reflexivity since it is derivable from the other two formulas. This brings the number of axioms down to two and a natural question to ask is whether there is a single axiom for the equivalential calculus. In 1933, Łukasiewicz found three formulas of length eleven that each could act as a single axiom for the calculus—here’s one of them: e(e(x,y),e(e(z,y),e(x,z)))—and he also showed that no shorter single axiom existed. Over time, other single axioms also of length eleven were found and the list kept growing with additions by Meredith, Kalman and Peterson to a total of 14 formulas of which 13 were known to be single axioms and one formula with a yet undetermined status: the formula XCB = e(x, e(e(e(x, y), e(z, y)), z)). (Actually, the list grew to 18 formulas but Wos, Winker, Veroff, Smith &amp; Henschen 1983 reduced it to 14.) Resisting the intense study of various researchers, it remained as an open question for many years whether the 14th formula, XCB, was a single axiom for the equivalential calculus (Peterson 1977). One way to answer the question in the affirmative would be to show that at least one of the 13 known single axioms is derivable from XCB alone; another approach would be to derive from XCB the 3-axiom set (E1)–(E3). While Wos, Ulrich &amp; Fitelson 2002 take shots at the former, their line of attack concentrates on the latter with the most challenging task being the proving of symmetry. Working with the assistance of a powerful automated reasoning program, Otter, they conducted a concerted, persistent and very aggressive assault on the open question. (Their article sometimes reads like a military briefing from the front lines!) For simpler problems, proofs can be found by the reasoning program automatically; deeper and more challenging ones like the one at hand require the guidance of the user. The relentless application of the reasoning tool involved much guidance in the setting of lemmas as targets and the deployment of an arsenal of strategies, including the set of support, forward and backward subsumption, lemma adjunction, formula complexity, hints strategy, ratio strategy, term avoidance, level saturation, and others. After much effort and CPU time, the open question finally succumbed to the combined effort of man and machine and a 61-step proof of symmetry was found, followed by one for transitivity after 10 more applications of condensed detachment. Subsequent runs of the theorem prover using demodulation blocking and the so-called cramming strategy delivered shorter proofs. Here are the last lines of their 25-step proof which in this case proves transitivity first followed by symmetry: 