YES
Time: 0.412385
TRS:
 {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
  a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
 DP:
  DP:
   {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
    a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
    a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
    a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
  TRS:
  {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
   a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
  EDG:
   {(a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
    (a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
    (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))
    (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))))
    (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))))
    (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))
    (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))))
    (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))}
   SCCS (1):
    Scc:
     {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
      a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
      a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
      a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
    SCC (4):
     Strict:
      {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))),
       a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))),
       a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))),
       a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))}
     Weak:
     {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))),
      a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))}
     BOUND:
      Bound: match(-raise)-bounded by 4
      Automaton:
       {       g_4() -> 41*
               g_3() -> 30*
               g_2() -> 11*
               g_1() -> 3*
               g_0() -> 1*
               f_4() -> 40*
               f_3() -> 29*
               f_2() -> 10*
               f_1() -> 2*
               f_0() -> 1*
        a#_2(11, 27) -> 1*
        a#_2(11, 24) -> 1*
        a#_2(11, 23) -> 1*
        a#_2(11, 20) -> 1*
        a#_2(11, 16) -> 1*
        a#_2(11, 13) -> 1*
         a#_2(11, 4) -> 1*
        a#_2(10, 28) -> 1*
        a#_2(10, 25) -> 1*
        a#_2(10, 22) -> 1*
        a#_2(10, 19) -> 1*
        a#_2(10, 17) -> 1*
        a#_2(10, 14) -> 1*
         a#_2(10, 1) -> 1*
          a#_1(3, 9) -> 1*
          a#_1(3, 7) -> 1*
          a#_1(3, 4) -> 1*
          a#_1(3, 1) -> 1*
          a#_1(2, 8) -> 1*
          a#_1(2, 6) -> 1*
          a#_1(2, 5) -> 1*
          a#_1(2, 4) -> 1*
          a#_1(2, 1) -> 1*
          a#_0(1, 1) -> 1*
         a_4(41, 43) -> 44*
         a_4(41, 42) -> 43*
         a_4(40, 44) -> 35*
         a_4(40, 38) -> 42*
         a_4(40, 28) -> 42*
         a_4(40, 25) -> 42*
         a_4(40, 22) -> 42*
         a_4(40, 19) -> 42*
         a_4(40, 17) -> 42*
         a_4(40, 14) -> 42*
         a_3(30, 39) -> 24*
         a_3(30, 36) -> 27*
         a_3(30, 32) -> 33*
         a_3(30, 31) -> 34 | 32 | 27
         a_3(30, 27) -> 37*
         a_3(30, 24) -> 37*
         a_3(30, 23) -> 34*
         a_3(30, 20) -> 34*
         a_3(30, 16) -> 37*
         a_3(30, 13) -> 37*
          a_3(30, 6) -> 34*
          a_3(30, 4) -> 37*
          a_3(30, 1) -> 34*
         a_3(29, 38) -> 39*
         a_3(29, 37) -> 38 | 25
         a_3(29, 35) -> 36*
         a_3(29, 34) -> 35*
         a_3(29, 33) -> 35 | 25
         a_3(29, 28) -> 31*
         a_3(29, 25) -> 31*
         a_3(29, 24) -> 35*
         a_3(29, 22) -> 31*
         a_3(29, 19) -> 31*
         a_3(29, 17) -> 31*
         a_3(29, 14) -> 31*
         a_2(11, 27) -> 28*
         a_2(11, 26) -> 27*
         a_2(11, 25) -> 27*
         a_2(11, 24) -> 28*
         a_2(11, 23) -> 27 | 24 | 7 | 4
         a_2(11, 20) -> 27 | 24 | 16 | 7 | 4
         a_2(11, 16) -> 17*
         a_2(11, 15) -> 16*
         a_2(11, 13) -> 14*
         a_2(11, 12) -> 13*
          a_2(11, 9) -> 21*
          a_2(11, 7) -> 18*
          a_2(11, 6) -> 24*
          a_2(11, 4) -> 28*
          a_2(11, 1) -> 24*
         a_2(10, 28) -> 35 | 26 | 25 | 22 | 6 | 5 | 1
         a_2(10, 25) -> 20*
         a_2(10, 24) -> 25*
         a_2(10, 22) -> 23*
         a_2(10, 21) -> 22*
         a_2(10, 19) -> 20*
         a_2(10, 18) -> 19*
         a_2(10, 17) -> 35 | 25 | 5 | 1
         a_2(10, 14) -> 26 | 25 | 22 | 6 | 5 | 1
          a_2(10, 8) -> 15*
          a_2(10, 6) -> 26*
          a_2(10, 5) -> 12*
          a_2(10, 4) -> 25*
          a_2(10, 1) -> 26*
           a_1(3, 9) -> 4 | 1
           a_1(3, 7) -> 8*
           a_1(3, 6) -> 7 | 4
           a_1(3, 4) -> 8*
           a_1(3, 1) -> 4*
           a_1(2, 8) -> 35 | 26 | 25 | 6 | 5 | 1
           a_1(2, 6) -> 9*
           a_1(2, 5) -> 9*
           a_1(2, 4) -> 5 | 1
           a_1(2, 1) -> 6*
           a_0(1, 1) -> 1*}
      Strict:
       {}
      Qed