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