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