MAYBE 454.72/185.64 MAYBE 454.72/185.64 454.72/185.64 We are left with following problem, upon which TcT provides the 454.72/185.64 certificate MAYBE. 454.72/185.64 454.72/185.64 Strict Trs: 454.72/185.64 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.64 , g(Nil(), y) -> h(Nil(), y) 454.72/185.64 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.64 , h(Nil(), y) -> h(Nil(), y) 454.72/185.64 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.64 , f(Nil(), y) -> g(Nil(), y) 454.72/185.64 , sp1(x, y) -> f(x, y) 454.72/185.64 , r(x, y) -> x } 454.72/185.64 Obligation: 454.72/185.64 innermost runtime complexity 454.72/185.64 Answer: 454.72/185.64 MAYBE 454.72/185.64 454.72/185.64 None of the processors succeeded. 454.72/185.64 454.72/185.64 Details of failed attempt(s): 454.72/185.64 ----------------------------- 454.72/185.64 1) 'empty' failed due to the following reason: 454.72/185.64 454.72/185.64 Empty strict component of the problem is NOT empty. 454.72/185.64 454.72/185.64 2) 'Best' failed due to the following reason: 454.72/185.64 454.72/185.64 None of the processors succeeded. 454.72/185.64 454.72/185.64 Details of failed attempt(s): 454.72/185.64 ----------------------------- 454.72/185.64 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 454.72/185.64 following reason: 454.72/185.64 454.72/185.64 We add the following weak dependency pairs: 454.72/185.64 454.72/185.64 Strict DPs: 454.72/185.64 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.64 , g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.64 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.64 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.64 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.64 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.64 , sp1^#(x, y) -> c_7(f^#(x, y)) 454.72/185.64 , r^#(x, y) -> c_8() } 454.72/185.64 454.72/185.64 and mark the set of starting terms. 454.72/185.64 454.72/185.64 We are left with following problem, upon which TcT provides the 454.72/185.64 certificate MAYBE. 454.72/185.64 454.72/185.64 Strict DPs: 454.72/185.64 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.64 , g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.64 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.64 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.64 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.64 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.64 , sp1^#(x, y) -> c_7(f^#(x, y)) 454.72/185.64 , r^#(x, y) -> c_8() } 454.72/185.64 Strict Trs: 454.72/185.64 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.64 , g(Nil(), y) -> h(Nil(), y) 454.72/185.64 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.64 , h(Nil(), y) -> h(Nil(), y) 454.72/185.64 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.64 , f(Nil(), y) -> g(Nil(), y) 454.72/185.64 , sp1(x, y) -> f(x, y) 454.72/185.64 , r(x, y) -> x } 454.72/185.64 Obligation: 454.72/185.64 innermost runtime complexity 454.72/185.64 Answer: 454.72/185.64 MAYBE 454.72/185.64 454.72/185.64 No rule is usable, rules are removed from the input problem. 454.72/185.64 454.72/185.64 We are left with following problem, upon which TcT provides the 454.72/185.64 certificate MAYBE. 454.72/185.64 454.72/185.64 Strict DPs: 454.72/185.64 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.64 , g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.64 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.64 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.64 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.64 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.64 , sp1^#(x, y) -> c_7(f^#(x, y)) 454.72/185.64 , r^#(x, y) -> c_8() } 454.72/185.64 Obligation: 454.72/185.64 innermost runtime complexity 454.72/185.64 Answer: 454.72/185.64 MAYBE 454.72/185.64 454.72/185.64 The weightgap principle applies (using the following constant 454.72/185.64 growth matrix-interpretation) 454.72/185.64 454.72/185.64 The following argument positions are usable: 454.72/185.64 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 454.72/185.64 Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1} 454.72/185.64 454.72/185.64 TcT has computed the following constructor-restricted matrix 454.72/185.64 interpretation. 454.72/185.64 454.72/185.64 [Cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 454.72/185.64 [0 0] [0 0] [0] 454.72/185.64 454.72/185.64 [Nil] = [0] 454.72/185.64 [0] 454.72/185.64 454.72/185.64 [g^#](x1, x2) = [2 2] x2 + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 454.72/185.64 [c_1] = [2] 454.72/185.64 [0] 454.72/185.64 454.72/185.64 [c_2](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [h^#](x1, x2) = [2 2] x2 + [0] 454.72/185.64 [1 1] [0] 454.72/185.64 454.72/185.64 [c_3](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [f^#](x1, x2) = [2 2] x2 + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 454.72/185.64 [c_4](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [c_5](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [c_6](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [sp1^#](x1, x2) = [1 1] x1 + [2 2] x2 + [1] 454.72/185.64 [2 1] [1 2] [1] 454.72/185.64 454.72/185.64 [c_7](x1) = [1 0] x1 + [2] 454.72/185.64 [0 1] [2] 454.72/185.64 454.72/185.64 [r^#](x1, x2) = [2] 454.72/185.64 [1] 454.72/185.64 454.72/185.64 [c_8] = [1] 454.72/185.64 [1] 454.72/185.64 454.72/185.64 The order satisfies the following ordering constraints: 454.72/185.64 454.72/185.64 [g^#(Cons(x, xs), y)] = [2 2] y + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 ? [2] 454.72/185.64 [0] 454.72/185.64 = [c_1()] 454.72/185.64 454.72/185.64 [g^#(Nil(), y)] = [2 2] y + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [1 1] [2] 454.72/185.64 = [c_2(h^#(Nil(), y))] 454.72/185.64 454.72/185.64 [h^#(Cons(x, xs), y)] = [2 2] y + [0] 454.72/185.64 [1 1] [0] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [2 2] [2] 454.72/185.64 = [c_3(f^#(Cons(x, xs), y))] 454.72/185.64 454.72/185.64 [h^#(Nil(), y)] = [2 2] y + [0] 454.72/185.64 [1 1] [0] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [1 1] [2] 454.72/185.64 = [c_4(h^#(Nil(), y))] 454.72/185.64 454.72/185.64 [f^#(Cons(x, xs), y)] = [2 2] y + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [1 1] [2] 454.72/185.64 = [c_5(h^#(Cons(x, xs), y))] 454.72/185.64 454.72/185.64 [f^#(Nil(), y)] = [2 2] y + [0] 454.72/185.64 [2 2] [0] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [2 2] [2] 454.72/185.64 = [c_6(g^#(Nil(), y))] 454.72/185.64 454.72/185.64 [sp1^#(x, y)] = [1 1] x + [2 2] y + [1] 454.72/185.64 [2 1] [1 2] [1] 454.72/185.64 ? [2 2] y + [2] 454.72/185.64 [2 2] [2] 454.72/185.64 = [c_7(f^#(x, y))] 454.72/185.64 454.72/185.65 [r^#(x, y)] = [2] 454.72/185.65 [1] 454.72/185.65 > [1] 454.72/185.65 [1] 454.72/185.65 = [c_8()] 454.72/185.65 454.72/185.65 454.72/185.65 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.65 , g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 , sp1^#(x, y) -> c_7(f^#(x, y)) } 454.72/185.65 Weak DPs: { r^#(x, y) -> c_8() } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 We estimate the number of application of {1} by applications of 454.72/185.65 Pre({1}) = {}. Here rules are labeled as follows: 454.72/185.65 454.72/185.65 DPs: 454.72/185.65 { 1: g^#(Cons(x, xs), y) -> c_1() 454.72/185.65 , 2: g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , 3: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , 4: h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , 5: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 , 6: f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 , 7: sp1^#(x, y) -> c_7(f^#(x, y)) 454.72/185.65 , 8: r^#(x, y) -> c_8() } 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 , sp1^#(x, y) -> c_7(f^#(x, y)) } 454.72/185.65 Weak DPs: 454.72/185.65 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.65 , r^#(x, y) -> c_8() } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 The following weak DPs constitute a sub-graph of the DG that is 454.72/185.65 closed under successors. The DPs are removed. 454.72/185.65 454.72/185.65 { g^#(Cons(x, xs), y) -> c_1() 454.72/185.65 , r^#(x, y) -> c_8() } 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 , sp1^#(x, y) -> c_7(f^#(x, y)) } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 Consider the dependency graph 454.72/185.65 454.72/185.65 1: g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4 454.72/185.65 454.72/185.65 3: h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2 454.72/185.65 454.72/185.65 5: f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 -->_1 g^#(Nil(), y) -> c_2(h^#(Nil(), y)) :1 454.72/185.65 454.72/185.65 6: sp1^#(x, y) -> c_7(f^#(x, y)) 454.72/185.65 -->_1 f^#(Nil(), y) -> c_6(g^#(Nil(), y)) :5 454.72/185.65 -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4 454.72/185.65 454.72/185.65 454.72/185.65 Following roots of the dependency graph are removed, as the 454.72/185.65 considered set of starting terms is closed under reduction with 454.72/185.65 respect to these rules (modulo compound contexts). 454.72/185.65 454.72/185.65 { sp1^#(x, y) -> c_7(f^#(x, y)) } 454.72/185.65 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 Consider the dependency graph 454.72/185.65 454.72/185.65 1: g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4 454.72/185.65 454.72/185.65 3: h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2 454.72/185.65 454.72/185.65 5: f^#(Nil(), y) -> c_6(g^#(Nil(), y)) 454.72/185.65 -->_1 g^#(Nil(), y) -> c_2(h^#(Nil(), y)) :1 454.72/185.65 454.72/185.65 454.72/185.65 Following roots of the dependency graph are removed, as the 454.72/185.65 considered set of starting terms is closed under reduction with 454.72/185.65 respect to these rules (modulo compound contexts). 454.72/185.65 454.72/185.65 { f^#(Nil(), y) -> c_6(g^#(Nil(), y)) } 454.72/185.65 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 Consider the dependency graph 454.72/185.65 454.72/185.65 1: g^#(Nil(), y) -> c_2(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4 454.72/185.65 454.72/185.65 3: h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3 454.72/185.65 454.72/185.65 4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) 454.72/185.65 -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2 454.72/185.65 454.72/185.65 454.72/185.65 Following roots of the dependency graph are removed, as the 454.72/185.65 considered set of starting terms is closed under reduction with 454.72/185.65 respect to these rules (modulo compound contexts). 454.72/185.65 454.72/185.65 { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) } 454.72/185.65 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict DPs: 454.72/185.65 { h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) 454.72/185.65 , h^#(Nil(), y) -> c_4(h^#(Nil(), y)) 454.72/185.65 , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 None of the processors succeeded. 454.72/185.65 454.72/185.65 Details of failed attempt(s): 454.72/185.65 ----------------------------- 454.72/185.65 1) 'empty' failed due to the following reason: 454.72/185.65 454.72/185.65 Empty strict component of the problem is NOT empty. 454.72/185.65 454.72/185.65 2) 'With Problem ...' failed due to the following reason: 454.72/185.65 454.72/185.65 None of the processors succeeded. 454.72/185.65 454.72/185.65 Details of failed attempt(s): 454.72/185.65 ----------------------------- 454.72/185.65 1) 'empty' failed due to the following reason: 454.72/185.65 454.72/185.65 Empty strict component of the problem is NOT empty. 454.72/185.65 454.72/185.65 2) 'Fastest' failed due to the following reason: 454.72/185.65 454.72/185.65 None of the processors succeeded. 454.72/185.65 454.72/185.65 Details of failed attempt(s): 454.72/185.65 ----------------------------- 454.72/185.65 1) 'With Problem ...' failed due to the following reason: 454.72/185.65 454.72/185.65 None of the processors succeeded. 454.72/185.65 454.72/185.65 Details of failed attempt(s): 454.72/185.65 ----------------------------- 454.72/185.65 1) 'empty' failed due to the following reason: 454.72/185.65 454.72/185.65 Empty strict component of the problem is NOT empty. 454.72/185.65 454.72/185.65 2) 'Polynomial Path Order (PS)' failed due to the following reason: 454.72/185.65 454.72/185.65 The input cannot be shown compatible 454.72/185.65 454.72/185.65 454.72/185.65 2) 'Fastest (timeout of 24 seconds)' failed due to the following 454.72/185.65 reason: 454.72/185.65 454.72/185.65 Computation stopped due to timeout after 24.0 seconds. 454.72/185.65 454.72/185.65 3) 'Polynomial Path Order (PS)' failed due to the following reason: 454.72/185.65 454.72/185.65 The input cannot be shown compatible 454.72/185.65 454.72/185.65 454.72/185.65 454.72/185.65 454.72/185.65 2) 'Best' failed due to the following reason: 454.72/185.65 454.72/185.65 None of the processors succeeded. 454.72/185.65 454.72/185.65 Details of failed attempt(s): 454.72/185.65 ----------------------------- 454.72/185.65 1) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 454.72/185.65 failed due to the following reason: 454.72/185.65 454.72/185.65 Computation stopped due to timeout after 24.0 seconds. 454.72/185.65 454.72/185.65 2) 'With Problem ... (timeout of 148 seconds) (timeout of 297 454.72/185.65 seconds)' failed due to the following reason: 454.72/185.65 454.72/185.65 We use the processor 'matrix interpretation of dimension 1' to 454.72/185.65 orient following rules strictly. 454.72/185.65 454.72/185.65 Trs: 454.72/185.65 { sp1(x, y) -> f(x, y) 454.72/185.65 , r(x, y) -> x } 454.72/185.65 454.72/185.65 The induced complexity on above rules (modulo remaining rules) is 454.72/185.65 YES(?,O(n^1)) . These rules are moved into the corresponding weak 454.72/185.65 component(s). 454.72/185.65 454.72/185.65 Sub-proof: 454.72/185.65 ---------- 454.72/185.65 The following argument positions are usable: 454.72/185.65 none 454.72/185.65 454.72/185.65 TcT has computed the following constructor-based matrix 454.72/185.65 interpretation satisfying not(EDA). 454.72/185.65 454.72/185.65 [g](x1, x2) = [7] x2 + [0] 454.72/185.65 454.72/185.65 [Cons](x1, x2) = [0] 454.72/185.65 454.72/185.65 [h](x1, x2) = [7] x2 + [0] 454.72/185.65 454.72/185.65 [Nil] = [0] 454.72/185.65 454.72/185.65 [f](x1, x2) = [7] x2 + [0] 454.72/185.65 454.72/185.65 [sp1](x1, x2) = [7] x1 + [7] x2 + [7] 454.72/185.65 454.72/185.65 [r](x1, x2) = [7] x1 + [7] x2 + [7] 454.72/185.65 454.72/185.65 The order satisfies the following ordering constraints: 454.72/185.65 454.72/185.65 [g(Cons(x, xs), y)] = [7] y + [0] 454.72/185.65 >= [0] 454.72/185.65 = [Cons(x, xs)] 454.72/185.65 454.72/185.65 [g(Nil(), y)] = [7] y + [0] 454.72/185.65 >= [7] y + [0] 454.72/185.65 = [h(Nil(), y)] 454.72/185.65 454.72/185.65 [h(Cons(x, xs), y)] = [7] y + [0] 454.72/185.65 >= [7] y + [0] 454.72/185.65 = [f(Cons(x, xs), y)] 454.72/185.65 454.72/185.65 [h(Nil(), y)] = [7] y + [0] 454.72/185.65 >= [7] y + [0] 454.72/185.65 = [h(Nil(), y)] 454.72/185.65 454.72/185.65 [f(Cons(x, xs), y)] = [7] y + [0] 454.72/185.65 >= [7] y + [0] 454.72/185.65 = [h(Cons(x, xs), y)] 454.72/185.65 454.72/185.65 [f(Nil(), y)] = [7] y + [0] 454.72/185.65 >= [7] y + [0] 454.72/185.65 = [g(Nil(), y)] 454.72/185.65 454.72/185.65 [sp1(x, y)] = [7] x + [7] y + [7] 454.72/185.65 > [7] y + [0] 454.72/185.65 = [f(x, y)] 454.72/185.65 454.72/185.65 [r(x, y)] = [7] x + [7] y + [7] 454.72/185.65 > [1] x + [0] 454.72/185.65 = [x] 454.72/185.65 454.72/185.65 454.72/185.65 We return to the main proof. 454.72/185.65 454.72/185.65 We are left with following problem, upon which TcT provides the 454.72/185.65 certificate MAYBE. 454.72/185.65 454.72/185.65 Strict Trs: 454.72/185.65 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.65 , g(Nil(), y) -> h(Nil(), y) 454.72/185.65 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.65 , h(Nil(), y) -> h(Nil(), y) 454.72/185.65 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.65 , f(Nil(), y) -> g(Nil(), y) } 454.72/185.65 Weak Trs: 454.72/185.65 { sp1(x, y) -> f(x, y) 454.72/185.65 , r(x, y) -> x } 454.72/185.65 Obligation: 454.72/185.65 innermost runtime complexity 454.72/185.65 Answer: 454.72/185.65 MAYBE 454.72/185.65 454.72/185.65 The weightgap principle applies (using the following nonconstant 454.72/185.65 growth matrix-interpretation) 454.72/185.65 454.72/185.65 The following argument positions are usable: 454.72/185.65 none 454.72/185.65 454.72/185.65 TcT has computed the following matrix interpretation satisfying 454.72/185.65 not(EDA) and not(IDA(1)). 454.72/185.65 454.72/185.65 [g](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.65 454.72/185.65 [Cons](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.65 454.72/185.65 [h](x1, x2) = [1] x2 + [0] 454.72/185.65 454.72/185.65 [Nil] = [4] 454.72/185.65 454.72/185.65 [f](x1, x2) = [1] x2 + [0] 454.72/185.65 454.72/185.65 [sp1](x1, x2) = [1] x1 + [1] x2 + [7] 454.72/185.65 454.72/185.65 [r](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.65 454.72/185.65 The order satisfies the following ordering constraints: 454.72/185.65 454.72/185.65 [g(Cons(x, xs), y)] = [1] x + [1] xs + [1] y + [0] 454.72/185.65 >= [1] x + [1] xs + [0] 454.72/185.65 = [Cons(x, xs)] 454.72/185.65 454.72/185.65 [g(Nil(), y)] = [1] y + [4] 454.72/185.65 > [1] y + [0] 454.72/185.65 = [h(Nil(), y)] 454.72/185.65 454.72/185.65 [h(Cons(x, xs), y)] = [1] y + [0] 454.72/185.65 >= [1] y + [0] 454.72/185.65 = [f(Cons(x, xs), y)] 454.72/185.65 454.72/185.65 [h(Nil(), y)] = [1] y + [0] 454.72/185.65 >= [1] y + [0] 454.72/185.65 = [h(Nil(), y)] 454.72/185.65 454.72/185.65 [f(Cons(x, xs), y)] = [1] y + [0] 454.72/185.65 >= [1] y + [0] 454.72/185.65 = [h(Cons(x, xs), y)] 454.72/185.65 454.72/185.65 [f(Nil(), y)] = [1] y + [0] 454.72/185.65 ? [1] y + [4] 454.72/185.65 = [g(Nil(), y)] 454.72/185.65 454.72/185.65 [sp1(x, y)] = [1] x + [1] y + [7] 454.72/185.65 > [1] y + [0] 454.72/185.65 = [f(x, y)] 454.72/185.65 454.72/185.65 [r(x, y)] = [1] x + [1] y + [0] 454.72/185.65 >= [1] x + [0] 454.72/185.65 = [x] 454.72/185.66 454.72/185.66 454.72/185.66 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 454.72/185.66 454.72/185.66 We are left with following problem, upon which TcT provides the 454.72/185.66 certificate MAYBE. 454.72/185.66 454.72/185.66 Strict Trs: 454.72/185.66 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.66 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.66 , h(Nil(), y) -> h(Nil(), y) 454.72/185.66 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.66 , f(Nil(), y) -> g(Nil(), y) } 454.72/185.66 Weak Trs: 454.72/185.66 { g(Nil(), y) -> h(Nil(), y) 454.72/185.66 , sp1(x, y) -> f(x, y) 454.72/185.66 , r(x, y) -> x } 454.72/185.66 Obligation: 454.72/185.66 innermost runtime complexity 454.72/185.66 Answer: 454.72/185.66 MAYBE 454.72/185.66 454.72/185.66 The weightgap principle applies (using the following nonconstant 454.72/185.66 growth matrix-interpretation) 454.72/185.66 454.72/185.66 The following argument positions are usable: 454.72/185.66 none 454.72/185.66 454.72/185.66 TcT has computed the following matrix interpretation satisfying 454.72/185.66 not(EDA) and not(IDA(1)). 454.72/185.66 454.72/185.66 [g](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 [Cons](x1, x2) = [4] 454.72/185.66 454.72/185.66 [h](x1, x2) = [1] x2 + [0] 454.72/185.66 454.72/185.66 [Nil] = [4] 454.72/185.66 454.72/185.66 [f](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 [sp1](x1, x2) = [1] x1 + [1] x2 + [7] 454.72/185.66 454.72/185.66 [r](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 The order satisfies the following ordering constraints: 454.72/185.66 454.72/185.66 [g(Cons(x, xs), y)] = [1] y + [4] 454.72/185.66 >= [4] 454.72/185.66 = [Cons(x, xs)] 454.72/185.66 454.72/185.66 [g(Nil(), y)] = [1] y + [4] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [h(Cons(x, xs), y)] = [1] y + [0] 454.72/185.66 ? [1] y + [4] 454.72/185.66 = [f(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [h(Nil(), y)] = [1] y + [0] 454.72/185.66 >= [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [f(Cons(x, xs), y)] = [1] y + [4] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [h(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [f(Nil(), y)] = [1] y + [4] 454.72/185.66 >= [1] y + [4] 454.72/185.66 = [g(Nil(), y)] 454.72/185.66 454.72/185.66 [sp1(x, y)] = [1] x + [1] y + [7] 454.72/185.66 > [1] x + [1] y + [0] 454.72/185.66 = [f(x, y)] 454.72/185.66 454.72/185.66 [r(x, y)] = [1] x + [1] y + [0] 454.72/185.66 >= [1] x + [0] 454.72/185.66 = [x] 454.72/185.66 454.72/185.66 454.72/185.66 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 454.72/185.66 454.72/185.66 We are left with following problem, upon which TcT provides the 454.72/185.66 certificate MAYBE. 454.72/185.66 454.72/185.66 Strict Trs: 454.72/185.66 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.66 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.66 , h(Nil(), y) -> h(Nil(), y) 454.72/185.66 , f(Nil(), y) -> g(Nil(), y) } 454.72/185.66 Weak Trs: 454.72/185.66 { g(Nil(), y) -> h(Nil(), y) 454.72/185.66 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.66 , sp1(x, y) -> f(x, y) 454.72/185.66 , r(x, y) -> x } 454.72/185.66 Obligation: 454.72/185.66 innermost runtime complexity 454.72/185.66 Answer: 454.72/185.66 MAYBE 454.72/185.66 454.72/185.66 The weightgap principle applies (using the following nonconstant 454.72/185.66 growth matrix-interpretation) 454.72/185.66 454.72/185.66 The following argument positions are usable: 454.72/185.66 none 454.72/185.66 454.72/185.66 TcT has computed the following matrix interpretation satisfying 454.72/185.66 not(EDA) and not(IDA(1)). 454.72/185.66 454.72/185.66 [g](x1, x2) = [1] x2 + [0] 454.72/185.66 454.72/185.66 [Cons](x1, x2) = [4] 454.72/185.66 454.72/185.66 [h](x1, x2) = [1] x2 + [0] 454.72/185.66 454.72/185.66 [Nil] = [4] 454.72/185.66 454.72/185.66 [f](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 [sp1](x1, x2) = [1] x1 + [1] x2 + [7] 454.72/185.66 454.72/185.66 [r](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 The order satisfies the following ordering constraints: 454.72/185.66 454.72/185.66 [g(Cons(x, xs), y)] = [1] y + [0] 454.72/185.66 ? [4] 454.72/185.66 = [Cons(x, xs)] 454.72/185.66 454.72/185.66 [g(Nil(), y)] = [1] y + [0] 454.72/185.66 >= [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [h(Cons(x, xs), y)] = [1] y + [0] 454.72/185.66 ? [1] y + [4] 454.72/185.66 = [f(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [h(Nil(), y)] = [1] y + [0] 454.72/185.66 >= [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [f(Cons(x, xs), y)] = [1] y + [4] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [h(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [f(Nil(), y)] = [1] y + [4] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [g(Nil(), y)] 454.72/185.66 454.72/185.66 [sp1(x, y)] = [1] x + [1] y + [7] 454.72/185.66 > [1] x + [1] y + [0] 454.72/185.66 = [f(x, y)] 454.72/185.66 454.72/185.66 [r(x, y)] = [1] x + [1] y + [0] 454.72/185.66 >= [1] x + [0] 454.72/185.66 = [x] 454.72/185.66 454.72/185.66 454.72/185.66 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 454.72/185.66 454.72/185.66 We are left with following problem, upon which TcT provides the 454.72/185.66 certificate MAYBE. 454.72/185.66 454.72/185.66 Strict Trs: 454.72/185.66 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.66 , h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.66 , h(Nil(), y) -> h(Nil(), y) } 454.72/185.66 Weak Trs: 454.72/185.66 { g(Nil(), y) -> h(Nil(), y) 454.72/185.66 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.66 , f(Nil(), y) -> g(Nil(), y) 454.72/185.66 , sp1(x, y) -> f(x, y) 454.72/185.66 , r(x, y) -> x } 454.72/185.66 Obligation: 454.72/185.66 innermost runtime complexity 454.72/185.66 Answer: 454.72/185.66 MAYBE 454.72/185.66 454.72/185.66 The weightgap principle applies (using the following nonconstant 454.72/185.66 growth matrix-interpretation) 454.72/185.66 454.72/185.66 The following argument positions are usable: 454.72/185.66 none 454.72/185.66 454.72/185.66 TcT has computed the following matrix interpretation satisfying 454.72/185.66 not(EDA) and not(IDA(1)). 454.72/185.66 454.72/185.66 [g](x1, x2) = [1] x1 + [1] x2 + [4] 454.72/185.66 454.72/185.66 [Cons](x1, x2) = [4] 454.72/185.66 454.72/185.66 [h](x1, x2) = [1] x2 + [0] 454.72/185.66 454.72/185.66 [Nil] = [4] 454.72/185.66 454.72/185.66 [f](x1, x2) = [1] x1 + [1] x2 + [4] 454.72/185.66 454.72/185.66 [sp1](x1, x2) = [1] x1 + [1] x2 + [7] 454.72/185.66 454.72/185.66 [r](x1, x2) = [1] x1 + [1] x2 + [0] 454.72/185.66 454.72/185.66 The order satisfies the following ordering constraints: 454.72/185.66 454.72/185.66 [g(Cons(x, xs), y)] = [1] y + [8] 454.72/185.66 > [4] 454.72/185.66 = [Cons(x, xs)] 454.72/185.66 454.72/185.66 [g(Nil(), y)] = [1] y + [8] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [h(Cons(x, xs), y)] = [1] y + [0] 454.72/185.66 ? [1] y + [8] 454.72/185.66 = [f(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [h(Nil(), y)] = [1] y + [0] 454.72/185.66 >= [1] y + [0] 454.72/185.66 = [h(Nil(), y)] 454.72/185.66 454.72/185.66 [f(Cons(x, xs), y)] = [1] y + [8] 454.72/185.66 > [1] y + [0] 454.72/185.66 = [h(Cons(x, xs), y)] 454.72/185.66 454.72/185.66 [f(Nil(), y)] = [1] y + [8] 454.72/185.66 >= [1] y + [8] 454.72/185.66 = [g(Nil(), y)] 454.72/185.66 454.72/185.66 [sp1(x, y)] = [1] x + [1] y + [7] 454.72/185.66 > [1] x + [1] y + [4] 454.72/185.66 = [f(x, y)] 454.72/185.66 454.72/185.66 [r(x, y)] = [1] x + [1] y + [0] 454.72/185.66 >= [1] x + [0] 454.72/185.66 = [x] 454.72/185.66 454.72/185.66 454.72/185.66 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 454.72/185.66 454.72/185.66 We are left with following problem, upon which TcT provides the 454.72/185.66 certificate MAYBE. 454.72/185.66 454.72/185.66 Strict Trs: 454.72/185.66 { h(Cons(x, xs), y) -> f(Cons(x, xs), y) 454.72/185.66 , h(Nil(), y) -> h(Nil(), y) } 454.72/185.66 Weak Trs: 454.72/185.66 { g(Cons(x, xs), y) -> Cons(x, xs) 454.72/185.66 , g(Nil(), y) -> h(Nil(), y) 454.72/185.66 , f(Cons(x, xs), y) -> h(Cons(x, xs), y) 454.72/185.66 , f(Nil(), y) -> g(Nil(), y) 454.72/185.66 , sp1(x, y) -> f(x, y) 454.72/185.66 , r(x, y) -> x } 454.72/185.66 Obligation: 454.72/185.66 innermost runtime complexity 454.72/185.66 Answer: 454.72/185.66 MAYBE 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'Fastest' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'empty' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 2) 'With Problem ...' failed due to the following reason: 454.72/185.66 454.72/185.66 Empty strict component of the problem is NOT empty. 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 3) 'Best' failed due to the following reason: 454.72/185.66 454.72/185.66 None of the processors succeeded. 454.72/185.66 454.72/185.66 Details of failed attempt(s): 454.72/185.66 ----------------------------- 454.72/185.66 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 454.72/185.66 following reason: 454.72/185.66 454.72/185.66 The input cannot be shown compatible 454.72/185.66 454.72/185.66 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 454.72/185.66 to the following reason: 454.72/185.66 454.72/185.66 The input cannot be shown compatible 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 454.72/185.66 Arrrr.. 454.98/185.89 EOF