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