MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs)))) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2(x) , max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, nil()) -> c_10() , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs)) , if2^#(true(), x, y, xs) -> c_12(xs) , if2^#(false(), x, y, xs) -> c_13(y, del^#(x, xs)) , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(nil()) -> c_18() , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(del(max(cons(x, xs)), cons(x, xs)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2(x) , max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, nil()) -> c_10() , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs)) , if2^#(true(), x, y, xs) -> c_12(xs) , if2^#(false(), x, y, xs) -> c_13(y, del^#(x, xs)) , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(nil()) -> c_18() , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(del(max(cons(x, xs)), cons(x, xs)))) } Strict Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs)))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,6,7,8,10,14,15,16,18} by applications of Pre({1,6,7,8,10,14,15,16,18}) = {2,9,12,13,17,19}. Here rules are labeled as follows: DPs: { 1: max^#(nil()) -> c_1() , 2: max^#(cons(x, nil())) -> c_2(x) , 3: max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs)) , 4: if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , 5: if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , 6: ge^#(0(), 0()) -> c_6() , 7: ge^#(0(), s(x)) -> c_7() , 8: ge^#(s(x), 0()) -> c_8() , 9: ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , 10: del^#(x, nil()) -> c_10() , 11: del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs)) , 12: if2^#(true(), x, y, xs) -> c_12(xs) , 13: if2^#(false(), x, y, xs) -> c_13(y, del^#(x, xs)) , 14: eq^#(0(), 0()) -> c_14() , 15: eq^#(0(), s(y)) -> c_15() , 16: eq^#(s(x), 0()) -> c_16() , 17: eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , 18: sort^#(nil()) -> c_18() , 19: sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(del(max(cons(x, xs)), cons(x, xs)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(cons(x, nil())) -> c_2(x) , max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs)) , if2^#(true(), x, y, xs) -> c_12(xs) , if2^#(false(), x, y, xs) -> c_13(y, del^#(x, xs)) , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(del(max(cons(x, xs)), cons(x, xs)))) } Strict Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs)))) } Weak DPs: { max^#(nil()) -> c_1() , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , del^#(x, nil()) -> c_10() , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , sort^#(nil()) -> c_18() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..