Applying Saturation-Based Theorem Proving to Open Problems in Positive Implicational Logic

We revisit a longstanding question about the shortest single axioms for positive implicational logic. Meredith discovered several 17-symbol single axioms and asked whether shorter ones exist. Later work reduced the problem to four candidate formulas of length 15. Using the automated theorem prover Vampire, we compute saturated clause sets that yield counter models showing that three of these candidates are not single axioms. This demonstrates the effectiveness of saturation-based reasoning for such problems, which have traditionally been studied via finite model searches.