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

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