YES

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

Proof:
 Uncurry Processor (mirror):
  a2(a1(a1(a())),x) -> f(x,a1(x))
  f(a1(x4),x5) -> a2(x4,x5)
  f(a(),x5) -> a1(x5)
  Bounds Processor:
   bound: 9
   enrichment: roof
   automaton:
    final states: {5,6}
    transitions:
     f3(9,15) -> 5*
     a{2,4}(5,15) -> 5*
     f4(14,16) -> 5*
     a{1,4}(14) -> 16*
     a{2,5}(5,16) -> 5*
     f5(15,20) -> 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*
     a{1,5}(15) -> 20*
     a{1,0}(5) -> 5*
     a{1,0}(6) -> 5*
     a{2,6}(9,20) -> 5*
     a0() -> 6*
     f6(16,22) -> 5*
     f0(5,5) -> 5*
     f0(6,6) -> 5*
     f0(5,6) -> 5*
     f0(6,5) -> 5*
     a{1,6}(16) -> 22*
     a{1,1}(5) -> 5,9
     a{1,1}(6) -> 5,8
     a{2,7}(14,22) -> 5*
     a{2,1}(13,5) -> 5*
     a{2,1}(8,5) -> 5*
     a{2,1}(5,5) -> 5*
     a{2,1}(6,6) -> 5*
     a{2,1}(13,6) -> 5*
     a{2,1}(8,6) -> 5*
     a{2,1}(5,6) -> 5*
     a{2,1}(6,5) -> 5*
     f7(20,23) -> 5*
     f1(5,9) -> 5*
     f1(6,8) -> 5*
     a{1,7}(20) -> 23*
     a{1,2}(5) -> 14*
     a{1,2}(6) -> 13*
     a{1,2}(8) -> 5*
     a{2,8}(15,23) -> 5*
     a{2,2}(13,9) -> 5*
     a{2,2}(8,9) -> 5*
     a{2,2}(5,9) -> 5*
     a{2,2}(6,9) -> 5*
     f8(22,24) -> 5*
     f2(5,14) -> 5*
     f2(6,13) -> 5*
     a{1,8}(22) -> 24*
     a{1,3}(9) -> 15*
     a{1,3}(13) -> 5*
     a{2,9}(16,24) -> 5*
     a{2,3}(6,14) -> 5*
     a{2,3}(13,14) -> 5*
     a{2,3}(8,14) -> 5*
     a{2,3}(5,14) -> 5*
   problem:
    
   Qed