MAYBE 1185.97/297.47 MAYBE 1185.97/297.47 1185.97/297.47 We are left with following problem, upon which TcT provides the 1185.97/297.47 certificate MAYBE. 1185.97/297.47 1185.97/297.47 Strict Trs: 1185.97/297.47 { bsort(nil()) -> nil() 1185.97/297.47 , bsort(.(x, y)) -> 1185.97/297.47 last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) 1185.97/297.47 , last(nil()) -> 0() 1185.97/297.47 , last(.(x, nil())) -> x 1185.97/297.47 , last(.(x, .(y, z))) -> last(.(y, z)) 1185.97/297.47 , bubble(nil()) -> nil() 1185.97/297.47 , bubble(.(x, nil())) -> .(x, nil()) 1185.97/297.47 , bubble(.(x, .(y, z))) -> 1185.97/297.47 if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) 1185.97/297.47 , butlast(nil()) -> nil() 1185.97/297.47 , butlast(.(x, nil())) -> nil() 1185.97/297.47 , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } 1185.97/297.47 Obligation: 1185.97/297.47 runtime complexity 1185.97/297.47 Answer: 1185.97/297.47 MAYBE 1185.97/297.47 1185.97/297.47 None of the processors succeeded. 1185.97/297.47 1185.97/297.47 Details of failed attempt(s): 1185.97/297.47 ----------------------------- 1185.97/297.47 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1185.97/297.47 following reason: 1185.97/297.47 1185.97/297.47 Computation stopped due to timeout after 297.0 seconds. 1185.97/297.47 1185.97/297.47 2) 'Best' failed due to the following reason: 1185.97/297.47 1185.97/297.47 None of the processors succeeded. 1185.97/297.47 1185.97/297.47 Details of failed attempt(s): 1185.97/297.47 ----------------------------- 1185.97/297.47 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1185.97/297.47 seconds)' failed due to the following reason: 1185.97/297.47 1185.97/297.47 Computation stopped due to timeout after 148.0 seconds. 1185.97/297.47 1185.97/297.47 2) 'Best' failed due to the following reason: 1185.97/297.47 1185.97/297.47 None of the processors succeeded. 1185.97/297.47 1185.97/297.47 Details of failed attempt(s): 1185.97/297.47 ----------------------------- 1185.97/297.47 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1185.97/297.47 following reason: 1185.97/297.47 1185.97/297.47 The processor is inapplicable, reason: 1185.97/297.47 Processor only applicable for innermost runtime complexity analysis 1185.97/297.47 1185.97/297.47 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1185.97/297.47 to the following reason: 1185.97/297.47 1185.97/297.47 The processor is inapplicable, reason: 1185.97/297.47 Processor only applicable for innermost runtime complexity analysis 1185.97/297.47 1185.97/297.47 1185.97/297.47 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1185.97/297.47 failed due to the following reason: 1185.97/297.47 1185.97/297.47 None of the processors succeeded. 1185.97/297.47 1185.97/297.47 Details of failed attempt(s): 1185.97/297.47 ----------------------------- 1185.97/297.47 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1185.97/297.47 failed due to the following reason: 1185.97/297.47 1185.97/297.47 match-boundness of the problem could not be verified. 1185.97/297.47 1185.97/297.47 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1185.97/297.47 failed due to the following reason: 1185.97/297.47 1185.97/297.47 match-boundness of the problem could not be verified. 1185.97/297.47 1185.97/297.47 1185.97/297.47 1185.97/297.47 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1185.97/297.47 the following reason: 1185.97/297.47 1185.97/297.47 We add the following weak dependency pairs: 1185.97/297.47 1185.97/297.47 Strict DPs: 1185.97/297.47 { bsort^#(nil()) -> c_1() 1185.97/297.47 , bsort^#(.(x, y)) -> 1185.97/297.47 c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) 1185.97/297.47 , last^#(nil()) -> c_3() 1185.97/297.47 , last^#(.(x, nil())) -> c_4(x) 1185.97/297.47 , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) 1185.97/297.47 , bubble^#(nil()) -> c_6() 1185.97/297.47 , bubble^#(.(x, nil())) -> c_7(x) 1185.97/297.47 , bubble^#(.(x, .(y, z))) -> 1185.97/297.47 c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) 1185.97/297.47 , butlast^#(nil()) -> c_9() 1185.97/297.47 , butlast^#(.(x, nil())) -> c_10() 1185.97/297.47 , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } 1185.97/297.47 1185.97/297.47 and mark the set of starting terms. 1185.97/297.47 1185.97/297.47 We are left with following problem, upon which TcT provides the 1185.97/297.47 certificate MAYBE. 1185.97/297.47 1185.97/297.47 Strict DPs: 1185.97/297.47 { bsort^#(nil()) -> c_1() 1185.97/297.47 , bsort^#(.(x, y)) -> 1185.97/297.47 c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) 1185.97/297.47 , last^#(nil()) -> c_3() 1185.97/297.47 , last^#(.(x, nil())) -> c_4(x) 1185.97/297.47 , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) 1185.97/297.47 , bubble^#(nil()) -> c_6() 1185.97/297.47 , bubble^#(.(x, nil())) -> c_7(x) 1185.97/297.47 , bubble^#(.(x, .(y, z))) -> 1185.97/297.47 c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) 1185.97/297.47 , butlast^#(nil()) -> c_9() 1185.97/297.47 , butlast^#(.(x, nil())) -> c_10() 1185.97/297.47 , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } 1185.97/297.47 Strict Trs: 1185.97/297.47 { bsort(nil()) -> nil() 1185.97/297.47 , bsort(.(x, y)) -> 1185.97/297.47 last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) 1185.97/297.47 , last(nil()) -> 0() 1185.97/297.47 , last(.(x, nil())) -> x 1185.97/297.47 , last(.(x, .(y, z))) -> last(.(y, z)) 1185.97/297.47 , bubble(nil()) -> nil() 1185.97/297.47 , bubble(.(x, nil())) -> .(x, nil()) 1185.97/297.47 , bubble(.(x, .(y, z))) -> 1185.97/297.47 if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) 1185.97/297.47 , butlast(nil()) -> nil() 1185.97/297.47 , butlast(.(x, nil())) -> nil() 1185.97/297.47 , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } 1185.97/297.47 Obligation: 1185.97/297.47 runtime complexity 1185.97/297.47 Answer: 1185.97/297.47 MAYBE 1185.97/297.47 1185.97/297.47 We estimate the number of application of {1,3,6,9,10} by 1185.97/297.47 applications of Pre({1,3,6,9,10}) = {4,7,8,11}. Here rules are 1185.97/297.47 labeled as follows: 1185.97/297.47 1185.97/297.47 DPs: 1185.97/297.47 { 1: bsort^#(nil()) -> c_1() 1185.97/297.47 , 2: bsort^#(.(x, y)) -> 1185.97/297.47 c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) 1185.97/297.47 , 3: last^#(nil()) -> c_3() 1185.97/297.47 , 4: last^#(.(x, nil())) -> c_4(x) 1185.97/297.47 , 5: last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) 1185.97/297.47 , 6: bubble^#(nil()) -> c_6() 1185.97/297.47 , 7: bubble^#(.(x, nil())) -> c_7(x) 1185.97/297.47 , 8: bubble^#(.(x, .(y, z))) -> 1185.97/297.47 c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) 1185.97/297.47 , 9: butlast^#(nil()) -> c_9() 1185.97/297.47 , 10: butlast^#(.(x, nil())) -> c_10() 1185.97/297.47 , 11: butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } 1185.97/297.47 1185.97/297.47 We are left with following problem, upon which TcT provides the 1185.97/297.47 certificate MAYBE. 1185.97/297.47 1185.97/297.47 Strict DPs: 1185.97/297.47 { bsort^#(.(x, y)) -> 1185.97/297.47 c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))) 1185.97/297.47 , last^#(.(x, nil())) -> c_4(x) 1185.97/297.47 , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z))) 1185.97/297.47 , bubble^#(.(x, nil())) -> c_7(x) 1185.97/297.47 , bubble^#(.(x, .(y, z))) -> 1185.97/297.47 c_8(x, y, y, bubble^#(.(x, z)), x, bubble^#(.(y, z))) 1185.97/297.47 , butlast^#(.(x, .(y, z))) -> c_11(x, butlast^#(.(y, z))) } 1185.97/297.47 Strict Trs: 1185.97/297.47 { bsort(nil()) -> nil() 1185.97/297.47 , bsort(.(x, y)) -> 1185.97/297.47 last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) 1185.97/297.47 , last(nil()) -> 0() 1185.97/297.47 , last(.(x, nil())) -> x 1185.97/297.47 , last(.(x, .(y, z))) -> last(.(y, z)) 1185.97/297.47 , bubble(nil()) -> nil() 1185.97/297.47 , bubble(.(x, nil())) -> .(x, nil()) 1185.97/297.47 , bubble(.(x, .(y, z))) -> 1185.97/297.47 if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) 1185.97/297.47 , butlast(nil()) -> nil() 1185.97/297.47 , butlast(.(x, nil())) -> nil() 1185.97/297.47 , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) } 1185.97/297.47 Weak DPs: 1185.97/297.47 { bsort^#(nil()) -> c_1() 1185.97/297.47 , last^#(nil()) -> c_3() 1185.97/297.47 , bubble^#(nil()) -> c_6() 1185.97/297.47 , butlast^#(nil()) -> c_9() 1185.97/297.47 , butlast^#(.(x, nil())) -> c_10() } 1185.97/297.47 Obligation: 1185.97/297.47 runtime complexity 1185.97/297.47 Answer: 1185.97/297.47 MAYBE 1185.97/297.47 1185.97/297.47 Empty strict component of the problem is NOT empty. 1185.97/297.47 1185.97/297.47 1185.97/297.47 Arrrr.. 1187.00/298.20 EOF