Resolution complexity versus a constrained SAT algorithm
While the deductions made by $M$ can have equivalent (possibly exponentially bigger) resolution proofs, I'm not sure what you mean by translating the rule system of $M$ into resolution form. If $M$ has a rule saying that if the problem is a PHP (pigeonhole principle) problem then output unsat if number of pigeons > number of holes, how would you translate that rule into resolution form? 
Edit: To elaborate on the last point, we know that Extended Resolution (ER) which in a nutshell, allows one to add new variables, has polynomial-size PHP proofs. Now suppose, $M$ uses ER to prove PHP. Such reasoning cannot be "directly" translated into a resolution proof as that would require adding new variables to the formula which is not allowed in pure resolution proofs.
As I mentioned in point 1, you can translate the deductions by $M$ into resolution proofs of those deductions but the resolution proof might be exponentially larger.