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