MAYBE 525.60/297.14 MAYBE 525.60/297.14 525.60/297.14 We are left with following problem, upon which TcT provides the 525.60/297.14 certificate MAYBE. 525.60/297.14 525.60/297.14 Strict Trs: 525.60/297.14 { g(x, 0()) -> 0() 525.60/297.14 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.14 , g(h(), s(0())) -> 0() 525.60/297.14 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.14 , double(x) -> g(d(), x) 525.60/297.14 , half(x) -> g(h(), x) 525.60/297.14 , f(s(x), y) -> f(half(s(x)), double(y)) 525.60/297.14 , f(s(0()), y) -> y 525.60/297.14 , id(x) -> f(x, s(0())) } 525.60/297.14 Obligation: 525.60/297.14 innermost runtime complexity 525.60/297.14 Answer: 525.60/297.14 MAYBE 525.60/297.14 525.60/297.14 None of the processors succeeded. 525.60/297.14 525.60/297.14 Details of failed attempt(s): 525.60/297.14 ----------------------------- 525.60/297.14 1) 'empty' failed due to the following reason: 525.60/297.14 525.60/297.14 Empty strict component of the problem is NOT empty. 525.60/297.14 525.60/297.14 2) 'Best' failed due to the following reason: 525.60/297.14 525.60/297.14 None of the processors succeeded. 525.60/297.14 525.60/297.14 Details of failed attempt(s): 525.60/297.14 ----------------------------- 525.60/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 525.60/297.14 following reason: 525.60/297.14 525.60/297.14 Computation stopped due to timeout after 297.0 seconds. 525.60/297.14 525.60/297.14 2) 'Best' failed due to the following reason: 525.60/297.14 525.60/297.14 None of the processors succeeded. 525.60/297.14 525.60/297.14 Details of failed attempt(s): 525.60/297.14 ----------------------------- 525.60/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 525.60/297.14 seconds)' failed due to the following reason: 525.60/297.14 525.60/297.14 The weightgap principle applies (using the following nonconstant 525.60/297.14 growth matrix-interpretation) 525.60/297.14 525.60/297.14 The following argument positions are usable: 525.60/297.14 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.14 525.60/297.14 TcT has computed the following matrix interpretation satisfying 525.60/297.14 not(EDA) and not(IDA(1)). 525.60/297.14 525.60/297.14 [g](x1, x2) = [1] x1 + [0] 525.60/297.14 525.60/297.14 [0] = [0] 525.60/297.14 525.60/297.14 [d] = [0] 525.60/297.14 525.60/297.14 [s](x1) = [1] x1 + [0] 525.60/297.14 525.60/297.14 [h] = [0] 525.60/297.14 525.60/297.14 [double](x1) = [1] x1 + [0] 525.60/297.14 525.60/297.14 [half](x1) = [0] 525.60/297.14 525.60/297.14 [f](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.14 525.60/297.14 [id](x1) = [1] x1 + [7] 525.60/297.14 525.60/297.14 The order satisfies the following ordering constraints: 525.60/297.14 525.60/297.14 [g(x, 0())] = [1] x + [0] 525.60/297.14 >= [0] 525.60/297.14 = [0()] 525.60/297.14 525.60/297.14 [g(d(), s(x))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [s(s(g(d(), x)))] 525.60/297.14 525.60/297.14 [g(h(), s(0()))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [0()] 525.60/297.14 525.60/297.14 [g(h(), s(s(x)))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [s(g(h(), x))] 525.60/297.14 525.60/297.14 [double(x)] = [1] x + [0] 525.60/297.14 >= [0] 525.60/297.14 = [g(d(), x)] 525.60/297.14 525.60/297.14 [half(x)] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [g(h(), x)] 525.60/297.14 525.60/297.14 [f(s(x), y)] = [1] x + [1] y + [0] 525.60/297.14 >= [1] y + [0] 525.60/297.14 = [f(half(s(x)), double(y))] 525.60/297.14 525.60/297.14 [f(s(0()), y)] = [1] y + [0] 525.60/297.14 >= [1] y + [0] 525.60/297.14 = [y] 525.60/297.14 525.60/297.14 [id(x)] = [1] x + [7] 525.60/297.14 > [1] x + [0] 525.60/297.14 = [f(x, s(0()))] 525.60/297.14 525.60/297.14 525.60/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 525.60/297.14 525.60/297.14 We are left with following problem, upon which TcT provides the 525.60/297.14 certificate MAYBE. 525.60/297.14 525.60/297.14 Strict Trs: 525.60/297.14 { g(x, 0()) -> 0() 525.60/297.14 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.14 , g(h(), s(0())) -> 0() 525.60/297.14 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.14 , double(x) -> g(d(), x) 525.60/297.14 , half(x) -> g(h(), x) 525.60/297.14 , f(s(x), y) -> f(half(s(x)), double(y)) 525.60/297.14 , f(s(0()), y) -> y } 525.60/297.14 Weak Trs: { id(x) -> f(x, s(0())) } 525.60/297.14 Obligation: 525.60/297.14 innermost runtime complexity 525.60/297.14 Answer: 525.60/297.14 MAYBE 525.60/297.14 525.60/297.14 The weightgap principle applies (using the following nonconstant 525.60/297.14 growth matrix-interpretation) 525.60/297.14 525.60/297.14 The following argument positions are usable: 525.60/297.14 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.14 525.60/297.14 TcT has computed the following matrix interpretation satisfying 525.60/297.14 not(EDA) and not(IDA(1)). 525.60/297.14 525.60/297.14 [g](x1, x2) = [1] x1 + [0] 525.60/297.14 525.60/297.14 [0] = [0] 525.60/297.14 525.60/297.14 [d] = [0] 525.60/297.14 525.60/297.14 [s](x1) = [1] x1 + [0] 525.60/297.14 525.60/297.14 [h] = [0] 525.60/297.14 525.60/297.14 [double](x1) = [1] x1 + [2] 525.60/297.14 525.60/297.14 [half](x1) = [6] 525.60/297.14 525.60/297.14 [f](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.14 525.60/297.14 [id](x1) = [1] x1 + [7] 525.60/297.14 525.60/297.14 The order satisfies the following ordering constraints: 525.60/297.14 525.60/297.14 [g(x, 0())] = [1] x + [0] 525.60/297.14 >= [0] 525.60/297.14 = [0()] 525.60/297.14 525.60/297.14 [g(d(), s(x))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [s(s(g(d(), x)))] 525.60/297.14 525.60/297.14 [g(h(), s(0()))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [0()] 525.60/297.14 525.60/297.14 [g(h(), s(s(x)))] = [0] 525.60/297.14 >= [0] 525.60/297.14 = [s(g(h(), x))] 525.60/297.14 525.60/297.14 [double(x)] = [1] x + [2] 525.60/297.14 > [0] 525.60/297.14 = [g(d(), x)] 525.60/297.14 525.60/297.14 [half(x)] = [6] 525.60/297.14 > [0] 525.60/297.14 = [g(h(), x)] 525.60/297.14 525.60/297.14 [f(s(x), y)] = [1] x + [1] y + [0] 525.60/297.14 ? [1] y + [8] 525.60/297.15 = [f(half(s(x)), double(y))] 525.60/297.15 525.60/297.15 [f(s(0()), y)] = [1] y + [0] 525.60/297.15 >= [1] y + [0] 525.60/297.15 = [y] 525.60/297.15 525.60/297.15 [id(x)] = [1] x + [7] 525.60/297.15 > [1] x + [0] 525.60/297.15 = [f(x, s(0()))] 525.60/297.15 525.60/297.15 525.60/297.15 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 525.60/297.15 525.60/297.15 We are left with following problem, upon which TcT provides the 525.60/297.15 certificate MAYBE. 525.60/297.15 525.60/297.15 Strict Trs: 525.60/297.15 { g(x, 0()) -> 0() 525.60/297.15 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.15 , g(h(), s(0())) -> 0() 525.60/297.15 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.15 , f(s(x), y) -> f(half(s(x)), double(y)) 525.60/297.15 , f(s(0()), y) -> y } 525.60/297.15 Weak Trs: 525.60/297.15 { double(x) -> g(d(), x) 525.60/297.15 , half(x) -> g(h(), x) 525.60/297.15 , id(x) -> f(x, s(0())) } 525.60/297.15 Obligation: 525.60/297.15 innermost runtime complexity 525.60/297.15 Answer: 525.60/297.15 MAYBE 525.60/297.15 525.60/297.15 We use the processor 'matrix interpretation of dimension 1' to 525.60/297.15 orient following rules strictly. 525.60/297.15 525.60/297.15 Trs: { f(s(0()), y) -> y } 525.60/297.15 525.60/297.15 The induced complexity on above rules (modulo remaining rules) is 525.60/297.15 YES(?,O(n^1)) . These rules are moved into the corresponding weak 525.60/297.15 component(s). 525.60/297.15 525.60/297.15 Sub-proof: 525.60/297.15 ---------- 525.60/297.15 The following argument positions are usable: 525.60/297.15 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.15 525.60/297.15 TcT has computed the following constructor-based matrix 525.60/297.15 interpretation satisfying not(EDA). 525.60/297.15 525.60/297.15 [g](x1, x2) = [0] 525.60/297.15 525.60/297.15 [0] = [0] 525.60/297.15 525.60/297.15 [d] = [0] 525.60/297.15 525.60/297.15 [s](x1) = [1] x1 + [0] 525.60/297.15 525.60/297.15 [h] = [0] 525.60/297.15 525.60/297.15 [double](x1) = [1] x1 + [0] 525.60/297.15 525.60/297.15 [half](x1) = [0] 525.60/297.15 525.60/297.15 [f](x1, x2) = [4] x1 + [4] x2 + [1] 525.60/297.15 525.60/297.15 [id](x1) = [7] x1 + [7] 525.60/297.15 525.60/297.15 The order satisfies the following ordering constraints: 525.60/297.15 525.60/297.15 [g(x, 0())] = [0] 525.60/297.15 >= [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(d(), s(x))] = [0] 525.60/297.15 >= [0] 525.60/297.15 = [s(s(g(d(), x)))] 525.60/297.15 525.60/297.15 [g(h(), s(0()))] = [0] 525.60/297.15 >= [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(h(), s(s(x)))] = [0] 525.60/297.15 >= [0] 525.60/297.15 = [s(g(h(), x))] 525.60/297.15 525.60/297.15 [double(x)] = [1] x + [0] 525.60/297.15 >= [0] 525.60/297.15 = [g(d(), x)] 525.60/297.15 525.60/297.15 [half(x)] = [0] 525.60/297.15 >= [0] 525.60/297.15 = [g(h(), x)] 525.60/297.15 525.60/297.15 [f(s(x), y)] = [4] x + [4] y + [1] 525.60/297.15 >= [4] y + [1] 525.60/297.15 = [f(half(s(x)), double(y))] 525.60/297.15 525.60/297.15 [f(s(0()), y)] = [4] y + [1] 525.60/297.15 > [1] y + [0] 525.60/297.15 = [y] 525.60/297.15 525.60/297.15 [id(x)] = [7] x + [7] 525.60/297.15 > [4] x + [1] 525.60/297.15 = [f(x, s(0()))] 525.60/297.15 525.60/297.15 525.60/297.15 We return to the main proof. 525.60/297.15 525.60/297.15 We are left with following problem, upon which TcT provides the 525.60/297.15 certificate MAYBE. 525.60/297.15 525.60/297.15 Strict Trs: 525.60/297.15 { g(x, 0()) -> 0() 525.60/297.15 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.15 , g(h(), s(0())) -> 0() 525.60/297.15 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.15 , f(s(x), y) -> f(half(s(x)), double(y)) } 525.60/297.15 Weak Trs: 525.60/297.15 { double(x) -> g(d(), x) 525.60/297.15 , half(x) -> g(h(), x) 525.60/297.15 , f(s(0()), y) -> y 525.60/297.15 , id(x) -> f(x, s(0())) } 525.60/297.15 Obligation: 525.60/297.15 innermost runtime complexity 525.60/297.15 Answer: 525.60/297.15 MAYBE 525.60/297.15 525.60/297.15 The weightgap principle applies (using the following nonconstant 525.60/297.15 growth matrix-interpretation) 525.60/297.15 525.60/297.15 The following argument positions are usable: 525.60/297.15 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.15 525.60/297.15 TcT has computed the following matrix interpretation satisfying 525.60/297.15 not(EDA) and not(IDA(1)). 525.60/297.15 525.60/297.15 [g](x1, x2) = [1] x1 + [0] 525.60/297.15 525.60/297.15 [0] = [0] 525.60/297.15 525.60/297.15 [d] = [0] 525.60/297.15 525.60/297.15 [s](x1) = [1] x1 + [4] 525.60/297.15 525.60/297.15 [h] = [4] 525.60/297.15 525.60/297.15 [double](x1) = [1] x1 + [2] 525.60/297.15 525.60/297.15 [half](x1) = [6] 525.60/297.15 525.60/297.15 [f](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.15 525.60/297.15 [id](x1) = [1] x1 + [7] 525.60/297.15 525.60/297.15 The order satisfies the following ordering constraints: 525.60/297.15 525.60/297.15 [g(x, 0())] = [1] x + [0] 525.60/297.15 >= [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(d(), s(x))] = [0] 525.60/297.15 ? [8] 525.60/297.15 = [s(s(g(d(), x)))] 525.60/297.15 525.60/297.15 [g(h(), s(0()))] = [4] 525.60/297.15 > [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(h(), s(s(x)))] = [4] 525.60/297.15 ? [8] 525.60/297.15 = [s(g(h(), x))] 525.60/297.15 525.60/297.15 [double(x)] = [1] x + [2] 525.60/297.15 > [0] 525.60/297.15 = [g(d(), x)] 525.60/297.15 525.60/297.15 [half(x)] = [6] 525.60/297.15 > [4] 525.60/297.15 = [g(h(), x)] 525.60/297.15 525.60/297.15 [f(s(x), y)] = [1] x + [1] y + [4] 525.60/297.15 ? [1] y + [8] 525.60/297.15 = [f(half(s(x)), double(y))] 525.60/297.15 525.60/297.15 [f(s(0()), y)] = [1] y + [4] 525.60/297.15 > [1] y + [0] 525.60/297.15 = [y] 525.60/297.15 525.60/297.15 [id(x)] = [1] x + [7] 525.60/297.15 > [1] x + [4] 525.60/297.15 = [f(x, s(0()))] 525.60/297.15 525.60/297.15 525.60/297.15 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 525.60/297.15 525.60/297.15 We are left with following problem, upon which TcT provides the 525.60/297.15 certificate MAYBE. 525.60/297.15 525.60/297.15 Strict Trs: 525.60/297.15 { g(x, 0()) -> 0() 525.60/297.15 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.15 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.15 , f(s(x), y) -> f(half(s(x)), double(y)) } 525.60/297.15 Weak Trs: 525.60/297.15 { g(h(), s(0())) -> 0() 525.60/297.15 , double(x) -> g(d(), x) 525.60/297.15 , half(x) -> g(h(), x) 525.60/297.15 , f(s(0()), y) -> y 525.60/297.15 , id(x) -> f(x, s(0())) } 525.60/297.15 Obligation: 525.60/297.15 innermost runtime complexity 525.60/297.15 Answer: 525.60/297.15 MAYBE 525.60/297.15 525.60/297.15 The weightgap principle applies (using the following nonconstant 525.60/297.15 growth matrix-interpretation) 525.60/297.15 525.60/297.15 The following argument positions are usable: 525.60/297.15 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.15 525.60/297.15 TcT has computed the following matrix interpretation satisfying 525.60/297.15 not(EDA) and not(IDA(1)). 525.60/297.15 525.60/297.15 [g](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.15 525.60/297.15 [0] = [0] 525.60/297.15 525.60/297.15 [d] = [0] 525.60/297.15 525.60/297.15 [s](x1) = [1] x1 + [4] 525.60/297.15 525.60/297.15 [h] = [4] 525.60/297.15 525.60/297.15 [double](x1) = [1] x1 + [0] 525.60/297.15 525.60/297.15 [half](x1) = [1] x1 + [4] 525.60/297.15 525.60/297.15 [f](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.15 525.60/297.15 [id](x1) = [1] x1 + [7] 525.60/297.15 525.60/297.15 The order satisfies the following ordering constraints: 525.60/297.15 525.60/297.15 [g(x, 0())] = [1] x + [0] 525.60/297.15 >= [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(d(), s(x))] = [1] x + [4] 525.60/297.15 ? [1] x + [8] 525.60/297.15 = [s(s(g(d(), x)))] 525.60/297.15 525.60/297.15 [g(h(), s(0()))] = [8] 525.60/297.15 > [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(h(), s(s(x)))] = [1] x + [12] 525.60/297.15 > [1] x + [8] 525.60/297.15 = [s(g(h(), x))] 525.60/297.15 525.60/297.15 [double(x)] = [1] x + [0] 525.60/297.15 >= [1] x + [0] 525.60/297.15 = [g(d(), x)] 525.60/297.15 525.60/297.15 [half(x)] = [1] x + [4] 525.60/297.15 >= [1] x + [4] 525.60/297.15 = [g(h(), x)] 525.60/297.15 525.60/297.15 [f(s(x), y)] = [1] x + [1] y + [4] 525.60/297.15 ? [1] x + [1] y + [8] 525.60/297.15 = [f(half(s(x)), double(y))] 525.60/297.15 525.60/297.15 [f(s(0()), y)] = [1] y + [4] 525.60/297.15 > [1] y + [0] 525.60/297.15 = [y] 525.60/297.15 525.60/297.15 [id(x)] = [1] x + [7] 525.60/297.15 > [1] x + [4] 525.60/297.15 = [f(x, s(0()))] 525.60/297.15 525.60/297.15 525.60/297.15 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 525.60/297.15 525.60/297.15 We are left with following problem, upon which TcT provides the 525.60/297.15 certificate MAYBE. 525.60/297.15 525.60/297.15 Strict Trs: 525.60/297.15 { g(x, 0()) -> 0() 525.60/297.15 , g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.15 , f(s(x), y) -> f(half(s(x)), double(y)) } 525.60/297.15 Weak Trs: 525.60/297.15 { g(h(), s(0())) -> 0() 525.60/297.15 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.15 , double(x) -> g(d(), x) 525.60/297.15 , half(x) -> g(h(), x) 525.60/297.15 , f(s(0()), y) -> y 525.60/297.15 , id(x) -> f(x, s(0())) } 525.60/297.15 Obligation: 525.60/297.15 innermost runtime complexity 525.60/297.15 Answer: 525.60/297.15 MAYBE 525.60/297.15 525.60/297.15 The weightgap principle applies (using the following nonconstant 525.60/297.15 growth matrix-interpretation) 525.60/297.15 525.60/297.15 The following argument positions are usable: 525.60/297.15 Uargs(s) = {1}, Uargs(f) = {1, 2} 525.60/297.15 525.60/297.15 TcT has computed the following matrix interpretation satisfying 525.60/297.15 not(EDA) and not(IDA(1)). 525.60/297.15 525.60/297.15 [g](x1, x2) = [1] x1 + [1] 525.60/297.15 525.60/297.15 [0] = [0] 525.60/297.15 525.60/297.15 [d] = [0] 525.60/297.15 525.60/297.15 [s](x1) = [1] x1 + [0] 525.60/297.15 525.60/297.15 [h] = [0] 525.60/297.15 525.60/297.15 [double](x1) = [1] x1 + [1] 525.60/297.15 525.60/297.15 [half](x1) = [7] 525.60/297.15 525.60/297.15 [f](x1, x2) = [1] x1 + [1] x2 + [0] 525.60/297.15 525.60/297.15 [id](x1) = [1] x1 + [7] 525.60/297.15 525.60/297.15 The order satisfies the following ordering constraints: 525.60/297.15 525.60/297.15 [g(x, 0())] = [1] x + [1] 525.60/297.15 > [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(d(), s(x))] = [1] 525.60/297.15 >= [1] 525.60/297.15 = [s(s(g(d(), x)))] 525.60/297.15 525.60/297.15 [g(h(), s(0()))] = [1] 525.60/297.15 > [0] 525.60/297.15 = [0()] 525.60/297.15 525.60/297.15 [g(h(), s(s(x)))] = [1] 525.60/297.15 >= [1] 525.60/297.15 = [s(g(h(), x))] 525.60/297.15 525.60/297.15 [double(x)] = [1] x + [1] 525.60/297.15 >= [1] 525.60/297.15 = [g(d(), x)] 525.60/297.15 525.60/297.15 [half(x)] = [7] 525.60/297.15 > [1] 525.60/297.15 = [g(h(), x)] 525.60/297.15 525.60/297.15 [f(s(x), y)] = [1] x + [1] y + [0] 525.60/297.15 ? [1] y + [8] 525.60/297.15 = [f(half(s(x)), double(y))] 525.60/297.15 525.60/297.15 [f(s(0()), y)] = [1] y + [0] 525.60/297.15 >= [1] y + [0] 525.60/297.15 = [y] 525.60/297.15 525.60/297.15 [id(x)] = [1] x + [7] 525.60/297.15 > [1] x + [0] 525.60/297.15 = [f(x, s(0()))] 525.60/297.15 525.60/297.15 525.60/297.15 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 525.60/297.15 525.60/297.15 We are left with following problem, upon which TcT provides the 525.60/297.15 certificate MAYBE. 525.60/297.15 525.60/297.15 Strict Trs: 525.60/297.15 { g(d(), s(x)) -> s(s(g(d(), x))) 525.60/297.15 , f(s(x), y) -> f(half(s(x)), double(y)) } 525.60/297.15 Weak Trs: 525.60/297.15 { g(x, 0()) -> 0() 525.60/297.15 , g(h(), s(0())) -> 0() 525.60/297.15 , g(h(), s(s(x))) -> s(g(h(), x)) 525.60/297.15 , double(x) -> g(d(), x) 525.60/297.15 , half(x) -> g(h(), x) 525.60/297.15 , f(s(0()), y) -> y 525.60/297.15 , id(x) -> f(x, s(0())) } 525.60/297.15 Obligation: 525.60/297.15 innermost runtime complexity 525.60/297.15 Answer: 525.60/297.15 MAYBE 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'Fastest' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'empty' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 2) 'With Problem ...' failed due to the following reason: 525.60/297.15 525.60/297.15 Empty strict component of the problem is NOT empty. 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 525.60/297.15 failed due to the following reason: 525.60/297.15 525.60/297.15 Computation stopped due to timeout after 24.0 seconds. 525.60/297.15 525.60/297.15 3) 'Best' failed due to the following reason: 525.60/297.15 525.60/297.15 None of the processors succeeded. 525.60/297.15 525.60/297.15 Details of failed attempt(s): 525.60/297.15 ----------------------------- 525.60/297.15 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 525.60/297.15 following reason: 525.60/297.15 525.60/297.15 The input cannot be shown compatible 525.60/297.15 525.60/297.15 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 525.60/297.15 to the following reason: 525.60/297.15 525.60/297.15 The input cannot be shown compatible 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 525.60/297.15 Arrrr.. 525.60/297.19 EOF