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