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

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