YES
TRS:
 {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
  f(b(), f(b(), x)) -> f(a(), f(c(), x)),
  f(a(), f(a(), x)) -> f(c(), f(b(), x))}
 DP:
  Strict:
   {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
    f#(c(), f(c(), x)) -> f#(a(), x),
    f#(b(), f(b(), x)) -> f#(c(), x),
    f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
    f#(a(), f(a(), x)) -> f#(c(), f(b(), x)),
    f#(a(), f(a(), x)) -> f#(b(), x)}
  Weak:
  {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
   f(b(), f(b(), x)) -> f(a(), f(c(), x)),
   f(a(), f(a(), x)) -> f(c(), f(b(), x))}
  EDG:
   {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(b(), x))
    (f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)))
    (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(b(), x))
    (f#(c(), f(c(), x)) -> f#(a(), x), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)))
    (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))
    (f#(a(), f(a(), x)) -> f#(b(), x), f#(b(), f(b(), x)) -> f#(c(), x))
    (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(b(), f(a(), x)))
    (f#(b(), f(b(), x)) -> f#(c(), x), f#(c(), f(c(), x)) -> f#(a(), x))
    (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x)))
    (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(a(), x))
    (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(c(), x))
    (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))}
   SCCS:
    Scc:
     {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
      f#(c(), f(c(), x)) -> f#(a(), x),
      f#(b(), f(b(), x)) -> f#(c(), x),
      f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
      f#(a(), f(a(), x)) -> f#(c(), f(b(), x)),
      f#(a(), f(a(), x)) -> f#(b(), x)}
    SCC:
     Strict:
      {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
       f#(c(), f(c(), x)) -> f#(a(), x),
       f#(b(), f(b(), x)) -> f#(c(), x),
       f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
       f#(a(), f(a(), x)) -> f#(c(), f(b(), x)),
       f#(a(), f(a(), x)) -> f#(b(), x)}
     Weak:
     {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
      f(b(), f(b(), x)) -> f(a(), f(c(), x)),
      f(a(), f(a(), x)) -> f(c(), f(b(), x))}
     POLY:
      Argument Filtering:
       pi(a) = [], pi(b) = [], pi(c) = [], pi(f#) = 1, pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f](x0, x1) = x0 + x1 + 1,
       [a] = 1,
       [b] = 1,
       [c] = 1
      Strict:
       {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
        f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
        f#(a(), f(a(), x)) -> f#(c(), f(b(), x))}
      Weak:
       {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
        f(b(), f(b(), x)) -> f(a(), f(c(), x)),
        f(a(), f(a(), x)) -> f(c(), f(b(), x))}
      EDG:
       {(f#(b(), f(b(), x)) -> f#(a(), f(c(), x)), f#(a(), f(a(), x)) -> f#(c(), f(b(), x)))
        (f#(a(), f(a(), x)) -> f#(c(), f(b(), x)), f#(c(), f(c(), x)) -> f#(b(), f(a(), x)))
        (f#(c(), f(c(), x)) -> f#(b(), f(a(), x)), f#(b(), f(b(), x)) -> f#(a(), f(c(), x)))}
       SCCS:
        Scc:
         {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
          f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
          f#(a(), f(a(), x)) -> f#(c(), f(b(), x))}
        SCC:
         Strict:
          {f#(c(), f(c(), x)) -> f#(b(), f(a(), x)),
           f#(b(), f(b(), x)) -> f#(a(), f(c(), x)),
           f#(a(), f(a(), x)) -> f#(c(), f(b(), x))}
         Weak:
         {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
          f(b(), f(b(), x)) -> f(a(), f(c(), x)),
          f(a(), f(a(), x)) -> f(c(), f(b(), x))}
         UR:
          {f(c(), f(c(), x)) -> f(b(), f(a(), x)),
           f(b(), f(b(), x)) -> f(a(), f(c(), x)),
           f(a(), f(a(), x)) -> f(c(), f(b(), x))}
          BOUND:
           Bound: match(-raise)-bounded by 0
           Automaton:
            {      d_0() -> 4*
                   a_0() -> 7*
                   b_0() -> 3*
                   c_0() -> 2*
             f#_0(7, 10) -> 13*
              f#_0(3, 8) -> 12*
              f#_0(2, 5) -> 11*
              f_0(7, 10) -> 9*
               f_0(7, 4) -> 8*
               f_0(3, 8) -> 6*
               f_0(3, 4) -> 5*
               f_0(2, 5) -> 1*
               f_0(2, 4) -> 10*
                       9 -> 5*
                       6 -> 10*
                       1 -> 8*}
           Strict:
            {}
           Qed