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