MAYBE 755.80/297.05 MAYBE 755.80/297.05 755.80/297.05 We are left with following problem, upon which TcT provides the 755.80/297.05 certificate MAYBE. 755.80/297.05 755.80/297.05 Strict Trs: 755.80/297.05 { +(x, 0()) -> x 755.80/297.05 , +(+(x, y), z) -> +(x, +(y, z)) 755.80/297.05 , +(0(), x) -> x 755.80/297.05 , +(s(x), s(y)) -> s(s(+(x, y))) 755.80/297.05 , *(x, 0()) -> 0() 755.80/297.05 , *(0(), x) -> 0() 755.80/297.05 , *(s(x), s(y)) -> s(+(*(x, y), +(x, y))) 755.80/297.05 , *(*(x, y), z) -> *(x, *(y, z)) 755.80/297.05 , app(nil(), l) -> l 755.80/297.05 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 755.80/297.05 , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) 755.80/297.05 , sum(nil()) -> 0() 755.80/297.05 , sum(cons(x, l)) -> +(x, sum(l)) 755.80/297.05 , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) 755.80/297.05 , prod(nil()) -> s(0()) 755.80/297.05 , prod(cons(x, l)) -> *(x, prod(l)) } 755.80/297.05 Obligation: 755.80/297.05 innermost runtime complexity 755.80/297.05 Answer: 755.80/297.05 MAYBE 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'Best' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 755.80/297.05 following reason: 755.80/297.05 755.80/297.05 Computation stopped due to timeout after 297.0 seconds. 755.80/297.05 755.80/297.05 2) 'Best' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 755.80/297.05 seconds)' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'Fastest' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'empty' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 2) 'With Problem ...' failed due to the following reason: 755.80/297.05 755.80/297.05 Empty strict component of the problem is NOT empty. 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 2) 'Best' failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 755.80/297.05 following reason: 755.80/297.05 755.80/297.05 The input cannot be shown compatible 755.80/297.05 755.80/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 755.80/297.05 to the following reason: 755.80/297.05 755.80/297.05 The input cannot be shown compatible 755.80/297.05 755.80/297.05 755.80/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 755.80/297.05 failed due to the following reason: 755.80/297.05 755.80/297.05 None of the processors succeeded. 755.80/297.05 755.80/297.05 Details of failed attempt(s): 755.80/297.05 ----------------------------- 755.80/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 755.80/297.05 failed due to the following reason: 755.80/297.05 755.80/297.05 match-boundness of the problem could not be verified. 755.80/297.05 755.80/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 755.80/297.05 failed due to the following reason: 755.80/297.05 755.80/297.05 match-boundness of the problem could not be verified. 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 755.80/297.05 Arrrr.. 755.94/297.17 EOF