Show that a set has no Herbrand model Given the Herbrand Theorem

A clausal theory Th is satisfiable iff the grounding of Th is satisfiable

And given $S = \{ G(c), B(a), G(x) \vee \neg G(y), \neg B(x) \vee \neg G(x) \}$
How can I show that set $S$ has no Herbrand model? 
I'm new to logic and have never had any experience in proofs before, what are the steps I should take to approach this? I've looked at Intuition about Herbrand Models. but I'm not quite clear on the Lemma, could someone elaborate a little more? (Sorry for the newbie question!)
 A: As per the linked post, the Herbrand structure is a mathematical structure built with the syntactical stuff: terms are used as objects of the domain of the interpretation. 
We consider the set $S$ of clauses. In it we have only two constants : $a$ and $c$. Thre are no function symbols; thus, the only two ground terms are $a$ and $c$.
This means that the H-universe will be: $H = \{ a, c \}$.
Having the domain $H$, we build the interpretation: constants are interpreted with themselves, and predicates are interpreted through ground instances obtained from clauses replacing variables with ground terms. 
With $H$ we may generate the following set $S'$ of ground instances :

$\{ G(c), B(a), G(a) \lor ¬ G(c), ¬ B(a) \lor ¬ G(a) \}$.

$S'$ s a finite set of ground instances of the set $S$ of clauses and it is clearly unsatisfiable.
Thus, by Herbrand's Theorem, also the set $S$ is unsatisfiable.

We may use Resolution to prove that $S$ is unsatisfiable :
1) $G(c)$
2) $B(a)$
Unifying $¬ B(x) \lor ¬ G(x)$ with $a \to x$ we get $¬ B(a) \lor ¬ G(a)$ and using 2) we get, by Resolution:
3) $¬ G(a)$
Unifying $G(x) \lor ¬ G(y)$ with $a \to x$ and $c \to y$ we get $G(a) \lor ¬ G(c)$ and using 3) we get, by Resolution:
4) $¬ G(c)$
Finally, using Resolution with 1) and 4) we get :

5) $\square$ --- the empty clause, showing the unsatisfiability of $S$.

which is cleary unsatisfiable.
