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