Fを単項、Gを２項演算子とする。２つの項
s＝G(F(G(F(x4),G(x3,F(G(x2,x2))))),G(x1,G(x3,F(x1))))
t＝G(F(G(x5,G(x5,x6))),G(x7,G(F(x6),F(G(x5,x6)))))
のmgu(most general unifier)はどうなりますか？
mguがあまりよく分からないので、過程も書いてくださるとうれしいです。