|Did you know ...||Search Documentation:|
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.