Resolution lower bounds for refutation statements

For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolutionrefutations of a propositional statement that the formula has a resolution refutation. We describethree applications. (1) An open question in [2] asks whether a certain natural propositional encodingof the above statement is hard for Resolution. We answer by giving an exponential size lower bound.(2) We show exponential resolution size lower bounds for reflection principles, thereby improvinga result in [1]. (3) We provide new examples of CNFs that exponentially separate Res(2) fromResolution (an exponential separation of these two proof systems was originally proved in [10]).Peer ReviewedPostprint (published version