Did you know ...  Search Documentation: 
dif.pl  The dif/2 constraint 
Term1 == Term2
. Succeeds if Term1
can never become identical to Term2. In other cases the
predicate succeeds after attaching constraints to the relevant
parts of Term1 and Term2 that prevent the two terms to become
identical.dif(X,Y)
that is related to the given OrNode. If X and Y are
equal we reduce the OrNode. If they cannot unify we are done.
Otherwise we extend the OrNode with new pairs and create/extend the
vardif/2 terms for the left hand side of the unifier as well as the
right hand if this is a variable.[V1 = f(a, V2), V2 = b]
. As a result of subsequent unifying
variables, the unifier may end up having multiple entries for the
same variable, possibly having different values, e.g., [X = a, X =
b]
. As these can never be satified both we have prove of
inequality.
Finally, we remove elements from the list that have become equal. If the OrNode is empty, the original terms are equal and thus we must fail.
On unification with a value, we recursively call dif_c_c/3 using the existing OrNodes.

and remove
this dead OrNode from every vardif/2 attribute we can find.