A propositional proof system is \emph{weakly automatizable} if thereis a polynomial time algorithm which separates satisfiable formulasfrom formulas which have a short refutation in the system, withrespect to a given length bound. We show that if the resolutionproof system is weakly automatizable, then parity games can bedecided in polynomial time. We give simple proofs that the sameholds for depth-1 propositional calculus (where resolution hasdepth 0) with respect to mean payoff and simple stochastic games.We define a new type of combinatorial game and prove that resolutionis weakly automatizable if and only if one can separate, by a set inP, the games in which the first player has a positional strategyfrom the games in which the second player has a positional winningstrategy.