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