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