MAYBE 967.42/297.05 MAYBE 967.42/297.05 967.42/297.05 We are left with following problem, upon which TcT provides the 967.42/297.05 certificate MAYBE. 967.42/297.05 967.42/297.05 Strict Trs: 967.42/297.05 { f(s(x), x) -> f(s(x), round(s(x))) 967.42/297.05 , round(s(s(x))) -> s(s(round(x))) 967.42/297.05 , round(s(0())) -> s(0()) 967.42/297.05 , round(0()) -> s(0()) 967.42/297.05 , round(0()) -> 0() } 967.42/297.05 Obligation: 967.42/297.05 runtime complexity 967.42/297.05 Answer: 967.42/297.05 MAYBE 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 967.42/297.05 following reason: 967.42/297.05 967.42/297.05 Computation stopped due to timeout after 297.0 seconds. 967.42/297.05 967.42/297.05 2) 'Best' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 967.42/297.05 seconds)' failed due to the following reason: 967.42/297.05 967.42/297.05 The weightgap principle applies (using the following nonconstant 967.42/297.05 growth matrix-interpretation) 967.42/297.05 967.42/297.05 The following argument positions are usable: 967.42/297.05 Uargs(f) = {2}, Uargs(s) = {1} 967.42/297.05 967.42/297.05 TcT has computed the following matrix interpretation satisfying 967.42/297.05 not(EDA) and not(IDA(1)). 967.42/297.05 967.42/297.05 [f](x1, x2) = [1] x1 + [1] x2 + [0] 967.42/297.05 967.42/297.05 [s](x1) = [1] x1 + [0] 967.42/297.05 967.42/297.05 [round](x1) = [1] 967.42/297.05 967.42/297.05 [0] = [0] 967.42/297.05 967.42/297.05 The order satisfies the following ordering constraints: 967.42/297.05 967.42/297.05 [f(s(x), x)] = [2] x + [0] 967.42/297.05 ? [1] x + [1] 967.42/297.05 = [f(s(x), round(s(x)))] 967.42/297.05 967.42/297.05 [round(s(s(x)))] = [1] 967.42/297.05 >= [1] 967.42/297.05 = [s(s(round(x)))] 967.42/297.05 967.42/297.05 [round(s(0()))] = [1] 967.42/297.05 > [0] 967.42/297.05 = [s(0())] 967.42/297.05 967.42/297.05 [round(0())] = [1] 967.42/297.05 > [0] 967.42/297.05 = [s(0())] 967.42/297.05 967.42/297.05 [round(0())] = [1] 967.42/297.05 > [0] 967.42/297.05 = [0()] 967.42/297.05 967.42/297.05 967.42/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 967.42/297.05 967.42/297.05 We are left with following problem, upon which TcT provides the 967.42/297.05 certificate MAYBE. 967.42/297.05 967.42/297.05 Strict Trs: 967.42/297.05 { f(s(x), x) -> f(s(x), round(s(x))) 967.42/297.05 , round(s(s(x))) -> s(s(round(x))) } 967.42/297.05 Weak Trs: 967.42/297.05 { round(s(0())) -> s(0()) 967.42/297.05 , round(0()) -> s(0()) 967.42/297.05 , round(0()) -> 0() } 967.42/297.05 Obligation: 967.42/297.05 runtime complexity 967.42/297.05 Answer: 967.42/297.05 MAYBE 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'Fastest' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'empty' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 2) 'With Problem ...' failed due to the following reason: 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 967.42/297.05 failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 967.42/297.05 failed due to the following reason: 967.42/297.05 967.42/297.05 match-boundness of the problem could not be verified. 967.42/297.05 967.42/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 967.42/297.05 failed due to the following reason: 967.42/297.05 967.42/297.05 match-boundness of the problem could not be verified. 967.42/297.05 967.42/297.05 967.42/297.05 3) 'Best' failed due to the following reason: 967.42/297.05 967.42/297.05 None of the processors succeeded. 967.42/297.05 967.42/297.05 Details of failed attempt(s): 967.42/297.05 ----------------------------- 967.42/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 967.42/297.05 following reason: 967.42/297.05 967.42/297.05 The processor is inapplicable, reason: 967.42/297.05 Processor only applicable for innermost runtime complexity analysis 967.42/297.05 967.42/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 967.42/297.05 to the following reason: 967.42/297.05 967.42/297.05 The processor is inapplicable, reason: 967.42/297.05 Processor only applicable for innermost runtime complexity analysis 967.42/297.05 967.42/297.05 967.42/297.05 967.42/297.05 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 967.42/297.05 the following reason: 967.42/297.05 967.42/297.05 We add the following weak dependency pairs: 967.42/297.05 967.42/297.05 Strict DPs: 967.42/297.05 { f^#(s(x), x) -> c_1(f^#(s(x), round(s(x)))) 967.42/297.05 , round^#(s(s(x))) -> c_2(round^#(x)) 967.42/297.05 , round^#(s(0())) -> c_3() 967.42/297.05 , round^#(0()) -> c_4() 967.42/297.05 , round^#(0()) -> c_5() } 967.42/297.05 967.42/297.05 and mark the set of starting terms. 967.42/297.05 967.42/297.05 We are left with following problem, upon which TcT provides the 967.42/297.05 certificate MAYBE. 967.42/297.05 967.42/297.05 Strict DPs: 967.42/297.05 { f^#(s(x), x) -> c_1(f^#(s(x), round(s(x)))) 967.42/297.05 , round^#(s(s(x))) -> c_2(round^#(x)) 967.42/297.05 , round^#(s(0())) -> c_3() 967.42/297.05 , round^#(0()) -> c_4() 967.42/297.05 , round^#(0()) -> c_5() } 967.42/297.05 Strict Trs: 967.42/297.05 { f(s(x), x) -> f(s(x), round(s(x))) 967.42/297.05 , round(s(s(x))) -> s(s(round(x))) 967.42/297.05 , round(s(0())) -> s(0()) 967.42/297.05 , round(0()) -> s(0()) 967.42/297.05 , round(0()) -> 0() } 967.42/297.05 Obligation: 967.42/297.05 runtime complexity 967.42/297.05 Answer: 967.42/297.05 MAYBE 967.42/297.05 967.42/297.05 We estimate the number of application of {3,4,5} by applications of 967.42/297.05 Pre({3,4,5}) = {2}. Here rules are labeled as follows: 967.42/297.05 967.42/297.05 DPs: 967.42/297.05 { 1: f^#(s(x), x) -> c_1(f^#(s(x), round(s(x)))) 967.42/297.05 , 2: round^#(s(s(x))) -> c_2(round^#(x)) 967.42/297.05 , 3: round^#(s(0())) -> c_3() 967.42/297.05 , 4: round^#(0()) -> c_4() 967.42/297.05 , 5: round^#(0()) -> c_5() } 967.42/297.05 967.42/297.05 We are left with following problem, upon which TcT provides the 967.42/297.05 certificate MAYBE. 967.42/297.05 967.42/297.05 Strict DPs: 967.42/297.05 { f^#(s(x), x) -> c_1(f^#(s(x), round(s(x)))) 967.42/297.05 , round^#(s(s(x))) -> c_2(round^#(x)) } 967.42/297.05 Strict Trs: 967.42/297.05 { f(s(x), x) -> f(s(x), round(s(x))) 967.42/297.05 , round(s(s(x))) -> s(s(round(x))) 967.42/297.05 , round(s(0())) -> s(0()) 967.42/297.05 , round(0()) -> s(0()) 967.42/297.05 , round(0()) -> 0() } 967.42/297.05 Weak DPs: 967.42/297.05 { round^#(s(0())) -> c_3() 967.42/297.05 , round^#(0()) -> c_4() 967.42/297.05 , round^#(0()) -> c_5() } 967.42/297.05 Obligation: 967.42/297.05 runtime complexity 967.42/297.05 Answer: 967.42/297.05 MAYBE 967.42/297.05 967.42/297.05 Empty strict component of the problem is NOT empty. 967.42/297.05 967.42/297.05 967.42/297.05 Arrrr.. 968.33/297.88 EOF