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