YES
Time: 0.005368
TRS:
 {f(x, x) -> f(a(), b()),
      b() -> c()}
 DP:
  DP:
   {f#(x, x) -> f#(a(), b()),
    f#(x, x) -> b#()}
  TRS:
  {f(x, x) -> f(a(), b()),
       b() -> c()}
  EDG:
   {(f#(x, x) -> f#(a(), b()), f#(x, x) -> f#(a(), b()))
    (f#(x, x) -> f#(a(), b()), f#(x, x) -> b#())}
   SCCS (1):
    Scc:
     {f#(x, x) -> f#(a(), b())}
    SCC (1):
     Strict:
      {f#(x, x) -> f#(a(), b())}
     Weak:
     {f(x, x) -> f(a(), b()),
          b() -> c()}
     BOUND:
      Bound: match(-raise)-bounded by 2
      Automaton:
       {     c_2() -> 6* | 4 | 1
             b_1() -> 4* | 3 | 1
             a_1() -> 5* | 2 | 1
        f#_1(5, 6) -> 1*
        f#_1(5, 4) -> 1*
        f#_1(5, 3) -> 1*
        f#_1(2, 6) -> 1*
        f#_1(2, 4) -> 1*
        f#_1(2, 3) -> 1*
        f#_0(6, 6) -> 1*
        f#_0(6, 5) -> 1*
        f#_0(6, 4) -> 1*
        f#_0(6, 1) -> 1*
        f#_0(5, 5) -> 1*
        f#_0(5, 1) -> 1*
        f#_0(4, 6) -> 1*
        f#_0(4, 5) -> 1*
        f#_0(4, 4) -> 1*
        f#_0(4, 1) -> 1*
        f#_0(1, 6) -> 1*
        f#_0(1, 5) -> 1*
        f#_0(1, 4) -> 1*
        f#_0(1, 1) -> 1*
         f_1(5, 6) -> 1*
         f_1(5, 4) -> 1*
         f_1(5, 3) -> 1*
         f_1(2, 6) -> 1*
         f_1(2, 4) -> 1*
         f_1(2, 3) -> 1*
         f_0(6, 6) -> 1*
         f_0(6, 5) -> 1*
         f_0(6, 4) -> 1*
         f_0(6, 1) -> 1*
         f_0(5, 5) -> 1*
         f_0(5, 1) -> 1*
         f_0(4, 6) -> 1*
         f_0(4, 5) -> 1*
         f_0(4, 4) -> 1*
         f_0(4, 1) -> 1*
         f_0(1, 6) -> 1*
         f_0(1, 5) -> 1*
         f_0(1, 4) -> 1*
         f_0(1, 1) -> 1*}
      Strict:
       {}
      Qed