MAYBE
TRS:
 {    a(1(), x) -> c(b(x)),
      a(0(), x) -> c(c(x)),
  b(c(b(c(x)))) -> a(0(), a(1(), x)),
  c(c(c(b(x)))) -> a(1(), b(c(x)))}
 DP:
  Strict:
   {    a#(1(), x) -> b#(x),
        a#(1(), x) -> c#(b(x)),
        a#(0(), x) -> c#(x),
        a#(0(), x) -> c#(c(x)),
    b#(c(b(c(x)))) -> a#(1(), x),
    b#(c(b(c(x)))) -> a#(0(), a(1(), x)),
    c#(c(c(b(x)))) -> a#(1(), b(c(x))),
    c#(c(c(b(x)))) -> b#(c(x)),
    c#(c(c(b(x)))) -> c#(x)}
  Weak:
  {    a(1(), x) -> c(b(x)),
       a(0(), x) -> c(c(x)),
   b(c(b(c(x)))) -> a(0(), a(1(), x)),
   c(c(c(b(x)))) -> a(1(), b(c(x)))}
  EDG:
   {(a#(1(), x) -> b#(x), b#(c(b(c(x)))) -> a#(0(), a(1(), x)))
    (a#(1(), x) -> b#(x), b#(c(b(c(x)))) -> a#(1(), x))
    (c#(c(c(b(x)))) -> a#(1(), b(c(x))), a#(1(), x) -> c#(b(x)))
    (c#(c(c(b(x)))) -> a#(1(), b(c(x))), a#(1(), x) -> b#(x))
    (a#(1(), x) -> c#(b(x)), c#(c(c(b(x)))) -> c#(x))
    (a#(1(), x) -> c#(b(x)), c#(c(c(b(x)))) -> b#(c(x)))
    (a#(1(), x) -> c#(b(x)), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
    (c#(c(c(b(x)))) -> b#(c(x)), b#(c(b(c(x)))) -> a#(0(), a(1(), x)))
    (c#(c(c(b(x)))) -> b#(c(x)), b#(c(b(c(x)))) -> a#(1(), x))
    (b#(c(b(c(x)))) -> a#(0(), a(1(), x)), a#(0(), x) -> c#(x))
    (b#(c(b(c(x)))) -> a#(0(), a(1(), x)), a#(0(), x) -> c#(c(x)))
    (a#(0(), x) -> c#(c(x)), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
    (a#(0(), x) -> c#(c(x)), c#(c(c(b(x)))) -> b#(c(x)))
    (a#(0(), x) -> c#(c(x)), c#(c(c(b(x)))) -> c#(x))
    (c#(c(c(b(x)))) -> c#(x), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
    (c#(c(c(b(x)))) -> c#(x), c#(c(c(b(x)))) -> b#(c(x)))
    (c#(c(c(b(x)))) -> c#(x), c#(c(c(b(x)))) -> c#(x))
    (a#(0(), x) -> c#(x), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
    (a#(0(), x) -> c#(x), c#(c(c(b(x)))) -> b#(c(x)))
    (a#(0(), x) -> c#(x), c#(c(c(b(x)))) -> c#(x))
    (b#(c(b(c(x)))) -> a#(1(), x), a#(1(), x) -> b#(x))
    (b#(c(b(c(x)))) -> a#(1(), x), a#(1(), x) -> c#(b(x)))}
   SCCS:
    Scc:
     {    a#(1(), x) -> b#(x),
          a#(1(), x) -> c#(b(x)),
          a#(0(), x) -> c#(x),
          a#(0(), x) -> c#(c(x)),
      b#(c(b(c(x)))) -> a#(1(), x),
      b#(c(b(c(x)))) -> a#(0(), a(1(), x)),
      c#(c(c(b(x)))) -> a#(1(), b(c(x))),
      c#(c(c(b(x)))) -> b#(c(x)),
      c#(c(c(b(x)))) -> c#(x)}
    SCC:
     Strict:
      {    a#(1(), x) -> b#(x),
           a#(1(), x) -> c#(b(x)),
           a#(0(), x) -> c#(x),
           a#(0(), x) -> c#(c(x)),
       b#(c(b(c(x)))) -> a#(1(), x),
       b#(c(b(c(x)))) -> a#(0(), a(1(), x)),
       c#(c(c(b(x)))) -> a#(1(), b(c(x))),
       c#(c(c(b(x)))) -> b#(c(x)),
       c#(c(c(b(x)))) -> c#(x)}
     Weak:
     {    a(1(), x) -> c(b(x)),
          a(0(), x) -> c(c(x)),
      b(c(b(c(x)))) -> a(0(), a(1(), x)),
      c(c(c(b(x)))) -> a(1(), b(c(x)))}
     POLY:
      Argument Filtering:
       pi(0) = [], pi(c#) = 0, pi(c) = [0], pi(b#) = [0], pi(b) = [0], pi(1) = [], pi(a#) = [1], pi(a) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [a#](x0) = x0 + 1,
       [b#](x0) = x0 + 1,
       [a](x0, x1) = x0 + x1 + 1,
       [c](x0) = x0 + 1,
       [b](x0) = x0 + 1,
       [1] = 1
      Strict:
       {    a#(1(), x) -> b#(x),
            a#(1(), x) -> c#(b(x)),
            a#(0(), x) -> c#(c(x)),
        c#(c(c(b(x)))) -> a#(1(), b(c(x)))}
      Weak:
       {    a(1(), x) -> c(b(x)),
            a(0(), x) -> c(c(x)),
        b(c(b(c(x)))) -> a(0(), a(1(), x)),
        c(c(c(b(x)))) -> a(1(), b(c(x)))}
      EDG:
       {(a#(0(), x) -> c#(c(x)), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
        (a#(1(), x) -> c#(b(x)), c#(c(c(b(x)))) -> a#(1(), b(c(x))))
        (c#(c(c(b(x)))) -> a#(1(), b(c(x))), a#(1(), x) -> b#(x))
        (c#(c(c(b(x)))) -> a#(1(), b(c(x))), a#(1(), x) -> c#(b(x)))}
       SCCS:
        Scc:
         {    a#(1(), x) -> c#(b(x)),
          c#(c(c(b(x)))) -> a#(1(), b(c(x)))}
        SCC:
         Strict:
          {    a#(1(), x) -> c#(b(x)),
           c#(c(c(b(x)))) -> a#(1(), b(c(x)))}
         Weak:
         {    a(1(), x) -> c(b(x)),
              a(0(), x) -> c(c(x)),
          b(c(b(c(x)))) -> a(0(), a(1(), x)),
          c(c(c(b(x)))) -> a(1(), b(c(x)))}
         Fail