MAYBE 18.95/5.90 MAYBE 18.95/5.90 18.95/5.90 We are left with following problem, upon which TcT provides the 18.95/5.90 certificate MAYBE. 18.95/5.90 18.95/5.90 Strict Trs: 18.95/5.90 { f(s(x), x) -> f(s(x), round(x)) 18.95/5.90 , round(s(s(x))) -> s(s(round(x))) 18.95/5.90 , round(s(0())) -> s(0()) 18.95/5.90 , round(0()) -> s(0()) 18.95/5.90 , round(0()) -> 0() } 18.95/5.90 Obligation: 18.95/5.90 derivational complexity 18.95/5.90 Answer: 18.95/5.90 MAYBE 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 18.95/5.90 the following reason: 18.95/5.90 18.95/5.90 The weightgap principle applies (using the following nonconstant 18.95/5.90 growth matrix-interpretation) 18.95/5.90 18.95/5.90 TcT has computed the following triangular matrix interpretation. 18.95/5.90 Note that the diagonal of the component-wise maxima of 18.95/5.90 interpretation-entries contains no more than 1 non-zero entries. 18.95/5.90 18.95/5.90 [f](x1, x2) = [1] x1 + [1] x2 + [0] 18.95/5.90 18.95/5.90 [s](x1) = [1] x1 + [0] 18.95/5.90 18.95/5.90 [round](x1) = [1] x1 + [1] 18.95/5.90 18.95/5.90 [0] = [0] 18.95/5.90 18.95/5.90 The order satisfies the following ordering constraints: 18.95/5.90 18.95/5.90 [f(s(x), x)] = [2] x + [0] 18.95/5.90 ? [2] x + [1] 18.95/5.90 = [f(s(x), round(x))] 18.95/5.90 18.95/5.90 [round(s(s(x)))] = [1] x + [1] 18.95/5.90 >= [1] x + [1] 18.95/5.90 = [s(s(round(x)))] 18.95/5.90 18.95/5.90 [round(s(0()))] = [1] 18.95/5.90 > [0] 18.95/5.90 = [s(0())] 18.95/5.90 18.95/5.90 [round(0())] = [1] 18.95/5.90 > [0] 18.95/5.90 = [s(0())] 18.95/5.90 18.95/5.90 [round(0())] = [1] 18.95/5.90 > [0] 18.95/5.90 = [0()] 18.95/5.90 18.95/5.90 18.95/5.90 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 18.95/5.90 18.95/5.90 We are left with following problem, upon which TcT provides the 18.95/5.90 certificate MAYBE. 18.95/5.90 18.95/5.90 Strict Trs: 18.95/5.90 { f(s(x), x) -> f(s(x), round(x)) 18.95/5.90 , round(s(s(x))) -> s(s(round(x))) } 18.95/5.90 Weak Trs: 18.95/5.90 { round(s(0())) -> s(0()) 18.95/5.90 , round(0()) -> s(0()) 18.95/5.90 , round(0()) -> 0() } 18.95/5.90 Obligation: 18.95/5.90 derivational complexity 18.95/5.90 Answer: 18.95/5.90 MAYBE 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'empty' failed due to the following reason: 18.95/5.90 18.95/5.90 Empty strict component of the problem is NOT empty. 18.95/5.90 18.95/5.90 2) 'Fastest' failed due to the following reason: 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'Fastest' failed due to the following reason: 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'matrix interpretation of dimension 6' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 2) 'matrix interpretation of dimension 5' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 3) 'matrix interpretation of dimension 4' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 4) 'matrix interpretation of dimension 3' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 5) 'matrix interpretation of dimension 2' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 6) 'matrix interpretation of dimension 1' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 18.95/5.90 2) 'iteProgress' failed due to the following reason: 18.95/5.90 18.95/5.90 Fail 18.95/5.90 18.95/5.90 3) 'bsearch-matrix' failed due to the following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 4) 'Fastest (timeout of 30 seconds)' failed due to the following 18.95/5.90 reason: 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 18.95/5.90 failed due to the following reason: 18.95/5.90 18.95/5.90 match-boundness of the problem could not be verified. 18.95/5.90 18.95/5.90 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 18.95/5.90 failed due to the following reason: 18.95/5.90 18.95/5.90 match-boundness of the problem could not be verified. 18.95/5.90 18.95/5.90 18.95/5.90 18.95/5.90 18.95/5.90 2) 'iteProgress (timeout of 297 seconds)' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 Fail 18.95/5.90 18.95/5.90 3) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 18.95/5.90 following reason: 18.95/5.90 18.95/5.90 The input cannot be shown compatible 18.95/5.90 18.95/5.90 4) 'Fastest (timeout of 60 seconds)' failed due to the following 18.95/5.90 reason: 18.95/5.90 18.95/5.90 None of the processors succeeded. 18.95/5.90 18.95/5.90 Details of failed attempt(s): 18.95/5.90 ----------------------------- 18.95/5.90 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 18.95/5.90 failed due to the following reason: 18.95/5.90 18.95/5.90 match-boundness of the problem could not be verified. 18.95/5.90 18.95/5.90 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 18.95/5.90 failed due to the following reason: 18.95/5.90 18.95/5.90 match-boundness of the problem could not be verified. 18.95/5.90 18.95/5.90 18.95/5.90 18.95/5.90 Arrrr.. 18.95/5.92 EOF