On the Automatizability of Resolution and Related Propositional Proof Systems