MAYBE Time: 0.130280 TRS: { zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt(), L) -> s length activate L, activate X -> X, activate n__zeros() -> zeros(), activate n__take(X1, X2) -> take(activate X1, activate X2), U11(tt(), L) -> U12(tt(), activate L), length cons(N, L) -> U11(tt(), activate L), length nil() -> 0(), U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N), U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N), U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> nil(), take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N)} DP: DP: { U12#(tt(), L) -> activate# L, U12#(tt(), L) -> length# activate L, activate# n__zeros() -> zeros#(), activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), U11#(tt(), L) -> U12#(tt(), activate L), U11#(tt(), L) -> activate# L, length# cons(N, L) -> activate# L, length# cons(N, L) -> U11#(tt(), activate L), U22#(tt(), IL, M, N) -> activate# IL, U22#(tt(), IL, M, N) -> activate# M, U22#(tt(), IL, M, N) -> activate# N, U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U21#(tt(), IL, M, N) -> activate# IL, U21#(tt(), IL, M, N) -> activate# M, U21#(tt(), IL, M, N) -> activate# N, U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# IL, U23#(tt(), IL, M, N) -> activate# M, U23#(tt(), IL, M, N) -> activate# N, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N)} TRS: { zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt(), L) -> s length activate L, activate X -> X, activate n__zeros() -> zeros(), activate n__take(X1, X2) -> take(activate X1, activate X2), U11(tt(), L) -> U12(tt(), activate L), length cons(N, L) -> U11(tt(), activate L), length nil() -> 0(), U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N), U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N), U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> nil(), take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N)} UR: { zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), activate X -> X, activate n__zeros() -> zeros(), activate n__take(X1, X2) -> take(activate X1, activate X2), U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N), U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N), U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> nil(), take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N)} EDG: {(activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N)) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> activate# IL) (length# cons(N, L) -> U11#(tt(), activate L), U11#(tt(), L) -> activate# L) (length# cons(N, L) -> U11#(tt(), activate L), U11#(tt(), L) -> U12#(tt(), activate L)) (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__zeros() -> zeros#()) (U22#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U22#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X2) (U22#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X1) (U22#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U23#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U23#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X2) (U23#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X1) (U23#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U11#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U11#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (U11#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (U11#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#()) (U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# N) (U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# M) (U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# IL) (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__take(X1, X2) -> activate# X2) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X2, activate# n__zeros() -> zeros#()) (U21#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U21#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (U21#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (U21#(tt(), IL, M, N) -> activate# N, activate# n__zeros() -> zeros#()) (U22#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U22#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (U22#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (U22#(tt(), IL, M, N) -> activate# IL, activate# n__zeros() -> zeros#()) (U23#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U23#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (U23#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (U23#(tt(), IL, M, N) -> activate# IL, activate# n__zeros() -> zeros#()) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__zeros() -> zeros#()) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U21#(tt(), IL, M, N) -> activate# IL, activate# n__zeros() -> zeros#()) (U21#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (U21#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (U21#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U23#(tt(), IL, M, N) -> activate# N, activate# n__zeros() -> zeros#()) (U23#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (U23#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (U23#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U22#(tt(), IL, M, N) -> activate# N, activate# n__zeros() -> zeros#()) (U22#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (U22#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (U22#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U22#(tt(), IL, M, N) -> activate# IL) (U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U22#(tt(), IL, M, N) -> activate# M) (U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U22#(tt(), IL, M, N) -> activate# N) (U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N)) (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#()) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U12#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#()) (U12#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (U12#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (U12#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (U21#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U21#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X1) (U21#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> activate# X2) (U21#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N), U21#(tt(), IL, M, N) -> activate# IL) (take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N), U21#(tt(), IL, M, N) -> activate# M) (take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N), U21#(tt(), IL, M, N) -> activate# N) (take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N), U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N)) (U11#(tt(), L) -> U12#(tt(), activate L), U12#(tt(), L) -> activate# L) (U11#(tt(), L) -> U12#(tt(), activate L), U12#(tt(), L) -> length# activate L) (U12#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L) (U12#(tt(), L) -> length# activate L, length# cons(N, L) -> U11#(tt(), activate L))} STATUS: arrows: 0.850662 SCCS (2): Scc: { U12#(tt(), L) -> length# activate L, U11#(tt(), L) -> U12#(tt(), activate L), length# cons(N, L) -> U11#(tt(), activate L)} Scc: {activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), U22#(tt(), IL, M, N) -> activate# IL, U22#(tt(), IL, M, N) -> activate# M, U22#(tt(), IL, M, N) -> activate# N, U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U21#(tt(), IL, M, N) -> activate# IL, U21#(tt(), IL, M, N) -> activate# M, U21#(tt(), IL, M, N) -> activate# N, U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# IL, U23#(tt(), IL, M, N) -> activate# M, U23#(tt(), IL, M, N) -> activate# N, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N)} SCC (3): Strict: { U12#(tt(), L) -> length# activate L, U11#(tt(), L) -> U12#(tt(), activate L), length# cons(N, L) -> U11#(tt(), activate L)} Weak: { zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt(), L) -> s length activate L, activate X -> X, activate n__zeros() -> zeros(), activate n__take(X1, X2) -> take(activate X1, activate X2), U11(tt(), L) -> U12(tt(), activate L), length cons(N, L) -> U11(tt(), activate L), length nil() -> 0(), U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N), U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N), U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> nil(), take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N)} Fail SCC (16): Strict: {activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), U22#(tt(), IL, M, N) -> activate# IL, U22#(tt(), IL, M, N) -> activate# M, U22#(tt(), IL, M, N) -> activate# N, U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N), U21#(tt(), IL, M, N) -> activate# IL, U21#(tt(), IL, M, N) -> activate# M, U21#(tt(), IL, M, N) -> activate# N, U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N), U23#(tt(), IL, M, N) -> activate# IL, U23#(tt(), IL, M, N) -> activate# M, U23#(tt(), IL, M, N) -> activate# N, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N)} Weak: { zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt(), L) -> s length activate L, activate X -> X, activate n__zeros() -> zeros(), activate n__take(X1, X2) -> take(activate X1, activate X2), U11(tt(), L) -> U12(tt(), activate L), length cons(N, L) -> U11(tt(), activate L), length nil() -> 0(), U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N), U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N), U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> nil(), take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U22](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [U21](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [U23](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [cons](x0, x1) = x0 + x1, [U12](x0, x1) = 0, [U11](x0, x1) = 0, [n__take](x0, x1) = x0 + x1 + 1, [take](x0, x1) = x0 + x1 + 1, [activate](x0) = x0, [s](x0) = x0 + 1, [length](x0) = 1, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 1, [nil] = 0, [U22#](x0, x1, x2, x3) = x0 + x1 + x2, [U21#](x0, x1, x2, x3) = x0 + x1 + x2, [U23#](x0, x1, x2, x3) = x0 + x1 + x2, [take#](x0, x1) = x0 + x1 + 1, [activate#](x0) = x0 Strict: take#(s M, cons(N, IL)) -> U21#(tt(), activate IL, M, N) 2 + 1IL + 1M + 1N >= 0 + 1IL + 1M + 1N take#(s M, cons(N, IL)) -> activate# IL 2 + 1IL + 1M + 1N >= 0 + 1IL U23#(tt(), IL, M, N) -> activate# N 0 + 1IL + 1M + 1N >= 0 + 1N U23#(tt(), IL, M, N) -> activate# M 0 + 1IL + 1M + 1N >= 0 + 1M U23#(tt(), IL, M, N) -> activate# IL 0 + 1IL + 1M + 1N >= 0 + 1IL U21#(tt(), IL, M, N) -> U22#(tt(), activate IL, activate M, activate N) 0 + 1IL + 1M + 1N >= 0 + 1IL + 1M + 1N U21#(tt(), IL, M, N) -> activate# N 0 + 1IL + 1M + 1N >= 0 + 1N U21#(tt(), IL, M, N) -> activate# M 0 + 1IL + 1M + 1N >= 0 + 1M U21#(tt(), IL, M, N) -> activate# IL 0 + 1IL + 1M + 1N >= 0 + 1IL U22#(tt(), IL, M, N) -> U23#(tt(), activate IL, activate M, activate N) 0 + 1IL + 1M + 1N >= 0 + 1IL + 1M + 1N U22#(tt(), IL, M, N) -> activate# N 0 + 1IL + 1M + 1N >= 0 + 1N U22#(tt(), IL, M, N) -> activate# M 0 + 1IL + 1M + 1N >= 0 + 1M U22#(tt(), IL, M, N) -> activate# IL 0 + 1IL + 1M + 1N >= 0 + 1IL activate# n__take(X1, X2) -> take#(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__take(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__take(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: take(s M, cons(N, IL)) -> U21(tt(), activate IL, M, N) 2 + 1IL + 1M + 1N >= 2 + 1IL + 1M + 1N take(0(), IL) -> nil() 1 + 1IL >= 0 take(X1, X2) -> n__take(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 U23(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)) 2 + 1IL + 1M + 1N >= 1 + 1IL + 1M + 1N U21(tt(), IL, M, N) -> U22(tt(), activate IL, activate M, activate N) 2 + 1IL + 1M + 1N >= 2 + 1IL + 1M + 1N U22(tt(), IL, M, N) -> U23(tt(), activate IL, activate M, activate N) 2 + 1IL + 1M + 1N >= 2 + 1IL + 1M + 1N length nil() -> 0() 1 >= 0 length cons(N, L) -> U11(tt(), activate L) 1 + 0L + 0N >= 0 + 0L U11(tt(), L) -> U12(tt(), activate L) 0 + 0L >= 0 + 0L activate n__take(X1, X2) -> take(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X U12(tt(), L) -> s length activate L 0 + 0L >= 2 + 0L zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 SCCS (0):