MAYBE
TRS:
 {                   a(y, x) -> y,
  a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()),
                     b(x, y) -> c(a(c(y), a(0(), x)))}
 DP:
  Strict:
   {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x),
    a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()),
    a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y),
                       b#(x, y) -> a#(c(y), a(0(), x)),
                       b#(x, y) -> a#(0(), x)}
  Weak:
  {                   a(y, x) -> y,
   a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()),
                      b(x, y) -> c(a(c(y), a(0(), x)))}
  EDG:
   {(a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), b#(x, y) -> a#(0(), x))
    (a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), b#(x, y) -> a#(c(y), a(0(), x)))
    (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y))
    (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()))
    (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x))
    (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x))
    (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()))
    (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y))
    (a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(c(y), a(0(), x)))
    (a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(0(), x))
    (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x))
    (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()))
    (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y))}
   SCCS:
    Scc:
     {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x),
      a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()),
      a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y),
                         b#(x, y) -> a#(c(y), a(0(), x)),
                         b#(x, y) -> a#(0(), x)}
    SCC:
     Strict:
      {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x),
       a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()),
       a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y),
                          b#(x, y) -> a#(c(y), a(0(), x)),
                          b#(x, y) -> a#(0(), x)}
     Weak:
     {                   a(y, x) -> y,
      a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()),
                         b(x, y) -> c(a(c(y), a(0(), x)))}
     Fail