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