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