MAYBE
Time: 0.024254
TRS:
 {a(0(), x) -> c c x,
      c c x -> b c b c x,
  c c b c x -> b a(0(), c x)}
 DP:
  DP:
   {a#(0(), x) -> c# x,
    a#(0(), x) -> c# c x,
        c# c x -> c# b c x,
    c# c b c x -> a#(0(), c x)}
  TRS:
  {a(0(), x) -> c c x,
       c c x -> b c b c x,
   c c b c x -> b a(0(), c x)}
  UR:
   {a(0(), x) -> c c x,
        c c x -> b c b c x,
    c c b c x -> b a(0(), c x)}
   EDG:
    {(a#(0(), x) -> c# x, c# c b c x -> a#(0(), c x))
     (a#(0(), x) -> c# x, c# c x -> c# b c x)
     (a#(0(), x) -> c# c x, c# c b c x -> a#(0(), c x))
     (a#(0(), x) -> c# c x, c# c x -> c# b c x)
     (c# c b c x -> a#(0(), c x), a#(0(), x) -> c# x)
     (c# c b c x -> a#(0(), c x), a#(0(), x) -> c# c x)}
    STATUS:
     arrows: 0.625000
     SCCS (1):
      Scc:
       {a#(0(), x) -> c# x,
        a#(0(), x) -> c# c x,
        c# c b c x -> a#(0(), c x)}
      
      SCC (3):
       Strict:
        {a#(0(), x) -> c# x,
         a#(0(), x) -> c# c x,
         c# c b c x -> a#(0(), c x)}
       Weak:
       {a(0(), x) -> c c x,
            c c x -> b c b c x,
        c c b c x -> b a(0(), c x)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a](x0, x1) = x0 + x1 + 1,
         
         [b](x0) = x0,
         
         [c](x0) = x0 + 1,
         
         [0] = 1,
         
         [a#](x0, x1) = x0 + x1 + 1,
         
         [c#](x0) = x0 + 1
        Strict:
         c# c b c x -> a#(0(), c x)
         3 + 1x >= 3 + 1x
         a#(0(), x) -> c# c x
         2 + 1x >= 2 + 1x
         a#(0(), x) -> c# x
         2 + 1x >= 1 + 1x
        Weak:
         c c b c x -> b a(0(), c x)
         3 + 1x >= 3 + 1x
         c c x -> b c b c x
         2 + 1x >= 2 + 1x
         a(0(), x) -> c c x
         2 + 1x >= 2 + 1x
       SCCS (1):
        Scc:
         {a#(0(), x) -> c# c x,
          c# c b c x -> a#(0(), c x)}
        
        SCC (2):
         Strict:
          {a#(0(), x) -> c# c x,
           c# c b c x -> a#(0(), c x)}
         Weak:
         {a(0(), x) -> c c x,
              c c x -> b c b c x,
          c c b c x -> b a(0(), c x)}
         Fail