Axioms of Minimum Size Resolution Refutations

Let $$\phi$$ be an unsatisfiable CNF formula and let $$\Pi$$ be a resolution refutation of $$\phi$$ of minimum size. Let $$\psi$$ be the subformula of $$\phi$$ containing the clauses that actually appear as axioms in $$\Pi$$. Is there anything interesting that can be said about $$\psi$$?

Some specific questions:

• Is $$\psi$$ minimally unsatisfable? (i.e., are all proper subsets of $$\psi$$ satisfiable?)
• Are all variables appearing in $$\psi$$ necessary for unsatisfiability? (i.e., is there an assignment to all but one variable that does not falsify any clauses in $$\psi$$?)
• Is $$\psi$$ a minimum unsatisfiable core of $$\phi$$?

All of these properties seem unlikely to hold in general but I cannot think of any counterexamples.

• What is an unsatiafiable core? – Joshua Grochow May 17 '19 at 13:25
• An unsatisfiable core is just a subformula that is unsatisfiable. So for the third question, I am just interested if the $\psi$ can always be assumed to be minimum in size. – NMEM May 17 '19 at 20:35