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