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