Ch2, Ex13

From the algorithm given in the book its clear that unification is a symmetric operation, so whatever order we follow; following is the resulting set of bindings:
X = Y = [a b]
W = a
Z = b

it can also be confirmed from mozart system by executing following

local X Y W Z in
   % try different order of unifications
   X = [a Z]
   Y = [W b]
   X = Y
   % No matter what the above sequence is, following sequence
   % always prints
   % true
   % [a b]
   % a
   % b
   {Browse X==Y}
   {Browse X}
   {Browse W}
   {Browse Z}
end