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.