MAYBE TRS: {b(a(), f(b(b(z, y), a()))) -> z, f(f(c(a(), y, z))) -> b(y, b(z, z)), c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))} DP: Strict: { f#(f(c(a(), y, z))) -> b#(z, z), f#(f(c(a(), y, z))) -> b#(y, b(z, z)), c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))), c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)), c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))), c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))} Weak: {b(a(), f(b(b(z, y), a()))) -> z, f(f(c(a(), y, z))) -> b(y, b(z, z)), c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))} EDG: {(c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)), f#(f(c(a(), y, z))) -> b#(y, b(z, z))) (c#(c(z, x, a()), a(), y) -> f#(c(z, y, x)), f#(f(c(a(), y, z))) -> b#(z, z)) (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))) (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(z, y, x)) (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x))))) (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(c(z, y, x))) (c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x)))))) (c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))), f#(f(c(a(), y, z))) -> b#(z, z)) (c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x)))), f#(f(c(a(), y, z))) -> b#(y, b(z, z))) (c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))), f#(f(c(a(), y, z))) -> b#(z, z)) (c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x))))), f#(f(c(a(), y, z))) -> b#(y, b(z, z))) (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(f(c(y, a(), f(c(z, y, x)))))) (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(c(z, y, x))) (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> f#(c(y, a(), f(c(z, y, x))))) (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> c#(z, y, x)) (c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x))))} SCCS: Scc: {c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))} SCC: Strict: {c#(c(z, x, a()), a(), y) -> c#(z, y, x), c#(c(z, x, a()), a(), y) -> c#(y, a(), f(c(z, y, x)))} Weak: {b(a(), f(b(b(z, y), a()))) -> z, f(f(c(a(), y, z))) -> b(y, b(z, z)), c(c(z, x, a()), a(), y) -> f(f(c(y, a(), f(c(z, y, x)))))} Fail