Resolution is not automatizable unless W[P] is tractable
Mikhail Alekhnovich, A.A. Razboro · 2001
We show that neither Resolution nor tree-like Resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error.