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