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