YES
TRS:
 {f(f(f(c(z, x, a())))) -> b(f(x), z),
           f(b(a(), z)) -> z,
        b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
 DP:
  Strict:
   {f#(f(f(c(z, x, a())))) -> f#(x),
    f#(f(f(c(z, x, a())))) -> b#(f(x), z),
          b#(y, b(a(), z)) -> f#(z),
          b#(y, b(a(), z)) -> f#(c(y, y, a())),
          b#(y, b(a(), z)) -> b#(f(z), a()),
          b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
  Weak:
  {f(f(f(c(z, x, a())))) -> b(f(x), z),
            f(b(a(), z)) -> z,
         b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
  EDG:
   {(f#(f(f(c(z, x, a())))) -> f#(x), f#(f(f(c(z, x, a())))) -> b#(f(x), z))
    (f#(f(f(c(z, x, a())))) -> f#(x), f#(f(f(c(z, x, a())))) -> f#(x))
    (b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())), b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())))
    (b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())), b#(y, b(a(), z)) -> b#(f(z), a()))
    (b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())), b#(y, b(a(), z)) -> f#(c(y, y, a())))
    (b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())), b#(y, b(a(), z)) -> f#(z))
    (f#(f(f(c(z, x, a())))) -> b#(f(x), z), b#(y, b(a(), z)) -> f#(z))
    (f#(f(f(c(z, x, a())))) -> b#(f(x), z), b#(y, b(a(), z)) -> f#(c(y, y, a())))
    (f#(f(f(c(z, x, a())))) -> b#(f(x), z), b#(y, b(a(), z)) -> b#(f(z), a()))
    (f#(f(f(c(z, x, a())))) -> b#(f(x), z), b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())))
    (b#(y, b(a(), z)) -> f#(z), f#(f(f(c(z, x, a())))) -> f#(x))
    (b#(y, b(a(), z)) -> f#(z), f#(f(f(c(z, x, a())))) -> b#(f(x), z))}
   SCCS:
    Scc:
     {f#(f(f(c(z, x, a())))) -> f#(x),
      f#(f(f(c(z, x, a())))) -> b#(f(x), z),
            b#(y, b(a(), z)) -> f#(z),
            b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
    SCC:
     Strict:
      {f#(f(f(c(z, x, a())))) -> f#(x),
       f#(f(f(c(z, x, a())))) -> b#(f(x), z),
             b#(y, b(a(), z)) -> f#(z),
             b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
     Weak:
     {f(f(f(c(z, x, a())))) -> b(f(x), z),
               f(b(a(), z)) -> z,
            b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
     POLY:
      Argument Filtering:
       pi(c) = [0,1], pi(a) = [], pi(b#) = 1, pi(b) = [1], pi(f#) = 0, pi(f) = 0
      Usable Rules:
       {}
      Interpretation:
       [c](x0, x1) = x0 + x1,
       [b](x0) = x0 + 1,
       [a] = 0
      Strict:
       {f#(f(f(c(z, x, a())))) -> f#(x),
        f#(f(f(c(z, x, a())))) -> b#(f(x), z),
              b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
      Weak:
       {f(f(f(c(z, x, a())))) -> b(f(x), z),
                 f(b(a(), z)) -> z,
              b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
      EDG:
       {(f#(f(f(c(z, x, a())))) -> b#(f(x), z), b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())))
        (b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())), b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a())))
        (f#(f(f(c(z, x, a())))) -> f#(x), f#(f(f(c(z, x, a())))) -> f#(x))
        (f#(f(f(c(z, x, a())))) -> f#(x), f#(f(f(c(z, x, a())))) -> b#(f(x), z))}
       SCCS:
        Scc:
         {b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
        Scc:
         {f#(f(f(c(z, x, a())))) -> f#(x)}
        SCC:
         Strict:
          {b#(y, b(a(), z)) -> b#(f(c(y, y, a())), b(f(z), a()))}
         Weak:
         {f(f(f(c(z, x, a())))) -> b(f(x), z),
                   f(b(a(), z)) -> z,
                b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
         BOUND:
          Bound: roof(-raise)-bounded by 3
          Automaton:
           {c_3(5, 5, 8) -> 9*
            c_2(2, 2, 3) -> 4*
            c_1(1, 1, 1) -> 1*
            c_0(1, 1, 1) -> 1*
                   a_3() -> 8*
                   a_2() -> 3*
                   a_1() -> 1*
                   a_0() -> 1*
            b#_3(10, 12) -> 1*
              b#_2(5, 7) -> 1*
              b#_1(2, 1) -> 1*
              b#_0(1, 1) -> 1*
              b_3(11, 8) -> 12*
             b_3(10, 12) -> 1*
               b_2(6, 3) -> 7*
               b_2(5, 7) -> 1*
               b_1(2, 1) -> 1*
               b_0(1, 1) -> 1*
                  f_3(9) -> 10*
                  f_3(3) -> 11*
                  f_2(4) -> 5*
                  f_2(1) -> 6*
                  f_1(1) -> 2*
                  f_0(1) -> 1*
                       1 -> 6 | 2}
          Strict:
           {}
          Qed
        SCC:
         Strict:
          {f#(f(f(c(z, x, a())))) -> f#(x)}
         Weak:
         {f(f(f(c(z, x, a())))) -> b(f(x), z),
                   f(b(a(), z)) -> z,
                b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed