de Nivelle, H. (2005). Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. Information and Computation, 199, 24-54.