Problem:
 g(f(x,y)) -> f(f(g(g(x)),g(g(y))),f(g(g(x)),g(g(y))))

Proof:
 Unfolding Processor:
  loop length: 2
  terms:
   g(g(f(x4,x5)))
   g(f(f(g(g(x4)),g(g(x5))),f(g(g(x4)),g(g(x5)))))
  context:
   f(f(g(g(f(g(g(x4)),g(g(x5))))),g(g(f(g(g(x4)),g(g(x5)))))),f(g(g(f(g(g(x4)),g(g(x5))))),[]))
  substitution:
   x4 -> g(g(x4))
   x5 -> g(g(x5))
  Qed