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