MAYBE 1031.67/297.04 MAYBE 1031.67/297.04 1031.67/297.04 We are left with following problem, upon which TcT provides the 1031.67/297.04 certificate MAYBE. 1031.67/297.04 1031.67/297.04 Strict Trs: 1031.67/297.04 { zeros() -> cons(0(), n__zeros()) 1031.67/297.04 , zeros() -> n__zeros() 1031.67/297.04 , cons(X1, X2) -> n__cons(X1, X2) 1031.67/297.04 , 0() -> n__0() 1031.67/297.04 , U11(tt(), L) -> s(length(activate(L))) 1031.67/297.04 , s(X) -> n__s(X) 1031.67/297.04 , length(X) -> n__length(X) 1031.67/297.04 , length(cons(N, L)) -> 1031.67/297.04 U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)) 1031.67/297.04 , length(nil()) -> 0() 1031.67/297.04 , activate(X) -> X 1031.67/297.04 , activate(n__zeros()) -> zeros() 1031.67/297.04 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1031.67/297.04 , activate(n__0()) -> 0() 1031.67/297.04 , activate(n__length(X)) -> length(activate(X)) 1031.67/297.04 , activate(n__s(X)) -> s(activate(X)) 1031.67/297.04 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1031.67/297.04 , activate(n__isNatIList(X)) -> isNatIList(X) 1031.67/297.04 , activate(n__nil()) -> nil() 1031.67/297.04 , activate(n__isNatList(X)) -> isNatList(X) 1031.67/297.04 , activate(n__isNat(X)) -> isNat(X) 1031.67/297.04 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1031.67/297.04 , U21(tt()) -> nil() 1031.67/297.04 , nil() -> n__nil() 1031.67/297.04 , U31(tt(), IL, M, N) -> 1031.67/297.04 cons(activate(N), n__take(activate(M), activate(IL))) 1031.67/297.04 , and(X1, X2) -> n__and(X1, X2) 1031.67/297.04 , and(tt(), X) -> activate(X) 1031.67/297.04 , isNat(X) -> n__isNat(X) 1031.67/297.04 , isNat(n__0()) -> tt() 1031.67/297.04 , isNat(n__length(V1)) -> isNatList(activate(V1)) 1031.67/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 1031.67/297.04 , isNatList(X) -> n__isNatList(X) 1031.67/297.04 , isNatList(n__take(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatIList(activate(V2))) 1031.67/297.04 , isNatList(n__cons(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatList(activate(V2))) 1031.67/297.04 , isNatList(n__nil()) -> tt() 1031.67/297.04 , isNatIList(V) -> isNatList(activate(V)) 1031.67/297.04 , isNatIList(X) -> n__isNatIList(X) 1031.67/297.04 , isNatIList(n__zeros()) -> tt() 1031.67/297.04 , isNatIList(n__cons(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatIList(activate(V2))) 1031.67/297.04 , take(X1, X2) -> n__take(X1, X2) 1031.67/297.04 , take(0(), IL) -> U21(isNatIList(IL)) 1031.67/297.04 , take(s(M), cons(N, IL)) -> 1031.67/297.04 U31(and(isNatIList(activate(IL)), 1031.67/297.04 n__and(n__isNat(M), n__isNat(N))), 1031.67/297.04 activate(IL), 1031.67/297.04 M, 1031.67/297.04 N) } 1031.67/297.04 Obligation: 1031.67/297.04 innermost runtime complexity 1031.67/297.04 Answer: 1031.67/297.04 MAYBE 1031.67/297.04 1031.67/297.04 Arguments of following rules are not normal-forms: 1031.67/297.04 1031.67/297.04 { length(cons(N, L)) -> 1031.67/297.04 U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)) 1031.67/297.04 , length(nil()) -> 0() 1031.67/297.04 , take(0(), IL) -> U21(isNatIList(IL)) 1031.67/297.04 , take(s(M), cons(N, IL)) -> 1031.67/297.04 U31(and(isNatIList(activate(IL)), 1031.67/297.04 n__and(n__isNat(M), n__isNat(N))), 1031.67/297.04 activate(IL), 1031.67/297.04 M, 1031.67/297.04 N) } 1031.67/297.04 1031.67/297.04 All above mentioned rules can be savely removed. 1031.67/297.04 1031.67/297.04 We are left with following problem, upon which TcT provides the 1031.67/297.04 certificate MAYBE. 1031.67/297.04 1031.67/297.04 Strict Trs: 1031.67/297.04 { zeros() -> cons(0(), n__zeros()) 1031.67/297.04 , zeros() -> n__zeros() 1031.67/297.04 , cons(X1, X2) -> n__cons(X1, X2) 1031.67/297.04 , 0() -> n__0() 1031.67/297.04 , U11(tt(), L) -> s(length(activate(L))) 1031.67/297.04 , s(X) -> n__s(X) 1031.67/297.04 , length(X) -> n__length(X) 1031.67/297.04 , activate(X) -> X 1031.67/297.04 , activate(n__zeros()) -> zeros() 1031.67/297.04 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1031.67/297.04 , activate(n__0()) -> 0() 1031.67/297.04 , activate(n__length(X)) -> length(activate(X)) 1031.67/297.04 , activate(n__s(X)) -> s(activate(X)) 1031.67/297.04 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1031.67/297.04 , activate(n__isNatIList(X)) -> isNatIList(X) 1031.67/297.04 , activate(n__nil()) -> nil() 1031.67/297.04 , activate(n__isNatList(X)) -> isNatList(X) 1031.67/297.04 , activate(n__isNat(X)) -> isNat(X) 1031.67/297.04 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1031.67/297.04 , U21(tt()) -> nil() 1031.67/297.04 , nil() -> n__nil() 1031.67/297.04 , U31(tt(), IL, M, N) -> 1031.67/297.04 cons(activate(N), n__take(activate(M), activate(IL))) 1031.67/297.04 , and(X1, X2) -> n__and(X1, X2) 1031.67/297.04 , and(tt(), X) -> activate(X) 1031.67/297.04 , isNat(X) -> n__isNat(X) 1031.67/297.04 , isNat(n__0()) -> tt() 1031.67/297.04 , isNat(n__length(V1)) -> isNatList(activate(V1)) 1031.67/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 1031.67/297.04 , isNatList(X) -> n__isNatList(X) 1031.67/297.04 , isNatList(n__take(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatIList(activate(V2))) 1031.67/297.04 , isNatList(n__cons(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatList(activate(V2))) 1031.67/297.04 , isNatList(n__nil()) -> tt() 1031.67/297.04 , isNatIList(V) -> isNatList(activate(V)) 1031.67/297.04 , isNatIList(X) -> n__isNatIList(X) 1031.67/297.04 , isNatIList(n__zeros()) -> tt() 1031.67/297.04 , isNatIList(n__cons(V1, V2)) -> 1031.67/297.04 and(isNat(activate(V1)), n__isNatIList(activate(V2))) 1031.67/297.04 , take(X1, X2) -> n__take(X1, X2) } 1031.67/297.04 Obligation: 1031.67/297.04 innermost runtime complexity 1031.67/297.04 Answer: 1031.67/297.04 MAYBE 1031.67/297.04 1031.67/297.04 None of the processors succeeded. 1031.67/297.04 1031.67/297.04 Details of failed attempt(s): 1031.67/297.04 ----------------------------- 1031.67/297.04 1) 'empty' failed due to the following reason: 1031.67/297.04 1031.67/297.04 Empty strict component of the problem is NOT empty. 1031.67/297.04 1031.67/297.04 2) 'Best' failed due to the following reason: 1031.67/297.04 1031.67/297.04 None of the processors succeeded. 1031.67/297.04 1031.67/297.04 Details of failed attempt(s): 1031.67/297.04 ----------------------------- 1031.67/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1031.67/297.04 following reason: 1031.67/297.04 1031.67/297.04 Computation stopped due to timeout after 297.0 seconds. 1031.67/297.04 1031.67/297.04 2) 'Best' failed due to the following reason: 1031.67/297.04 1031.67/297.04 None of the processors succeeded. 1031.67/297.04 1031.67/297.04 Details of failed attempt(s): 1031.67/297.04 ----------------------------- 1031.67/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1031.67/297.04 seconds)' failed due to the following reason: 1031.67/297.04 1031.67/297.04 Computation stopped due to timeout after 148.0 seconds. 1031.67/297.04 1031.67/297.04 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1031.67/297.04 failed due to the following reason: 1031.67/297.04 1031.67/297.04 Computation stopped due to timeout after 24.0 seconds. 1031.67/297.04 1031.67/297.04 3) 'Best' failed due to the following reason: 1031.67/297.04 1031.67/297.04 None of the processors succeeded. 1031.67/297.04 1031.67/297.04 Details of failed attempt(s): 1031.67/297.04 ----------------------------- 1031.67/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1031.67/297.04 following reason: 1031.67/297.04 1031.67/297.04 The input cannot be shown compatible 1031.67/297.04 1031.67/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1031.67/297.04 to the following reason: 1031.67/297.04 1031.67/297.04 The input cannot be shown compatible 1031.67/297.04 1031.67/297.04 1031.67/297.04 1031.67/297.04 1031.67/297.04 1031.67/297.04 Arrrr.. 1033.85/299.17 EOF