YES

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

Proof:
 Uncurry Processor (mirror):
  a2(a(),x) -> f(x,a1(x))
  f(a1(x2),x3) -> a2(x2,x3)
  f(a(),x3) -> a1(x3)
  Bounds Processor:
   bound: 5
   enrichment: roof
   automaton:
    final states: {5,6}
    transitions:
     a{2,4}(5,15) -> 5*
     f4(13,16) -> 5*
     a{1,4}(13) -> 16*
     a{2,5}(5,16) -> 5*
     a{2,0}(5,5) -> 5*
     a{2,0}(6,6) -> 5*
     a{2,0}(5,6) -> 5*
     a{2,0}(6,5) -> 5*
     a0() -> 6*
     f0(5,5) -> 5*
     f0(6,6) -> 5*
     f0(5,6) -> 5*
     f0(6,5) -> 5*
     a{1,0}(5) -> 5*
     a{1,0}(6) -> 5*
     a{1,1}(5) -> 5,8
     a{1,1}(6) -> 5,9
     a{2,1}(14,6) -> 5*
     a{2,1}(9,6) -> 5*
     a{2,1}(5,5) -> 5*
     a{2,1}(6,6) -> 5*
     a{2,1}(14,5) -> 5*
     a{2,1}(9,5) -> 5*
     a{2,1}(5,6) -> 5*
     a{2,1}(6,5) -> 5*
     f1(5,8) -> 5*
     f1(6,9) -> 5*
     a{1,2}(5) -> 13*
     a{1,2}(9) -> 5*
     a{1,2}(6) -> 14*
     a{2,2}(14,8) -> 5*
     a{2,2}(9,8) -> 5*
     a{2,2}(6,8) -> 5*
     a{2,2}(5,8) -> 5*
     f2(5,13) -> 5*
     f2(6,14) -> 5*
     a{1,3}(14) -> 5*
     a{1,3}(8) -> 15*
     a{2,3}(5,13) -> 5*
     a{2,3}(14,13) -> 5*
     a{2,3}(9,13) -> 5*
     a{2,3}(6,13) -> 5*
     f3(8,15) -> 5*
   problem:
    
   Qed