MAYBE
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:
  Strict:
   {    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))}
  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)))}
  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)))}
   SCCS:
    Scc:
     {    a#(0(), x) -> c#(x),
          a#(0(), x) -> c#(c(x)),
      c#(c(b(c(x)))) -> a#(0(), c(x))}
    SCC:
     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:
      Argument Filtering:
       pi(c#) = [0], pi(c) = [0], pi(0) = [], pi(a#) = [0,1], pi(a) = [0,1], pi(b) = 0
      Usable Rules:
       {}
      Interpretation:
       [a#](x0, x1) = x0 + x1 + 1,
       [c#](x0) = x0 + 1,
       [c](x0) = x0 + 1,
       [0] = 1
      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)))}
      EDG:
       {(a#(0(), x) -> c#(c(x)), c#(c(b(c(x)))) -> a#(0(), c(x)))
        (c#(c(b(c(x)))) -> a#(0(), c(x)), a#(0(), x) -> c#(c(x)))}
       SCCS:
        Scc:
         {    a#(0(), x) -> c#(c(x)),
          c#(c(b(c(x)))) -> a#(0(), c(x))}
        SCC:
         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