MAYBE
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:
  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),
                          b#(y, z) -> c#(c(y, z, z), a(), a())}
  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}
  EDG:
   {(b#(y, z) -> c#(y, z, 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) -> 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) -> 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))
    (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) -> c#(z, y, 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()))
    (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) -> 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()))}
   SCCS:
    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:
     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}
     Fail