MAYBE 765.58/297.06 MAYBE 765.58/297.06 765.58/297.06 We are left with following problem, upon which TcT provides the 765.58/297.06 certificate MAYBE. 765.58/297.06 765.58/297.06 Strict Trs: 765.58/297.06 { a__from(X) -> cons(mark(X), from(s(X))) 765.58/297.06 , a__from(X) -> from(X) 765.58/297.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 765.58/297.06 , mark(from(X)) -> a__from(mark(X)) 765.58/297.06 , mark(s(X)) -> s(mark(X)) 765.58/297.06 , mark(0()) -> 0() 765.58/297.06 , mark(nil()) -> nil() 765.58/297.06 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 765.58/297.06 , mark(head(X)) -> a__head(mark(X)) 765.58/297.06 , mark(2nd(X)) -> a__2nd(mark(X)) 765.58/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 765.58/297.06 , a__head(X) -> head(X) 765.58/297.06 , a__head(cons(X, XS)) -> mark(X) 765.58/297.06 , a__2nd(X) -> 2nd(X) 765.58/297.06 , a__2nd(cons(X, XS)) -> a__head(mark(XS)) 765.58/297.06 , a__take(X1, X2) -> take(X1, X2) 765.58/297.06 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 765.58/297.06 , a__take(0(), XS) -> nil() 765.58/297.06 , a__sel(X1, X2) -> sel(X1, X2) 765.58/297.06 , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS)) 765.58/297.06 , a__sel(0(), cons(X, XS)) -> mark(X) } 765.58/297.06 Obligation: 765.58/297.06 innermost runtime complexity 765.58/297.06 Answer: 765.58/297.06 MAYBE 765.58/297.06 765.58/297.06 None of the processors succeeded. 765.58/297.06 765.58/297.06 Details of failed attempt(s): 765.58/297.06 ----------------------------- 765.58/297.06 1) 'empty' failed due to the following reason: 765.58/297.06 765.58/297.06 Empty strict component of the problem is NOT empty. 765.58/297.06 765.58/297.06 2) 'Best' failed due to the following reason: 765.58/297.06 765.58/297.06 None of the processors succeeded. 765.58/297.06 765.58/297.06 Details of failed attempt(s): 765.58/297.06 ----------------------------- 765.58/297.06 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 765.58/297.06 following reason: 765.58/297.06 765.58/297.06 Computation stopped due to timeout after 297.0 seconds. 765.58/297.06 765.58/297.06 2) 'Best' failed due to the following reason: 765.58/297.06 765.58/297.06 None of the processors succeeded. 765.58/297.06 765.58/297.06 Details of failed attempt(s): 765.58/297.06 ----------------------------- 765.58/297.06 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 765.58/297.06 seconds)' failed due to the following reason: 765.58/297.06 765.58/297.06 The weightgap principle applies (using the following nonconstant 765.58/297.06 growth matrix-interpretation) 765.58/297.06 765.58/297.06 The following argument positions are usable: 765.58/297.06 Uargs(a__from) = {1}, Uargs(cons) = {1}, Uargs(s) = {1}, 765.58/297.06 Uargs(a__head) = {1}, Uargs(a__2nd) = {1}, Uargs(a__take) = {1, 2}, 765.58/297.06 Uargs(a__sel) = {1, 2} 765.58/297.06 765.58/297.06 TcT has computed the following matrix interpretation satisfying 765.58/297.06 not(EDA) and not(IDA(1)). 765.58/297.06 765.58/297.06 [a__from](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [cons](x1, x2) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [mark](x1) = [7] 765.58/297.06 765.58/297.06 [from](x1) = [1] x1 + [6] 765.58/297.06 765.58/297.06 [s](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [a__head](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [a__2nd](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [a__take](x1, x2) = [1] x1 + [1] x2 + [1] 765.58/297.06 765.58/297.06 [0] = [7] 765.58/297.06 765.58/297.06 [nil] = [6] 765.58/297.06 765.58/297.06 [take](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [1] 765.58/297.06 765.58/297.06 [head](x1) = [1] x1 + [6] 765.58/297.06 765.58/297.06 [2nd](x1) = [1] x1 + [6] 765.58/297.06 765.58/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 The order satisfies the following ordering constraints: 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [7] 765.58/297.06 ? [14] 765.58/297.06 = [cons(mark(X), from(s(X)))] 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [7] 765.58/297.06 > [1] X + [6] 765.58/297.06 = [from(X)] 765.58/297.06 765.58/297.06 [mark(cons(X1, X2))] = [7] 765.58/297.06 ? [14] 765.58/297.06 = [cons(mark(X1), X2)] 765.58/297.06 765.58/297.06 [mark(from(X))] = [7] 765.58/297.06 ? [14] 765.58/297.06 = [a__from(mark(X))] 765.58/297.06 765.58/297.06 [mark(s(X))] = [7] 765.58/297.06 ? [14] 765.58/297.06 = [s(mark(X))] 765.58/297.06 765.58/297.06 [mark(0())] = [7] 765.58/297.06 >= [7] 765.58/297.06 = [0()] 765.58/297.06 765.58/297.06 [mark(nil())] = [7] 765.58/297.06 > [6] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [mark(take(X1, X2))] = [7] 765.58/297.06 ? [15] 765.58/297.06 = [a__take(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [mark(head(X))] = [7] 765.58/297.06 ? [14] 765.58/297.06 = [a__head(mark(X))] 765.58/297.06 765.58/297.06 [mark(2nd(X))] = [7] 765.58/297.06 ? [14] 765.58/297.06 = [a__2nd(mark(X))] 765.58/297.06 765.58/297.06 [mark(sel(X1, X2))] = [7] 765.58/297.06 ? [15] 765.58/297.06 = [a__sel(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [a__head(X)] = [1] X + [7] 765.58/297.06 > [1] X + [6] 765.58/297.06 = [head(X)] 765.58/297.06 765.58/297.06 [a__head(cons(X, XS))] = [1] X + [14] 765.58/297.06 > [7] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 [a__2nd(X)] = [1] X + [7] 765.58/297.06 > [1] X + [6] 765.58/297.06 = [2nd(X)] 765.58/297.06 765.58/297.06 [a__2nd(cons(X, XS))] = [1] X + [14] 765.58/297.06 >= [14] 765.58/297.06 = [a__head(mark(XS))] 765.58/297.06 765.58/297.06 [a__take(X1, X2)] = [1] X1 + [1] X2 + [1] 765.58/297.06 > [1] X1 + [1] X2 + [0] 765.58/297.06 = [take(X1, X2)] 765.58/297.06 765.58/297.06 [a__take(s(N), cons(X, XS))] = [1] X + [1] N + [15] 765.58/297.06 > [14] 765.58/297.06 = [cons(mark(X), take(N, XS))] 765.58/297.06 765.58/297.06 [a__take(0(), XS)] = [1] XS + [8] 765.58/297.06 > [6] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [1] 765.58/297.06 > [1] X1 + [1] X2 + [0] 765.58/297.06 = [sel(X1, X2)] 765.58/297.06 765.58/297.06 [a__sel(s(N), cons(X, XS))] = [1] X + [1] N + [15] 765.58/297.06 >= [15] 765.58/297.06 = [a__sel(mark(N), mark(XS))] 765.58/297.06 765.58/297.06 [a__sel(0(), cons(X, XS))] = [1] X + [15] 765.58/297.06 > [7] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 765.58/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 765.58/297.06 765.58/297.06 We are left with following problem, upon which TcT provides the 765.58/297.06 certificate MAYBE. 765.58/297.06 765.58/297.06 Strict Trs: 765.58/297.06 { a__from(X) -> cons(mark(X), from(s(X))) 765.58/297.06 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 765.58/297.06 , mark(from(X)) -> a__from(mark(X)) 765.58/297.06 , mark(s(X)) -> s(mark(X)) 765.58/297.06 , mark(0()) -> 0() 765.58/297.06 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 765.58/297.06 , mark(head(X)) -> a__head(mark(X)) 765.58/297.06 , mark(2nd(X)) -> a__2nd(mark(X)) 765.58/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 765.58/297.06 , a__2nd(cons(X, XS)) -> a__head(mark(XS)) 765.58/297.06 , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS)) } 765.58/297.06 Weak Trs: 765.58/297.06 { a__from(X) -> from(X) 765.58/297.06 , mark(nil()) -> nil() 765.58/297.06 , a__head(X) -> head(X) 765.58/297.06 , a__head(cons(X, XS)) -> mark(X) 765.58/297.06 , a__2nd(X) -> 2nd(X) 765.58/297.06 , a__take(X1, X2) -> take(X1, X2) 765.58/297.06 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 765.58/297.06 , a__take(0(), XS) -> nil() 765.58/297.06 , a__sel(X1, X2) -> sel(X1, X2) 765.58/297.06 , a__sel(0(), cons(X, XS)) -> mark(X) } 765.58/297.06 Obligation: 765.58/297.06 innermost runtime complexity 765.58/297.06 Answer: 765.58/297.06 MAYBE 765.58/297.06 765.58/297.06 The weightgap principle applies (using the following nonconstant 765.58/297.06 growth matrix-interpretation) 765.58/297.06 765.58/297.06 The following argument positions are usable: 765.58/297.06 Uargs(a__from) = {1}, Uargs(cons) = {1}, Uargs(s) = {1}, 765.58/297.06 Uargs(a__head) = {1}, Uargs(a__2nd) = {1}, Uargs(a__take) = {1, 2}, 765.58/297.06 Uargs(a__sel) = {1, 2} 765.58/297.06 765.58/297.06 TcT has computed the following matrix interpretation satisfying 765.58/297.06 not(EDA) and not(IDA(1)). 765.58/297.06 765.58/297.06 [a__from](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [cons](x1, x2) = [1] x1 + [0] 765.58/297.06 765.58/297.06 [mark](x1) = [0] 765.58/297.06 765.58/297.06 [from](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [s](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__head](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__2nd](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__take](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 [0] = [4] 765.58/297.06 765.58/297.06 [nil] = [0] 765.58/297.06 765.58/297.06 [take](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 [head](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [2nd](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 The order satisfies the following ordering constraints: 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [cons(mark(X), from(s(X)))] 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [4] 765.58/297.06 >= [1] X + [4] 765.58/297.06 = [from(X)] 765.58/297.06 765.58/297.06 [mark(cons(X1, X2))] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [cons(mark(X1), X2)] 765.58/297.06 765.58/297.06 [mark(from(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__from(mark(X))] 765.58/297.06 765.58/297.06 [mark(s(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [s(mark(X))] 765.58/297.06 765.58/297.06 [mark(0())] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [0()] 765.58/297.06 765.58/297.06 [mark(nil())] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [mark(take(X1, X2))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__take(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [mark(head(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__head(mark(X))] 765.58/297.06 765.58/297.06 [mark(2nd(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__2nd(mark(X))] 765.58/297.06 765.58/297.06 [mark(sel(X1, X2))] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [a__sel(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [a__head(X)] = [1] X + [4] 765.58/297.06 >= [1] X + [4] 765.58/297.06 = [head(X)] 765.58/297.06 765.58/297.06 [a__head(cons(X, XS))] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 [a__2nd(X)] = [1] X + [4] 765.58/297.06 >= [1] X + [4] 765.58/297.06 = [2nd(X)] 765.58/297.06 765.58/297.06 [a__2nd(cons(X, XS))] = [1] X + [4] 765.58/297.06 >= [4] 765.58/297.06 = [a__head(mark(XS))] 765.58/297.06 765.58/297.06 [a__take(X1, X2)] = [1] X1 + [1] X2 + [4] 765.58/297.06 >= [1] X1 + [1] X2 + [4] 765.58/297.06 = [take(X1, X2)] 765.58/297.06 765.58/297.06 [a__take(s(N), cons(X, XS))] = [1] X + [1] N + [8] 765.58/297.06 > [0] 765.58/297.06 = [cons(mark(X), take(N, XS))] 765.58/297.06 765.58/297.06 [a__take(0(), XS)] = [1] XS + [8] 765.58/297.06 > [0] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 765.58/297.06 >= [1] X1 + [1] X2 + [0] 765.58/297.06 = [sel(X1, X2)] 765.58/297.06 765.58/297.06 [a__sel(s(N), cons(X, XS))] = [1] X + [1] N + [4] 765.58/297.06 > [0] 765.58/297.06 = [a__sel(mark(N), mark(XS))] 765.58/297.06 765.58/297.06 [a__sel(0(), cons(X, XS))] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 765.58/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 765.58/297.06 765.58/297.06 We are left with following problem, upon which TcT provides the 765.58/297.06 certificate MAYBE. 765.58/297.06 765.58/297.06 Strict Trs: 765.58/297.06 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 765.58/297.06 , mark(from(X)) -> a__from(mark(X)) 765.58/297.06 , mark(s(X)) -> s(mark(X)) 765.58/297.06 , mark(0()) -> 0() 765.58/297.06 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 765.58/297.06 , mark(head(X)) -> a__head(mark(X)) 765.58/297.06 , mark(2nd(X)) -> a__2nd(mark(X)) 765.58/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 765.58/297.06 , a__2nd(cons(X, XS)) -> a__head(mark(XS)) } 765.58/297.06 Weak Trs: 765.58/297.06 { a__from(X) -> cons(mark(X), from(s(X))) 765.58/297.06 , a__from(X) -> from(X) 765.58/297.06 , mark(nil()) -> nil() 765.58/297.06 , a__head(X) -> head(X) 765.58/297.06 , a__head(cons(X, XS)) -> mark(X) 765.58/297.06 , a__2nd(X) -> 2nd(X) 765.58/297.06 , a__take(X1, X2) -> take(X1, X2) 765.58/297.06 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 765.58/297.06 , a__take(0(), XS) -> nil() 765.58/297.06 , a__sel(X1, X2) -> sel(X1, X2) 765.58/297.06 , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS)) 765.58/297.06 , a__sel(0(), cons(X, XS)) -> mark(X) } 765.58/297.06 Obligation: 765.58/297.06 innermost runtime complexity 765.58/297.06 Answer: 765.58/297.06 MAYBE 765.58/297.06 765.58/297.06 The weightgap principle applies (using the following nonconstant 765.58/297.06 growth matrix-interpretation) 765.58/297.06 765.58/297.06 The following argument positions are usable: 765.58/297.06 Uargs(a__from) = {1}, Uargs(cons) = {1}, Uargs(s) = {1}, 765.58/297.06 Uargs(a__head) = {1}, Uargs(a__2nd) = {1}, Uargs(a__take) = {1, 2}, 765.58/297.06 Uargs(a__sel) = {1, 2} 765.58/297.06 765.58/297.06 TcT has computed the following matrix interpretation satisfying 765.58/297.06 not(EDA) and not(IDA(1)). 765.58/297.06 765.58/297.06 [a__from](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [cons](x1, x2) = [1] x1 + [0] 765.58/297.06 765.58/297.06 [mark](x1) = [0] 765.58/297.06 765.58/297.06 [from](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [s](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__head](x1) = [1] x1 + [0] 765.58/297.06 765.58/297.06 [a__2nd](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__take](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 [0] = [0] 765.58/297.06 765.58/297.06 [nil] = [0] 765.58/297.06 765.58/297.06 [take](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 [head](x1) = [1] x1 + [0] 765.58/297.06 765.58/297.06 [2nd](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [sel](x1, x2) = [1] x1 + [1] x2 + [4] 765.58/297.06 765.58/297.06 The order satisfies the following ordering constraints: 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [cons(mark(X), from(s(X)))] 765.58/297.06 765.58/297.06 [a__from(X)] = [1] X + [4] 765.58/297.06 >= [1] X + [4] 765.58/297.06 = [from(X)] 765.58/297.06 765.58/297.06 [mark(cons(X1, X2))] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [cons(mark(X1), X2)] 765.58/297.06 765.58/297.06 [mark(from(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__from(mark(X))] 765.58/297.06 765.58/297.06 [mark(s(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [s(mark(X))] 765.58/297.06 765.58/297.06 [mark(0())] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [0()] 765.58/297.06 765.58/297.06 [mark(nil())] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [mark(take(X1, X2))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__take(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [mark(head(X))] = [0] 765.58/297.06 >= [0] 765.58/297.06 = [a__head(mark(X))] 765.58/297.06 765.58/297.06 [mark(2nd(X))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__2nd(mark(X))] 765.58/297.06 765.58/297.06 [mark(sel(X1, X2))] = [0] 765.58/297.06 ? [4] 765.58/297.06 = [a__sel(mark(X1), mark(X2))] 765.58/297.06 765.58/297.06 [a__head(X)] = [1] X + [0] 765.58/297.06 >= [1] X + [0] 765.58/297.06 = [head(X)] 765.58/297.06 765.58/297.06 [a__head(cons(X, XS))] = [1] X + [0] 765.58/297.06 >= [0] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 [a__2nd(X)] = [1] X + [4] 765.58/297.06 >= [1] X + [4] 765.58/297.06 = [2nd(X)] 765.58/297.06 765.58/297.06 [a__2nd(cons(X, XS))] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [a__head(mark(XS))] 765.58/297.06 765.58/297.06 [a__take(X1, X2)] = [1] X1 + [1] X2 + [4] 765.58/297.06 >= [1] X1 + [1] X2 + [4] 765.58/297.06 = [take(X1, X2)] 765.58/297.06 765.58/297.06 [a__take(s(N), cons(X, XS))] = [1] X + [1] N + [8] 765.58/297.06 > [0] 765.58/297.06 = [cons(mark(X), take(N, XS))] 765.58/297.06 765.58/297.06 [a__take(0(), XS)] = [1] XS + [4] 765.58/297.06 > [0] 765.58/297.06 = [nil()] 765.58/297.06 765.58/297.06 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [4] 765.58/297.06 >= [1] X1 + [1] X2 + [4] 765.58/297.06 = [sel(X1, X2)] 765.58/297.06 765.58/297.06 [a__sel(s(N), cons(X, XS))] = [1] X + [1] N + [8] 765.58/297.06 > [4] 765.58/297.06 = [a__sel(mark(N), mark(XS))] 765.58/297.06 765.58/297.06 [a__sel(0(), cons(X, XS))] = [1] X + [4] 765.58/297.06 > [0] 765.58/297.06 = [mark(X)] 765.58/297.06 765.58/297.06 765.58/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 765.58/297.06 765.58/297.06 We are left with following problem, upon which TcT provides the 765.58/297.06 certificate MAYBE. 765.58/297.06 765.58/297.06 Strict Trs: 765.58/297.06 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 765.58/297.06 , mark(from(X)) -> a__from(mark(X)) 765.58/297.06 , mark(s(X)) -> s(mark(X)) 765.58/297.06 , mark(0()) -> 0() 765.58/297.06 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 765.58/297.06 , mark(head(X)) -> a__head(mark(X)) 765.58/297.06 , mark(2nd(X)) -> a__2nd(mark(X)) 765.58/297.06 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) } 765.58/297.06 Weak Trs: 765.58/297.06 { a__from(X) -> cons(mark(X), from(s(X))) 765.58/297.06 , a__from(X) -> from(X) 765.58/297.06 , mark(nil()) -> nil() 765.58/297.06 , a__head(X) -> head(X) 765.58/297.06 , a__head(cons(X, XS)) -> mark(X) 765.58/297.06 , a__2nd(X) -> 2nd(X) 765.58/297.06 , a__2nd(cons(X, XS)) -> a__head(mark(XS)) 765.58/297.06 , a__take(X1, X2) -> take(X1, X2) 765.58/297.06 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 765.58/297.06 , a__take(0(), XS) -> nil() 765.58/297.06 , a__sel(X1, X2) -> sel(X1, X2) 765.58/297.06 , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS)) 765.58/297.06 , a__sel(0(), cons(X, XS)) -> mark(X) } 765.58/297.06 Obligation: 765.58/297.06 innermost runtime complexity 765.58/297.06 Answer: 765.58/297.06 MAYBE 765.58/297.06 765.58/297.06 The weightgap principle applies (using the following nonconstant 765.58/297.06 growth matrix-interpretation) 765.58/297.06 765.58/297.06 The following argument positions are usable: 765.58/297.06 Uargs(a__from) = {1}, Uargs(cons) = {1}, Uargs(s) = {1}, 765.58/297.06 Uargs(a__head) = {1}, Uargs(a__2nd) = {1}, Uargs(a__take) = {1, 2}, 765.58/297.06 Uargs(a__sel) = {1, 2} 765.58/297.06 765.58/297.06 TcT has computed the following matrix interpretation satisfying 765.58/297.06 not(EDA) and not(IDA(1)). 765.58/297.06 765.58/297.06 [a__from](x1) = [1] x1 + [5] 765.58/297.06 765.58/297.06 [cons](x1, x2) = [1] x1 + [1] 765.58/297.06 765.58/297.06 [mark](x1) = [4] 765.58/297.06 765.58/297.06 [from](x1) = [1] x1 + [5] 765.58/297.06 765.58/297.06 [s](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [a__head](x1) = [1] x1 + [4] 765.58/297.06 765.58/297.06 [a__2nd](x1) = [1] x1 + [7] 765.58/297.06 765.58/297.06 [a__take](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 [0] = [3] 765.58/297.06 765.58/297.06 [nil] = [0] 765.58/297.06 765.58/297.06 [take](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.06 [a__sel](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.06 765.58/297.07 [head](x1) = [1] x1 + [4] 765.58/297.07 765.58/297.07 [2nd](x1) = [1] x1 + [7] 765.58/297.07 765.58/297.07 [sel](x1, x2) = [1] x1 + [1] x2 + [0] 765.58/297.07 765.58/297.07 The order satisfies the following ordering constraints: 765.58/297.07 765.58/297.07 [a__from(X)] = [1] X + [5] 765.58/297.07 >= [5] 765.58/297.07 = [cons(mark(X), from(s(X)))] 765.58/297.07 765.58/297.07 [a__from(X)] = [1] X + [5] 765.58/297.07 >= [1] X + [5] 765.58/297.07 = [from(X)] 765.58/297.07 765.58/297.07 [mark(cons(X1, X2))] = [4] 765.58/297.07 ? [5] 765.58/297.07 = [cons(mark(X1), X2)] 765.58/297.07 765.58/297.07 [mark(from(X))] = [4] 765.58/297.07 ? [9] 765.58/297.07 = [a__from(mark(X))] 765.58/297.07 765.58/297.07 [mark(s(X))] = [4] 765.58/297.07 ? [11] 765.58/297.07 = [s(mark(X))] 765.58/297.07 765.58/297.07 [mark(0())] = [4] 765.58/297.07 > [3] 765.58/297.07 = [0()] 765.58/297.07 765.58/297.07 [mark(nil())] = [4] 765.58/297.07 > [0] 765.58/297.07 = [nil()] 765.58/297.07 765.58/297.07 [mark(take(X1, X2))] = [4] 765.58/297.07 ? [8] 765.58/297.07 = [a__take(mark(X1), mark(X2))] 765.58/297.07 765.58/297.07 [mark(head(X))] = [4] 765.58/297.07 ? [8] 765.58/297.07 = [a__head(mark(X))] 765.58/297.07 765.58/297.07 [mark(2nd(X))] = [4] 765.58/297.07 ? [11] 765.58/297.07 = [a__2nd(mark(X))] 765.58/297.07 765.58/297.07 [mark(sel(X1, X2))] = [4] 765.58/297.07 ? [8] 765.58/297.07 = [a__sel(mark(X1), mark(X2))] 765.58/297.07 765.58/297.07 [a__head(X)] = [1] X + [4] 765.58/297.07 >= [1] X + [4] 765.58/297.07 = [head(X)] 765.58/297.07 765.58/297.07 [a__head(cons(X, XS))] = [1] X + [5] 765.58/297.07 > [4] 765.58/297.07 = [mark(X)] 765.58/297.07 765.58/297.07 [a__2nd(X)] = [1] X + [7] 765.58/297.07 >= [1] X + [7] 765.58/297.07 = [2nd(X)] 765.58/297.07 765.58/297.07 [a__2nd(cons(X, XS))] = [1] X + [8] 765.58/297.07 >= [8] 765.58/297.07 = [a__head(mark(XS))] 765.58/297.07 765.58/297.07 [a__take(X1, X2)] = [1] X1 + [1] X2 + [0] 765.58/297.07 >= [1] X1 + [1] X2 + [0] 765.58/297.07 = [take(X1, X2)] 765.58/297.07 765.58/297.07 [a__take(s(N), cons(X, XS))] = [1] X + [1] N + [8] 765.58/297.07 > [5] 765.58/297.07 = [cons(mark(X), take(N, XS))] 765.58/297.07 765.58/297.07 [a__take(0(), XS)] = [1] XS + [3] 765.58/297.07 > [0] 765.58/297.07 = [nil()] 765.58/297.07 765.58/297.07 [a__sel(X1, X2)] = [1] X1 + [1] X2 + [0] 765.58/297.07 >= [1] X1 + [1] X2 + [0] 765.58/297.07 = [sel(X1, X2)] 765.58/297.07 765.58/297.07 [a__sel(s(N), cons(X, XS))] = [1] X + [1] N + [8] 765.58/297.07 >= [8] 765.58/297.07 = [a__sel(mark(N), mark(XS))] 765.58/297.07 765.58/297.07 [a__sel(0(), cons(X, XS))] = [1] X + [4] 765.58/297.07 >= [4] 765.58/297.07 = [mark(X)] 765.58/297.07 765.58/297.07 765.58/297.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 765.58/297.07 765.58/297.07 We are left with following problem, upon which TcT provides the 765.58/297.07 certificate MAYBE. 765.58/297.07 765.58/297.07 Strict Trs: 765.58/297.07 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 765.58/297.07 , mark(from(X)) -> a__from(mark(X)) 765.58/297.07 , mark(s(X)) -> s(mark(X)) 765.58/297.07 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 765.58/297.07 , mark(head(X)) -> a__head(mark(X)) 765.58/297.07 , mark(2nd(X)) -> a__2nd(mark(X)) 765.58/297.07 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) } 765.58/297.07 Weak Trs: 765.58/297.07 { a__from(X) -> cons(mark(X), from(s(X))) 765.58/297.07 , a__from(X) -> from(X) 765.58/297.07 , mark(0()) -> 0() 765.58/297.07 , mark(nil()) -> nil() 765.58/297.07 , a__head(X) -> head(X) 765.58/297.07 , a__head(cons(X, XS)) -> mark(X) 765.58/297.07 , a__2nd(X) -> 2nd(X) 765.58/297.07 , a__2nd(cons(X, XS)) -> a__head(mark(XS)) 765.58/297.07 , a__take(X1, X2) -> take(X1, X2) 765.58/297.07 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 765.58/297.07 , a__take(0(), XS) -> nil() 765.58/297.07 , a__sel(X1, X2) -> sel(X1, X2) 765.58/297.07 , a__sel(s(N), cons(X, XS)) -> a__sel(mark(N), mark(XS)) 765.58/297.07 , a__sel(0(), cons(X, XS)) -> mark(X) } 765.58/297.07 Obligation: 765.58/297.07 innermost runtime complexity 765.58/297.07 Answer: 765.58/297.07 MAYBE 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'Fastest' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'empty' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 2) 'With Problem ...' failed due to the following reason: 765.58/297.07 765.58/297.07 Empty strict component of the problem is NOT empty. 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 2) 'Best' failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 765.58/297.07 to the following reason: 765.58/297.07 765.58/297.07 The input cannot be shown compatible 765.58/297.07 765.58/297.07 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 765.58/297.07 following reason: 765.58/297.07 765.58/297.07 The input cannot be shown compatible 765.58/297.07 765.58/297.07 765.58/297.07 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 765.58/297.07 failed due to the following reason: 765.58/297.07 765.58/297.07 None of the processors succeeded. 765.58/297.07 765.58/297.07 Details of failed attempt(s): 765.58/297.07 ----------------------------- 765.58/297.07 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 765.58/297.07 failed due to the following reason: 765.58/297.07 765.58/297.07 match-boundness of the problem could not be verified. 765.58/297.07 765.58/297.07 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 765.58/297.07 failed due to the following reason: 765.58/297.07 765.58/297.07 match-boundness of the problem could not be verified. 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 765.58/297.07 Arrrr.. 766.11/297.58 EOF