Checking Most General Unifier I've just taken a logic course in college. However, there's something that I'm still unsure about MGU. I will like to use an example to illustrate my query.
Suppose we have to unify $Q(y, G(A,z)), Q(G(x,B),y)$.
The MGU I got was $ x\leftarrow A, y \leftarrow G(x,B), z\leftarrow B$.
I am supposed to find another MGU (if it exists).
I gave the answer as $ x\leftarrow A, y \leftarrow G(A,z), z\leftarrow B$. Is this correct? Or is the MGU $ x\leftarrow A, y \leftarrow G(A,B), z\leftarrow B$?
Thank you.
 A: Expanding on @MauroALLEGRANZA 's comments.

Suppose we have to unify $Q(y, G(A,z)), Q(G(x,B),y)$.
The MGU I got was $ x\gets A, y \gets G(x,B), z\gets B$.

Simultaneous substitutions have to be applied carefully and consistently to always obtain a sensible result.   One must only substitute into the statement's pre-existing literals; please do not substitute into the literals of other substitutions being made at the same time.   (We want to avoid recursions, among other reasons.)
[ For example, applying $x\gets y, y\gets x$ simultaneously to $P(x,y,y,x)$ must give $P(y,x,x,y)$ ]
So your proposed substitution would obtain : $Q(G(x,B), G(A,B)), Q(G(A,B),G(x,B))$
$$Q(\underset{G(x,B)}{\underset{\uparrow}{y}}, G(A,\underset{B}{\underset{\uparrow}{z}})), Q(G(\underset{A}{\underset{\uparrow}{x}},B),\underset{G(x,B)}{\underset{\uparrow}{y}})$$
This is an intermediate result; the strings are still non-identical.   Now, applying the substitution $x\gets A$ again will make them identical.   However, we are required to do it all in one step.
Thus to immediately obtain the required result, you must make a simultaneous substitution of $x\gets A, y\gets G(A,B), z\gets B$.
