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がよく分かりません。
途中過程などもお願いします。