Combine the incoming unifier with the OrNode's current pending set,
then recompute the most-general unifier for the whole using
unifiable/3 over the accumulated left- and right-hand-side lists.
That gives canonical propagation and avoids the infinite oscillation
pair-wise simplification hits on cyclic terms.
Fails if the recomputed set is empty — that means all pending
equations are trivially satisfied and thus the original dif/2 terms
are equal, so dif/2 must fail. Calls or_succeed/1 when unifiable/3
itself fails: the pending equations can never all hold, so the two
terms are definitely unequal and dif/2 is satisfied.
