MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , div(plus(x, y), z) -> plus(div(x, z), div(y, z)) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } 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) '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 2) '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 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: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), 0()) -> c_6() , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), 0()) -> c_10() , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y)) , div^#(plus(x, y), z) -> c_14(plus^#(div(x, z), div(y, z))) , ify^#(true(), x, y) -> c_15(if^#(ge(x, y), x, y)) , ify^#(false(), x, y) -> c_16() , if^#(true(), x, y) -> c_17(div^#(minus(x, y), y)) , if^#(false(), x, y) -> c_18() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), 0()) -> c_6() , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), 0()) -> c_10() , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y)) , div^#(plus(x, y), z) -> c_14(plus^#(div(x, z), div(y, z))) , ify^#(true(), x, y) -> c_15(if^#(ge(x, y), x, y)) , ify^#(false(), x, y) -> c_16() , if^#(true(), x, y) -> c_17(div^#(minus(x, y), y)) , if^#(false(), x, y) -> c_18() } Strict Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , div(plus(x, y), z) -> plus(div(x, z), div(y, z)) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,6,10,16,18} by applications of Pre({1,2,6,10,16,18}) = {3,4,5,7,8,9,11,12,13,14,15}. Here rules are labeled as follows: DPs: { 1: ge^#(0(), 0()) -> c_1() , 2: ge^#(0(), s(0())) -> c_2() , 3: ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , 4: ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , 5: ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , 6: minus^#(0(), 0()) -> c_6() , 7: minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , 8: minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , 9: minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , 10: plus^#(0(), 0()) -> c_10() , 11: plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , 12: plus^#(s(x), y) -> c_12(plus^#(x, y)) , 13: div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y)) , 14: div^#(plus(x, y), z) -> c_14(plus^#(div(x, z), div(y, z))) , 15: ify^#(true(), x, y) -> c_15(if^#(ge(x, y), x, y)) , 16: ify^#(false(), x, y) -> c_16() , 17: if^#(true(), x, y) -> c_17(div^#(minus(x, y), y)) , 18: if^#(false(), x, y) -> c_18() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y)) , div^#(plus(x, y), z) -> c_14(plus^#(div(x, z), div(y, z))) , ify^#(true(), x, y) -> c_15(if^#(ge(x, y), x, y)) , if^#(true(), x, y) -> c_17(div^#(minus(x, y), y)) } Strict Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , div(plus(x, y), z) -> plus(div(x, z), div(y, z)) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } Weak DPs: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , minus^#(0(), 0()) -> c_6() , plus^#(0(), 0()) -> c_10() , ify^#(false(), x, y) -> c_16() , if^#(false(), x, y) -> c_18() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..