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