Problem:
 f(h(x),y) -> h(f(y,f(x,h(a()))))

Proof:
 Unfolding Processor:
  loop length: 6
  terms:
   f(h(h(x660)),h(h(x888)))
   h(f(h(h(x888)),f(h(x660),h(a()))))
   h(h(f(f(h(x660),h(a())),f(h(x888),h(a())))))
   h(h(f(h(f(h(a()),f(x660,h(a())))),f(h(x888),h(a())))))
   h(h(f(h(h(f(f(x660,h(a())),f(a(),h(a()))))),f(h(x888),h(a())))))
   h(h(f(h(h(f(f(x660,h(a())),f(a(),h(a()))))),h(f(h(a()),f(x888,h(a())))))))
  context: h(h([]))
  substitution:
   x660 -> f(f(x660,h(a())),f(a(),h(a())))
   x888 -> f(f(x888,h(a())),f(a(),h(a())))
  Qed