MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(0(), x) -> x , plus(s(x), y) -> s(plus(x, y)) , times(0(), y) -> 0() , times(s(x), y) -> plus(y, times(x, y)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , tower(x, y) -> towerIter(0(), x, y, s(0())) , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) , help(true(), c, x, y, z) -> z , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: 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: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, Uargs(towerIter) = {4}, Uargs(help) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [plus](x1, x2) = [1] x2 + [7] [0] = [7] [s](x1) = [1] x1 + [7] [times](x1, x2) = [1] x2 + [7] [exp](x1, x2) = [1] x2 + [7] [ge](x1, x2) = [7] [true] = [7] [false] = [7] [tower](x1, x2) = [1] x1 + [1] x2 + [7] [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x4 + [1] [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x5 + [7] The following symbols are considered usable {plus, times, exp, ge, tower, towerIter, help} The order satisfies the following ordering constraints: [plus(0(), x)] = [1] x + [7] > [1] x + [0] = [x] [plus(s(x), y)] = [1] y + [7] ? [1] y + [14] = [s(plus(x, y))] [times(0(), y)] = [1] y + [7] >= [7] = [0()] [times(s(x), y)] = [1] y + [7] ? [1] y + [14] = [plus(y, times(x, y))] [exp(x, 0())] = [14] >= [14] = [s(0())] [exp(x, s(y))] = [1] y + [14] >= [1] y + [14] = [times(x, exp(x, y))] [ge(x, 0())] = [7] >= [7] = [true()] [ge(0(), s(x))] = [7] >= [7] = [false()] [ge(s(x), s(y))] = [7] >= [7] = [ge(x, y)] [tower(x, y)] = [1] x + [1] y + [7] ? [1] x + [15] = [towerIter(0(), x, y, s(0()))] [towerIter(c, x, y, z)] = [1] x + [1] z + [1] ? [1] x + [1] z + [14] = [help(ge(c, x), c, x, y, z)] [help(true(), c, x, y, z)] = [1] x + [1] z + [14] > [1] z + [0] = [z] [help(false(), c, x, y, z)] = [1] x + [1] z + [14] > [1] x + [1] z + [8] = [towerIter(s(c), x, y, exp(y, z))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(s(x), y) -> s(plus(x, y)) , times(0(), y) -> 0() , times(s(x), y) -> plus(y, times(x, y)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , tower(x, y) -> towerIter(0(), x, y, s(0())) , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } Weak Trs: { plus(0(), x) -> x , help(true(), c, x, y, z) -> z , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, Uargs(towerIter) = {4}, Uargs(help) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [plus](x1, x2) = [1] x2 + [7] [0] = [0] [s](x1) = [1] x1 + [0] [times](x1, x2) = [1] x2 + [7] [exp](x1, x2) = [1] x2 + [0] [ge](x1, x2) = [7] [true] = [3] [false] = [6] [tower](x1, x2) = [1] x1 + [1] x2 + [7] [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [1] [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [5] The following symbols are considered usable {plus, times, exp, ge, tower, towerIter, help} The order satisfies the following ordering constraints: [plus(0(), x)] = [1] x + [7] > [1] x + [0] = [x] [plus(s(x), y)] = [1] y + [7] >= [1] y + [7] = [s(plus(x, y))] [times(0(), y)] = [1] y + [7] > [0] = [0()] [times(s(x), y)] = [1] y + [7] ? [1] y + [14] = [plus(y, times(x, y))] [exp(x, 0())] = [0] >= [0] = [s(0())] [exp(x, s(y))] = [1] y + [0] ? [1] y + [7] = [times(x, exp(x, y))] [ge(x, 0())] = [7] > [3] = [true()] [ge(0(), s(x))] = [7] > [6] = [false()] [ge(s(x), s(y))] = [7] >= [7] = [ge(x, y)] [tower(x, y)] = [1] x + [1] y + [7] > [1] x + [1] y + [1] = [towerIter(0(), x, y, s(0()))] [towerIter(c, x, y, z)] = [1] x + [1] y + [1] z + [1] ? [1] x + [1] y + [1] z + [12] = [help(ge(c, x), c, x, y, z)] [help(true(), c, x, y, z)] = [1] x + [1] y + [1] z + [8] > [1] z + [0] = [z] [help(false(), c, x, y, z)] = [1] x + [1] y + [1] z + [11] > [1] x + [1] y + [1] z + [1] = [towerIter(s(c), x, y, exp(y, z))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(s(x), y) -> s(plus(x, y)) , times(s(x), y) -> plus(y, times(x, y)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , ge(s(x), s(y)) -> ge(x, y) , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } Weak Trs: { plus(0(), x) -> x , times(0(), y) -> 0() , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , tower(x, y) -> towerIter(0(), x, y, s(0())) , help(true(), c, x, y, z) -> z , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, Uargs(towerIter) = {4}, Uargs(help) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [plus](x1, x2) = [1] x2 + [4] [0] = [0] [s](x1) = [1] x1 + [0] [times](x1, x2) = [1] x2 + [0] [exp](x1, x2) = [1] [ge](x1, x2) = [1] [true] = [1] [false] = [1] [tower](x1, x2) = [1] x1 + [1] x2 + [7] [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [0] [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [0] The following symbols are considered usable {plus, times, exp, ge, tower, towerIter, help} The order satisfies the following ordering constraints: [plus(0(), x)] = [1] x + [4] > [1] x + [0] = [x] [plus(s(x), y)] = [1] y + [4] >= [1] y + [4] = [s(plus(x, y))] [times(0(), y)] = [1] y + [0] >= [0] = [0()] [times(s(x), y)] = [1] y + [0] ? [1] y + [4] = [plus(y, times(x, y))] [exp(x, 0())] = [1] > [0] = [s(0())] [exp(x, s(y))] = [1] >= [1] = [times(x, exp(x, y))] [ge(x, 0())] = [1] >= [1] = [true()] [ge(0(), s(x))] = [1] >= [1] = [false()] [ge(s(x), s(y))] = [1] >= [1] = [ge(x, y)] [tower(x, y)] = [1] x + [1] y + [7] > [1] x + [1] y + [0] = [towerIter(0(), x, y, s(0()))] [towerIter(c, x, y, z)] = [1] x + [1] y + [1] z + [0] ? [1] x + [1] y + [1] z + [1] = [help(ge(c, x), c, x, y, z)] [help(true(), c, x, y, z)] = [1] x + [1] y + [1] z + [1] > [1] z + [0] = [z] [help(false(), c, x, y, z)] = [1] x + [1] y + [1] z + [1] >= [1] x + [1] y + [1] = [towerIter(s(c), x, y, exp(y, z))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(s(x), y) -> s(plus(x, y)) , times(s(x), y) -> plus(y, times(x, y)) , exp(x, s(y)) -> times(x, exp(x, y)) , ge(s(x), s(y)) -> ge(x, y) , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } Weak Trs: { plus(0(), x) -> x , times(0(), y) -> 0() , exp(x, 0()) -> s(0()) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , tower(x, y) -> towerIter(0(), x, y, s(0())) , help(true(), c, x, y, z) -> z , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, Uargs(towerIter) = {4}, Uargs(help) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [plus](x1, x2) = [1] x2 + [4] [0] = [0] [s](x1) = [1] x1 + [5] [times](x1, x2) = [1] x2 + [1] [exp](x1, x2) = [1] x2 + [7] [ge](x1, x2) = [4] [true] = [4] [false] = [4] [tower](x1, x2) = [1] x1 + [1] x2 + [7] [towerIter](x1, x2, x3, x4) = [1] x3 + [1] x4 + [0] [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x4 + [1] x5 + [4] The following symbols are considered usable {plus, times, exp, ge, tower, towerIter, help} The order satisfies the following ordering constraints: [plus(0(), x)] = [1] x + [4] > [1] x + [0] = [x] [plus(s(x), y)] = [1] y + [4] ? [1] y + [9] = [s(plus(x, y))] [times(0(), y)] = [1] y + [1] > [0] = [0()] [times(s(x), y)] = [1] y + [1] ? [1] y + [5] = [plus(y, times(x, y))] [exp(x, 0())] = [7] > [5] = [s(0())] [exp(x, s(y))] = [1] y + [12] > [1] y + [8] = [times(x, exp(x, y))] [ge(x, 0())] = [4] >= [4] = [true()] [ge(0(), s(x))] = [4] >= [4] = [false()] [ge(s(x), s(y))] = [4] >= [4] = [ge(x, y)] [tower(x, y)] = [1] x + [1] y + [7] > [1] y + [5] = [towerIter(0(), x, y, s(0()))] [towerIter(c, x, y, z)] = [1] y + [1] z + [0] ? [1] y + [1] z + [8] = [help(ge(c, x), c, x, y, z)] [help(true(), c, x, y, z)] = [1] y + [1] z + [8] > [1] z + [0] = [z] [help(false(), c, x, y, z)] = [1] y + [1] z + [8] > [1] y + [1] z + [7] = [towerIter(s(c), x, y, exp(y, z))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(s(x), y) -> s(plus(x, y)) , times(s(x), y) -> plus(y, times(x, y)) , ge(s(x), s(y)) -> ge(x, y) , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } Weak Trs: { plus(0(), x) -> x , times(0(), y) -> 0() , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , tower(x, y) -> towerIter(0(), x, y, s(0())) , help(true(), c, x, y, z) -> z , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 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 input cannot be shown compatible 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 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. Arrrr..