The unification procedure does not contain an occur check. Hence, cyclic structures can be created during unification. These cyclic structures may cause loops in attempting unification. eg. X = f(X,Y), Y = f(X,Y).
Success: atom = atom. atom = X. (gives X = atom) X = atom. (gives X = atom) f(1) = X. (gives X = f(1)) Y = X. (gives Y = _g68, X = _g68) [1,X] = [Y,2]. (gives X = 2, Y = 1) [1,X|Y] = [W,2|Z]. (gives X = 2, Y = _g78, W = 1, Z = _g78) [1,A,2,B] = [C|D]. (gives A = _g80, B = _g88, C = 1, D = [_g80, 2, _g88]) Fail: atom = neutron. 1.0 = 1. [a|b] = [a,b].