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