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