YES

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

Proof:
 Extended Uncurrying Processor:
  application symbol: f
  symbol table:
   a ==> a0/0 a1/1 a2/2
   
  uncurry-rules:
   f(a1(x2),x3) -> a2(x2,x3)
   f(a0(),x2) -> a1(x2)
  eta-rules:
   f(f(a(),f(a(),x)),x1) -> f(f(x,f(a(),f(f(a(),a()),a()))),x1)
  problem:
   a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
   a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
   f(a1(x2),x3) -> a2(x2,x3)
   f(a0(),x2) -> a1(x2)
  DP Processor:
   DPs:
    a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
    a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
    a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
    a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
    a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
    a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
    a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
    f#(a1(x2),x3) -> a{2,#}(x2,x3)
    f#(a0(),x2) -> a{1,#}(x2)
   TRS:
    a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
    a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
    f(a1(x2),x3) -> a2(x2,x3)
    f(a0(),x2) -> a1(x2)
   TDG Processor:
    DPs:
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
     a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
     f#(a1(x2),x3) -> a{2,#}(x2,x3)
     f#(a0(),x2) -> a{1,#}(x2)
    TRS:
     a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
     a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
     f(a1(x2),x3) -> a2(x2,x3)
     f(a0(),x2) -> a1(x2)
    graph:
     f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
     f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
     f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
     f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
     f#(a0(),x2) -> a{1,#}(x2) -> a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
     f#(a0(),x2) -> a{1,#}(x2) -> a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
     f#(a0(),x2) -> a{1,#}(x2) ->
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1) ->
     f#(a0(),x2) -> a{1,#}(x2)
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1) ->
     f#(a1(x2),x3) -> a{2,#}(x2,x3)
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0()))) ->
     f#(a0(),x2) -> a{1,#}(x2)
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0()))) ->
     f#(a1(x2),x3) -> a{2,#}(x2,x3)
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0())) ->
     a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0())) ->
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0())) ->
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
     a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0()))) ->
     f#(a0(),x2) -> a{1,#}(x2)
     a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0()))) ->
     f#(a1(x2),x3) -> a{2,#}(x2,x3)
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
     a{1,#}(a1(x)) -> a{2,#}(a0(),a0()) ->
     a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0())) ->
     a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0())) ->
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
     a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0())) -> a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
    EDG Processor:
     DPs:
      a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
      a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
      a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
      a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
      a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
      a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
      a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
      f#(a1(x2),x3) -> a{2,#}(x2,x3)
      f#(a0(),x2) -> a{1,#}(x2)
     TRS:
      a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
      a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
      f(a1(x2),x3) -> a2(x2,x3)
      f(a0(),x2) -> a1(x2)
     graph:
      f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
      a{2,#}(a1(x),x1) -> a{2,#}(a0(),a0())
      f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
      a{2,#}(a1(x),x1) -> a{1,#}(a2(a0(),a0()))
      f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
      a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
      f#(a1(x2),x3) -> a{2,#}(x2,x3) ->
      a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
      f#(a0(),x2) -> a{1,#}(x2) -> a{1,#}(a1(x)) -> a{2,#}(a0(),a0())
      f#(a0(),x2) -> a{1,#}(x2) -> a{1,#}(a1(x)) -> a{1,#}(a2(a0(),a0()))
      f#(a0(),x2) -> a{1,#}(x2) ->
      a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
      a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1) ->
      f#(a1(x2),x3) -> a{2,#}(x2,x3)
      a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0()))) ->
      f#(a1(x2),x3) -> a{2,#}(x2,x3)
      a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0()))) ->
      f#(a0(),x2) -> a{1,#}(x2)
      a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0()))) ->
      f#(a1(x2),x3) -> a{2,#}(x2,x3)
      a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0()))) -> f#(a0(),x2) -> a{1,#}(x2)
     SCC Processor:
      #sccs: 1
      #rules: 5
      #arcs: 12/81
      DPs:
       f#(a1(x2),x3) -> a{2,#}(x2,x3)
       a{2,#}(a1(x),x1) -> f#(f(x,a1(a2(a0(),a0()))),x1)
       a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
       f#(a0(),x2) -> a{1,#}(x2)
       a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
      TRS:
       a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
       a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
       f(a1(x2),x3) -> a2(x2,x3)
       f(a0(),x2) -> a1(x2)
      Bounds Processor:
       bound: 1
       enrichment: match-dp
       automaton:
        final states: {3}
        transitions:
         f0(8,7) -> 8*
         f0(4,7) -> 8*
         f0(6,7) -> 8*
         a{1,0}(7) -> 8*
         a{1,0}(6) -> 7*
         a{2,0}(5,5) -> 6*
         a{2,0}(7,7) -> 8*
         a{2,0}(4,7) -> 8*
         a{0,0}() -> 5*
         f{#,1}(34,4) -> 3*
         a{1,1}(32) -> 33*
         a{2,1}(31,31) -> 32*
         a{0,1}() -> 31*
         f1(6,33) -> 34*
         f80() -> 4*
         a{2,#,0}(7,4) -> 3*
         f{#,0}(8,4) -> 3*
         f{#,0}(6,7) -> 3*
       problem:
        DPs:
         f#(a1(x2),x3) -> a{2,#}(x2,x3)
         a{2,#}(a1(x),x1) -> f#(x,a1(a2(a0(),a0())))
         f#(a0(),x2) -> a{1,#}(x2)
         a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
        TRS:
         a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
         a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
         f(a1(x2),x3) -> a2(x2,x3)
         f(a0(),x2) -> a1(x2)
       Bounds Processor:
        bound: 0
        enrichment: match-dp
        automaton:
         final states: {3}
         transitions:
          a{2,#,0}(7,6) -> 3*
          f{#,0}(5,6) -> 3*
          f{#,0}(7,6) -> 3*
          a{1,0}(5) -> 6*
          f230() -> 7*
          a{2,0}(4,4) -> 5*
          a{0,0}() -> 4*
          a{1,#,0}(6) -> 3*
        problem:
         DPs:
          f#(a1(x2),x3) -> a{2,#}(x2,x3)
          f#(a0(),x2) -> a{1,#}(x2)
          a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
         TRS:
          a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
          a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
          f(a1(x2),x3) -> a2(x2,x3)
          f(a0(),x2) -> a1(x2)
        SCC Processor:
         #sccs: 1
         #rules: 2
         #arcs: 8/9
         DPs:
          f#(a0(),x2) -> a{1,#}(x2)
          a{1,#}(a1(x)) -> f#(x,a1(a2(a0(),a0())))
         TRS:
          a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
          a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
          f(a1(x2),x3) -> a2(x2,x3)
          f(a0(),x2) -> a1(x2)
         Bounds Processor:
          bound: 1
          enrichment: match-dp
          automaton:
           final states: {3}
           transitions:
            a{0,1}() -> 11*
            f{#,0}(7,6) -> 3*
            a{1,0}(5) -> 6*
            a{2,0}(4,4) -> 5*
            a{0,0}() -> 4*
            a{1,#,0}(6) -> 3*
            f250() -> 7*
            f{#,1}(5,13) -> 3*
            a{1,1}(12) -> 13*
            a{2,1}(11,11) -> 12*
          problem:
           DPs:
            f#(a0(),x2) -> a{1,#}(x2)
           TRS:
            a1(a1(x)) -> f(x,a1(a2(a0(),a0())))
            a2(a1(x),x1) -> f(f(x,a1(a2(a0(),a0()))),x1)
            f(a1(x2),x3) -> a2(x2,x3)
            f(a0(),x2) -> a1(x2)
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 2/1