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