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