Did you know ... Search Documentation:
Predicate dif_c_c/3
 dif_c_c(+X, +Y, !OrNode)[private]
Enforce 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.