YES
TRS:
 {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
        f(b(x), y) -> f(x, b(y)),
        f(c(x), y) -> f(x, c(y)),
        f(a(x), y) -> f(x, a(y))}
 DP:
  Strict:
   {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
          f#(b(x), y) -> f#(x, b(y)),
          f#(c(x), y) -> f#(x, c(y)),
          f#(a(x), y) -> f#(x, a(y))}
  Weak:
  {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
         f(b(x), y) -> f(x, b(y)),
         f(c(x), y) -> f(x, c(y)),
         f(a(x), y) -> f(x, a(y))}
  EDG:
   {(f#(b(x), y) -> f#(x, b(y)), f#(a(x), y) -> f#(x, a(y)))
    (f#(b(x), y) -> f#(x, b(y)), f#(c(x), y) -> f#(x, c(y)))
    (f#(b(x), y) -> f#(x, b(y)), f#(b(x), y) -> f#(x, b(y)))
    (f#(a(x), y) -> f#(x, a(y)), f#(a(x), y) -> f#(x, a(y)))
    (f#(a(x), y) -> f#(x, a(y)), f#(c(x), y) -> f#(x, c(y)))
    (f#(a(x), y) -> f#(x, a(y)), f#(b(x), y) -> f#(x, b(y)))
    (f#(a(x), y) -> f#(x, a(y)), f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y))
    (f#(c(x), y) -> f#(x, c(y)), f#(b(x), y) -> f#(x, b(y)))
    (f#(c(x), y) -> f#(x, c(y)), f#(c(x), y) -> f#(x, c(y)))
    (f#(c(x), y) -> f#(x, c(y)), f#(a(x), y) -> f#(x, a(y)))
    (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y))
    (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(b(x), y) -> f#(x, b(y)))}
   SCCS:
    Scc:
     {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
            f#(b(x), y) -> f#(x, b(y)),
            f#(c(x), y) -> f#(x, c(y)),
            f#(a(x), y) -> f#(x, a(y))}
    SCC:
     Strict:
      {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
             f#(b(x), y) -> f#(x, b(y)),
             f#(c(x), y) -> f#(x, c(y)),
             f#(a(x), y) -> f#(x, a(y))}
     Weak:
     {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
            f(b(x), y) -> f(x, b(y)),
            f(c(x), y) -> f(x, c(y)),
            f(a(x), y) -> f(x, a(y))}
     UR:
      {}
      BOUND:
       Bound: match(-raise)-DP-bounded by 2
       Automaton:
        {     a_2(16) -> 17*
              a_1(18) -> 11*
              a_1(15) -> 13*
              a_1(12) -> 13*
              a_1(11) -> 11*
              a_0(10) -> 9*
               a_0(9) -> 9*
               a_0(7) -> 9*
              c_2(18) -> 16*
              c_2(12) -> 16*
              c_2(11) -> 16*
              c_1(18) -> 11*
              c_1(13) -> 14*
              c_1(11) -> 11*
              c_1(10) -> 11*
               c_1(9) -> 11*
               c_1(7) -> 11*
              c_0(10) -> 10*
               c_0(9) -> 10*
               c_0(7) -> 10*
              b_2(18) -> 18*
              b_2(17) -> 18*
              b_1(18) -> 11*
              b_1(15) -> 12*
              b_1(14) -> 15*
              b_1(11) -> 11*
              b_1(10) -> 12*
               b_1(9) -> 12*
               b_1(7) -> 12*
              b_0(10) -> 7*
               b_0(9) -> 7*
               b_0(7) -> 7*
         f#_2(15, 18) -> 5*
         f#_2(15, 17) -> 5*
         f#_2(14, 18) -> 5*
         f#_2(13, 16) -> 5*
         f#_2(12, 17) -> 5*
         f#_2(10, 18) -> 5*
          f#_2(9, 18) -> 5*
          f#_2(7, 18) -> 5*
         f#_1(15, 18) -> 5*
         f#_1(15, 11) -> 5*
         f#_1(15, 10) -> 5*
          f#_1(15, 9) -> 5*
          f#_1(15, 7) -> 5*
         f#_1(14, 12) -> 5*
         f#_1(14, 11) -> 5*
         f#_1(10, 11) -> 5*
          f#_1(9, 11) -> 5*
          f#_1(7, 11) -> 5*
         f#_0(10, 10) -> 5*
          f#_0(10, 9) -> 5*
          f#_0(10, 7) -> 5*
          f#_0(9, 10) -> 5*
           f#_0(9, 9) -> 5*
           f#_0(9, 7) -> 5*
          f#_0(7, 10) -> 5*
           f#_0(7, 9) -> 5*
           f#_0(7, 7) -> 5*}
       Strict:
        {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
               f#(b(x), y) -> f#(x, b(y)),
               f#(a(x), y) -> f#(x, a(y))}
       EDG:
        {(f#(b(x), y) -> f#(x, b(y)), f#(a(x), y) -> f#(x, a(y)))
         (f#(b(x), y) -> f#(x, b(y)), f#(b(x), y) -> f#(x, b(y)))
         (f#(a(x), y) -> f#(x, a(y)), f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y))
         (f#(a(x), y) -> f#(x, a(y)), f#(b(x), y) -> f#(x, b(y)))
         (f#(a(x), y) -> f#(x, a(y)), f#(a(x), y) -> f#(x, a(y)))
         (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y))
         (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(b(x), y) -> f#(x, b(y)))}
        SCCS:
         Scc:
          {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
                 f#(b(x), y) -> f#(x, b(y)),
                 f#(a(x), y) -> f#(x, a(y))}
         SCC:
          Strict:
           {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
                  f#(b(x), y) -> f#(x, b(y)),
                  f#(a(x), y) -> f#(x, a(y))}
          Weak:
          {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
                 f(b(x), y) -> f(x, b(y)),
                 f(c(x), y) -> f(x, c(y)),
                 f(a(x), y) -> f(x, a(y))}
          POLY:
           Argument Filtering:
            pi(a) = [0], pi(c) = [], pi(b) = 0, pi(f#) = 0, pi(f) = []
           Usable Rules:
            {}
           Interpretation:
            [a](x0) = x0 + 1,
            [c] = 0
           Strict:
            {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y),
                   f#(b(x), y) -> f#(x, b(y))}
           Weak:
            {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
                   f(b(x), y) -> f(x, b(y)),
                   f(c(x), y) -> f(x, c(y)),
                   f(a(x), y) -> f(x, a(y))}
           EDG:
            {(f#(b(x), y) -> f#(x, b(y)), f#(b(x), y) -> f#(x, b(y)))
             (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y))
             (f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y), f#(b(x), y) -> f#(x, b(y)))}
            SCCS:
             Scc:
              {f#(b(x), y) -> f#(x, b(y))}
             Scc:
              {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y)}
             SCC:
              Strict:
               {f#(b(x), y) -> f#(x, b(y))}
              Weak:
              {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
                     f(b(x), y) -> f(x, b(y)),
                     f(c(x), y) -> f(x, c(y)),
                     f(a(x), y) -> f(x, a(y))}
              SPSC:
               Simple Projection:
                pi(f#) = 0
               Strict:
                {}
               Qed
             SCC:
              Strict:
               {f#(x, a(b(c(y)))) -> f#(b(c(a(b(x)))), y)}
              Weak:
              {f(x, a(b(c(y)))) -> f(b(c(a(b(x)))), y),
                     f(b(x), y) -> f(x, b(y)),
                     f(c(x), y) -> f(x, c(y)),
                     f(a(x), y) -> f(x, a(y))}
              SPSC:
               Simple Projection:
                pi(f#) = 1
               Strict:
                {}
               Qed