MAYBE 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 We are left with following problem, upon which TcT provides the 716.07/297.03 certificate MAYBE. 716.07/297.03 716.07/297.03 Strict Trs: 716.07/297.03 { plus(0(), x) -> x 716.07/297.03 , plus(s(x), y) -> s(plus(x, y)) 716.07/297.03 , times(0(), y) -> 0() 716.07/297.03 , times(s(x), y) -> plus(y, times(x, y)) 716.07/297.03 , exp(x, 0()) -> s(0()) 716.07/297.03 , exp(x, s(y)) -> times(x, exp(x, y)) 716.07/297.03 , ge(x, 0()) -> true() 716.07/297.03 , ge(0(), s(x)) -> false() 716.07/297.03 , ge(s(x), s(y)) -> ge(x, y) 716.07/297.03 , tower(x, y) -> towerIter(0(), x, y, s(0())) 716.07/297.03 , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) 716.07/297.03 , help(true(), c, x, y, z) -> z 716.07/297.03 , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } 716.07/297.03 Obligation: 716.07/297.03 innermost runtime complexity 716.07/297.03 Answer: 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'Best' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 716.07/297.03 following reason: 716.07/297.03 716.07/297.03 Computation stopped due to timeout after 297.0 seconds. 716.07/297.03 716.07/297.03 2) 'Best' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 716.07/297.03 seconds)' failed due to the following reason: 716.07/297.03 716.07/297.03 The weightgap principle applies (using the following nonconstant 716.07/297.03 growth matrix-interpretation) 716.07/297.03 716.07/297.03 The following argument positions are usable: 716.07/297.03 Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, 716.07/297.03 Uargs(towerIter) = {4}, Uargs(help) = {1} 716.07/297.03 716.07/297.03 TcT has computed the following matrix interpretation satisfying 716.07/297.03 not(EDA) and not(IDA(1)). 716.07/297.03 716.07/297.03 [plus](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [0] = [7] 716.07/297.03 716.07/297.03 [s](x1) = [1] x1 + [7] 716.07/297.03 716.07/297.03 [times](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [exp](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [ge](x1, x2) = [7] 716.07/297.03 716.07/297.03 [true] = [7] 716.07/297.03 716.07/297.03 [false] = [7] 716.07/297.03 716.07/297.03 [tower](x1, x2) = [1] x1 + [1] x2 + [7] 716.07/297.03 716.07/297.03 [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x4 + [1] 716.07/297.03 716.07/297.03 [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x5 + [7] 716.07/297.03 716.07/297.03 The order satisfies the following ordering constraints: 716.07/297.03 716.07/297.03 [plus(0(), x)] = [1] x + [7] 716.07/297.03 > [1] x + [0] 716.07/297.03 = [x] 716.07/297.03 716.07/297.03 [plus(s(x), y)] = [1] y + [7] 716.07/297.03 ? [1] y + [14] 716.07/297.03 = [s(plus(x, y))] 716.07/297.03 716.07/297.03 [times(0(), y)] = [1] y + [7] 716.07/297.03 >= [7] 716.07/297.03 = [0()] 716.07/297.03 716.07/297.03 [times(s(x), y)] = [1] y + [7] 716.07/297.03 ? [1] y + [14] 716.07/297.03 = [plus(y, times(x, y))] 716.07/297.03 716.07/297.03 [exp(x, 0())] = [14] 716.07/297.03 >= [14] 716.07/297.03 = [s(0())] 716.07/297.03 716.07/297.03 [exp(x, s(y))] = [1] y + [14] 716.07/297.03 >= [1] y + [14] 716.07/297.03 = [times(x, exp(x, y))] 716.07/297.03 716.07/297.03 [ge(x, 0())] = [7] 716.07/297.03 >= [7] 716.07/297.03 = [true()] 716.07/297.03 716.07/297.03 [ge(0(), s(x))] = [7] 716.07/297.03 >= [7] 716.07/297.03 = [false()] 716.07/297.03 716.07/297.03 [ge(s(x), s(y))] = [7] 716.07/297.03 >= [7] 716.07/297.03 = [ge(x, y)] 716.07/297.03 716.07/297.03 [tower(x, y)] = [1] x + [1] y + [7] 716.07/297.03 ? [1] x + [15] 716.07/297.03 = [towerIter(0(), x, y, s(0()))] 716.07/297.03 716.07/297.03 [towerIter(c, x, y, z)] = [1] x + [1] z + [1] 716.07/297.03 ? [1] x + [1] z + [14] 716.07/297.03 = [help(ge(c, x), c, x, y, z)] 716.07/297.03 716.07/297.03 [help(true(), c, x, y, z)] = [1] x + [1] z + [14] 716.07/297.03 > [1] z + [0] 716.07/297.03 = [z] 716.07/297.03 716.07/297.03 [help(false(), c, x, y, z)] = [1] x + [1] z + [14] 716.07/297.03 > [1] x + [1] z + [8] 716.07/297.03 = [towerIter(s(c), x, y, exp(y, z))] 716.07/297.03 716.07/297.03 716.07/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 716.07/297.03 716.07/297.03 We are left with following problem, upon which TcT provides the 716.07/297.03 certificate MAYBE. 716.07/297.03 716.07/297.03 Strict Trs: 716.07/297.03 { plus(s(x), y) -> s(plus(x, y)) 716.07/297.03 , times(0(), y) -> 0() 716.07/297.03 , times(s(x), y) -> plus(y, times(x, y)) 716.07/297.03 , exp(x, 0()) -> s(0()) 716.07/297.03 , exp(x, s(y)) -> times(x, exp(x, y)) 716.07/297.03 , ge(x, 0()) -> true() 716.07/297.03 , ge(0(), s(x)) -> false() 716.07/297.03 , ge(s(x), s(y)) -> ge(x, y) 716.07/297.03 , tower(x, y) -> towerIter(0(), x, y, s(0())) 716.07/297.03 , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } 716.07/297.03 Weak Trs: 716.07/297.03 { plus(0(), x) -> x 716.07/297.03 , help(true(), c, x, y, z) -> z 716.07/297.03 , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } 716.07/297.03 Obligation: 716.07/297.03 innermost runtime complexity 716.07/297.03 Answer: 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 The weightgap principle applies (using the following nonconstant 716.07/297.03 growth matrix-interpretation) 716.07/297.03 716.07/297.03 The following argument positions are usable: 716.07/297.03 Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, 716.07/297.03 Uargs(towerIter) = {4}, Uargs(help) = {1} 716.07/297.03 716.07/297.03 TcT has computed the following matrix interpretation satisfying 716.07/297.03 not(EDA) and not(IDA(1)). 716.07/297.03 716.07/297.03 [plus](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [0] = [0] 716.07/297.03 716.07/297.03 [s](x1) = [1] x1 + [0] 716.07/297.03 716.07/297.03 [times](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [exp](x1, x2) = [1] x2 + [0] 716.07/297.03 716.07/297.03 [ge](x1, x2) = [7] 716.07/297.03 716.07/297.03 [true] = [3] 716.07/297.03 716.07/297.03 [false] = [6] 716.07/297.03 716.07/297.03 [tower](x1, x2) = [1] x1 + [1] x2 + [7] 716.07/297.03 716.07/297.03 [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [1] 716.07/297.03 716.07/297.03 [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [5] 716.07/297.03 716.07/297.03 The order satisfies the following ordering constraints: 716.07/297.03 716.07/297.03 [plus(0(), x)] = [1] x + [7] 716.07/297.03 > [1] x + [0] 716.07/297.03 = [x] 716.07/297.03 716.07/297.03 [plus(s(x), y)] = [1] y + [7] 716.07/297.03 >= [1] y + [7] 716.07/297.03 = [s(plus(x, y))] 716.07/297.03 716.07/297.03 [times(0(), y)] = [1] y + [7] 716.07/297.03 > [0] 716.07/297.03 = [0()] 716.07/297.03 716.07/297.03 [times(s(x), y)] = [1] y + [7] 716.07/297.03 ? [1] y + [14] 716.07/297.03 = [plus(y, times(x, y))] 716.07/297.03 716.07/297.03 [exp(x, 0())] = [0] 716.07/297.03 >= [0] 716.07/297.03 = [s(0())] 716.07/297.03 716.07/297.03 [exp(x, s(y))] = [1] y + [0] 716.07/297.03 ? [1] y + [7] 716.07/297.03 = [times(x, exp(x, y))] 716.07/297.03 716.07/297.03 [ge(x, 0())] = [7] 716.07/297.03 > [3] 716.07/297.03 = [true()] 716.07/297.03 716.07/297.03 [ge(0(), s(x))] = [7] 716.07/297.03 > [6] 716.07/297.03 = [false()] 716.07/297.03 716.07/297.03 [ge(s(x), s(y))] = [7] 716.07/297.03 >= [7] 716.07/297.03 = [ge(x, y)] 716.07/297.03 716.07/297.03 [tower(x, y)] = [1] x + [1] y + [7] 716.07/297.03 > [1] x + [1] y + [1] 716.07/297.03 = [towerIter(0(), x, y, s(0()))] 716.07/297.03 716.07/297.03 [towerIter(c, x, y, z)] = [1] x + [1] y + [1] z + [1] 716.07/297.03 ? [1] x + [1] y + [1] z + [12] 716.07/297.03 = [help(ge(c, x), c, x, y, z)] 716.07/297.03 716.07/297.03 [help(true(), c, x, y, z)] = [1] x + [1] y + [1] z + [8] 716.07/297.03 > [1] z + [0] 716.07/297.03 = [z] 716.07/297.03 716.07/297.03 [help(false(), c, x, y, z)] = [1] x + [1] y + [1] z + [11] 716.07/297.03 > [1] x + [1] y + [1] z + [1] 716.07/297.03 = [towerIter(s(c), x, y, exp(y, z))] 716.07/297.03 716.07/297.03 716.07/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 716.07/297.03 716.07/297.03 We are left with following problem, upon which TcT provides the 716.07/297.03 certificate MAYBE. 716.07/297.03 716.07/297.03 Strict Trs: 716.07/297.03 { plus(s(x), y) -> s(plus(x, y)) 716.07/297.03 , times(s(x), y) -> plus(y, times(x, y)) 716.07/297.03 , exp(x, 0()) -> s(0()) 716.07/297.03 , exp(x, s(y)) -> times(x, exp(x, y)) 716.07/297.03 , ge(s(x), s(y)) -> ge(x, y) 716.07/297.03 , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } 716.07/297.03 Weak Trs: 716.07/297.03 { plus(0(), x) -> x 716.07/297.03 , times(0(), y) -> 0() 716.07/297.03 , ge(x, 0()) -> true() 716.07/297.03 , ge(0(), s(x)) -> false() 716.07/297.03 , tower(x, y) -> towerIter(0(), x, y, s(0())) 716.07/297.03 , help(true(), c, x, y, z) -> z 716.07/297.03 , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } 716.07/297.03 Obligation: 716.07/297.03 innermost runtime complexity 716.07/297.03 Answer: 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 The weightgap principle applies (using the following nonconstant 716.07/297.03 growth matrix-interpretation) 716.07/297.03 716.07/297.03 The following argument positions are usable: 716.07/297.03 Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, 716.07/297.03 Uargs(towerIter) = {4}, Uargs(help) = {1} 716.07/297.03 716.07/297.03 TcT has computed the following matrix interpretation satisfying 716.07/297.03 not(EDA) and not(IDA(1)). 716.07/297.03 716.07/297.03 [plus](x1, x2) = [1] x2 + [4] 716.07/297.03 716.07/297.03 [0] = [0] 716.07/297.03 716.07/297.03 [s](x1) = [1] x1 + [0] 716.07/297.03 716.07/297.03 [times](x1, x2) = [1] x2 + [0] 716.07/297.03 716.07/297.03 [exp](x1, x2) = [1] 716.07/297.03 716.07/297.03 [ge](x1, x2) = [1] 716.07/297.03 716.07/297.03 [true] = [1] 716.07/297.03 716.07/297.03 [false] = [1] 716.07/297.03 716.07/297.03 [tower](x1, x2) = [1] x1 + [1] x2 + [7] 716.07/297.03 716.07/297.03 [towerIter](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [0] 716.07/297.03 716.07/297.03 [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [0] 716.07/297.03 716.07/297.03 The order satisfies the following ordering constraints: 716.07/297.03 716.07/297.03 [plus(0(), x)] = [1] x + [4] 716.07/297.03 > [1] x + [0] 716.07/297.03 = [x] 716.07/297.03 716.07/297.03 [plus(s(x), y)] = [1] y + [4] 716.07/297.03 >= [1] y + [4] 716.07/297.03 = [s(plus(x, y))] 716.07/297.03 716.07/297.03 [times(0(), y)] = [1] y + [0] 716.07/297.03 >= [0] 716.07/297.03 = [0()] 716.07/297.03 716.07/297.03 [times(s(x), y)] = [1] y + [0] 716.07/297.03 ? [1] y + [4] 716.07/297.03 = [plus(y, times(x, y))] 716.07/297.03 716.07/297.03 [exp(x, 0())] = [1] 716.07/297.03 > [0] 716.07/297.03 = [s(0())] 716.07/297.03 716.07/297.03 [exp(x, s(y))] = [1] 716.07/297.03 >= [1] 716.07/297.03 = [times(x, exp(x, y))] 716.07/297.03 716.07/297.03 [ge(x, 0())] = [1] 716.07/297.03 >= [1] 716.07/297.03 = [true()] 716.07/297.03 716.07/297.03 [ge(0(), s(x))] = [1] 716.07/297.03 >= [1] 716.07/297.03 = [false()] 716.07/297.03 716.07/297.03 [ge(s(x), s(y))] = [1] 716.07/297.03 >= [1] 716.07/297.03 = [ge(x, y)] 716.07/297.03 716.07/297.03 [tower(x, y)] = [1] x + [1] y + [7] 716.07/297.03 > [1] x + [1] y + [0] 716.07/297.03 = [towerIter(0(), x, y, s(0()))] 716.07/297.03 716.07/297.03 [towerIter(c, x, y, z)] = [1] x + [1] y + [1] z + [0] 716.07/297.03 ? [1] x + [1] y + [1] z + [1] 716.07/297.03 = [help(ge(c, x), c, x, y, z)] 716.07/297.03 716.07/297.03 [help(true(), c, x, y, z)] = [1] x + [1] y + [1] z + [1] 716.07/297.03 > [1] z + [0] 716.07/297.03 = [z] 716.07/297.03 716.07/297.03 [help(false(), c, x, y, z)] = [1] x + [1] y + [1] z + [1] 716.07/297.03 >= [1] x + [1] y + [1] 716.07/297.03 = [towerIter(s(c), x, y, exp(y, z))] 716.07/297.03 716.07/297.03 716.07/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 716.07/297.03 716.07/297.03 We are left with following problem, upon which TcT provides the 716.07/297.03 certificate MAYBE. 716.07/297.03 716.07/297.03 Strict Trs: 716.07/297.03 { plus(s(x), y) -> s(plus(x, y)) 716.07/297.03 , times(s(x), y) -> plus(y, times(x, y)) 716.07/297.03 , exp(x, s(y)) -> times(x, exp(x, y)) 716.07/297.03 , ge(s(x), s(y)) -> ge(x, y) 716.07/297.03 , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } 716.07/297.03 Weak Trs: 716.07/297.03 { plus(0(), x) -> x 716.07/297.03 , times(0(), y) -> 0() 716.07/297.03 , exp(x, 0()) -> s(0()) 716.07/297.03 , ge(x, 0()) -> true() 716.07/297.03 , ge(0(), s(x)) -> false() 716.07/297.03 , tower(x, y) -> towerIter(0(), x, y, s(0())) 716.07/297.03 , help(true(), c, x, y, z) -> z 716.07/297.03 , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } 716.07/297.03 Obligation: 716.07/297.03 innermost runtime complexity 716.07/297.03 Answer: 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 The weightgap principle applies (using the following nonconstant 716.07/297.03 growth matrix-interpretation) 716.07/297.03 716.07/297.03 The following argument positions are usable: 716.07/297.03 Uargs(plus) = {2}, Uargs(s) = {1}, Uargs(times) = {2}, 716.07/297.03 Uargs(towerIter) = {4}, Uargs(help) = {1} 716.07/297.03 716.07/297.03 TcT has computed the following matrix interpretation satisfying 716.07/297.03 not(EDA) and not(IDA(1)). 716.07/297.03 716.07/297.03 [plus](x1, x2) = [1] x2 + [4] 716.07/297.03 716.07/297.03 [0] = [0] 716.07/297.03 716.07/297.03 [s](x1) = [1] x1 + [5] 716.07/297.03 716.07/297.03 [times](x1, x2) = [1] x2 + [1] 716.07/297.03 716.07/297.03 [exp](x1, x2) = [1] x2 + [7] 716.07/297.03 716.07/297.03 [ge](x1, x2) = [4] 716.07/297.03 716.07/297.03 [true] = [4] 716.07/297.03 716.07/297.03 [false] = [4] 716.07/297.03 716.07/297.03 [tower](x1, x2) = [1] x1 + [1] x2 + [7] 716.07/297.03 716.07/297.03 [towerIter](x1, x2, x3, x4) = [1] x3 + [1] x4 + [0] 716.07/297.03 716.07/297.03 [help](x1, x2, x3, x4, x5) = [1] x1 + [1] x4 + [1] x5 + [4] 716.07/297.03 716.07/297.03 The order satisfies the following ordering constraints: 716.07/297.03 716.07/297.03 [plus(0(), x)] = [1] x + [4] 716.07/297.03 > [1] x + [0] 716.07/297.03 = [x] 716.07/297.03 716.07/297.03 [plus(s(x), y)] = [1] y + [4] 716.07/297.03 ? [1] y + [9] 716.07/297.03 = [s(plus(x, y))] 716.07/297.03 716.07/297.03 [times(0(), y)] = [1] y + [1] 716.07/297.03 > [0] 716.07/297.03 = [0()] 716.07/297.03 716.07/297.03 [times(s(x), y)] = [1] y + [1] 716.07/297.03 ? [1] y + [5] 716.07/297.03 = [plus(y, times(x, y))] 716.07/297.03 716.07/297.03 [exp(x, 0())] = [7] 716.07/297.03 > [5] 716.07/297.03 = [s(0())] 716.07/297.03 716.07/297.03 [exp(x, s(y))] = [1] y + [12] 716.07/297.03 > [1] y + [8] 716.07/297.03 = [times(x, exp(x, y))] 716.07/297.03 716.07/297.03 [ge(x, 0())] = [4] 716.07/297.03 >= [4] 716.07/297.03 = [true()] 716.07/297.03 716.07/297.03 [ge(0(), s(x))] = [4] 716.07/297.03 >= [4] 716.07/297.03 = [false()] 716.07/297.03 716.07/297.03 [ge(s(x), s(y))] = [4] 716.07/297.03 >= [4] 716.07/297.03 = [ge(x, y)] 716.07/297.03 716.07/297.03 [tower(x, y)] = [1] x + [1] y + [7] 716.07/297.03 > [1] y + [5] 716.07/297.03 = [towerIter(0(), x, y, s(0()))] 716.07/297.03 716.07/297.03 [towerIter(c, x, y, z)] = [1] y + [1] z + [0] 716.07/297.03 ? [1] y + [1] z + [8] 716.07/297.03 = [help(ge(c, x), c, x, y, z)] 716.07/297.03 716.07/297.03 [help(true(), c, x, y, z)] = [1] y + [1] z + [8] 716.07/297.03 > [1] z + [0] 716.07/297.03 = [z] 716.07/297.03 716.07/297.03 [help(false(), c, x, y, z)] = [1] y + [1] z + [8] 716.07/297.03 > [1] y + [1] z + [7] 716.07/297.03 = [towerIter(s(c), x, y, exp(y, z))] 716.07/297.03 716.07/297.03 716.07/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 716.07/297.03 716.07/297.03 We are left with following problem, upon which TcT provides the 716.07/297.03 certificate MAYBE. 716.07/297.03 716.07/297.03 Strict Trs: 716.07/297.03 { plus(s(x), y) -> s(plus(x, y)) 716.07/297.03 , times(s(x), y) -> plus(y, times(x, y)) 716.07/297.03 , ge(s(x), s(y)) -> ge(x, y) 716.07/297.03 , towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z) } 716.07/297.03 Weak Trs: 716.07/297.03 { plus(0(), x) -> x 716.07/297.03 , times(0(), y) -> 0() 716.07/297.03 , exp(x, 0()) -> s(0()) 716.07/297.03 , exp(x, s(y)) -> times(x, exp(x, y)) 716.07/297.03 , ge(x, 0()) -> true() 716.07/297.03 , ge(0(), s(x)) -> false() 716.07/297.03 , tower(x, y) -> towerIter(0(), x, y, s(0())) 716.07/297.03 , help(true(), c, x, y, z) -> z 716.07/297.03 , help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z)) } 716.07/297.03 Obligation: 716.07/297.03 innermost runtime complexity 716.07/297.03 Answer: 716.07/297.03 MAYBE 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'Fastest' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'empty' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 2) 'With Problem ...' failed due to the following reason: 716.07/297.03 716.07/297.03 Empty strict component of the problem is NOT empty. 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 2) 'Best' failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 716.07/297.03 to the following reason: 716.07/297.03 716.07/297.03 The input cannot be shown compatible 716.07/297.03 716.07/297.03 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 716.07/297.03 following reason: 716.07/297.03 716.07/297.03 The input cannot be shown compatible 716.07/297.03 716.07/297.03 716.07/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 716.07/297.03 failed due to the following reason: 716.07/297.03 716.07/297.03 None of the processors succeeded. 716.07/297.03 716.07/297.03 Details of failed attempt(s): 716.07/297.03 ----------------------------- 716.07/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 716.07/297.03 failed due to the following reason: 716.07/297.03 716.07/297.03 match-boundness of the problem could not be verified. 716.07/297.03 716.07/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 716.07/297.03 failed due to the following reason: 716.07/297.03 716.07/297.03 match-boundness of the problem could not be verified. 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 716.07/297.03 Arrrr.. 716.29/297.20 EOF