MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { bsort(nil()) -> nil() , bsort(.(x, y)) -> last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) , last(nil()) -> 0() , last(.(x, nil())) -> x , last(.(x, .(y, z))) -> last(.(y, z)) , bubble(nil()) -> nil() , bubble(.(x, nil())) -> .(x, nil()) , bubble(.(x, .(y, z))) -> if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) , butlast(nil()) -> nil() , butlast(.(x, nil())) -> nil() , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } 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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 3) '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 perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { bsort^#(nil()) -> c_1() , bsort^#(.(x, y)) -> c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) , last^#(nil()) -> c_3() , last^#(.(x, nil())) -> c_4(x) , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) , bubble^#(nil()) -> c_6() , bubble^#(.(x, nil())) -> c_7(x) , bubble^#(.(x, .(y, z))) -> c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) , butlast^#(nil()) -> c_9() , butlast^#(.(x, nil())) -> c_10() , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { bsort^#(nil()) -> c_1() , bsort^#(.(x, y)) -> c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) , last^#(nil()) -> c_3() , last^#(.(x, nil())) -> c_4(x) , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) , bubble^#(nil()) -> c_6() , bubble^#(.(x, nil())) -> c_7(x) , bubble^#(.(x, .(y, z))) -> c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) , butlast^#(nil()) -> c_9() , butlast^#(.(x, nil())) -> c_10() , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } Strict Trs: { bsort(nil()) -> nil() , bsort(.(x, y)) -> last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) , last(nil()) -> 0() , last(.(x, nil())) -> x , last(.(x, .(y, z))) -> last(.(y, z)) , bubble(nil()) -> nil() , bubble(.(x, nil())) -> .(x, nil()) , bubble(.(x, .(y, z))) -> if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) , butlast(nil()) -> nil() , butlast(.(x, nil())) -> nil() , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,3,6,9,10} by applications of Pre({1,3,6,9,10}) = {4,7,8,11}. Here rules are labeled as follows: DPs: { 1: bsort^#(nil()) -> c_1() , 2: bsort^#(.(x, y)) -> c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) , 3: last^#(nil()) -> c_3() , 4: last^#(.(x, nil())) -> c_4(x) , 5: last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) , 6: bubble^#(nil()) -> c_6() , 7: bubble^#(.(x, nil())) -> c_7(x) , 8: bubble^#(.(x, .(y, z))) -> c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) , 9: butlast^#(nil()) -> c_9() , 10: butlast^#(.(x, nil())) -> c_10() , 11: butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { bsort^#(.(x, y)) -> c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) , last^#(.(x, nil())) -> c_4(x) , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) , bubble^#(.(x, nil())) -> c_7(x) , bubble^#(.(x, .(y, z))) -> c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } Strict Trs: { bsort(nil()) -> nil() , bsort(.(x, y)) -> last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) , last(nil()) -> 0() , last(.(x, nil())) -> x , last(.(x, .(y, z))) -> last(.(y, z)) , bubble(nil()) -> nil() , bubble(.(x, nil())) -> .(x, nil()) , bubble(.(x, .(y, z))) -> if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) , butlast(nil()) -> nil() , butlast(.(x, nil())) -> nil() , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } Weak DPs: { bsort^#(nil()) -> c_1() , last^#(nil()) -> c_3() , bubble^#(nil()) -> c_6() , butlast^#(nil()) -> c_9() , butlast^#(.(x, nil())) -> c_10() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..