See Resolution (logic) :
the resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in Conjunctive Normal Form.
1st step :
the negation of the sentence to be proved (the conjecture) is to be considered.
In your case, we have :
$$\lnot [A ∨ (B∧C) ∨ (¬A∧¬B) ∨ (¬A∧B∧¬C)] \equiv [¬A ∧ (¬B ∨ ¬C) ∧ (A ∨ B) ∧ (A ∨ ¬B ∨ C)].$$
As said above, the proof procedure works by contradicition : assume the formula $\lnot \varphi$ (where $\varphi$ is the conjecture) and apply iteratively the rule.
If the procedure gives us as result that the formula $\lnot \varphi$ is unsatisfiable, we can conclude that the original conjecture ($\varphi$) is a tautology.
2nd step :
the sentence is transformed into a Conjunctive Normal Form with the conjuncts viewed as elements in a set, $S$, of clauses, where a clause is a disjunction of literals.
Thus, the formula above will correspond to the set of clauses :
$S = \{ ¬A, (¬B ∨ ¬C), (A ∨ B), (A ∨ ¬B ∨ C) \}$.
3rd step :
The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set $S$, it is added to $S$, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause, $\square$ (or : $\bot$), is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture is a tautology.
We have to apply the rule to the set $S$ above :
1) $¬A$
2) $¬B ∨ ¬C$
3) $A ∨ B$
4) $A ∨ ¬B ∨ C$
5) $B$ --- from 1) and 3)
6) $¬B ∨ C$ --- from 1) and 4)
7) $¬C$ --- from 5) and 2)
8) $C$ --- from 5) and 6)
$\square$ --- the empty clause : from 7) and 8).
The rule has the property that preserves satisfiability, i.e. the new set of clauses is satisfiable iff the original one is.
Thus, if after iterated applications of the rule the empty clause is produced, being it unsatisfiable (the empty clause in another way of representing a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.
