MAYBE 701.14/297.03 MAYBE 701.14/297.03 701.14/297.03 We are left with following problem, upon which TcT provides the 701.14/297.03 certificate MAYBE. 701.14/297.03 701.14/297.03 Strict Trs: 701.14/297.03 { f(X, X) -> f(a(), n__b()) 701.14/297.03 , b() -> a() 701.14/297.03 , b() -> n__b() 701.14/297.03 , activate(X) -> X 701.14/297.03 , activate(n__b()) -> b() } 701.14/297.03 Obligation: 701.14/297.03 derivational complexity 701.14/297.03 Answer: 701.14/297.03 MAYBE 701.14/297.03 701.14/297.03 None of the processors succeeded. 701.14/297.03 701.14/297.03 Details of failed attempt(s): 701.14/297.03 ----------------------------- 701.14/297.03 1) 'iteProgress (timeout of 297 seconds)' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 Computation stopped due to timeout after 297.0 seconds. 701.14/297.03 701.14/297.03 2) 'Fastest (timeout of 60 seconds)' failed due to the following 701.14/297.03 reason: 701.14/297.03 701.14/297.03 Computation stopped due to timeout after 60.0 seconds. 701.14/297.03 701.14/297.03 3) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 701.14/297.03 the following reason: 701.14/297.03 701.14/297.03 We use the processor 'matrix interpretation of dimension 1' to 701.14/297.03 orient following rules strictly. 701.14/297.03 701.14/297.03 Trs: 701.14/297.03 { b() -> a() 701.14/297.03 , b() -> n__b() 701.14/297.03 , activate(X) -> X 701.14/297.03 , activate(n__b()) -> b() } 701.14/297.03 701.14/297.03 The induced complexity on above rules (modulo remaining rules) is 701.14/297.03 YES(?,O(n^1)) . These rules are moved into the corresponding weak 701.14/297.03 component(s). 701.14/297.03 701.14/297.03 Sub-proof: 701.14/297.03 ---------- 701.14/297.03 TcT has computed the following triangular matrix interpretation. 701.14/297.03 701.14/297.03 [f](x1, x2) = [1] x1 + [1] x2 + [1] 701.14/297.03 701.14/297.03 [a] = [0] 701.14/297.03 701.14/297.03 [n__b] = [0] 701.14/297.03 701.14/297.03 [b] = [1] 701.14/297.03 701.14/297.03 [activate](x1) = [1] x1 + [2] 701.14/297.03 701.14/297.03 The order satisfies the following ordering constraints: 701.14/297.03 701.14/297.03 [f(X, X)] = [2] X + [1] 701.14/297.03 >= [1] 701.14/297.03 = [f(a(), n__b())] 701.14/297.03 701.14/297.03 [b()] = [1] 701.14/297.03 > [0] 701.14/297.03 = [a()] 701.14/297.03 701.14/297.03 [b()] = [1] 701.14/297.03 > [0] 701.14/297.03 = [n__b()] 701.14/297.03 701.14/297.03 [activate(X)] = [1] X + [2] 701.14/297.03 > [1] X + [0] 701.14/297.03 = [X] 701.14/297.03 701.14/297.03 [activate(n__b())] = [2] 701.14/297.03 > [1] 701.14/297.03 = [b()] 701.14/297.03 701.14/297.03 701.14/297.03 We return to the main proof. 701.14/297.03 701.14/297.03 We are left with following problem, upon which TcT provides the 701.14/297.03 certificate MAYBE. 701.14/297.03 701.14/297.03 Strict Trs: { f(X, X) -> f(a(), n__b()) } 701.14/297.03 Weak Trs: 701.14/297.03 { b() -> a() 701.14/297.03 , b() -> n__b() 701.14/297.03 , activate(X) -> X 701.14/297.03 , activate(n__b()) -> b() } 701.14/297.03 Obligation: 701.14/297.03 derivational complexity 701.14/297.03 Answer: 701.14/297.03 MAYBE 701.14/297.03 701.14/297.03 None of the processors succeeded. 701.14/297.03 701.14/297.03 Details of failed attempt(s): 701.14/297.03 ----------------------------- 701.14/297.03 1) 'empty' failed due to the following reason: 701.14/297.03 701.14/297.03 Empty strict component of the problem is NOT empty. 701.14/297.03 701.14/297.03 2) 'Fastest' failed due to the following reason: 701.14/297.03 701.14/297.03 None of the processors succeeded. 701.14/297.03 701.14/297.03 Details of failed attempt(s): 701.14/297.03 ----------------------------- 701.14/297.03 1) 'Fastest (timeout of 30 seconds)' failed due to the following 701.14/297.03 reason: 701.14/297.03 701.14/297.03 Computation stopped due to timeout after 30.0 seconds. 701.14/297.03 701.14/297.03 2) 'iteProgress' failed due to the following reason: 701.14/297.03 701.14/297.03 Fail 701.14/297.03 701.14/297.03 3) 'Fastest' failed due to the following reason: 701.14/297.03 701.14/297.03 None of the processors succeeded. 701.14/297.03 701.14/297.03 Details of failed attempt(s): 701.14/297.03 ----------------------------- 701.14/297.03 1) 'matrix interpretation of dimension 6' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 2) 'matrix interpretation of dimension 5' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 3) 'matrix interpretation of dimension 4' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 4) 'matrix interpretation of dimension 3' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 5) 'matrix interpretation of dimension 2' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 6) 'matrix interpretation of dimension 1' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 701.14/297.03 4) 'bsearch-matrix' failed due to the following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 701.14/297.03 701.14/297.03 4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 701.14/297.03 following reason: 701.14/297.03 701.14/297.03 The input cannot be shown compatible 701.14/297.03 701.14/297.03 701.14/297.03 Arrrr.. 701.27/297.12 EOF