MAYBE 846.33/297.03 MAYBE 846.33/297.03 846.33/297.03 We are left with following problem, upon which TcT provides the 846.33/297.03 certificate MAYBE. 846.33/297.03 846.33/297.03 Strict Trs: 846.33/297.03 { dbl(X) -> n__dbl(X) 846.33/297.03 , dbl(0()) -> 0() 846.33/297.03 , dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) 846.33/297.03 , s(X) -> n__s(X) 846.33/297.03 , activate(X) -> X 846.33/297.03 , activate(n__s(X)) -> s(X) 846.33/297.03 , activate(n__dbl(X)) -> dbl(activate(X)) 846.33/297.03 , activate(n__dbls(X)) -> dbls(activate(X)) 846.33/297.03 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 846.33/297.03 , activate(n__indx(X1, X2)) -> indx(activate(X1), X2) 846.33/297.03 , activate(n__from(X)) -> from(X) 846.33/297.03 , dbls(X) -> n__dbls(X) 846.33/297.03 , dbls(nil()) -> nil() 846.33/297.03 , dbls(cons(X, Y)) -> 846.33/297.03 cons(n__dbl(activate(X)), n__dbls(activate(Y))) 846.33/297.03 , sel(X1, X2) -> n__sel(X1, X2) 846.33/297.03 , sel(0(), cons(X, Y)) -> activate(X) 846.33/297.03 , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)) 846.33/297.03 , indx(X1, X2) -> n__indx(X1, X2) 846.33/297.03 , indx(nil(), X) -> nil() 846.33/297.03 , indx(cons(X, Y), Z) -> 846.33/297.03 cons(n__sel(activate(X), activate(Z)), 846.33/297.03 n__indx(activate(Y), activate(Z))) 846.33/297.03 , from(X) -> cons(activate(X), n__from(n__s(activate(X)))) 846.33/297.03 , from(X) -> n__from(X) } 846.33/297.03 Obligation: 846.33/297.03 innermost runtime complexity 846.33/297.03 Answer: 846.33/297.03 MAYBE 846.33/297.03 846.33/297.03 Arguments of following rules are not normal-forms: 846.33/297.03 846.33/297.03 { dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) 846.33/297.03 , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)) } 846.33/297.03 846.33/297.03 All above mentioned rules can be savely removed. 846.33/297.03 846.33/297.03 We are left with following problem, upon which TcT provides the 846.33/297.03 certificate MAYBE. 846.33/297.03 846.33/297.03 Strict Trs: 846.33/297.03 { dbl(X) -> n__dbl(X) 846.33/297.03 , dbl(0()) -> 0() 846.33/297.03 , s(X) -> n__s(X) 846.33/297.03 , activate(X) -> X 846.33/297.03 , activate(n__s(X)) -> s(X) 846.33/297.03 , activate(n__dbl(X)) -> dbl(activate(X)) 846.33/297.03 , activate(n__dbls(X)) -> dbls(activate(X)) 846.33/297.03 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 846.33/297.03 , activate(n__indx(X1, X2)) -> indx(activate(X1), X2) 846.33/297.03 , activate(n__from(X)) -> from(X) 846.33/297.03 , dbls(X) -> n__dbls(X) 846.33/297.03 , dbls(nil()) -> nil() 846.33/297.03 , dbls(cons(X, Y)) -> 846.33/297.03 cons(n__dbl(activate(X)), n__dbls(activate(Y))) 846.33/297.03 , sel(X1, X2) -> n__sel(X1, X2) 846.33/297.03 , sel(0(), cons(X, Y)) -> activate(X) 846.33/297.03 , indx(X1, X2) -> n__indx(X1, X2) 846.33/297.03 , indx(nil(), X) -> nil() 846.33/297.03 , indx(cons(X, Y), Z) -> 846.33/297.03 cons(n__sel(activate(X), activate(Z)), 846.33/297.03 n__indx(activate(Y), activate(Z))) 846.33/297.03 , from(X) -> cons(activate(X), n__from(n__s(activate(X)))) 846.33/297.03 , from(X) -> n__from(X) } 846.33/297.03 Obligation: 846.33/297.03 innermost runtime complexity 846.33/297.03 Answer: 846.33/297.03 MAYBE 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'Best' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 846.33/297.03 following reason: 846.33/297.03 846.33/297.03 Computation stopped due to timeout after 297.0 seconds. 846.33/297.03 846.33/297.03 2) 'Best' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 846.33/297.03 seconds)' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'Fastest' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'empty' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 2) 'With Problem ...' failed due to the following reason: 846.33/297.03 846.33/297.03 Empty strict component of the problem is NOT empty. 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 2) 'Best' failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 846.33/297.03 following reason: 846.33/297.03 846.33/297.03 The input cannot be shown compatible 846.33/297.03 846.33/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 846.33/297.03 to the following reason: 846.33/297.03 846.33/297.03 The input cannot be shown compatible 846.33/297.03 846.33/297.03 846.33/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 846.33/297.03 failed due to the following reason: 846.33/297.03 846.33/297.03 None of the processors succeeded. 846.33/297.03 846.33/297.03 Details of failed attempt(s): 846.33/297.03 ----------------------------- 846.33/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 846.33/297.03 failed due to the following reason: 846.33/297.03 846.33/297.03 match-boundness of the problem could not be verified. 846.33/297.03 846.33/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 846.33/297.03 failed due to the following reason: 846.33/297.03 846.33/297.03 match-boundness of the problem could not be verified. 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 846.33/297.03 Arrrr.. 846.55/297.22 EOF