YES
TRS:
 {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
 DP:
  Strict:
   {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(a(), a()), y),
    f#(x, f(y, a())) -> f#(a(), a())}
  Weak:
  {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
  EDG:
   {(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))
    (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(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(a(), a()), y))
    (f#(x, f(y, a())) -> f#(f(f(f(a(), a()), y), h(a())), x), f#(x, f(y, a())) -> f#(a(), a()))}
   SCCS:
    Scc:
     {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)}
    SCC:
     Strict:
      {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)}
     Weak:
     {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
     BOUND:
      Bound: match(-raise)-DP-bounded by 1
      Automaton:
       {      b_0() -> 4*
             h_0(2) -> 6*
              a_1() -> 8*
              a_0() -> 2*
         f#_1(9, 2) -> 1*
        f#_0(11, 7) -> 1*
         f#_0(7, 3) -> 1*
         f#_0(3, 4) -> 1*
          f_1(8, 8) -> 9*
         f_0(11, 7) -> 5*
         f_0(10, 6) -> 11*
          f_0(7, 3) -> 5*
          f_0(5, 6) -> 7*
          f_0(3, 4) -> 5*
          f_0(3, 2) -> 10*
          f_0(2, 2) -> 3*}
      Strict:
       {f#(x, f(y, a())) -> f#(f(f(f(a(), a()), y), h(a())), x)}
      EDG:
       {(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))}
       SCCS:
        Scc:
         {f#(x, f(y, a())) -> f#(f(f(f(a(), a()), y), h(a())), x)}
        SCC:
         Strict:
          {f#(x, f(y, a())) -> f#(f(f(f(a(), a()), y), h(a())), x)}
         Weak:
         {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {     c_0() -> 4*
                h_0(2) -> 6*
                 a_0() -> 2*
            f#_0(7, 7) -> 1*
            f#_0(7, 4) -> 1*
             f_0(9, 7) -> 5*
             f_0(8, 6) -> 9*
             f_0(7, 3) -> 5*
             f_0(5, 6) -> 7*
             f_0(3, 4) -> 5*
             f_0(3, 2) -> 8*
             f_0(2, 2) -> 3*}
          Strict:
           {}
          Qed