MAYBE 803.69/297.02 MAYBE 803.69/297.02 803.69/297.02 We are left with following problem, upon which TcT provides the 803.69/297.02 certificate MAYBE. 803.69/297.02 803.69/297.02 Strict Trs: 803.69/297.02 { tower(x) -> f(a(), x, s(0())) 803.69/297.02 , f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.02 , f(a(), 0(), y) -> y 803.69/297.02 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.02 , half(s(s(x))) -> s(half(x)) 803.69/297.02 , half(s(0())) -> half(0()) 803.69/297.02 , half(0()) -> double(0()) 803.69/297.02 , exp(s(x)) -> double(exp(x)) 803.69/297.02 , exp(0()) -> s(0()) 803.69/297.02 , double(s(x)) -> s(s(double(x))) 803.69/297.02 , double(0()) -> 0() } 803.69/297.02 Obligation: 803.69/297.02 innermost runtime complexity 803.69/297.02 Answer: 803.69/297.02 MAYBE 803.69/297.02 803.69/297.02 None of the processors succeeded. 803.69/297.02 803.69/297.02 Details of failed attempt(s): 803.69/297.02 ----------------------------- 803.69/297.02 1) 'empty' failed due to the following reason: 803.69/297.02 803.69/297.02 Empty strict component of the problem is NOT empty. 803.69/297.02 803.69/297.02 2) 'Best' failed due to the following reason: 803.69/297.02 803.69/297.02 None of the processors succeeded. 803.69/297.02 803.69/297.02 Details of failed attempt(s): 803.69/297.02 ----------------------------- 803.69/297.02 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 803.69/297.02 following reason: 803.69/297.02 803.69/297.02 Computation stopped due to timeout after 297.0 seconds. 803.69/297.02 803.69/297.02 2) 'Best' failed due to the following reason: 803.69/297.02 803.69/297.02 None of the processors succeeded. 803.69/297.02 803.69/297.02 Details of failed attempt(s): 803.69/297.02 ----------------------------- 803.69/297.02 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 803.69/297.02 seconds)' failed due to the following reason: 803.69/297.02 803.69/297.02 The weightgap principle applies (using the following nonconstant 803.69/297.02 growth matrix-interpretation) 803.69/297.02 803.69/297.02 The following argument positions are usable: 803.69/297.02 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.02 803.69/297.02 TcT has computed the following matrix interpretation satisfying 803.69/297.02 not(EDA) and not(IDA(1)). 803.69/297.02 803.69/297.02 [tower](x1) = [1] x1 + [7] 803.69/297.02 803.69/297.02 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.02 803.69/297.02 [a] = [0] 803.69/297.02 803.69/297.02 [s](x1) = [1] x1 + [0] 803.69/297.02 803.69/297.02 [0] = [0] 803.69/297.02 803.69/297.02 [b] = [0] 803.69/297.02 803.69/297.02 [half](x1) = [0] 803.69/297.02 803.69/297.02 [exp](x1) = [0] 803.69/297.02 803.69/297.02 [double](x1) = [1] x1 + [0] 803.69/297.02 803.69/297.02 The order satisfies the following ordering constraints: 803.69/297.02 803.69/297.02 [tower(x)] = [1] x + [7] 803.69/297.02 > [1] x + [0] 803.69/297.02 = [f(a(), x, s(0()))] 803.69/297.02 803.69/297.02 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.02 >= [1] x + [1] y + [0] 803.69/297.02 = [f(b(), y, s(x))] 803.69/297.02 803.69/297.02 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.02 >= [1] y + [0] 803.69/297.02 = [y] 803.69/297.02 803.69/297.02 [f(b(), y, x)] = [1] x + [1] y + [0] 803.69/297.02 >= [0] 803.69/297.02 = [f(a(), half(x), exp(y))] 803.69/297.02 803.69/297.02 [half(s(s(x)))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [s(half(x))] 803.69/297.02 803.69/297.02 [half(s(0()))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [half(0())] 803.69/297.02 803.69/297.02 [half(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [double(0())] 803.69/297.02 803.69/297.02 [exp(s(x))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [double(exp(x))] 803.69/297.02 803.69/297.02 [exp(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [s(0())] 803.69/297.02 803.69/297.02 [double(s(x))] = [1] x + [0] 803.69/297.02 >= [1] x + [0] 803.69/297.02 = [s(s(double(x)))] 803.69/297.02 803.69/297.02 [double(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [0()] 803.69/297.02 803.69/297.02 803.69/297.02 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.02 803.69/297.02 We are left with following problem, upon which TcT provides the 803.69/297.02 certificate MAYBE. 803.69/297.02 803.69/297.02 Strict Trs: 803.69/297.02 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.02 , f(a(), 0(), y) -> y 803.69/297.02 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.02 , half(s(s(x))) -> s(half(x)) 803.69/297.02 , half(s(0())) -> half(0()) 803.69/297.02 , half(0()) -> double(0()) 803.69/297.02 , exp(s(x)) -> double(exp(x)) 803.69/297.02 , exp(0()) -> s(0()) 803.69/297.02 , double(s(x)) -> s(s(double(x))) 803.69/297.02 , double(0()) -> 0() } 803.69/297.02 Weak Trs: { tower(x) -> f(a(), x, s(0())) } 803.69/297.02 Obligation: 803.69/297.02 innermost runtime complexity 803.69/297.02 Answer: 803.69/297.02 MAYBE 803.69/297.02 803.69/297.02 The weightgap principle applies (using the following nonconstant 803.69/297.02 growth matrix-interpretation) 803.69/297.02 803.69/297.02 The following argument positions are usable: 803.69/297.02 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.02 803.69/297.02 TcT has computed the following matrix interpretation satisfying 803.69/297.02 not(EDA) and not(IDA(1)). 803.69/297.02 803.69/297.02 [tower](x1) = [1] x1 + [7] 803.69/297.02 803.69/297.02 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.02 803.69/297.02 [a] = [0] 803.69/297.02 803.69/297.02 [s](x1) = [1] x1 + [0] 803.69/297.02 803.69/297.02 [0] = [0] 803.69/297.02 803.69/297.02 [b] = [4] 803.69/297.02 803.69/297.02 [half](x1) = [0] 803.69/297.02 803.69/297.02 [exp](x1) = [0] 803.69/297.02 803.69/297.02 [double](x1) = [1] x1 + [0] 803.69/297.02 803.69/297.02 The order satisfies the following ordering constraints: 803.69/297.02 803.69/297.02 [tower(x)] = [1] x + [7] 803.69/297.02 > [1] x + [0] 803.69/297.02 = [f(a(), x, s(0()))] 803.69/297.02 803.69/297.02 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.02 ? [1] x + [1] y + [4] 803.69/297.02 = [f(b(), y, s(x))] 803.69/297.02 803.69/297.02 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.02 >= [1] y + [0] 803.69/297.02 = [y] 803.69/297.02 803.69/297.02 [f(b(), y, x)] = [1] x + [1] y + [4] 803.69/297.02 > [0] 803.69/297.02 = [f(a(), half(x), exp(y))] 803.69/297.02 803.69/297.02 [half(s(s(x)))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [s(half(x))] 803.69/297.02 803.69/297.02 [half(s(0()))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [half(0())] 803.69/297.02 803.69/297.02 [half(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [double(0())] 803.69/297.02 803.69/297.02 [exp(s(x))] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [double(exp(x))] 803.69/297.02 803.69/297.02 [exp(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [s(0())] 803.69/297.02 803.69/297.02 [double(s(x))] = [1] x + [0] 803.69/297.02 >= [1] x + [0] 803.69/297.02 = [s(s(double(x)))] 803.69/297.02 803.69/297.02 [double(0())] = [0] 803.69/297.02 >= [0] 803.69/297.02 = [0()] 803.69/297.02 803.69/297.02 803.69/297.02 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.02 803.69/297.02 We are left with following problem, upon which TcT provides the 803.69/297.02 certificate MAYBE. 803.69/297.02 803.69/297.02 Strict Trs: 803.69/297.02 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.02 , f(a(), 0(), y) -> y 803.69/297.02 , half(s(s(x))) -> s(half(x)) 803.69/297.02 , half(s(0())) -> half(0()) 803.69/297.02 , half(0()) -> double(0()) 803.69/297.02 , exp(s(x)) -> double(exp(x)) 803.69/297.02 , exp(0()) -> s(0()) 803.69/297.02 , double(s(x)) -> s(s(double(x))) 803.69/297.02 , double(0()) -> 0() } 803.69/297.02 Weak Trs: 803.69/297.02 { tower(x) -> f(a(), x, s(0())) 803.69/297.02 , f(b(), y, x) -> f(a(), half(x), exp(y)) } 803.69/297.02 Obligation: 803.69/297.02 innermost runtime complexity 803.69/297.02 Answer: 803.69/297.02 MAYBE 803.69/297.02 803.69/297.02 The weightgap principle applies (using the following nonconstant 803.69/297.02 growth matrix-interpretation) 803.69/297.02 803.69/297.02 The following argument positions are usable: 803.69/297.02 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.02 803.69/297.02 TcT has computed the following matrix interpretation satisfying 803.69/297.02 not(EDA) and not(IDA(1)). 803.69/297.02 803.69/297.02 [tower](x1) = [1] x1 + [7] 803.69/297.02 803.69/297.02 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.02 803.69/297.02 [a] = [0] 803.69/297.02 803.69/297.02 [s](x1) = [1] x1 + [0] 803.69/297.02 803.69/297.02 [0] = [1] 803.69/297.02 803.69/297.02 [b] = [0] 803.69/297.02 803.69/297.02 [half](x1) = [0] 803.69/297.03 803.69/297.03 [exp](x1) = [0] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [1] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.03 >= [1] x + [1] y + [0] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [1] 803.69/297.03 > [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [0] 803.69/297.03 >= [0] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [0] 803.69/297.03 ? [1] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [0] 803.69/297.03 ? [1] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [0] 803.69/297.03 >= [1] x + [0] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , exp(0()) -> s(0()) 803.69/297.03 , double(s(x)) -> s(s(double(x))) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 The weightgap principle applies (using the following nonconstant 803.69/297.03 growth matrix-interpretation) 803.69/297.03 803.69/297.03 The following argument positions are usable: 803.69/297.03 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.03 803.69/297.03 TcT has computed the following matrix interpretation satisfying 803.69/297.03 not(EDA) and not(IDA(1)). 803.69/297.03 803.69/297.03 [tower](x1) = [1] x1 + [7] 803.69/297.03 803.69/297.03 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.03 803.69/297.03 [a] = [0] 803.69/297.03 803.69/297.03 [s](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 [0] = [0] 803.69/297.03 803.69/297.03 [b] = [1] 803.69/297.03 803.69/297.03 [half](x1) = [0] 803.69/297.03 803.69/297.03 [exp](x1) = [1] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [0] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.03 ? [1] x + [1] y + [1] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.03 >= [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [1] 803.69/297.03 >= [1] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [1] 803.69/297.03 > [0] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [0] 803.69/297.03 >= [1] x + [0] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , double(s(x)) -> s(s(double(x))) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.03 , exp(0()) -> s(0()) } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 The weightgap principle applies (using the following nonconstant 803.69/297.03 growth matrix-interpretation) 803.69/297.03 803.69/297.03 The following argument positions are usable: 803.69/297.03 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.03 803.69/297.03 TcT has computed the following matrix interpretation satisfying 803.69/297.03 not(EDA) and not(IDA(1)). 803.69/297.03 803.69/297.03 [tower](x1) = [1] x1 + [7] 803.69/297.03 803.69/297.03 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.03 803.69/297.03 [a] = [0] 803.69/297.03 803.69/297.03 [s](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 [0] = [0] 803.69/297.03 803.69/297.03 [b] = [4] 803.69/297.03 803.69/297.03 [half](x1) = [1] 803.69/297.03 803.69/297.03 [exp](x1) = [0] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [0] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.03 ? [1] x + [1] y + [4] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.03 >= [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [4] 803.69/297.03 > [1] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [1] 803.69/297.03 > [0] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [0] 803.69/297.03 >= [1] x + [0] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , double(s(x)) -> s(s(double(x))) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(0()) -> s(0()) } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 The weightgap principle applies (using the following nonconstant 803.69/297.03 growth matrix-interpretation) 803.69/297.03 803.69/297.03 The following argument positions are usable: 803.69/297.03 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.03 803.69/297.03 TcT has computed the following matrix interpretation satisfying 803.69/297.03 not(EDA) and not(IDA(1)). 803.69/297.03 803.69/297.03 [tower](x1) = [1] x1 + [7] 803.69/297.03 803.69/297.03 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.03 803.69/297.03 [a] = [0] 803.69/297.03 803.69/297.03 [s](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 [0] = [0] 803.69/297.03 803.69/297.03 [b] = [1] 803.69/297.03 803.69/297.03 [half](x1) = [1] 803.69/297.03 803.69/297.03 [exp](x1) = [0] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [1] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [0] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [0] 803.69/297.03 ? [1] x + [1] y + [1] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.03 >= [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [1] 803.69/297.03 >= [1] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [0] 803.69/297.03 ? [1] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [1] 803.69/297.03 >= [1] x + [1] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [1] 803.69/297.03 > [0] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , double(s(x)) -> s(s(double(x))) } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(0()) -> s(0()) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 The weightgap principle applies (using the following nonconstant 803.69/297.03 growth matrix-interpretation) 803.69/297.03 803.69/297.03 The following argument positions are usable: 803.69/297.03 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.03 803.69/297.03 TcT has computed the following matrix interpretation satisfying 803.69/297.03 not(EDA) and not(IDA(1)). 803.69/297.03 803.69/297.03 [tower](x1) = [1] x1 + [7] 803.69/297.03 803.69/297.03 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.03 803.69/297.03 [a] = [2] 803.69/297.03 803.69/297.03 [s](x1) = [1] x1 + [2] 803.69/297.03 803.69/297.03 [0] = [0] 803.69/297.03 803.69/297.03 [b] = [4] 803.69/297.03 803.69/297.03 [half](x1) = [0] 803.69/297.03 803.69/297.03 [exp](x1) = [1] x1 + [2] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [4] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [4] 803.69/297.03 ? [1] x + [1] y + [6] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [2] 803.69/297.03 > [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [4] 803.69/297.03 >= [1] y + [4] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [0] 803.69/297.03 ? [2] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [1] x + [4] 803.69/297.03 > [1] x + [2] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [2] 803.69/297.03 >= [2] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [2] 803.69/297.03 ? [1] x + [4] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , double(s(x)) -> s(s(double(x))) } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , exp(0()) -> s(0()) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 The weightgap principle applies (using the following nonconstant 803.69/297.03 growth matrix-interpretation) 803.69/297.03 803.69/297.03 The following argument positions are usable: 803.69/297.03 Uargs(f) = {2, 3}, Uargs(s) = {1}, Uargs(double) = {1} 803.69/297.03 803.69/297.03 TcT has computed the following matrix interpretation satisfying 803.69/297.03 not(EDA) and not(IDA(1)). 803.69/297.03 803.69/297.03 [tower](x1) = [1] x1 + [7] 803.69/297.03 803.69/297.03 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 803.69/297.03 803.69/297.03 [a] = [0] 803.69/297.03 803.69/297.03 [s](x1) = [1] x1 + [1] 803.69/297.03 803.69/297.03 [0] = [0] 803.69/297.03 803.69/297.03 [b] = [4] 803.69/297.03 803.69/297.03 [half](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 [exp](x1) = [1] 803.69/297.03 803.69/297.03 [double](x1) = [1] x1 + [0] 803.69/297.03 803.69/297.03 The order satisfies the following ordering constraints: 803.69/297.03 803.69/297.03 [tower(x)] = [1] x + [7] 803.69/297.03 > [1] x + [1] 803.69/297.03 = [f(a(), x, s(0()))] 803.69/297.03 803.69/297.03 [f(a(), s(x), y)] = [1] x + [1] y + [1] 803.69/297.03 ? [1] x + [1] y + [5] 803.69/297.03 = [f(b(), y, s(x))] 803.69/297.03 803.69/297.03 [f(a(), 0(), y)] = [1] y + [0] 803.69/297.03 >= [1] y + [0] 803.69/297.03 = [y] 803.69/297.03 803.69/297.03 [f(b(), y, x)] = [1] x + [1] y + [4] 803.69/297.03 > [1] x + [1] 803.69/297.03 = [f(a(), half(x), exp(y))] 803.69/297.03 803.69/297.03 [half(s(s(x)))] = [1] x + [2] 803.69/297.03 > [1] x + [1] 803.69/297.03 = [s(half(x))] 803.69/297.03 803.69/297.03 [half(s(0()))] = [1] 803.69/297.03 > [0] 803.69/297.03 = [half(0())] 803.69/297.03 803.69/297.03 [half(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [double(0())] 803.69/297.03 803.69/297.03 [exp(s(x))] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [double(exp(x))] 803.69/297.03 803.69/297.03 [exp(0())] = [1] 803.69/297.03 >= [1] 803.69/297.03 = [s(0())] 803.69/297.03 803.69/297.03 [double(s(x))] = [1] x + [1] 803.69/297.03 ? [1] x + [2] 803.69/297.03 = [s(s(double(x)))] 803.69/297.03 803.69/297.03 [double(0())] = [0] 803.69/297.03 >= [0] 803.69/297.03 = [0()] 803.69/297.03 803.69/297.03 803.69/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 803.69/297.03 803.69/297.03 We are left with following problem, upon which TcT provides the 803.69/297.03 certificate MAYBE. 803.69/297.03 803.69/297.03 Strict Trs: 803.69/297.03 { f(a(), s(x), y) -> f(b(), y, s(x)) 803.69/297.03 , double(s(x)) -> s(s(double(x))) } 803.69/297.03 Weak Trs: 803.69/297.03 { tower(x) -> f(a(), x, s(0())) 803.69/297.03 , f(a(), 0(), y) -> y 803.69/297.03 , f(b(), y, x) -> f(a(), half(x), exp(y)) 803.69/297.03 , half(s(s(x))) -> s(half(x)) 803.69/297.03 , half(s(0())) -> half(0()) 803.69/297.03 , half(0()) -> double(0()) 803.69/297.03 , exp(s(x)) -> double(exp(x)) 803.69/297.03 , exp(0()) -> s(0()) 803.69/297.03 , double(0()) -> 0() } 803.69/297.03 Obligation: 803.69/297.03 innermost runtime complexity 803.69/297.03 Answer: 803.69/297.03 MAYBE 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'Fastest' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'empty' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 2) 'With Problem ...' failed due to the following reason: 803.69/297.03 803.69/297.03 Empty strict component of the problem is NOT empty. 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 803.69/297.03 failed due to the following reason: 803.69/297.03 803.69/297.03 Computation stopped due to timeout after 24.0 seconds. 803.69/297.03 803.69/297.03 3) 'Best' failed due to the following reason: 803.69/297.03 803.69/297.03 None of the processors succeeded. 803.69/297.03 803.69/297.03 Details of failed attempt(s): 803.69/297.03 ----------------------------- 803.69/297.03 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 803.69/297.03 to the following reason: 803.69/297.03 803.69/297.03 The input cannot be shown compatible 803.69/297.03 803.69/297.03 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 803.69/297.03 following reason: 803.69/297.03 803.69/297.03 The input cannot be shown compatible 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 803.69/297.03 Arrrr.. 804.12/297.43 EOF