Needs text improvement
"Finally, if A and B can unify, goals are delayed that prevent A and B to become equal." doesn't sense to me.
The text in library(dif) is much clearer:
"Among the most important coroutining predicates is dif/2, which expresses disequality of terms in a sound way. The actual test is delayed until the terms are sufficiently different, or have become identical."
I prefer to look at it this way:
dif(A,B) call, any unification involving A or B or subterms thereof
that would make A and B identical (
A == B) will fail (and this applies to unification in clause heads, too).
If A and B are already identical at call time,
dif(A,B) fails at once.
These seem to be equivalent views, unless I missed something.
Writeup on dif
I made a writeup, including examples, here: About dif/2
That has turned into a lot of text, hopefully clear.