# How does negation as failure work with variables?

Let's say we have the following rule:

p -: X ≠ Y, X = Y


Stating that $$\forall x.y. x \neq y \land x = y \implies p$$. Now let us suppose that we are searching for a proof of $$p$$. Such a proof does not exist, of course, but we will search for it.

Our starting goal is p. We replace it with the subgoals X ≠ Y and X = Y. To resolve X ≠ Y, we use negation as failure. We must show that exists an $$x$$ and $$y$$ such that $$x = y$$ is unprovable. So we know have a goal of X = Y. Since $$x$$ and $$y$$ are not the same variable (remember, $$x$$ and $$y$$ were bound by the quantifier of the top level rule), there is no way to resolve $$x = y$$. So we fail to show $$x = y$$, and the subgoal X ≠ Y is resolved. We now resolve the subgoal X = Y. This is done by unification, which means we set Y := X. Since all subgoals have been resolved, the original goal p has succeeded, with the solution X := X and Y := X.

However, this is obviously incorrect since $$p$$ should not be provable. $$x \neq y \land x = y$$ is always false, so we can not use the rule to deduce it.

The problem seems to be that negation as failure is not actually negation. Being unable to show that $$x \neq y$$ does not mean it is false. Resolving something like I did above "loses" consequences of negated statements.

What is the correct way to resolve rules like the above?