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