If X and Y cannot unify then the goal succeeds. If X and Y are equal then the goal fails. If X and Y could unify then a restriction is added to prevent X and Y from unifying in the future.
Examples
?- dif(a,b).
yes
?- dif(a,a).
no
?- dif(X,X).
no
?- X=Z, Y=Z, dif(X,Y).
no
?- dif(X,Y), X=Z, Y=Z.
no
?- dif(p(X),p(X)).
no
?- dif(X,Y), X=1, Y=1.
no
?- dif(X,Y), Y=1, X=1.
no
?- dif(X,Y), X=1, Y=2.
X = 1
Y = 2
yes
?- dif(X,Y), Y=1, X=2.
X = 2
Y = 1
yes
?- dif(X,Y), dif(X,Z), X=1, Y=1, Z=2.
no
?- dif(X,Y), dif(X,Z), X=1, Y=2, Z=1.
no
?- dif(X,Y), dif(X,Z), X=1, Y=2, Z=2.
X = 1
Y = 2
Z = 2
yes
?- dif(Y,X), dif(Z,X), X=1, Y=1, Z=2.
no
?- dif(Y,X), dif(Z,X), X=1, Y=2, Z=1.
no
?- dif(Y,X), dif(Z,X), X=1, Y=2, Z=2.
X = 1
Y = 2
Z = 2
yes
?- dif(Y,X), dif(X,Z), X=1, Y=1, Z=2.
no
?- dif(Y,X), dif(X,Z), X=1, Y=2, Z=1.
no
?- dif(Y,X), dif(X,Z), X=1, Y=2, Z=2.
X = 1
Y = 2
Z = 2
yes
?- dif(p(A,B),p(X,Y)), A=1, X=1, B=2, Y=2.
no
?- dif(p(A,B),p(X,Y)), Y=1, A=2, B=1, X=2.
no
?- A=1, X=1, B=2, Y=2, dif(p(A,B),p(X,Y)).
no
?- Y=1, A=2, B=1, X=2, dif(p(A,B),p(X,Y)).
no
?- A=1, Y=2, dif(p(A,B),p(X,Y)), X=1, B=2.
no
?- dif(p(A,B),p(X,Y)), A=1, B=1, X=1, Y=2.
A = 1
B = 1
X = 1
Y = 2
yes
?- A=1, B=1, X=2, Y=1, dif(p(A,B),p(X,Y)).
A = 1
B = 1
X = 2
Y = 1
yes
?- A=1, B=2, dif(p(A,B),p(X,Y)), X=1, Y=1.
A = 1
B = 2
X = 1
Y = 1
yes
?- dif(a(z(Z,p(X))), a(z(Y,p(S)))), Z=1, Y=1, X=2, S=2.
no
?- dif(a(z(Z,p(X))), a(z(Y,p(S)))), Z=1, Y=1, X=2, S=1.
S = 1
X = 2
Y = 1
Z = 1
yes
?- dif(a(z(Z,p(X))), a(z(Y,p(S)))), Z=1, Y=2, X=2, S=2.
S = 2
X = 2
Y = 2
Z = 1
yes
?- dif(a(Q,W,E,R,T,Y), a(A,B,C,D,E,F)), Q=1, W=2, E=3, R=4, T=3, Y=6, A=1, B=2, C=3, D=4, E=3, F=6.
no
?- dif(a(Q,W,E,R,T,Y), a(A,B,C,D,E,F)), Q=1, W=1, E=1, R=1, T=1, Y=1, A=1, B=1, C=1, D=1, E=1, F=2.
A = 1
B = 1
C = 1
D = 1
E = 1
F = 2
Q = 1
R = 1
T = 1
W = 1
Y = 1
yes
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, X=2.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, X=3.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Y=2.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Y=3.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Z=2.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Z=3.
no
?- dif(X,2), dif(Y, 3), Z=X, Z=Y, Z=2.
no
?- dif(X,2), dif(Y, 3), Z=X, Z=Y, Z=3.
no
?- dif(X,2), dif(Y, 3), X=Z, Y=Z, Z=2.
no
?- dif(X,2), dif(Y, 3), X=Z, Y=Z, Z=3.
no
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, X=4.
X = 4
Y = 4
Z = 4
yes
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Y=1.
X = 1
Y = 1
Z = 1
yes
?- dif(X,2), dif(Y, 3), X=Z, Z=Y, Z=a.
X = a
Y = a
Z = a
yes
?- dif(X, a(b,c)), X=a(B,C), B=b, C=c.
no