Why is factoring causing wrong answer in resolution logic?

Question

When performing resolution for the following KB:

1. Game(x) ^ Game(y) ^ Loves(z,x) => Loves(z,y)
2. Game(ResidentEvil)
3. Game(GodofWar)
4. Loves(John,GodofWar)

Query: Loves(John,ResidentEvil) ?

The answer should be true but when performing factoring it becomes false.

Resolve sentence 1 and query:

~Game(x) v ~Game(ResidentEvil) v ~Loves(John,x)

Now if we perform factoring (for Game literal) on the result we get

~Game(ResidentEvil) v ~Loves(John,ResidentEvil)

Since ~Loves(John,ResidentEvil) is again part of the result this will eventually result in false.

Why is factoring causing the query to be false when it should be true?

Answer 1

Factoring is sometimes necessary to obtain the empty clause, but it is just an extra inference. That is, the original clause

$\neg Game(x) \lor \neg Game(ResidentEvil) \lor \neg Loves(John,x)$

does not get replaced by

$\neg Game(ResidentEvil) \lor \neg Loves(John,ResidentEvil)$

but rather the latter clause gets added to the clause set.

But in this case, the added clause does nothing for you, and it is the original clause (that is still there!) that eventually gets you to the empty clause.