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

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