Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms