The authors wish to thank the anonymous referees for providing useful comments and for pointing out the existence of short tree-like RES(k) proofs of pebbling formulas. This research was supported by NSF Grant ITR-0219468 and parts of this paper appeared earlier in IJCAI '03 and SAT '03 conferences (Beame et al., 2003b, Sabharwal et al., 2003).