YES
Time: 0.340549
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:
  DP:
   {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)}
  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)}
  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 (1):
    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 (4):
     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)}
     BOUND:
      Bound: match(-raise)-DP-bounded by 2
      Automaton:
       {     a_2(18) -> 23*
             a_1(24) -> 13*
             a_1(22) -> 20*
             a_1(19) -> 20*
             a_1(17) -> 20*
             a_1(14) -> 15*
             a_1(13) -> 13*
             a_0(12) -> 11*
             a_0(11) -> 11*
              a_0(9) -> 11*
              a_0(8) -> 11*
             c_2(24) -> 18*
             c_2(14) -> 18*
             c_2(13) -> 18*
             c_1(24) -> 13*
             c_1(20) -> 21*
             c_1(15) -> 16*
             c_1(13) -> 13*
             c_1(12) -> 13*
             c_1(11) -> 13*
              c_1(9) -> 13*
             c_0(12) -> 12*
             c_0(11) -> 12*
              c_0(9) -> 12*
              c_0(8) -> 12*
             b_2(24) -> 24*
             b_2(23) -> 24*
             b_1(24) -> 13*
             b_1(22) -> 19*
             b_1(21) -> 22*
             b_1(17) -> 19*
             b_1(16) -> 17*
             b_1(13) -> 13*
             b_1(12) -> 14*
             b_1(11) -> 14*
              b_1(9) -> 14*
              b_1(8) -> 14*
             b_0(12) -> 9*
             b_0(11) -> 9*
              b_0(9) -> 9*
              b_0(8) -> 9*
        f#_2(22, 24) -> 6*
        f#_2(22, 23) -> 6*
        f#_2(21, 24) -> 6*
        f#_2(20, 18) -> 6*
        f#_2(19, 23) -> 6*
        f#_2(17, 24) -> 6*
        f#_2(17, 23) -> 6*
        f#_2(16, 24) -> 6*
        f#_2(15, 18) -> 6*
        f#_2(14, 23) -> 6*
        f#_2(12, 24) -> 6*
        f#_2(11, 24) -> 6*
         f#_2(9, 24) -> 6*
         f#_2(8, 24) -> 6*
        f#_1(22, 24) -> 6*
        f#_1(22, 13) -> 6*
        f#_1(22, 12) -> 6*
        f#_1(22, 11) -> 6*
         f#_1(22, 9) -> 6*
         f#_1(22, 8) -> 6*
        f#_1(21, 14) -> 6*
        f#_1(21, 13) -> 6*
        f#_1(17, 24) -> 6*
        f#_1(17, 13) -> 6*
        f#_1(17, 12) -> 6*
        f#_1(17, 11) -> 6*
         f#_1(17, 9) -> 6*
        f#_1(16, 14) -> 6*
        f#_1(16, 13) -> 6*
        f#_1(12, 13) -> 6*
        f#_1(11, 13) -> 6*
         f#_1(9, 13) -> 6*
         f#_1(8, 13) -> 6*
        f#_0(12, 12) -> 6*
        f#_0(12, 11) -> 6*
         f#_0(12, 9) -> 6*
        f#_0(11, 12) -> 6*
        f#_0(11, 11) -> 6*
         f#_0(11, 9) -> 6*
         f#_0(9, 12) -> 6*
         f#_0(9, 11) -> 6*
          f#_0(9, 9) -> 6*
          f#_0(9, 8) -> 6*
         f#_0(8, 12) -> 6*
         f#_0(8, 11) -> 6*
          f#_0(8, 9) -> 6*
         f_0(12, 12) -> 8*
         f_0(12, 11) -> 8*
          f_0(12, 9) -> 8*
          f_0(12, 8) -> 8*
         f_0(11, 12) -> 8*
         f_0(11, 11) -> 8*
          f_0(11, 9) -> 8*
          f_0(11, 8) -> 8*
          f_0(9, 12) -> 8*
          f_0(9, 11) -> 8*
           f_0(9, 9) -> 8*
           f_0(9, 8) -> 8*
          f_0(8, 12) -> 8*
          f_0(8, 11) -> 8*
           f_0(8, 9) -> 8*
           f_0(8, 8) -> 8*}
      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 (1):
        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 (3):
         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:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = 0,
           
           [b](x0) = x0,
           
           [c](x0) = 0,
           
           [a](x0) = x0 + 1,
           
           [f#](x0, x1) = x0
          Strict:
           f#(a x, y) -> f#(x, a y)
           1 + 1x + 0y >= 0 + 1x + 0y
           f#(b x, y) -> f#(x, b y)
           0 + 1x + 0y >= 0 + 1x + 0y
           f#(x, a b c y) -> f#(b c a b x, y)
           0 + 1x + 0y >= 0 + 0x + 0y
          Weak:
           
         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 (2):
           Scc:
            {f#(b x, y) -> f#(x, b y)}
           Scc:
            {f#(x, a b c y) -> f#(b c a b x, y)}
           SCC (1):
            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 (1):
            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