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