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