MAYBE
Time: 35.313826
TRS:
 {  b(a(), b(c(z, x, y), a())) -> b(b(z, c(y, z, a())), x),
     c(f c(a(), y, a()), x, z) -> f b(b(z, z), f b(y, b(x, a()))),
  f c(a(), b(b(z, a()), y), x) -> f c(x, b(z, x), y)}
 DP:
  DP:
   {  b#(a(), b(c(z, x, y), a())) -> b#(z, c(y, z, a())),
      b#(a(), b(c(z, x, y), a())) -> b#(b(z, c(y, z, a())), x),
      b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()),
       c#(f c(a(), y, a()), x, z) -> b#(z, z),
       c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())),
       c#(f c(a(), y, a()), x, z) -> b#(x, a()),
       c#(f c(a(), y, a()), x, z) -> b#(b(z, z), f b(y, b(x, a()))),
       c#(f c(a(), y, a()), x, z) -> f# b(y, b(x, a())),
       c#(f c(a(), y, a()), x, z) -> f# b(b(z, z), f b(y, b(x, a()))),
    f# c(a(), b(b(z, a()), y), x) -> b#(z, x),
    f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y),
    f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y)}
  TRS:
  {  b(a(), b(c(z, x, y), a())) -> b(b(z, c(y, z, a())), x),
      c(f c(a(), y, a()), x, z) -> f b(b(z, z), f b(y, b(x, a()))),
   f c(a(), b(b(z, a()), y), x) -> f c(x, b(z, x), y)}
  UR:
   {  b(a(), b(c(z, x, y), a())) -> b(b(z, c(y, z, a())), x),
       c(f c(a(), y, a()), x, z) -> f b(b(z, z), f b(y, b(x, a()))),
    f c(a(), b(b(z, a()), y), x) -> f c(x, b(z, x), y),
                         d(w, v) -> w,
                         d(w, v) -> v}
   EDG:
    {(f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y), f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y))
     (f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y), f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y))
     (f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y), f# c(a(), b(b(z, a()), y), x) -> b#(z, x))
     (f# c(a(), b(b(z, a()), y), x) -> b#(z, x), b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()))
     (f# c(a(), b(b(z, a()), y), x) -> b#(z, x), b#(a(), b(c(z, x, y), a())) -> b#(b(z, c(y, z, a())), x))
     (f# c(a(), b(b(z, a()), y), x) -> b#(z, x), b#(a(), b(c(z, x, y), a())) -> b#(z, c(y, z, a())))
     (c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())), b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()))
     (c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())), b#(a(), b(c(z, x, y), a())) -> b#(b(z, c(y, z, a())), x))
     (c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())), b#(a(), b(c(z, x, y), a())) -> b#(z, c(y, z, a())))
     (c#(f c(a(), y, a()), x, z) -> b#(z, z), b#(a(), b(c(z, x, y), a())) -> b#(z, c(y, z, a())))
     (c#(f c(a(), y, a()), x, z) -> b#(z, z), b#(a(), b(c(z, x, y), a())) -> b#(b(z, c(y, z, a())), x))
     (c#(f c(a(), y, a()), x, z) -> b#(z, z), b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> b#(z, z))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> b#(x, a()))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> b#(b(z, z), f b(y, b(x, a()))))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> f# b(y, b(x, a())))
     (b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()), c#(f c(a(), y, a()), x, z) -> f# b(b(z, z), f b(y, b(x, a()))))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> b#(z, z))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a())))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> b#(x, a()))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> b#(b(z, z), f b(y, b(x, a()))))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> f# b(y, b(x, a())))
     (f# c(a(), b(b(z, a()), y), x) -> c#(x, b(z, x), y), c#(f c(a(), y, a()), x, z) -> f# b(b(z, z), f b(y, b(x, a()))))}
    STATUS:
     arrows: 0.833333
     SCCS (2):
      Scc:
       {f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y)}
      Scc:
       {b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()),
         c#(f c(a(), y, a()), x, z) -> b#(z, z),
         c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a()))}
      
      SCC (1):
       Strict:
        {f# c(a(), b(b(z, a()), y), x) -> f# c(x, b(z, x), y)}
       Weak:
       {  b(a(), b(c(z, x, y), a())) -> b(b(z, c(y, z, a())), x),
           c(f c(a(), y, a()), x, z) -> f b(b(z, z), f b(y, b(x, a()))),
        f c(a(), b(b(z, a()), y), x) -> f c(x, b(z, x), y)}
       Open
      
      
      SCC (3):
       Strict:
        {b#(a(), b(c(z, x, y), a())) -> c#(y, z, a()),
          c#(f c(a(), y, a()), x, z) -> b#(z, z),
          c#(f c(a(), y, a()), x, z) -> b#(y, b(x, a()))}
       Weak:
       {  b(a(), b(c(z, x, y), a())) -> b(b(z, c(y, z, a())), x),
           c(f c(a(), y, a()), x, z) -> f b(b(z, z), f b(y, b(x, a()))),
        f c(a(), b(b(z, a()), y), x) -> f c(x, b(z, x), y)}
       Open