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