Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the pigeon hole problem).
How can a clausal proof efficiently (i.e. in polynomial time) be converted to a resolution proof?
Is there any relationship between the size of the clausal proof and the corresponding size of the transformed resolution proof?