YES
Time: 0.004978
TRS:
 {f(g(x, y), f(y, y)) -> f(g(y, x), y)}
 BOUND:
  Bound: match(-raise)-bounded by 2
  Automaton:
   {g_2(5, 5) -> 5* | 4 | 3 | 2 | 1
    g_2(5, 3) -> 5* | 4 | 3 | 2 | 1
    g_2(5, 1) -> 5* | 4 | 3 | 2 | 1
    g_2(3, 5) -> 5* | 4 | 3 | 2 | 1
    g_2(3, 3) -> 5* | 4 | 3 | 2 | 1
    g_2(3, 1) -> 5* | 4 | 3 | 2 | 1
    g_1(5, 5) -> 3* | 2 | 1
    g_1(5, 3) -> 3* | 2 | 1
    g_1(5, 1) -> 3* | 2 | 1
    g_1(3, 5) -> 3* | 2 | 1
    g_1(3, 3) -> 3* | 2 | 1
    g_1(3, 1) -> 3* | 2 | 1
    g_1(1, 5) -> 3* | 2 | 1
    g_1(1, 3) -> 3* | 2 | 1
    g_1(1, 1) -> 3* | 2 | 1
    g_0(5, 5) -> 1*
    g_0(5, 3) -> 1*
    g_0(5, 1) -> 1*
    g_0(3, 5) -> 1*
    g_0(3, 3) -> 1*
    g_0(3, 1) -> 1*
    g_0(1, 5) -> 1*
    g_0(1, 3) -> 1*
    g_0(1, 1) -> 1*
    f_2(5, 5) -> 1*
    f_2(5, 3) -> 1*
    f_2(4, 5) -> 1*
    f_2(4, 3) -> 1*
    f_1(5, 5) -> 1*
    f_1(5, 3) -> 1*
    f_1(5, 1) -> 1*
    f_1(3, 5) -> 1*
    f_1(3, 3) -> 1*
    f_1(3, 1) -> 1*
    f_1(2, 5) -> 1*
    f_1(2, 3) -> 1*
    f_1(2, 1) -> 1*
    f_0(5, 5) -> 1*
    f_0(5, 3) -> 1*
    f_0(5, 1) -> 1*
    f_0(3, 5) -> 1*
    f_0(3, 3) -> 1*
    f_0(3, 1) -> 1*
    f_0(1, 5) -> 1*
    f_0(1, 3) -> 1*
    f_0(1, 1) -> 1*}
  Strict:
   {}
  Qed