 To show that each of (2) and (3) is necessary and sufficient for (1), a circle of proofs was produced using the automated reasoning tool: (1) ⇒ (3) ⇒ (2) ⇒ (1). As for C5, its axiomatization was originally published in a paper by Lemmon, A. Meredith, D. Meredith, Prior &amp; Thomas (1957) giving several 4-, 3-, 2- and 1-axiom bases for C5, including the following 3-axiom basis: 