For simpler questions involving proof by resolution, it is easy to see whether or not a contradiction can be found by inferring the empty clause, and somewhat easy to show there is no empty clause inference. However, for questions involving a larger number of clauses and terms, such as:
$a ∨ b ∨ c \\ a ∨ ¬c ∨ d \\ ¬a ∨ e ∨ f \\ c ∨ ¬e ∨ f \\ c ∨ ¬d ∨ ¬f $
How exactly, using a formal method, can we show that an empty clause cannot be inferred?