YES
TRS:
 {f(c(c(z, a(), a()), x, a())) -> z,
               b(y, b(z, a())) -> f(b(c(f(a()), y, z), z)),
                  c(z, x, a()) -> f(b(b(f(z), z), x))}
 DP:
  Strict:
   {b#(y, b(z, a())) -> f#(b(c(f(a()), y, z), z)),
    b#(y, b(z, a())) -> f#(a()),
    b#(y, b(z, a())) -> b#(c(f(a()), y, z), z),
    b#(y, b(z, a())) -> c#(f(a()), y, z),
       c#(z, x, a()) -> f#(z),
       c#(z, x, a()) -> f#(b(b(f(z), z), x)),
       c#(z, x, a()) -> b#(f(z), z),
       c#(z, x, a()) -> b#(b(f(z), z), x)}
  Weak:
  {f(c(c(z, a(), a()), x, a())) -> z,
                b(y, b(z, a())) -> f(b(c(f(a()), y, z), z)),
                   c(z, x, a()) -> f(b(b(f(z), z), x))}
  EDG:
   {(c#(z, x, a()) -> b#(f(z), z), b#(y, b(z, a())) -> c#(f(a()), y, z))
    (c#(z, x, a()) -> b#(f(z), z), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))
    (c#(z, x, a()) -> b#(f(z), z), b#(y, b(z, a())) -> f#(a()))
    (c#(z, x, a()) -> b#(f(z), z), b#(y, b(z, a())) -> f#(b(c(f(a()), y, z), z)))
    (c#(z, x, a()) -> b#(b(f(z), z), x), b#(y, b(z, a())) -> c#(f(a()), y, z))
    (c#(z, x, a()) -> b#(b(f(z), z), x), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))
    (c#(z, x, a()) -> b#(b(f(z), z), x), b#(y, b(z, a())) -> f#(a()))
    (c#(z, x, a()) -> b#(b(f(z), z), x), b#(y, b(z, a())) -> f#(b(c(f(a()), y, z), z)))
    (b#(y, b(z, a())) -> c#(f(a()), y, z), c#(z, x, a()) -> f#(z))
    (b#(y, b(z, a())) -> c#(f(a()), y, z), c#(z, x, a()) -> f#(b(b(f(z), z), x)))
    (b#(y, b(z, a())) -> c#(f(a()), y, z), c#(z, x, a()) -> b#(f(z), z))
    (b#(y, b(z, a())) -> c#(f(a()), y, z), c#(z, x, a()) -> b#(b(f(z), z), x))
    (b#(y, b(z, a())) -> b#(c(f(a()), y, z), z), b#(y, b(z, a())) -> f#(b(c(f(a()), y, z), z)))
    (b#(y, b(z, a())) -> b#(c(f(a()), y, z), z), b#(y, b(z, a())) -> f#(a()))
    (b#(y, b(z, a())) -> b#(c(f(a()), y, z), z), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))
    (b#(y, b(z, a())) -> b#(c(f(a()), y, z), z), b#(y, b(z, a())) -> c#(f(a()), y, z))}
   SCCS:
    Scc:
     {b#(y, b(z, a())) -> b#(c(f(a()), y, z), z),
      b#(y, b(z, a())) -> c#(f(a()), y, z),
         c#(z, x, a()) -> b#(f(z), z),
         c#(z, x, a()) -> b#(b(f(z), z), x)}
    SCC:
     Strict:
      {b#(y, b(z, a())) -> b#(c(f(a()), y, z), z),
       b#(y, b(z, a())) -> c#(f(a()), y, z),
          c#(z, x, a()) -> b#(f(z), z),
          c#(z, x, a()) -> b#(b(f(z), z), x)}
     Weak:
     {f(c(c(z, a(), a()), x, a())) -> z,
                   b(y, b(z, a())) -> f(b(c(f(a()), y, z), z)),
                      c(z, x, a()) -> f(b(b(f(z), z), x))}
     UR:
      {f(c(c(z, a(), a()), x, a())) -> z,
                    b(y, b(z, a())) -> f(b(c(f(a()), y, z), z)),
                       c(z, x, a()) -> f(b(b(f(z), z), x)),
                            d(w, v) -> w,
                            d(w, v) -> v}
      BOUND:
       Bound: top(-raise)-DP-bounded by 2
       Automaton:
        {      d_0(6, 6) -> 5*
               d_0(6, 5) -> 5*
               d_0(5, 6) -> 5*
               d_0(5, 5) -> 5*
                   a_2() -> 11*
                   a_1() -> 7*
                   a_0() -> 5*
         c#_2(12, 15, 6) -> 3*
         c#_2(12, 15, 5) -> 3*
         c#_2(12, 10, 6) -> 3*
         c#_2(12, 10, 5) -> 3*
           c#_1(8, 6, 6) -> 3*
           c#_1(8, 6, 5) -> 3*
           c#_1(8, 5, 6) -> 3*
           c#_1(8, 5, 5) -> 3*
           c#_0(6, 6, 6) -> 3*
           c#_0(6, 6, 5) -> 3*
           c#_0(6, 5, 6) -> 3*
           c#_0(6, 5, 5) -> 3*
           c_1(8, 15, 6) -> 15*
           c_1(8, 15, 5) -> 15*
           c_1(8, 10, 6) -> 15*
           c_1(8, 10, 5) -> 10*
            c_0(6, 6, 6) -> 5*
            c_0(6, 6, 5) -> 5*
            c_0(6, 5, 6) -> 5*
            c_0(6, 5, 5) -> 5*
            c_0(5, 6, 6) -> 5*
            c_0(5, 6, 5) -> 5*
            c_0(5, 5, 6) -> 5*
            c_0(5, 5, 5) -> 5*
            b#_2(14, 15) -> 3*
            b#_2(14, 10) -> 3*
            b#_2(13, 12) -> 3*
             b#_1(15, 6) -> 3*
             b#_1(10, 6) -> 3*
             b#_1(10, 5) -> 3*
              b#_1(9, 8) -> 3*
              b#_0(6, 6) -> 3*
              b#_0(5, 6) -> 3*
              b#_0(5, 5) -> 3*
             b_2(13, 12) -> 14*
             b_1(10, 15) -> 16*
             b_1(10, 10) -> 16*
               b_1(9, 8) -> 10*
               b_0(6, 6) -> 5*
               b_0(6, 5) -> 5*
               b_0(5, 6) -> 5*
               b_0(5, 5) -> 5*
                 f_2(12) -> 13*
                 f_2(11) -> 12*
                 f_1(16) -> 15 | 10
                  f_1(8) -> 9*
                  f_1(7) -> 8*
                  f_0(6) -> 6*
                  f_0(5) -> 6*
                       6 -> 5*
                       5 -> 6*}
       Strict:
        {b#(y, b(z, a())) -> b#(c(f(a()), y, z), z),
            c#(z, x, a()) -> b#(f(z), z),
            c#(z, x, a()) -> b#(b(f(z), z), x)}
       EDG:
        {(b#(y, b(z, a())) -> b#(c(f(a()), y, z), z), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))
         (c#(z, x, a()) -> b#(f(z), z), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))
         (c#(z, x, a()) -> b#(b(f(z), z), x), b#(y, b(z, a())) -> b#(c(f(a()), y, z), z))}
        SCCS:
         Scc:
          {b#(y, b(z, a())) -> b#(c(f(a()), y, z), z)}
         SCC:
          Strict:
           {b#(y, b(z, a())) -> b#(c(f(a()), y, z), z)}
          Weak:
          {f(c(c(z, a(), a()), x, a())) -> z,
                        b(y, b(z, a())) -> f(b(c(f(a()), y, z), z)),
                           c(z, x, a()) -> f(b(b(f(z), z), x))}
          SPSC:
           Simple Projection:
            pi(b#) = 1
           Strict:
            {}
           Qed