Constrains X and Y to represent different terms i.e. to be non-unifiable.
dif/2 either succeed, fail, or are blocked depending
on whether X and Y are sufficiently instantiated. It is
defined as if by:
dif(X, Y) :- when(?=(X,Y), X\==Y).