MAYBE 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , +(s(x), y) -> s(+(x, y)) 533.96/277.96 , f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'Best' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 533.96/277.96 seconds)' failed due to the following reason: 533.96/277.96 533.96/277.96 The weightgap principle applies (using the following nonconstant 533.96/277.96 growth matrix-interpretation) 533.96/277.96 533.96/277.96 The following argument positions are usable: 533.96/277.96 Uargs(+) = {1}, Uargs(s) = {1}, Uargs(f) = {1}, Uargs(h) = {1} 533.96/277.96 533.96/277.96 TcT has computed the following matrix interpretation satisfying 533.96/277.96 not(EDA) and not(IDA(1)). 533.96/277.96 533.96/277.96 [+](x1, x2) = [1] x1 + [1] x2 + [0] 533.96/277.96 533.96/277.96 [0] = [0] 533.96/277.96 533.96/277.96 [s](x1) = [1] x1 + [0] 533.96/277.96 533.96/277.96 [f](x1) = [1] x1 + [0] 533.96/277.96 533.96/277.96 [g](x1) = [1] x1 + [4] 533.96/277.96 533.96/277.96 [h](x1, x2) = [1] x1 + [1] x2 + [0] 533.96/277.96 533.96/277.96 The order satisfies the following ordering constraints: 533.96/277.96 533.96/277.96 [+(x, +(y, z))] = [1] x + [1] y + [1] z + [0] 533.96/277.96 >= [1] x + [1] y + [1] z + [0] 533.96/277.96 = [+(+(x, y), z)] 533.96/277.96 533.96/277.96 [+(x, 0())] = [1] x + [0] 533.96/277.96 >= [1] x + [0] 533.96/277.96 = [x] 533.96/277.96 533.96/277.96 [+(x, s(y))] = [1] x + [1] y + [0] 533.96/277.96 >= [1] x + [1] y + [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [+(0(), y)] = [1] y + [0] 533.96/277.96 >= [1] y + [0] 533.96/277.96 = [y] 533.96/277.96 533.96/277.96 [+(s(x), y)] = [1] x + [1] y + [0] 533.96/277.96 >= [1] x + [1] y + [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [f(g(f(x)))] = [1] x + [4] 533.96/277.96 > [1] x + [0] 533.96/277.96 = [f(h(s(0()), x))] 533.96/277.96 533.96/277.96 [f(g(h(x, y)))] = [1] x + [1] y + [4] 533.96/277.96 > [1] x + [1] y + [0] 533.96/277.96 = [f(h(s(x), y))] 533.96/277.96 533.96/277.96 [f(h(x, h(y, z)))] = [1] x + [1] y + [1] z + [0] 533.96/277.96 >= [1] x + [1] y + [1] z + [0] 533.96/277.96 = [f(h(+(x, y), z))] 533.96/277.96 533.96/277.96 533.96/277.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , +(s(x), y) -> s(+(x, y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Weak Trs: 533.96/277.96 { f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 The weightgap principle applies (using the following nonconstant 533.96/277.96 growth matrix-interpretation) 533.96/277.96 533.96/277.96 The following argument positions are usable: 533.96/277.96 Uargs(+) = {1}, Uargs(s) = {1}, Uargs(f) = {1}, Uargs(h) = {1} 533.96/277.96 533.96/277.96 TcT has computed the following matrix interpretation satisfying 533.96/277.96 not(EDA) and not(IDA(1)). 533.96/277.96 533.96/277.96 [+](x1, x2) = [1] x1 + [1] x2 + [0] 533.96/277.96 533.96/277.96 [0] = [0] 533.96/277.96 533.96/277.96 [s](x1) = [1] x1 + [0] 533.96/277.96 533.96/277.96 [f](x1) = [1] x1 + [0] 533.96/277.96 533.96/277.96 [g](x1) = [1] x1 + [4] 533.96/277.96 533.96/277.96 [h](x1, x2) = [1] x1 + [1] x2 + [4] 533.96/277.96 533.96/277.96 The order satisfies the following ordering constraints: 533.96/277.96 533.96/277.96 [+(x, +(y, z))] = [1] x + [1] y + [1] z + [0] 533.96/277.96 >= [1] x + [1] y + [1] z + [0] 533.96/277.96 = [+(+(x, y), z)] 533.96/277.96 533.96/277.96 [+(x, 0())] = [1] x + [0] 533.96/277.96 >= [1] x + [0] 533.96/277.96 = [x] 533.96/277.96 533.96/277.96 [+(x, s(y))] = [1] x + [1] y + [0] 533.96/277.96 >= [1] x + [1] y + [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [+(0(), y)] = [1] y + [0] 533.96/277.96 >= [1] y + [0] 533.96/277.96 = [y] 533.96/277.96 533.96/277.96 [+(s(x), y)] = [1] x + [1] y + [0] 533.96/277.96 >= [1] x + [1] y + [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [f(g(f(x)))] = [1] x + [4] 533.96/277.96 >= [1] x + [4] 533.96/277.96 = [f(h(s(0()), x))] 533.96/277.96 533.96/277.96 [f(g(h(x, y)))] = [1] x + [1] y + [8] 533.96/277.96 > [1] x + [1] y + [4] 533.96/277.96 = [f(h(s(x), y))] 533.96/277.96 533.96/277.96 [f(h(x, h(y, z)))] = [1] x + [1] y + [1] z + [8] 533.96/277.96 > [1] x + [1] y + [1] z + [4] 533.96/277.96 = [f(h(+(x, y), z))] 533.96/277.96 533.96/277.96 533.96/277.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , +(s(x), y) -> s(+(x, y)) } 533.96/277.96 Weak Trs: 533.96/277.96 { f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 The weightgap principle applies (using the following nonconstant 533.96/277.96 growth matrix-interpretation) 533.96/277.96 533.96/277.96 The following argument positions are usable: 533.96/277.96 Uargs(+) = {1}, Uargs(s) = {1}, Uargs(f) = {1}, Uargs(h) = {1} 533.96/277.96 533.96/277.96 TcT has computed the following matrix interpretation satisfying 533.96/277.96 not(EDA) and not(IDA(1)). 533.96/277.96 533.96/277.96 [+](x1, x2) = [1] x1 + [1] x2 + [1] 533.96/277.96 533.96/277.96 [0] = [0] 533.96/277.96 533.96/277.96 [s](x1) = [1] x1 + [0] 533.96/277.96 533.96/277.96 [f](x1) = [1] x1 + [1] 533.96/277.96 533.96/277.96 [g](x1) = [1] x1 + [6] 533.96/277.96 533.96/277.96 [h](x1, x2) = [1] x1 + [1] x2 + [1] 533.96/277.96 533.96/277.96 The order satisfies the following ordering constraints: 533.96/277.96 533.96/277.96 [+(x, +(y, z))] = [1] x + [1] y + [1] z + [2] 533.96/277.96 >= [1] x + [1] y + [1] z + [2] 533.96/277.96 = [+(+(x, y), z)] 533.96/277.96 533.96/277.96 [+(x, 0())] = [1] x + [1] 533.96/277.96 > [1] x + [0] 533.96/277.96 = [x] 533.96/277.96 533.96/277.96 [+(x, s(y))] = [1] x + [1] y + [1] 533.96/277.96 >= [1] x + [1] y + [1] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [+(0(), y)] = [1] y + [1] 533.96/277.96 > [1] y + [0] 533.96/277.96 = [y] 533.96/277.96 533.96/277.96 [+(s(x), y)] = [1] x + [1] y + [1] 533.96/277.96 >= [1] x + [1] y + [1] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [f(g(f(x)))] = [1] x + [8] 533.96/277.96 > [1] x + [2] 533.96/277.96 = [f(h(s(0()), x))] 533.96/277.96 533.96/277.96 [f(g(h(x, y)))] = [1] x + [1] y + [8] 533.96/277.96 > [1] x + [1] y + [2] 533.96/277.96 = [f(h(s(x), y))] 533.96/277.96 533.96/277.96 [f(h(x, h(y, z)))] = [1] x + [1] y + [1] z + [3] 533.96/277.96 >= [1] x + [1] y + [1] z + [3] 533.96/277.96 = [f(h(+(x, y), z))] 533.96/277.96 533.96/277.96 533.96/277.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(s(x), y) -> s(+(x, y)) } 533.96/277.96 Weak Trs: 533.96/277.96 { +(x, 0()) -> x 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'Fastest' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 We use the processor 'matrix interpretation of dimension 2' to 533.96/277.96 orient following rules strictly. 533.96/277.96 533.96/277.96 Trs: { +(x, +(y, z)) -> +(+(x, y), z) } 533.96/277.96 533.96/277.96 The induced complexity on above rules (modulo remaining rules) is 533.96/277.96 YES(?,O(n^1)) . These rules are moved into the corresponding weak 533.96/277.96 component(s). 533.96/277.96 533.96/277.96 Sub-proof: 533.96/277.96 ---------- 533.96/277.96 The following argument positions are usable: 533.96/277.96 Uargs(+) = {1}, Uargs(s) = {1}, Uargs(f) = {1}, Uargs(h) = {1} 533.96/277.96 533.96/277.96 TcT has computed the following constructor-based matrix 533.96/277.96 interpretation satisfying not(EDA) and not(IDA(1)). 533.96/277.96 533.96/277.96 [+](x1, x2) = [1 0] x1 + [2 0] x2 + [2] 533.96/277.96 [0 1] [0 1] [0] 533.96/277.96 533.96/277.96 [0] = [0] 533.96/277.96 [0] 533.96/277.96 533.96/277.96 [s](x1) = [1 0] x1 + [0] 533.96/277.96 [0 0] [0] 533.96/277.96 533.96/277.96 [f](x1) = [1 1] x1 + [0] 533.96/277.96 [3 3] [1] 533.96/277.96 533.96/277.96 [g](x1) = [0 1] x1 + [0] 533.96/277.96 [1 0] [0] 533.96/277.96 533.96/277.96 [h](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 533.96/277.96 [0 0] [1 0] [0] 533.96/277.96 533.96/277.96 The order satisfies the following ordering constraints: 533.96/277.96 533.96/277.96 [+(x, +(y, z))] = [1 0] x + [2 0] y + [4 0] z + [6] 533.96/277.96 [0 1] [0 1] [0 1] [0] 533.96/277.96 > [1 0] x + [2 0] y + [2 0] z + [4] 533.96/277.96 [0 1] [0 1] [0 1] [0] 533.96/277.96 = [+(+(x, y), z)] 533.96/277.96 533.96/277.96 [+(x, 0())] = [1 0] x + [2] 533.96/277.96 [0 1] [0] 533.96/277.96 > [1 0] x + [0] 533.96/277.96 [0 1] [0] 533.96/277.96 = [x] 533.96/277.96 533.96/277.96 [+(x, s(y))] = [1 0] x + [2 0] y + [2] 533.96/277.96 [0 1] [0 0] [0] 533.96/277.96 >= [1 0] x + [2 0] y + [2] 533.96/277.96 [0 0] [0 0] [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [+(0(), y)] = [2 0] y + [2] 533.96/277.96 [0 1] [0] 533.96/277.96 > [1 0] y + [0] 533.96/277.96 [0 1] [0] 533.96/277.96 = [y] 533.96/277.96 533.96/277.96 [+(s(x), y)] = [1 0] x + [2 0] y + [2] 533.96/277.96 [0 0] [0 1] [0] 533.96/277.96 >= [1 0] x + [2 0] y + [2] 533.96/277.96 [0 0] [0 0] [0] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [f(g(f(x)))] = [ 4 4] x + [1] 533.96/277.96 [12 12] [4] 533.96/277.96 >= [2 0] x + [1] 533.96/277.96 [6 0] [4] 533.96/277.96 = [f(h(s(0()), x))] 533.96/277.96 533.96/277.96 [f(g(h(x, y)))] = [1 0] x + [2 0] y + [1] 533.96/277.96 [3 0] [6 0] [4] 533.96/277.96 >= [1 0] x + [2 0] y + [1] 533.96/277.96 [3 0] [6 0] [4] 533.96/277.96 = [f(h(s(x), y))] 533.96/277.96 533.96/277.96 [f(h(x, h(y, z)))] = [1 0] x + [2 0] y + [2 0] z + [3] 533.96/277.96 [3 0] [6 0] [6 0] [10] 533.96/277.96 >= [1 0] x + [2 0] y + [2 0] z + [3] 533.96/277.96 [3 0] [6 0] [6 0] [10] 533.96/277.96 = [f(h(+(x, y), z))] 533.96/277.96 533.96/277.96 533.96/277.96 We return to the main proof. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(s(x), y) -> s(+(x, y)) } 533.96/277.96 Weak Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 We use the processor 'matrix interpretation of dimension 2' to 533.96/277.96 orient following rules strictly. 533.96/277.96 533.96/277.96 Trs: { +(x, s(y)) -> s(+(x, y)) } 533.96/277.96 533.96/277.96 The induced complexity on above rules (modulo remaining rules) is 533.96/277.96 YES(?,O(n^1)) . These rules are moved into the corresponding weak 533.96/277.96 component(s). 533.96/277.96 533.96/277.96 Sub-proof: 533.96/277.96 ---------- 533.96/277.96 The following argument positions are usable: 533.96/277.96 Uargs(+) = {1}, Uargs(s) = {1}, Uargs(f) = {1}, Uargs(h) = {1} 533.96/277.96 533.96/277.96 TcT has computed the following constructor-based matrix 533.96/277.96 interpretation satisfying not(EDA) and not(IDA(1)). 533.96/277.96 533.96/277.96 [+](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 533.96/277.96 [0 1] [0 3] [0] 533.96/277.96 533.96/277.96 [0] = [0] 533.96/277.96 [0] 533.96/277.96 533.96/277.96 [s](x1) = [1 0] x1 + [0] 533.96/277.96 [0 1] [4] 533.96/277.96 533.96/277.96 [f](x1) = [1 1] x1 + [1] 533.96/277.96 [1 1] [1] 533.96/277.96 533.96/277.96 [g](x1) = [1 7] x1 + [0] 533.96/277.96 [0 0] [0] 533.96/277.96 533.96/277.96 [h](x1, x2) = [1 0] x1 + [1 5] x2 + [0] 533.96/277.96 [0 1] [0 0] [2] 533.96/277.96 533.96/277.96 The order satisfies the following ordering constraints: 533.96/277.96 533.96/277.96 [+(x, +(y, z))] = [1 0] x + [1 2] y + [1 8] z + [0] 533.96/277.96 [0 1] [0 3] [0 9] [0] 533.96/277.96 >= [1 0] x + [1 2] y + [1 2] z + [0] 533.96/277.96 [0 1] [0 3] [0 3] [0] 533.96/277.96 = [+(+(x, y), z)] 533.96/277.96 533.96/277.96 [+(x, 0())] = [1 0] x + [0] 533.96/277.96 [0 1] [0] 533.96/277.96 >= [1 0] x + [0] 533.96/277.96 [0 1] [0] 533.96/277.96 = [x] 533.96/277.96 533.96/277.96 [+(x, s(y))] = [1 0] x + [1 2] y + [8] 533.96/277.96 [0 1] [0 3] [12] 533.96/277.96 > [1 0] x + [1 2] y + [0] 533.96/277.96 [0 1] [0 3] [4] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [+(0(), y)] = [1 2] y + [0] 533.96/277.96 [0 3] [0] 533.96/277.96 >= [1 0] y + [0] 533.96/277.96 [0 1] [0] 533.96/277.96 = [y] 533.96/277.96 533.96/277.96 [+(s(x), y)] = [1 0] x + [1 2] y + [0] 533.96/277.96 [0 1] [0 3] [4] 533.96/277.96 >= [1 0] x + [1 2] y + [0] 533.96/277.96 [0 1] [0 3] [4] 533.96/277.96 = [s(+(x, y))] 533.96/277.96 533.96/277.96 [f(g(f(x)))] = [8 8] x + [9] 533.96/277.96 [8 8] [9] 533.96/277.96 > [1 5] x + [7] 533.96/277.96 [1 5] [7] 533.96/277.96 = [f(h(s(0()), x))] 533.96/277.96 533.96/277.96 [f(g(h(x, y)))] = [1 7] x + [1 5] y + [15] 533.96/277.96 [1 7] [1 5] [15] 533.96/277.96 > [1 1] x + [1 5] y + [7] 533.96/277.96 [1 1] [1 5] [7] 533.96/277.96 = [f(h(s(x), y))] 533.96/277.96 533.96/277.96 [f(h(x, h(y, z)))] = [1 1] x + [1 5] y + [1 5] z + [13] 533.96/277.96 [1 1] [1 5] [1 5] [13] 533.96/277.96 > [1 1] x + [1 5] y + [1 5] z + [3] 533.96/277.96 [1 1] [1 5] [1 5] [3] 533.96/277.96 = [f(h(+(x, y), z))] 533.96/277.96 533.96/277.96 533.96/277.96 We return to the main proof. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict Trs: { +(s(x), y) -> s(+(x, y)) } 533.96/277.96 Weak Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'empty' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 2) 'With Problem ...' failed due to the following reason: 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 533.96/277.96 failed due to the following reason: 533.96/277.96 533.96/277.96 Computation stopped due to timeout after 24.0 seconds. 533.96/277.96 533.96/277.96 3) 'Best' failed due to the following reason: 533.96/277.96 533.96/277.96 None of the processors succeeded. 533.96/277.96 533.96/277.96 Details of failed attempt(s): 533.96/277.96 ----------------------------- 533.96/277.96 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 533.96/277.96 following reason: 533.96/277.96 533.96/277.96 The processor is inapplicable, reason: 533.96/277.96 Processor only applicable for innermost runtime complexity analysis 533.96/277.96 533.96/277.96 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 533.96/277.96 to the following reason: 533.96/277.96 533.96/277.96 The processor is inapplicable, reason: 533.96/277.96 Processor only applicable for innermost runtime complexity analysis 533.96/277.96 533.96/277.96 533.96/277.96 533.96/277.96 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 533.96/277.96 the following reason: 533.96/277.96 533.96/277.96 We add the following weak dependency pairs: 533.96/277.96 533.96/277.96 Strict DPs: 533.96/277.96 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z)) 533.96/277.96 , +^#(x, 0()) -> c_2(x) 533.96/277.96 , +^#(x, s(y)) -> c_3(+^#(x, y)) 533.96/277.96 , +^#(0(), y) -> c_4(y) 533.96/277.96 , +^#(s(x), y) -> c_5(+^#(x, y)) 533.96/277.96 , f^#(g(f(x))) -> c_6(f^#(h(s(0()), x))) 533.96/277.96 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 533.96/277.96 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z))) } 533.96/277.96 533.96/277.96 and mark the set of starting terms. 533.96/277.96 533.96/277.96 We are left with following problem, upon which TcT provides the 533.96/277.96 certificate MAYBE. 533.96/277.96 533.96/277.96 Strict DPs: 533.96/277.96 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z)) 533.96/277.96 , +^#(x, 0()) -> c_2(x) 533.96/277.96 , +^#(x, s(y)) -> c_3(+^#(x, y)) 533.96/277.96 , +^#(0(), y) -> c_4(y) 533.96/277.96 , +^#(s(x), y) -> c_5(+^#(x, y)) 533.96/277.96 , f^#(g(f(x))) -> c_6(f^#(h(s(0()), x))) 533.96/277.96 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 533.96/277.96 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z))) } 533.96/277.96 Strict Trs: 533.96/277.96 { +(x, +(y, z)) -> +(+(x, y), z) 533.96/277.96 , +(x, 0()) -> x 533.96/277.96 , +(x, s(y)) -> s(+(x, y)) 533.96/277.96 , +(0(), y) -> y 533.96/277.96 , +(s(x), y) -> s(+(x, y)) 533.96/277.96 , f(g(f(x))) -> f(h(s(0()), x)) 533.96/277.96 , f(g(h(x, y))) -> f(h(s(x), y)) 533.96/277.96 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 533.96/277.96 Obligation: 533.96/277.96 runtime complexity 533.96/277.96 Answer: 533.96/277.96 MAYBE 533.96/277.96 533.96/277.96 Empty strict component of the problem is NOT empty. 533.96/277.96 533.96/277.96 533.96/277.96 Arrrr.. 534.32/278.26 EOF