MAYBE 807.63/297.03 MAYBE 807.63/297.03 807.63/297.03 We are left with following problem, upon which TcT provides the 807.63/297.03 certificate MAYBE. 807.63/297.03 807.63/297.03 Strict Trs: 807.63/297.03 { le(0(), y) -> true() 807.63/297.03 , le(s(x), 0()) -> false() 807.63/297.03 , le(s(x), s(y)) -> le(x, y) 807.63/297.03 , app(nil(), y) -> y 807.63/297.03 , app(add(n, x), y) -> add(n, app(x, y)) 807.63/297.03 , low(n, nil()) -> nil() 807.63/297.03 , low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 807.63/297.03 , if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 807.63/297.03 , if_low(false(), n, add(m, x)) -> low(n, x) 807.63/297.03 , high(n, nil()) -> nil() 807.63/297.03 , high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 807.63/297.03 , if_high(true(), n, add(m, x)) -> high(n, x) 807.63/297.03 , if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 807.63/297.03 , head(add(n, x)) -> n 807.63/297.03 , tail(add(n, x)) -> x 807.63/297.03 , isempty(nil()) -> true() 807.63/297.03 , isempty(add(n, x)) -> false() 807.63/297.03 , quicksort(x) -> 807.63/297.03 if_qs(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x))) 807.63/297.03 , if_qs(true(), x, n, y) -> nil() 807.63/297.03 , if_qs(false(), x, n, y) -> 807.63/297.03 app(quicksort(x), add(n, quicksort(y))) } 807.63/297.03 Obligation: 807.63/297.03 runtime complexity 807.63/297.03 Answer: 807.63/297.03 MAYBE 807.63/297.03 807.63/297.03 None of the processors succeeded. 807.63/297.03 807.63/297.03 Details of failed attempt(s): 807.63/297.03 ----------------------------- 807.63/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 807.63/297.03 following reason: 807.63/297.03 807.63/297.03 Computation stopped due to timeout after 297.0 seconds. 807.63/297.03 807.63/297.03 2) 'Best' failed due to the following reason: 807.63/297.03 807.63/297.03 None of the processors succeeded. 807.63/297.03 807.63/297.03 Details of failed attempt(s): 807.63/297.03 ----------------------------- 807.63/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 807.63/297.03 seconds)' failed due to the following reason: 807.63/297.03 807.63/297.03 Computation stopped due to timeout after 148.0 seconds. 807.63/297.03 807.63/297.03 2) 'Best' failed due to the following reason: 807.63/297.03 807.63/297.03 None of the processors succeeded. 807.63/297.03 807.63/297.03 Details of failed attempt(s): 807.63/297.03 ----------------------------- 807.63/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 807.63/297.03 following reason: 807.63/297.03 807.63/297.03 The processor is inapplicable, reason: 807.63/297.03 Processor only applicable for innermost runtime complexity analysis 807.63/297.03 807.63/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 807.63/297.03 to the following reason: 807.63/297.03 807.63/297.03 The processor is inapplicable, reason: 807.63/297.03 Processor only applicable for innermost runtime complexity analysis 807.63/297.03 807.63/297.03 807.63/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 807.63/297.03 failed due to the following reason: 807.63/297.03 807.63/297.03 None of the processors succeeded. 807.63/297.03 807.63/297.03 Details of failed attempt(s): 807.63/297.03 ----------------------------- 807.63/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 807.63/297.03 failed due to the following reason: 807.63/297.03 807.63/297.03 match-boundness of the problem could not be verified. 807.63/297.03 807.63/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 807.63/297.03 failed due to the following reason: 807.63/297.03 807.63/297.03 match-boundness of the problem could not be verified. 807.63/297.03 807.63/297.03 807.63/297.03 807.63/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 807.63/297.03 the following reason: 807.63/297.03 807.63/297.03 We add the following weak dependency pairs: 807.63/297.03 807.63/297.03 Strict DPs: 807.63/297.03 { le^#(0(), y) -> c_1() 807.63/297.03 , le^#(s(x), 0()) -> c_2() 807.63/297.03 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 807.63/297.03 , app^#(nil(), y) -> c_4(y) 807.63/297.03 , app^#(add(n, x), y) -> c_5(n, app^#(x, y)) 807.63/297.03 , low^#(n, nil()) -> c_6() 807.63/297.03 , low^#(n, add(m, x)) -> c_7(if_low^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_low^#(true(), n, add(m, x)) -> c_8(m, low^#(n, x)) 807.63/297.03 , if_low^#(false(), n, add(m, x)) -> c_9(low^#(n, x)) 807.63/297.03 , high^#(n, nil()) -> c_10() 807.63/297.03 , high^#(n, add(m, x)) -> c_11(if_high^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_high^#(true(), n, add(m, x)) -> c_12(high^#(n, x)) 807.63/297.03 , if_high^#(false(), n, add(m, x)) -> c_13(m, high^#(n, x)) 807.63/297.03 , head^#(add(n, x)) -> c_14(n) 807.63/297.03 , tail^#(add(n, x)) -> c_15(x) 807.63/297.03 , isempty^#(nil()) -> c_16() 807.63/297.03 , isempty^#(add(n, x)) -> c_17() 807.63/297.03 , quicksort^#(x) -> 807.63/297.03 c_18(if_qs^#(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x)))) 807.63/297.03 , if_qs^#(true(), x, n, y) -> c_19() 807.63/297.03 , if_qs^#(false(), x, n, y) -> 807.63/297.03 c_20(app^#(quicksort(x), add(n, quicksort(y)))) } 807.63/297.03 807.63/297.03 and mark the set of starting terms. 807.63/297.03 807.63/297.03 We are left with following problem, upon which TcT provides the 807.63/297.03 certificate MAYBE. 807.63/297.03 807.63/297.03 Strict DPs: 807.63/297.03 { le^#(0(), y) -> c_1() 807.63/297.03 , le^#(s(x), 0()) -> c_2() 807.63/297.03 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 807.63/297.03 , app^#(nil(), y) -> c_4(y) 807.63/297.03 , app^#(add(n, x), y) -> c_5(n, app^#(x, y)) 807.63/297.03 , low^#(n, nil()) -> c_6() 807.63/297.03 , low^#(n, add(m, x)) -> c_7(if_low^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_low^#(true(), n, add(m, x)) -> c_8(m, low^#(n, x)) 807.63/297.03 , if_low^#(false(), n, add(m, x)) -> c_9(low^#(n, x)) 807.63/297.03 , high^#(n, nil()) -> c_10() 807.63/297.03 , high^#(n, add(m, x)) -> c_11(if_high^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_high^#(true(), n, add(m, x)) -> c_12(high^#(n, x)) 807.63/297.03 , if_high^#(false(), n, add(m, x)) -> c_13(m, high^#(n, x)) 807.63/297.03 , head^#(add(n, x)) -> c_14(n) 807.63/297.03 , tail^#(add(n, x)) -> c_15(x) 807.63/297.03 , isempty^#(nil()) -> c_16() 807.63/297.03 , isempty^#(add(n, x)) -> c_17() 807.63/297.03 , quicksort^#(x) -> 807.63/297.03 c_18(if_qs^#(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x)))) 807.63/297.03 , if_qs^#(true(), x, n, y) -> c_19() 807.63/297.03 , if_qs^#(false(), x, n, y) -> 807.63/297.03 c_20(app^#(quicksort(x), add(n, quicksort(y)))) } 807.63/297.03 Strict Trs: 807.63/297.03 { le(0(), y) -> true() 807.63/297.03 , le(s(x), 0()) -> false() 807.63/297.03 , le(s(x), s(y)) -> le(x, y) 807.63/297.03 , app(nil(), y) -> y 807.63/297.03 , app(add(n, x), y) -> add(n, app(x, y)) 807.63/297.03 , low(n, nil()) -> nil() 807.63/297.03 , low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 807.63/297.03 , if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 807.63/297.03 , if_low(false(), n, add(m, x)) -> low(n, x) 807.63/297.03 , high(n, nil()) -> nil() 807.63/297.03 , high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 807.63/297.03 , if_high(true(), n, add(m, x)) -> high(n, x) 807.63/297.03 , if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 807.63/297.03 , head(add(n, x)) -> n 807.63/297.03 , tail(add(n, x)) -> x 807.63/297.03 , isempty(nil()) -> true() 807.63/297.03 , isempty(add(n, x)) -> false() 807.63/297.03 , quicksort(x) -> 807.63/297.03 if_qs(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x))) 807.63/297.03 , if_qs(true(), x, n, y) -> nil() 807.63/297.03 , if_qs(false(), x, n, y) -> 807.63/297.03 app(quicksort(x), add(n, quicksort(y))) } 807.63/297.03 Obligation: 807.63/297.03 runtime complexity 807.63/297.03 Answer: 807.63/297.03 MAYBE 807.63/297.03 807.63/297.03 We estimate the number of application of {1,2,6,10,16,17,19} by 807.63/297.03 applications of Pre({1,2,6,10,16,17,19}) = 807.63/297.03 {3,4,5,8,9,12,13,14,15,18}. Here rules are labeled as follows: 807.63/297.03 807.63/297.03 DPs: 807.63/297.03 { 1: le^#(0(), y) -> c_1() 807.63/297.03 , 2: le^#(s(x), 0()) -> c_2() 807.63/297.03 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 807.63/297.03 , 4: app^#(nil(), y) -> c_4(y) 807.63/297.03 , 5: app^#(add(n, x), y) -> c_5(n, app^#(x, y)) 807.63/297.03 , 6: low^#(n, nil()) -> c_6() 807.63/297.03 , 7: low^#(n, add(m, x)) -> c_7(if_low^#(le(m, n), n, add(m, x))) 807.63/297.03 , 8: if_low^#(true(), n, add(m, x)) -> c_8(m, low^#(n, x)) 807.63/297.03 , 9: if_low^#(false(), n, add(m, x)) -> c_9(low^#(n, x)) 807.63/297.03 , 10: high^#(n, nil()) -> c_10() 807.63/297.03 , 11: high^#(n, add(m, x)) -> 807.63/297.03 c_11(if_high^#(le(m, n), n, add(m, x))) 807.63/297.03 , 12: if_high^#(true(), n, add(m, x)) -> c_12(high^#(n, x)) 807.63/297.03 , 13: if_high^#(false(), n, add(m, x)) -> c_13(m, high^#(n, x)) 807.63/297.03 , 14: head^#(add(n, x)) -> c_14(n) 807.63/297.03 , 15: tail^#(add(n, x)) -> c_15(x) 807.63/297.03 , 16: isempty^#(nil()) -> c_16() 807.63/297.03 , 17: isempty^#(add(n, x)) -> c_17() 807.63/297.03 , 18: quicksort^#(x) -> 807.63/297.03 c_18(if_qs^#(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x)))) 807.63/297.03 , 19: if_qs^#(true(), x, n, y) -> c_19() 807.63/297.03 , 20: if_qs^#(false(), x, n, y) -> 807.63/297.03 c_20(app^#(quicksort(x), add(n, quicksort(y)))) } 807.63/297.03 807.63/297.03 We are left with following problem, upon which TcT provides the 807.63/297.03 certificate MAYBE. 807.63/297.03 807.63/297.03 Strict DPs: 807.63/297.03 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 807.63/297.03 , app^#(nil(), y) -> c_4(y) 807.63/297.03 , app^#(add(n, x), y) -> c_5(n, app^#(x, y)) 807.63/297.03 , low^#(n, add(m, x)) -> c_7(if_low^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_low^#(true(), n, add(m, x)) -> c_8(m, low^#(n, x)) 807.63/297.03 , if_low^#(false(), n, add(m, x)) -> c_9(low^#(n, x)) 807.63/297.03 , high^#(n, add(m, x)) -> c_11(if_high^#(le(m, n), n, add(m, x))) 807.63/297.03 , if_high^#(true(), n, add(m, x)) -> c_12(high^#(n, x)) 807.63/297.03 , if_high^#(false(), n, add(m, x)) -> c_13(m, high^#(n, x)) 807.63/297.03 , head^#(add(n, x)) -> c_14(n) 807.63/297.03 , tail^#(add(n, x)) -> c_15(x) 807.63/297.03 , quicksort^#(x) -> 807.63/297.03 c_18(if_qs^#(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x)))) 807.63/297.03 , if_qs^#(false(), x, n, y) -> 807.63/297.03 c_20(app^#(quicksort(x), add(n, quicksort(y)))) } 807.63/297.03 Strict Trs: 807.63/297.03 { le(0(), y) -> true() 807.63/297.03 , le(s(x), 0()) -> false() 807.63/297.03 , le(s(x), s(y)) -> le(x, y) 807.63/297.03 , app(nil(), y) -> y 807.63/297.03 , app(add(n, x), y) -> add(n, app(x, y)) 807.63/297.03 , low(n, nil()) -> nil() 807.63/297.03 , low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 807.63/297.03 , if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 807.63/297.03 , if_low(false(), n, add(m, x)) -> low(n, x) 807.63/297.03 , high(n, nil()) -> nil() 807.63/297.03 , high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 807.63/297.03 , if_high(true(), n, add(m, x)) -> high(n, x) 807.63/297.03 , if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 807.63/297.03 , head(add(n, x)) -> n 807.63/297.03 , tail(add(n, x)) -> x 807.63/297.03 , isempty(nil()) -> true() 807.63/297.03 , isempty(add(n, x)) -> false() 807.63/297.03 , quicksort(x) -> 807.63/297.03 if_qs(isempty(x), 807.63/297.03 low(head(x), tail(x)), 807.63/297.03 head(x), 807.63/297.03 high(head(x), tail(x))) 807.63/297.03 , if_qs(true(), x, n, y) -> nil() 807.63/297.03 , if_qs(false(), x, n, y) -> 807.63/297.03 app(quicksort(x), add(n, quicksort(y))) } 807.63/297.03 Weak DPs: 807.63/297.03 { le^#(0(), y) -> c_1() 807.63/297.03 , le^#(s(x), 0()) -> c_2() 807.63/297.03 , low^#(n, nil()) -> c_6() 807.63/297.03 , high^#(n, nil()) -> c_10() 807.63/297.03 , isempty^#(nil()) -> c_16() 807.63/297.03 , isempty^#(add(n, x)) -> c_17() 807.63/297.03 , if_qs^#(true(), x, n, y) -> c_19() } 807.63/297.03 Obligation: 807.63/297.03 runtime complexity 807.63/297.03 Answer: 807.63/297.03 MAYBE 807.63/297.03 807.63/297.03 Empty strict component of the problem is NOT empty. 807.63/297.03 807.63/297.03 807.63/297.03 Arrrr.. 807.85/297.21 EOF