 A question was posed sometime after: Is there a shorter such axiomatization for C4, using a 2-axiom basis or even a single axiom? Using the automated reasoning program Otter, the authors Ernst, Fitelson, Harris &amp; Wos (2001) settled both questions in the affirmative. In fact, several 2-axiom bases were discovered of which the following turned out to be shortest: 