MAYBE 1023.58/297.04 MAYBE 1023.58/297.04 1023.58/297.04 We are left with following problem, upon which TcT provides the 1023.58/297.04 certificate MAYBE. 1023.58/297.04 1023.58/297.04 Strict Trs: 1023.58/297.04 { average(x, y) -> if(ge(x, y), x, y) 1023.58/297.04 , if(true(), x, y) -> averIter(y, x, y) 1023.58/297.04 , if(false(), x, y) -> averIter(x, y, x) 1023.58/297.04 , ge(x, 0()) -> true() 1023.58/297.04 , ge(s(x), s(y)) -> ge(x, y) 1023.58/297.04 , ge(0(), s(y)) -> false() 1023.58/297.04 , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) 1023.58/297.04 , ifIter(true(), x, y, z) -> z 1023.58/297.04 , ifIter(false(), x, y, z) -> 1023.58/297.04 averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) 1023.58/297.04 , plus(s(x), y) -> s(plus(x, y)) 1023.58/297.04 , plus(0(), y) -> y 1023.58/297.04 , append(nil(), y) -> y 1023.58/297.04 , append(cons(n, x), y) -> cons(n, app(x, y)) 1023.58/297.04 , low(n, nil()) -> nil() 1023.58/297.04 , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) 1023.58/297.04 , if_low(true(), n, cons(m, x)) -> low(n, x) 1023.58/297.04 , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) 1023.58/297.04 , high(n, nil()) -> nil() 1023.58/297.04 , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) 1023.58/297.04 , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) 1023.58/297.04 , if_high(false(), n, cons(m, x)) -> high(n, x) 1023.58/297.04 , quicksort(x) -> ifquick(isempty(x), x) 1023.58/297.04 , ifquick(true(), x) -> nil() 1023.58/297.04 , ifquick(false(), x) -> 1023.58/297.04 append(quicksort(low(head(x), tail(x))), 1023.58/297.04 cons(tail(x), quicksort(high(head(x), tail(x))))) 1023.58/297.04 , isempty(nil()) -> true() 1023.58/297.04 , isempty(cons(n, x)) -> false() 1023.58/297.04 , head(nil()) -> error() 1023.58/297.04 , head(cons(n, x)) -> n 1023.58/297.04 , tail(nil()) -> nil() 1023.58/297.04 , tail(cons(n, x)) -> x 1023.58/297.04 , a() -> b() 1023.58/297.04 , a() -> c() } 1023.58/297.04 Obligation: 1023.58/297.04 innermost runtime complexity 1023.58/297.04 Answer: 1023.58/297.04 MAYBE 1023.58/297.04 1023.58/297.04 None of the processors succeeded. 1023.58/297.04 1023.58/297.04 Details of failed attempt(s): 1023.58/297.04 ----------------------------- 1023.58/297.04 1) 'empty' failed due to the following reason: 1023.58/297.04 1023.58/297.04 Empty strict component of the problem is NOT empty. 1023.58/297.04 1023.58/297.04 2) 'Best' failed due to the following reason: 1023.58/297.04 1023.58/297.04 None of the processors succeeded. 1023.58/297.04 1023.58/297.04 Details of failed attempt(s): 1023.58/297.04 ----------------------------- 1023.58/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1023.58/297.04 following reason: 1023.58/297.04 1023.58/297.04 Computation stopped due to timeout after 297.0 seconds. 1023.58/297.04 1023.58/297.04 2) 'Best' failed due to the following reason: 1023.58/297.04 1023.58/297.04 None of the processors succeeded. 1023.58/297.04 1023.58/297.04 Details of failed attempt(s): 1023.58/297.04 ----------------------------- 1023.58/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1023.58/297.04 seconds)' failed due to the following reason: 1023.58/297.04 1023.58/297.04 Computation stopped due to timeout after 148.0 seconds. 1023.58/297.04 1023.58/297.04 2) 'Best' failed due to the following reason: 1023.58/297.04 1023.58/297.04 None of the processors succeeded. 1023.58/297.04 1023.58/297.04 Details of failed attempt(s): 1023.58/297.04 ----------------------------- 1023.58/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1023.58/297.04 following reason: 1023.58/297.04 1023.58/297.04 The input cannot be shown compatible 1023.58/297.04 1023.58/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1023.58/297.04 to the following reason: 1023.58/297.04 1023.58/297.04 The input cannot be shown compatible 1023.58/297.04 1023.58/297.04 1023.58/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1023.58/297.04 failed due to the following reason: 1023.58/297.04 1023.58/297.04 None of the processors succeeded. 1023.58/297.04 1023.58/297.04 Details of failed attempt(s): 1023.58/297.04 ----------------------------- 1023.58/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1023.58/297.04 failed due to the following reason: 1023.58/297.04 1023.58/297.04 match-boundness of the problem could not be verified. 1023.58/297.04 1023.58/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1023.58/297.04 failed due to the following reason: 1023.58/297.04 1023.58/297.04 match-boundness of the problem could not be verified. 1023.58/297.04 1023.58/297.04 1023.58/297.04 1023.58/297.04 1023.58/297.04 1023.58/297.04 Arrrr.. 1023.96/297.30 EOF