YES

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

Proof:
 Uncurry Processor:
  a2(a(),x) -> f(f(x,a1(a1(a()))),a())
  f(a1(x1),x2) -> a2(x1,x2)
  f(a(),x2) -> a1(x2)
  DP Processor:
   DPs:
    a{2,#}(a(),x) -> f#(x,a1(a1(a())))
    a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a())
    f#(a1(x1),x2) -> a{2,#}(x1,x2)
   TRS:
    a2(a(),x) -> f(f(x,a1(a1(a()))),a())
    f(a1(x1),x2) -> a2(x1,x2)
    f(a(),x2) -> a1(x2)
   TDG Processor:
    DPs:
     a{2,#}(a(),x) -> f#(x,a1(a1(a())))
     a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a())
     f#(a1(x1),x2) -> a{2,#}(x1,x2)
    TRS:
     a2(a(),x) -> f(f(x,a1(a1(a()))),a())
     f(a1(x1),x2) -> a2(x1,x2)
     f(a(),x2) -> a1(x2)
    graph:
     f#(a1(x1),x2) -> a{2,#}(x1,x2) ->
     a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a())
     f#(a1(x1),x2) -> a{2,#}(x1,x2) ->
     a{2,#}(a(),x) -> f#(x,a1(a1(a())))
     a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a()) ->
     f#(a1(x1),x2) -> a{2,#}(x1,x2)
     a{2,#}(a(),x) -> f#(x,a1(a1(a()))) -> f#(a1(x1),x2) -> a{2,#}(x1,x2)
    CDG Processor:
     DPs:
      a{2,#}(a(),x) -> f#(x,a1(a1(a())))
      a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a())
      f#(a1(x1),x2) -> a{2,#}(x1,x2)
     TRS:
      a2(a(),x) -> f(f(x,a1(a1(a()))),a())
      f(a1(x1),x2) -> a2(x1,x2)
      f(a(),x2) -> a1(x2)
     graph:
      a{2,#}(a(),x) -> f#(f(x,a1(a1(a()))),a()) ->
      f#(a1(x1),x2) -> a{2,#}(x1,x2)
      a{2,#}(a(),x) -> f#(x,a1(a1(a()))) -> f#(a1(x1),x2) -> a{2,#}(x1,x2)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/9