I know I am making a mistake somewhere but consider the following truth table:
p0 p1 p2 | ------------------- 0 0 0 | 1 0 0 1 | 0 0 1 0 | 0 0 1 1 | 1 1 0 0 | 1 1 0 1 | 1 1 1 0 | 1 1 1 1 | 1
This coresponds to the boolean formula in DNF:
p0 v (~p1 ^ ~p2) v (p1 ^ p2)
or in CNF:
(p0 v ~p1 v p2) ^ (p0 v p1 v ~p2)
Using the last two clauses and applying the resolution inference rule on p1:
(p0 v ~p1 v p2) ^ (p0 v p1 v ~p2) |- (p0 v p2 v ~p2) = (p0 v T) = p0
So from the two clauses I can infer p0. This does not seem right since p0 does not always have to be true according to the truth table.