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