MAYBE Time: 0.434192 TRS: { eq(X, Y) -> false(), eq(n__0(), n__0()) -> true(), eq(n__s X, n__s Y) -> eq(activate X, activate Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s X, activate n__inf X -> inf activate X, activate n__take(X1, X2) -> take(activate X1, activate X2), activate n__length X -> length activate X, inf X -> cons(X, n__inf n__s X), inf X -> n__inf X, take(X1, X2) -> n__take(X1, X2), take(0(), X) -> nil(), take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)), 0() -> n__0(), s X -> n__s X, length X -> n__length X, length cons(X, L) -> s n__length activate L, length nil() -> 0()} DP: DP: { eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X, eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#(), activate# n__s X -> s# X, activate# n__inf X -> activate# X, activate# n__inf X -> inf# activate X, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), activate# n__length X -> activate# X, activate# n__length X -> length# activate X, take#(s X, cons(Y, L)) -> activate# X, take#(s X, cons(Y, L)) -> activate# Y, take#(s X, cons(Y, L)) -> activate# L, length# cons(X, L) -> activate# L, length# cons(X, L) -> s# n__length activate L, length# nil() -> 0#()} TRS: { eq(X, Y) -> false(), eq(n__0(), n__0()) -> true(), eq(n__s X, n__s Y) -> eq(activate X, activate Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s X, activate n__inf X -> inf activate X, activate n__take(X1, X2) -> take(activate X1, activate X2), activate n__length X -> length activate X, inf X -> cons(X, n__inf n__s X), inf X -> n__inf X, take(X1, X2) -> n__take(X1, X2), take(0(), X) -> nil(), take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)), 0() -> n__0(), s X -> n__s X, length X -> n__length X, length cons(X, L) -> s n__length activate L, length nil() -> 0()} UR: { activate X -> X, activate n__0() -> 0(), activate n__s X -> s X, activate n__inf X -> inf activate X, activate n__take(X1, X2) -> take(activate X1, activate X2), activate n__length X -> length activate X, inf X -> cons(X, n__inf n__s X), inf X -> n__inf X, take(X1, X2) -> n__take(X1, X2), take(0(), X) -> nil(), take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)), 0() -> n__0(), s X -> n__s X, length X -> n__length X, length cons(X, L) -> s n__length activate L, length nil() -> 0(), a(x, y) -> x, a(x, y) -> y} EDG: {(length# cons(X, L) -> activate# L, activate# n__length X -> length# activate X) (length# cons(X, L) -> activate# L, activate# n__length X -> activate# X) (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# activate X) (length# cons(X, L) -> activate# L, activate# n__inf X -> activate# X) (length# cons(X, L) -> activate# L, activate# n__s X -> s# X) (length# cons(X, L) -> activate# L, activate# n__0() -> 0#()) (activate# n__length X -> length# activate X, length# nil() -> 0#()) (activate# n__length X -> length# activate X, length# cons(X, L) -> s# n__length activate L) (activate# n__length X -> length# activate X, length# cons(X, L) -> activate# L) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# activate X) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> activate# X) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> activate# X2) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> activate# X1) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# activate X) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> activate# X) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X) (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#()) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s X, cons(Y, L)) -> activate# L) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s X, cons(Y, L)) -> activate# Y) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s X, cons(Y, L)) -> activate# X) (activate# n__length X -> activate# X, activate# n__length X -> length# activate X) (activate# n__length X -> activate# X, activate# n__length X -> activate# X) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> activate# X2) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> activate# X1) (activate# n__length X -> activate# X, activate# n__inf X -> inf# activate X) (activate# n__length X -> activate# X, activate# n__inf X -> activate# X) (activate# n__length X -> activate# X, activate# n__s X -> s# X) (activate# n__length X -> activate# X, activate# n__0() -> 0#()) (activate# n__take(X1, X2) -> activate# X1, activate# n__length X -> length# activate X) (activate# n__take(X1, X2) -> activate# X1, activate# n__length X -> activate# X) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X1, activate# n__inf X -> inf# activate X) (activate# n__take(X1, X2) -> activate# X1, activate# n__inf X -> activate# X) (activate# n__take(X1, X2) -> activate# X1, activate# n__s X -> s# X) (activate# n__take(X1, X2) -> activate# X1, activate# n__0() -> 0#()) (activate# n__take(X1, X2) -> activate# X2, activate# n__0() -> 0#()) (activate# n__take(X1, X2) -> activate# X2, activate# n__s X -> s# X) (activate# n__take(X1, X2) -> activate# X2, activate# n__inf X -> activate# X) (activate# n__take(X1, X2) -> activate# X2, activate# n__inf X -> inf# activate X) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> activate# X2) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__take(X1, X2) -> activate# X2, activate# n__length X -> activate# X) (activate# n__take(X1, X2) -> activate# X2, activate# n__length X -> length# activate X) (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#()) (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X) (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> activate# X) (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# activate X) (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> activate# X1) (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> activate# X2) (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> activate# X) (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# activate X) (activate# n__inf X -> activate# X, activate# n__0() -> 0#()) (activate# n__inf X -> activate# X, activate# n__s X -> s# X) (activate# n__inf X -> activate# X, activate# n__inf X -> activate# X) (activate# n__inf X -> activate# X, activate# n__inf X -> inf# activate X) (activate# n__inf X -> activate# X, activate# n__take(X1, X2) -> activate# X1) (activate# n__inf X -> activate# X, activate# n__take(X1, X2) -> activate# X2) (activate# n__inf X -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__inf X -> activate# X, activate# n__length X -> activate# X) (activate# n__inf X -> activate# X, activate# n__length X -> length# activate X) (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#()) (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X) (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> activate# X) (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# activate X) (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> activate# X1) (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> activate# X2) (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> activate# X) (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# activate X) (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)) (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X) (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#()) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> activate# X) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# activate X) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> activate# X1) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> activate# X2) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> activate# X) (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# activate X) (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#()) (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X) (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> activate# X) (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# activate X) (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> activate# X) (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# activate X)} STATUS: arrows: 0.694444 SCCS (2): Scc: {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)} Scc: { activate# n__inf X -> activate# X, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), activate# n__length X -> activate# X, activate# n__length X -> length# activate X, take#(s X, cons(Y, L)) -> activate# X, take#(s X, cons(Y, L)) -> activate# Y, take#(s X, cons(Y, L)) -> activate# L, length# cons(X, L) -> activate# L} SCC (1): Strict: {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)} Weak: { eq(X, Y) -> false(), eq(n__0(), n__0()) -> true(), eq(n__s X, n__s Y) -> eq(activate X, activate Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s X, activate n__inf X -> inf activate X, activate n__take(X1, X2) -> take(activate X1, activate X2), activate n__length X -> length activate X, inf X -> cons(X, n__inf n__s X), inf X -> n__inf X, take(X1, X2) -> n__take(X1, X2), take(0(), X) -> nil(), take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)), 0() -> n__0(), s X -> n__s X, length X -> n__length X, length cons(X, L) -> s n__length activate L, length nil() -> 0()} Open SCC (10): Strict: { activate# n__inf X -> activate# X, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), activate# n__length X -> activate# X, activate# n__length X -> length# activate X, take#(s X, cons(Y, L)) -> activate# X, take#(s X, cons(Y, L)) -> activate# Y, take#(s X, cons(Y, L)) -> activate# L, length# cons(X, L) -> activate# L} Weak: { eq(X, Y) -> false(), eq(n__0(), n__0()) -> true(), eq(n__s X, n__s Y) -> eq(activate X, activate Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s X, activate n__inf X -> inf activate X, activate n__take(X1, X2) -> take(activate X1, activate X2), activate n__length X -> length activate X, inf X -> cons(X, n__inf n__s X), inf X -> n__inf X, take(X1, X2) -> n__take(X1, X2), take(0(), X) -> nil(), take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)), 0() -> n__0(), s X -> n__s X, length X -> n__length X, length cons(X, L) -> s n__length activate L, length nil() -> 0()} Open