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