MAYBE 1010.49/297.02 MAYBE 1010.49/297.02 1010.49/297.02 We are left with following problem, upon which TcT provides the 1010.49/297.02 certificate MAYBE. 1010.49/297.02 1010.49/297.02 Strict Trs: 1010.49/297.02 { le(0(), Y) -> true() 1010.49/297.02 , le(s(X), 0()) -> false() 1010.49/297.02 , le(s(X), s(Y)) -> le(X, Y) 1010.49/297.02 , app(nil(), Y) -> Y 1010.49/297.02 , app(cons(N, L), Y) -> cons(N, app(L, Y)) 1010.49/297.02 , low(N, nil()) -> nil() 1010.49/297.02 , low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 1010.49/297.02 , iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 1010.49/297.02 , iflow(false(), N, cons(M, L)) -> low(N, L) 1010.49/297.02 , high(N, nil()) -> nil() 1010.49/297.02 , high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 1010.49/297.02 , ifhigh(true(), N, cons(M, L)) -> high(N, L) 1010.49/297.02 , ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 1010.49/297.02 , quicksort(nil()) -> nil() 1010.49/297.02 , quicksort(cons(N, L)) -> 1010.49/297.02 app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) } 1010.49/297.02 Obligation: 1010.49/297.02 innermost runtime complexity 1010.49/297.02 Answer: 1010.49/297.02 MAYBE 1010.49/297.02 1010.49/297.02 None of the processors succeeded. 1010.49/297.02 1010.49/297.02 Details of failed attempt(s): 1010.49/297.02 ----------------------------- 1010.49/297.02 1) 'empty' failed due to the following reason: 1010.49/297.02 1010.49/297.02 Empty strict component of the problem is NOT empty. 1010.49/297.02 1010.49/297.02 2) 'Best' failed due to the following reason: 1010.49/297.02 1010.49/297.02 None of the processors succeeded. 1010.49/297.02 1010.49/297.02 Details of failed attempt(s): 1010.49/297.02 ----------------------------- 1010.49/297.02 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1010.49/297.02 following reason: 1010.49/297.02 1010.49/297.02 Computation stopped due to timeout after 297.0 seconds. 1010.49/297.02 1010.49/297.02 2) 'Best' failed due to the following reason: 1010.49/297.02 1010.49/297.02 None of the processors succeeded. 1010.49/297.02 1010.49/297.02 Details of failed attempt(s): 1010.49/297.02 ----------------------------- 1010.49/297.02 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1010.49/297.02 seconds)' failed due to the following reason: 1010.49/297.02 1010.49/297.02 Computation stopped due to timeout after 148.0 seconds. 1010.49/297.02 1010.49/297.02 2) 'Best' failed due to the following reason: 1010.49/297.02 1010.49/297.02 None of the processors succeeded. 1010.49/297.02 1010.49/297.02 Details of failed attempt(s): 1010.49/297.02 ----------------------------- 1010.49/297.02 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1010.49/297.02 to the following reason: 1010.49/297.02 1010.49/297.02 The input cannot be shown compatible 1010.49/297.02 1010.49/297.02 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1010.49/297.02 following reason: 1010.49/297.02 1010.49/297.02 The input cannot be shown compatible 1010.49/297.02 1010.49/297.02 1010.49/297.02 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1010.49/297.02 failed due to the following reason: 1010.49/297.02 1010.49/297.02 None of the processors succeeded. 1010.49/297.02 1010.49/297.02 Details of failed attempt(s): 1010.49/297.02 ----------------------------- 1010.49/297.02 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1010.49/297.02 failed due to the following reason: 1010.49/297.02 1010.49/297.02 match-boundness of the problem could not be verified. 1010.49/297.02 1010.49/297.02 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1010.49/297.02 failed due to the following reason: 1010.49/297.02 1010.49/297.02 match-boundness of the problem could not be verified. 1010.49/297.02 1010.49/297.02 1010.49/297.02 1010.49/297.02 1010.49/297.02 1010.49/297.02 Arrrr.. 1010.70/297.25 EOF