Avigad, Jeremy Plausibly Hard Combinatorial Tautologies We present a simple propositional proof system which consists of a single axiom schema and a single rule, and use this system to construct a sequence of combinatorial tautologies that, when added to any Frege system, p-simulates extended-Frege systems. Philosophy 1997-01-01
    https://kilthub.cmu.edu/articles/journal_contribution/Plausibly_Hard_Combinatorial_Tautologies/6492443
10.1184/R1/6492443.v1