I am afraid, your question seems to be not very clear. I know resolution but I do not understand your question. What relation between the set of Horn clauses and S?

I assume that the set of Horn clauses is S, and that you are working in classical predicate logic.

This is a classical results that you can find e.g. in L. Henschen and L. Wos

Unit Refutations and Horn Sets. JACM, Volume 21 Issue 4, Oct. 1974, Pages 590-605 

http://dl.acm.org/citation.cfm?id=321857

You'll also find it (or variants) in many Prolog textbooks.

Resolution, thus unit resolution, is sound. So the "only if" part is immediate.

At the ground level, the "if" part is really easy, but the trick at the first order level is showing that "factoring" is not needed. JACM 21,4 is overkill, but it does this amongst other results.

Intuitively, a ground positive unit proof can be lifted to (a proof of) the first order clauses, of which it is a set of instances, in the usual way -- EXCEPT that a single ground step may correspond to a unit resolution involving a clause in which k literals have been factored together into one. But unification theory allows this one step on a factor  to be replaced by k (unit) steps on the original clause, resulting in the same resolvent produced by the one step with the factor.

(This is mostly intuition and not even a proof sketch.)