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