Some Hard Examples for the Resolution Method

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