YES

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

Proof:
 DP Processor:
  DPs:
   f#(x,f(y,a())) -> f#(a(),a())
   f#(x,f(y,a())) -> f#(f(a(),a()),y)
   f#(x,f(y,a())) -> f#(f(f(a(),a()),y),h(a()))
   f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
  TRS:
   f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
  EDG Processor:
   DPs:
    f#(x,f(y,a())) -> f#(a(),a())
    f#(x,f(y,a())) -> f#(f(a(),a()),y)
    f#(x,f(y,a())) -> f#(f(f(a(),a()),y),h(a()))
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
   TRS:
    f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
   graph:
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x) ->
    f#(x,f(y,a())) -> f#(a(),a())
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x) ->
    f#(x,f(y,a())) -> f#(f(a(),a()),y)
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x) ->
    f#(x,f(y,a())) -> f#(f(f(a(),a()),y),h(a()))
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x) ->
    f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
    f#(x,f(y,a())) -> f#(f(a(),a()),y) ->
    f#(x,f(y,a())) -> f#(a(),a())
    f#(x,f(y,a())) -> f#(f(a(),a()),y) ->
    f#(x,f(y,a())) -> f#(f(a(),a()),y)
    f#(x,f(y,a())) -> f#(f(a(),a()),y) ->
    f#(x,f(y,a())) -> f#(f(f(a(),a()),y),h(a()))
    f#(x,f(y,a())) -> f#(f(a(),a()),y) -> f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 8/16
    DPs:
     f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
     f#(x,f(y,a())) -> f#(f(a(),a()),y)
    TRS:
     f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
    Bounds Processor:
     bound: 2
     enrichment: match-dp
     automaton:
      final states: {16}
      transitions:
       f{#,1}(27,24) -> 16,13
       f{#,1}(24,12) -> 16,13
       f{#,1}(24,14) -> 16,13
       f{#,1}(24,11) -> 16,13
       f{#,1}(24,13) -> 16,13
       f{#,1}(36,27) -> 13,15,16
       f1(27,24) -> 26*
       f1(23,23) -> 24*
       f1(24,12) -> 26*
       f1(24,14) -> 26*
       f1(35,25) -> 36*
       f1(24,11) -> 26*
       f1(24,13) -> 26*
       f1(24,23) -> 35*
       f1(36,27) -> 26*
       f1(26,25) -> 27*
       a1() -> 23*
       h1(23) -> 25*
       f{#,2}(29,23) -> 16,13,15
       f{#,0}(13,11) -> 13*
       f{#,0}(13,13) -> 13*
       f{#,0}(14,12) -> 13*
       f{#,0}(14,14) -> 13*
       f{#,0}(11,12) -> 13*
       f{#,0}(11,14) -> 13*
       f{#,0}(12,11) -> 13*
       f{#,0}(12,13) -> 13*
       f{#,0}(17,15) -> 16*
       f{#,0}(12,17) -> 16*
       f{#,0}(13,12) -> 13*
       f{#,0}(13,14) -> 13*
       f{#,0}(14,11) -> 13*
       f{#,0}(14,13) -> 13*
       f{#,0}(11,11) -> 13*
       f{#,0}(11,13) -> 13*
       f{#,0}(12,12) -> 16,13
       f{#,0}(12,14) -> 13*
       f2(28,28) -> 29*
       f0(12,14) -> 12*
       f0(13,11) -> 12*
       f0(13,13) -> 12*
       f0(14,12) -> 12*
       f0(14,14) -> 12*
       f0(11,12) -> 12*
       f0(11,14) -> 12*
       f0(12,11) -> 12*
       f0(12,13) -> 12*
       f0(13,12) -> 12*
       f0(13,14) -> 12*
       f0(14,11) -> 12*
       f0(14,13) -> 12*
       f0(11,11) -> 17,12
       f0(11,13) -> 12*
       f0(12,12) -> 12*
       a2() -> 28*
       a0() -> 11*
       h0(12) -> 14*
       h0(14) -> 14*
       h0(11) -> 14*
       h0(13) -> 14*
       11 -> 15*
       12 -> 15*
       13 -> 15*
       14 -> 15*
     problem:
      DPs:
       f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
      TRS:
       f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
     Restore Modifier:
      DPs:
       f#(x,f(y,a())) -> f#(f(f(f(a(),a()),y),h(a())),x)
      TRS:
       f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
      Bounds Processor:
       bound: 1
       enrichment: match-dp
       automaton:
        final states: {5}
        transitions:
         f{#,1}(14,9) -> 5*
         f1(13,11) -> 14*
         f1(14,12) -> 13*
         f1(20,11) -> 21*
         f1(21,14) -> 13*
         f1(12,1) -> 13*
         f1(12,3) -> 13*
         f1(10,10) -> 12*
         f1(12,2) -> 13*
         f1(12,10) -> 20*
         a1() -> 10*
         h1(10) -> 11*
         f{#,0}(9,4) -> 5*
         f0(3,1) -> 3*
         f0(3,3) -> 8,3
         f0(3,7) -> 8*
         f0(1,2) -> 3*
         f0(2,1) -> 3*
         f0(2,3) -> 3*
         f0(3,2) -> 3*
         f0(8,6) -> 9*
         f0(1,1) -> 3*
         f0(1,3) -> 3*
         f0(2,2) -> 7,3
         f0(7,4) -> 8*
         a0() -> 2*
         h0(2) -> 6,1
         h0(1) -> 1*
         h0(3) -> 1*
         1 -> 4*
         2 -> 4*
         3 -> 4*
       problem:
        DPs:
         
        TRS:
         f(x,f(y,a())) -> f(f(f(f(a(),a()),y),h(a())),x)
       Qed