Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a worst-case family of boolean formulae? Since no superpolynomial lower bounds are known on Extended Resolution, we don't have a good upper bound on $D$, so I'm interested in lower bounds on $D$.Edit: Clarified question as per Kaveh's answer below
Resolution vs Extended Resolution
cc.complexity theory;lo.logic;proof complexity;proof theory