de Nivelle, H. (2003). Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. In Automated deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 365-379). Berlin, Germany: Springer.