Prove theorem 320- a renamable horn clause set s is

Question

Prove Theorem 3.20.

Hints: prove the theorem first for Horn clauses. Then note that a unit resolution proof before renaming is a unit resolution proof after renaming.

Theorem 3.20
A renamable Horn clause set S is unsatisfiable if and only if the unit resolution algorithm derives the empty clause from S.