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