Some Hard Examples for the Resolution Method

Given n propositional variables,let Kn(i,j),0≤i≤j≤n,be the set(or disjunction)of all conjunctions of i literals of which exactly j literals are negative.Dunham and Wang conjectured that it may require exponential time to decide that every disjunction Kn(i,j)is not valid by the resolution metho.This paper gives a proof of the conjecture and then exhibits a new counterexample to the feasibility of the resolution or consensus method.