Hi, when running a very classical example of rational tree unification, I get the following:

?- f(X, Y, X) = f(g(X), g(Y), Y). X = Y, Y = g(Y).

However, with unifiable/3, I have this:

?- unifiable(f(X, Y, X), f(g(X), g(Y), Y), U). U = [Y=g(Y), X=g(X)].

The result of unifiable/3 is exactly what I expected from the Prolog-II-style base reduction algorithm, but the first response is more accurate. Why do these two differ? Can you please point me to the specification of the SWI Prolog unification algorithm used in =/2 ?