MAYBE 212.91/115.73 MAYBE 212.91/115.73 212.91/115.73 We are left with following problem, upon which TcT provides the 212.91/115.73 certificate MAYBE. 212.91/115.73 212.91/115.73 Strict Trs: 212.91/115.73 { sqr(0()) -> 0() 212.91/115.73 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.73 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.73 , +(x, 0()) -> x 212.91/115.73 , +(x, s(y)) -> s(+(x, y)) 212.91/115.73 , double(0()) -> 0() 212.91/115.73 , double(s(x)) -> s(s(double(x))) } 212.91/115.73 Obligation: 212.91/115.73 runtime complexity 212.91/115.73 Answer: 212.91/115.73 MAYBE 212.91/115.73 212.91/115.73 None of the processors succeeded. 212.91/115.73 212.91/115.73 Details of failed attempt(s): 212.91/115.73 ----------------------------- 212.91/115.73 1) 'Best' failed due to the following reason: 212.91/115.73 212.91/115.73 None of the processors succeeded. 212.91/115.73 212.91/115.73 Details of failed attempt(s): 212.91/115.73 ----------------------------- 212.91/115.73 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 212.91/115.73 seconds)' failed due to the following reason: 212.91/115.73 212.91/115.73 The weightgap principle applies (using the following nonconstant 212.91/115.73 growth matrix-interpretation) 212.91/115.73 212.91/115.73 The following argument positions are usable: 212.91/115.73 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.73 212.91/115.73 TcT has computed the following matrix interpretation satisfying 212.91/115.74 not(EDA) and not(IDA(1)). 212.91/115.74 212.91/115.74 [sqr](x1) = [0] 212.91/115.74 212.91/115.74 [0] = [1] 212.91/115.74 212.91/115.74 [s](x1) = [1] x1 + [0] 212.91/115.74 212.91/115.74 [+](x1, x2) = [1] x1 + [1] x2 + [0] 212.91/115.74 212.91/115.74 [double](x1) = [0] 212.91/115.74 212.91/115.74 The order satisfies the following ordering constraints: 212.91/115.74 212.91/115.74 [sqr(0())] = [0] 212.91/115.74 ? [1] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0] 212.91/115.74 >= [0] 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0] 212.91/115.74 >= [0] 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = [1] x + [1] 212.91/115.74 > [1] x + [0] 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = [1] x + [1] y + [0] 212.91/115.74 >= [1] x + [1] y + [0] 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = [0] 212.91/115.74 ? [1] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = [0] 212.91/115.74 >= [0] 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(0()) -> 0() 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: { +(x, 0()) -> x } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 The weightgap principle applies (using the following nonconstant 212.91/115.74 growth matrix-interpretation) 212.91/115.74 212.91/115.74 The following argument positions are usable: 212.91/115.74 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.74 212.91/115.74 TcT has computed the following matrix interpretation satisfying 212.91/115.74 not(EDA) and not(IDA(1)). 212.91/115.74 212.91/115.74 [sqr](x1) = [0] 212.91/115.74 212.91/115.74 [0] = [0] 212.91/115.74 212.91/115.74 [s](x1) = [1] x1 + [0] 212.91/115.74 212.91/115.74 [+](x1, x2) = [1] x1 + [1] x2 + [0] 212.91/115.74 212.91/115.74 [double](x1) = [1] 212.91/115.74 212.91/115.74 The order satisfies the following ordering constraints: 212.91/115.74 212.91/115.74 [sqr(0())] = [0] 212.91/115.74 >= [0] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0] 212.91/115.74 ? [1] 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0] 212.91/115.74 ? [1] 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = [1] x + [0] 212.91/115.74 >= [1] x + [0] 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = [1] x + [1] y + [0] 212.91/115.74 >= [1] x + [1] y + [0] 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = [1] 212.91/115.74 > [0] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = [1] 212.91/115.74 >= [1] 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: 212.91/115.74 { +(x, 0()) -> x 212.91/115.74 , double(0()) -> 0() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 The weightgap principle applies (using the following nonconstant 212.91/115.74 growth matrix-interpretation) 212.91/115.74 212.91/115.74 The following argument positions are usable: 212.91/115.74 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.74 212.91/115.74 TcT has computed the following matrix interpretation satisfying 212.91/115.74 not(EDA) and not(IDA(1)). 212.91/115.74 212.91/115.74 [sqr](x1) = [1] x1 + [4] 212.91/115.74 212.91/115.74 [0] = [4] 212.91/115.74 212.91/115.74 [s](x1) = [1] x1 + [0] 212.91/115.74 212.91/115.74 [+](x1, x2) = [1] x1 + [1] x2 + [0] 212.91/115.74 212.91/115.74 [double](x1) = [4] 212.91/115.74 212.91/115.74 The order satisfies the following ordering constraints: 212.91/115.74 212.91/115.74 [sqr(0())] = [8] 212.91/115.74 > [4] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [1] x + [4] 212.91/115.74 ? [1] x + [8] 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [1] x + [4] 212.91/115.74 ? [1] x + [8] 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = [1] x + [4] 212.91/115.74 > [1] x + [0] 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = [1] x + [1] y + [0] 212.91/115.74 >= [1] x + [1] y + [0] 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = [4] 212.91/115.74 >= [4] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = [4] 212.91/115.74 >= [4] 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , double(0()) -> 0() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'Fastest' failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 The weightgap principle applies (using the following nonconstant 212.91/115.74 growth matrix-interpretation) 212.91/115.74 212.91/115.74 The following argument positions are usable: 212.91/115.74 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.74 212.91/115.74 TcT has computed the following matrix interpretation satisfying 212.91/115.74 not(EDA) and not(IDA(1)). 212.91/115.74 212.91/115.74 [sqr](x1) = [0 1] x1 + [0] 212.91/115.74 [0 1] [0] 212.91/115.74 212.91/115.74 [0] = [0] 212.91/115.74 [0] 212.91/115.74 212.91/115.74 [s](x1) = [1 0] x1 + [0] 212.91/115.74 [0 1] [4] 212.91/115.74 212.91/115.74 [+](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 212.91/115.74 [0 1] [0 0] [0] 212.91/115.74 212.91/115.74 [double](x1) = [0] 212.91/115.74 [4] 212.91/115.74 212.91/115.74 The order satisfies the following ordering constraints: 212.91/115.74 212.91/115.74 [sqr(0())] = [0] 212.91/115.74 [0] 212.91/115.74 >= [0] 212.91/115.74 [0] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0 1] x + [4] 212.91/115.74 [0 1] [4] 212.91/115.74 > [0 1] x + [0] 212.91/115.74 [0 1] [4] 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = [0 1] x + [4] 212.91/115.74 [0 1] [4] 212.91/115.74 > [0 1] x + [0] 212.91/115.74 [0 1] [0] 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = [1 0] x + [0] 212.91/115.74 [0 1] [0] 212.91/115.74 >= [1 0] x + [0] 212.91/115.74 [0 1] [0] 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = [1 0] x + [1 0] y + [0] 212.91/115.74 [0 1] [0 0] [0] 212.91/115.74 ? [1 0] x + [1 0] y + [0] 212.91/115.74 [0 1] [0 0] [4] 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = [0] 212.91/115.74 [4] 212.91/115.74 >= [0] 212.91/115.74 [0] 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = [0] 212.91/115.74 [4] 212.91/115.74 ? [0] 212.91/115.74 [12] 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: 212.91/115.74 { +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , double(0()) -> 0() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 We use the processor 'polynomial interpretation' to orient 212.91/115.74 following rules strictly. 212.91/115.74 212.91/115.74 Trs: 212.91/115.74 { sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) } 212.91/115.74 212.91/115.74 The induced complexity on above rules (modulo remaining rules) is 212.91/115.74 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.91/115.74 component(s). 212.91/115.74 212.91/115.74 Sub-proof: 212.91/115.74 ---------- 212.91/115.74 We consider the following typing: 212.91/115.74 212.91/115.74 sqr :: a -> a 212.91/115.74 0 :: a 212.91/115.74 s :: a -> a 212.91/115.74 + :: (a,a) -> a 212.91/115.74 double :: a -> a 212.91/115.74 212.91/115.74 The following argument positions are considered usable: 212.91/115.74 212.91/115.74 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.74 212.91/115.74 TcT has computed the following constructor-restricted 212.91/115.74 typedpolynomial interpretation. 212.91/115.74 212.91/115.74 [sqr](x1) = 2*x1^2 212.91/115.74 212.91/115.74 [0]() = 0 212.91/115.74 212.91/115.74 [s](x1) = 1 + x1 212.91/115.74 212.91/115.74 [+](x1, x2) = x1 + 2*x2 212.91/115.74 212.91/115.74 [double](x1) = 2*x1 212.91/115.74 212.91/115.74 212.91/115.74 This order satisfies the following ordering constraints. 212.91/115.74 212.91/115.74 [sqr(0())] = 212.91/115.74 >= 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = 2 + 4*x + 2*x^2 212.91/115.74 > 1 + 2*x^2 + 4*x 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = 2 + 4*x + 2*x^2 212.91/115.74 >= 2*x^2 + 2 + 4*x 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = x 212.91/115.74 >= x 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = x + 2 + 2*y 212.91/115.74 > 1 + x + 2*y 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = 212.91/115.74 >= 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = 2 + 2*x 212.91/115.74 >= 2 + 2*x 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 We return to the main proof. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(0()) -> 0() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 We use the processor 'polynomial interpretation' to orient 212.91/115.74 following rules strictly. 212.91/115.74 212.91/115.74 Trs: { sqr(s(x)) -> +(sqr(x), s(double(x))) } 212.91/115.74 212.91/115.74 The induced complexity on above rules (modulo remaining rules) is 212.91/115.74 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.91/115.74 component(s). 212.91/115.74 212.91/115.74 Sub-proof: 212.91/115.74 ---------- 212.91/115.74 We consider the following typing: 212.91/115.74 212.91/115.74 sqr :: a -> a 212.91/115.74 0 :: a 212.91/115.74 s :: a -> a 212.91/115.74 + :: (a,a) -> a 212.91/115.74 double :: a -> a 212.91/115.74 212.91/115.74 The following argument positions are considered usable: 212.91/115.74 212.91/115.74 Uargs(s) = {1}, Uargs(+) = {1, 2} 212.91/115.74 212.91/115.74 TcT has computed the following constructor-restricted 212.91/115.74 typedpolynomial interpretation. 212.91/115.74 212.91/115.74 [sqr](x1) = 2*x1 + 2*x1^2 212.91/115.74 212.91/115.74 [0]() = 0 212.91/115.74 212.91/115.74 [s](x1) = 1 + x1 212.91/115.74 212.91/115.74 [+](x1, x2) = x1 + x2 212.91/115.74 212.91/115.74 [double](x1) = 2*x1 212.91/115.74 212.91/115.74 212.91/115.74 This order satisfies the following ordering constraints. 212.91/115.74 212.91/115.74 [sqr(0())] = 212.91/115.74 >= 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [sqr(s(x))] = 4 + 6*x + 2*x^2 212.91/115.74 > 1 + 4*x + 2*x^2 212.91/115.74 = [s(+(sqr(x), double(x)))] 212.91/115.74 212.91/115.74 [sqr(s(x))] = 4 + 6*x + 2*x^2 212.91/115.74 > 4*x + 2*x^2 + 1 212.91/115.74 = [+(sqr(x), s(double(x)))] 212.91/115.74 212.91/115.74 [+(x, 0())] = x 212.91/115.74 >= x 212.91/115.74 = [x] 212.91/115.74 212.91/115.74 [+(x, s(y))] = x + 1 + y 212.91/115.74 >= 1 + x + y 212.91/115.74 = [s(+(x, y))] 212.91/115.74 212.91/115.74 [double(0())] = 212.91/115.74 >= 212.91/115.74 = [0()] 212.91/115.74 212.91/115.74 [double(s(x))] = 2 + 2*x 212.91/115.74 >= 2 + 2*x 212.91/115.74 = [s(s(double(x)))] 212.91/115.74 212.91/115.74 212.91/115.74 We return to the main proof. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict Trs: { double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(0()) -> 0() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'empty' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 2) 'With Problem ...' failed due to the following reason: 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 2) 'Best' failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 212.91/115.74 to the following reason: 212.91/115.74 212.91/115.74 The processor is inapplicable, reason: 212.91/115.74 Processor only applicable for innermost runtime complexity analysis 212.91/115.74 212.91/115.74 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 212.91/115.74 following reason: 212.91/115.74 212.91/115.74 The processor is inapplicable, reason: 212.91/115.74 Processor only applicable for innermost runtime complexity analysis 212.91/115.74 212.91/115.74 212.91/115.74 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 212.91/115.74 failed due to the following reason: 212.91/115.74 212.91/115.74 None of the processors succeeded. 212.91/115.74 212.91/115.74 Details of failed attempt(s): 212.91/115.74 ----------------------------- 212.91/115.74 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 212.91/115.74 failed due to the following reason: 212.91/115.74 212.91/115.74 match-boundness of the problem could not be verified. 212.91/115.74 212.91/115.74 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 212.91/115.74 failed due to the following reason: 212.91/115.74 212.91/115.74 match-boundness of the problem could not be verified. 212.91/115.74 212.91/115.74 212.91/115.74 212.91/115.74 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 212.91/115.74 the following reason: 212.91/115.74 212.91/115.74 We add the following weak dependency pairs: 212.91/115.74 212.91/115.74 Strict DPs: 212.91/115.74 { sqr^#(0()) -> c_1() 212.91/115.74 , sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x))) 212.91/115.74 , sqr^#(s(x)) -> c_3(+^#(sqr(x), s(double(x)))) 212.91/115.74 , +^#(x, 0()) -> c_4(x) 212.91/115.74 , +^#(x, s(y)) -> c_5(+^#(x, y)) 212.91/115.74 , double^#(0()) -> c_6() 212.91/115.74 , double^#(s(x)) -> c_7(double^#(x)) } 212.91/115.74 212.91/115.74 and mark the set of starting terms. 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict DPs: 212.91/115.74 { sqr^#(0()) -> c_1() 212.91/115.74 , sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x))) 212.91/115.74 , sqr^#(s(x)) -> c_3(+^#(sqr(x), s(double(x)))) 212.91/115.74 , +^#(x, 0()) -> c_4(x) 212.91/115.74 , +^#(x, s(y)) -> c_5(+^#(x, y)) 212.91/115.74 , double^#(0()) -> c_6() 212.91/115.74 , double^#(s(x)) -> c_7(double^#(x)) } 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(0()) -> 0() 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 We estimate the number of application of {1,6} by applications of 212.91/115.74 Pre({1,6}) = {4,7}. Here rules are labeled as follows: 212.91/115.74 212.91/115.74 DPs: 212.91/115.74 { 1: sqr^#(0()) -> c_1() 212.91/115.74 , 2: sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x))) 212.91/115.74 , 3: sqr^#(s(x)) -> c_3(+^#(sqr(x), s(double(x)))) 212.91/115.74 , 4: +^#(x, 0()) -> c_4(x) 212.91/115.74 , 5: +^#(x, s(y)) -> c_5(+^#(x, y)) 212.91/115.74 , 6: double^#(0()) -> c_6() 212.91/115.74 , 7: double^#(s(x)) -> c_7(double^#(x)) } 212.91/115.74 212.91/115.74 We are left with following problem, upon which TcT provides the 212.91/115.74 certificate MAYBE. 212.91/115.74 212.91/115.74 Strict DPs: 212.91/115.74 { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x))) 212.91/115.74 , sqr^#(s(x)) -> c_3(+^#(sqr(x), s(double(x)))) 212.91/115.74 , +^#(x, 0()) -> c_4(x) 212.91/115.74 , +^#(x, s(y)) -> c_5(+^#(x, y)) 212.91/115.74 , double^#(s(x)) -> c_7(double^#(x)) } 212.91/115.74 Strict Trs: 212.91/115.74 { sqr(0()) -> 0() 212.91/115.74 , sqr(s(x)) -> s(+(sqr(x), double(x))) 212.91/115.74 , sqr(s(x)) -> +(sqr(x), s(double(x))) 212.91/115.74 , +(x, 0()) -> x 212.91/115.74 , +(x, s(y)) -> s(+(x, y)) 212.91/115.74 , double(0()) -> 0() 212.91/115.74 , double(s(x)) -> s(s(double(x))) } 212.91/115.74 Weak DPs: 212.91/115.74 { sqr^#(0()) -> c_1() 212.91/115.74 , double^#(0()) -> c_6() } 212.91/115.74 Obligation: 212.91/115.74 runtime complexity 212.91/115.74 Answer: 212.91/115.74 MAYBE 212.91/115.74 212.91/115.74 Empty strict component of the problem is NOT empty. 212.91/115.74 212.91/115.74 212.91/115.74 Arrrr.. 213.05/115.89 EOF