(¬a ∨ ¬b) is a blocked clause with respect to (a ∨ b ∨ c) ∧ (¬a) ∧ (¬c) ∧ (¬e ∨ ¬d) ∧ (a ∨ b ∨ c ∨ d) ∧ (f ∨ d).

If φ is not valid, then ¬φ is satisfiable. 

(a ∨ ¬b) is a blocked clause with respect to (a ∨ b ∨ c) ∧ (¬a) ∧ (¬c) ∧ (¬e ∨ ¬d) ∧ (a ∨ b ∨ c ∨ d) ∧ (f ∨ d).

Two formulas are satisfiable-equivalent if they have the same set of models. 

The resolvent of (a ∨ b ∨ c) and  (¬a) is (b ∨ c). 

The resolvent of (a ∨ b ∨ c) and  (¬a ∨ ¬b) is (c).