MGU Examples From Class, slide 91
=================================

- f(X,a) and f(a,Y) 
unifies
substitutions:
  X=a 
  Y=a
Resulting term:
  f(a,a)

- f(h(X,a),b) and f(h(g(a,b),Y),b)
unifies
substitution:
  X=g(a,b)
  Y=a
Resulting term:
  f(h(g(a,b),a),b)

- g(a,W,h(X)) and g(Y,f(Y,Z),Z)
unifies
substitution:
  W=f(a,h(X))
  Y=a
  Z=h(X)
Resulting term:
  g(a,f(a,h(X)),h(X))

- f(X,g(X),Z) and f(Z,Y,h(Y))
does not unify
attempted substitution (does not terminate):
  X=h(g(h(g(h...))))
  Z=h(g(h(g...)))
  Y=g(h(g(h...)))

- f(X,h(b,X)) and f(g(P,a),h(b,g(Q,Q)))
unifies
substitution:
  P=a
  Q=a
  X=g(a,a)
Resulting term:
  f(g(a,a),h(b,g(a,a)))