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