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