YES

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

Proof:
 Uncurry Processor:
  a2(a1(x),x3) -> f(f(x,a1(a2(a(),a()))),x3)
  a1(a1(x)) -> f(x,a1(a2(a(),a())))
  f(a1(x1),x2) -> a2(x1,x2)
  f(a(),x2) -> a1(x2)
  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {8,7,6,1}
    transitions:
     a{2,1}(5,5) -> 6*
     a{2,1}(2,5) -> 6*
     a{2,1}(9,9) -> 10*
     a{2,1}(5,2) -> 1,7
     a{2,1}(2,2) -> 1,7
     f1(12,5) -> 6*
     f1(4,11) -> 8,12
     f1(12,2) -> 1*
     a{1,1}(10) -> 11*
     a1() -> 9*
     f40() -> 2*
     f0(6,2) -> 1*
     f0(2,5) -> 6*
     f0(4,5) -> 6,8
     f0(6,5) -> 8*
     a{1,0}(5) -> 6*
     a{1,0}(2) -> 8*
     a{1,0}(4) -> 5*
     a{2,0}(3,3) -> 4*
     a{2,0}(5,5) -> 8*
     a{2,0}(2,5) -> 6*
     a{2,0}(5,2) -> 1,7
     a{2,0}(2,2) -> 1,7
     a0() -> 3*
     1 -> 7*
     6 -> 8*
     8 -> 6*
   problem:
    
   Qed