YES
Time: 0.006638
TRS:
 {    a X -> e(),
      b X -> e(),
      c X -> e(),
  c b a X -> a a b b c c X}
 DP:
  DP:
   {c# b a X -> a# a b b c c X,
    c# b a X -> a# b b c c X,
    c# b a X -> b# b c c X,
    c# b a X -> b# c c X,
    c# b a X -> c# X,
    c# b a X -> c# c X}
  TRS:
  {    a X -> e(),
       b X -> e(),
       c X -> e(),
   c b a X -> a a b b c c X}
  UR:
   {    a X -> e(),
        b X -> e(),
        c X -> e(),
    c b a X -> a a b b c c X}
   EDG:
    {(c# b a X -> c# X, c# b a X -> c# c X)
     (c# b a X -> c# X, c# b a X -> c# X)
     (c# b a X -> c# X, c# b a X -> b# c c X)
     (c# b a X -> c# X, c# b a X -> b# b c c X)
     (c# b a X -> c# X, c# b a X -> a# b b c c X)
     (c# b a X -> c# X, c# b a X -> a# a b b c c X)}
    STATUS:
     arrows: 0.833333
     SCCS (1):
      Scc:
       {c# b a X -> c# X}
      
      SCC (1):
       Strict:
        {c# b a X -> c# X}
       Weak:
       {    a X -> e(),
            b X -> e(),
            c X -> e(),
        c b a X -> a a b b c c X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a](x0) = x0 + 1,
         
         [b](x0) = x0,
         
         [c](x0) = x0 + 1,
         
         [e] = 0,
         
         [c#](x0) = x0
        Strict:
         c# b a X -> c# X
         1 + 1X >= 0 + 1X
        Weak:
         c b a X -> a a b b c c X
         2 + 1X >= 4 + 1X
         c X -> e()
         1 + 1X >= 0
         b X -> e()
         0 + 1X >= 0
         a X -> e()
         1 + 1X >= 0
       Qed