MAYBE Time: 1.862357 TRS: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} DP: DP: { q# s X -> q# X, q# s X -> s# p(q X, d X), q# s X -> p#(q X, d X), q# s X -> d# X, t# N -> q# N, p#(s X, s Y) -> s# s p(X, Y), p#(s X, s Y) -> s# p(X, Y), p#(s X, s Y) -> p#(X, Y), d# s X -> s# s d X, d# s X -> s# d X, d# s X -> d# X, f#(s X, cs(Y, Z)) -> a# Z, a# nt X -> t# a X, a# nt X -> a# X, a# ns X -> s# a X, a# ns X -> a# X, a# nf(X1, X2) -> f#(a X1, a X2), a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> a# X2} TRS: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} UR: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2), b(x, y) -> x, b(x, y) -> y} EDG: {(q# s X -> p#(q X, d X), p#(s X, s Y) -> p#(X, Y)) (q# s X -> p#(q X, d X), p#(s X, s Y) -> s# p(X, Y)) (q# s X -> p#(q X, d X), p#(s X, s Y) -> s# s p(X, Y)) (a# nf(X1, X2) -> f#(a X1, a X2), f#(s X, cs(Y, Z)) -> a# Z) (a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> a# X2) (a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> a# X1) (a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> f#(a X1, a X2)) (a# nf(X1, X2) -> a# X1, a# ns X -> a# X) (a# nf(X1, X2) -> a# X1, a# ns X -> s# a X) (a# nf(X1, X2) -> a# X1, a# nt X -> a# X) (a# nf(X1, X2) -> a# X1, a# nt X -> t# a X) (a# nt X -> t# a X, t# N -> q# N) (q# s X -> d# X, d# s X -> d# X) (q# s X -> d# X, d# s X -> s# d X) (q# s X -> d# X, d# s X -> s# s d X) (f#(s X, cs(Y, Z)) -> a# Z, a# nf(X1, X2) -> a# X2) (f#(s X, cs(Y, Z)) -> a# Z, a# nf(X1, X2) -> a# X1) (f#(s X, cs(Y, Z)) -> a# Z, a# nf(X1, X2) -> f#(a X1, a X2)) (f#(s X, cs(Y, Z)) -> a# Z, a# ns X -> a# X) (f#(s X, cs(Y, Z)) -> a# Z, a# ns X -> s# a X) (f#(s X, cs(Y, Z)) -> a# Z, a# nt X -> a# X) (f#(s X, cs(Y, Z)) -> a# Z, a# nt X -> t# a X) (a# ns X -> a# X, a# nf(X1, X2) -> a# X2) (a# ns X -> a# X, a# nf(X1, X2) -> a# X1) (a# ns X -> a# X, a# nf(X1, X2) -> f#(a X1, a X2)) (a# ns X -> a# X, a# ns X -> a# X) (a# ns X -> a# X, a# ns X -> s# a X) (a# ns X -> a# X, a# nt X -> a# X) (a# ns X -> a# X, a# nt X -> t# a X) (a# nf(X1, X2) -> a# X2, a# nt X -> t# a X) (a# nf(X1, X2) -> a# X2, a# nt X -> a# X) (a# nf(X1, X2) -> a# X2, a# ns X -> s# a X) (a# nf(X1, X2) -> a# X2, a# ns X -> a# X) (a# nf(X1, X2) -> a# X2, a# nf(X1, X2) -> f#(a X1, a X2)) (a# nf(X1, X2) -> a# X2, a# nf(X1, X2) -> a# X1) (a# nf(X1, X2) -> a# X2, a# nf(X1, X2) -> a# X2) (a# nt X -> a# X, a# nt X -> t# a X) (a# nt X -> a# X, a# nt X -> a# X) (a# nt X -> a# X, a# ns X -> s# a X) (a# nt X -> a# X, a# ns X -> a# X) (a# nt X -> a# X, a# nf(X1, X2) -> f#(a X1, a X2)) (a# nt X -> a# X, a# nf(X1, X2) -> a# X1) (a# nt X -> a# X, a# nf(X1, X2) -> a# X2) (d# s X -> d# X, d# s X -> s# s d X) (d# s X -> d# X, d# s X -> s# d X) (d# s X -> d# X, d# s X -> d# X) (q# s X -> q# X, q# s X -> q# X) (q# s X -> q# X, q# s X -> s# p(q X, d X)) (q# s X -> q# X, q# s X -> p#(q X, d X)) (q# s X -> q# X, q# s X -> d# X) (t# N -> q# N, q# s X -> q# X) (t# N -> q# N, q# s X -> s# p(q X, d X)) (t# N -> q# N, q# s X -> p#(q X, d X)) (t# N -> q# N, q# s X -> d# X) (p#(s X, s Y) -> p#(X, Y), p#(s X, s Y) -> s# s p(X, Y)) (p#(s X, s Y) -> p#(X, Y), p#(s X, s Y) -> s# p(X, Y)) (p#(s X, s Y) -> p#(X, Y), p#(s X, s Y) -> p#(X, Y))} STATUS: arrows: 0.842105 SCCS (4): Scc: {f#(s X, cs(Y, Z)) -> a# Z, a# nt X -> a# X, a# ns X -> a# X, a# nf(X1, X2) -> f#(a X1, a X2), a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> a# X2} Scc: {q# s X -> q# X} Scc: {d# s X -> d# X} Scc: {p#(s X, s Y) -> p#(X, Y)} SCC (6): Strict: {f#(s X, cs(Y, Z)) -> a# Z, a# nt X -> a# X, a# ns X -> a# X, a# nf(X1, X2) -> f#(a X1, a X2), a# nf(X1, X2) -> a# X1, a# nf(X1, X2) -> a# X2} Weak: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} Open SCC (1): Strict: {q# s X -> q# X} Weak: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} Open SCC (1): Strict: {d# s X -> d# X} Weak: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} Open SCC (1): Strict: {p#(s X, s Y) -> p#(X, Y)} Weak: { q 0() -> 0(), q s X -> s p(q X, d X), t N -> cs(r q N, nt ns N), t X -> nt X, s X -> ns X, p(X, 0()) -> X, p(0(), X) -> X, p(s X, s Y) -> s s p(X, Y), d 0() -> 0(), d s X -> s s d X, f(X1, X2) -> nf(X1, X2), f(0(), X) -> nil(), f(s X, cs(Y, Z)) -> cs(Y, nf(X, a Z)), a X -> X, a nt X -> t a X, a ns X -> s a X, a nf(X1, X2) -> f(a X1, a X2)} Open