MAYBE
Time: 0.869524
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:
  DP:
   {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)}
  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())}
  UR:
   {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()),
                           d(w, v) -> w,
                           d(w, v) -> v}
   EDG:
    {(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))
     (c#(c(z, y, a()), a(), a()) -> b#(z, y), 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))
     (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) -> 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) -> f# 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))
     (f# c(x, y, z) -> c#(z, f b(y, z), a()), c#(c(z, y, a()), a(), a()) -> b#(z, y))}
    STATUS:
     arrows: 0.722222
     SCCS (2):
      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 (1):
       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())}
       Open
      
      
      SCC (3):
       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())}
       Open