How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?

I'm working on a program which must use inference in first-order logic, and everything is working great except for 1 thing which I don't understand.

The book I'm using, "Artificial Intelligence A Modern Approach" by Russell and Norvig, shows a proof on page 349 which has me confused.
They combine the two following sentences:
~Loves(x,F(x)) v Loves(G(x),x)

~Animal(x) v Loves(Jack,x)

And they combine into:

~Animal(F(Jack)) v Loves(G(Jack),Jack)

This makes absolutely no sense to me because the variable "x" becomes both "F(Jack)" and "Jack", and that seems wrong to me.

Using the Unify function which I created by following the pseudocode provided in the book returns a failed substitution, but if the combination of the previously mentioned sentences is correct then what kind of substitution would need to be returned? (I know it's not just {x/Jack} because that would result in the sentence "~Animal(Jack) v Loves(G(Jack),Jack)", Animal would be missing the function F as shown in the example.)

Any help would be extremely appreciated!

The variables called x in the two sentences are not related. We can rename them to make it clear:

~Loves(x1,F(x1)) v Loves(G(x1),x1)
~Animal(x2) v Loves(Jack,x2)

Now when matching ~Loves(x1,F(x1)) and Loves(Jack,x2), you can see you'll get Jack/x1, F(Jack)/x2 and the final result as in the book.

StackExchange Computer Science Q#65827, answer score: 3