MAYBE 586.39/297.13 MAYBE 586.39/297.13 586.39/297.13 We are left with following problem, upon which TcT provides the 586.39/297.13 certificate MAYBE. 586.39/297.13 586.39/297.13 Strict Trs: 586.39/297.13 { active(f(X, X)) -> mark(f(a(), b())) 586.39/297.13 , active(f(X1, X2)) -> f(active(X1), X2) 586.39/297.13 , active(b()) -> mark(a()) 586.39/297.13 , f(mark(X1), X2) -> mark(f(X1, X2)) 586.39/297.13 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 586.39/297.13 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 586.39/297.13 , proper(a()) -> ok(a()) 586.39/297.13 , proper(b()) -> ok(b()) 586.39/297.13 , top(mark(X)) -> top(proper(X)) 586.39/297.13 , top(ok(X)) -> top(active(X)) } 586.39/297.13 Obligation: 586.39/297.13 runtime complexity 586.39/297.13 Answer: 586.39/297.13 MAYBE 586.39/297.13 586.39/297.13 None of the processors succeeded. 586.39/297.13 586.39/297.13 Details of failed attempt(s): 586.39/297.13 ----------------------------- 586.39/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 586.39/297.13 following reason: 586.39/297.13 586.39/297.13 Computation stopped due to timeout after 297.0 seconds. 586.39/297.13 586.39/297.13 2) 'Best' failed due to the following reason: 586.39/297.13 586.39/297.13 None of the processors succeeded. 586.39/297.13 586.39/297.13 Details of failed attempt(s): 586.39/297.13 ----------------------------- 586.39/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 586.39/297.13 seconds)' failed due to the following reason: 586.39/297.13 586.39/297.13 Computation stopped due to timeout after 148.0 seconds. 586.39/297.13 586.39/297.13 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 586.39/297.13 failed due to the following reason: 586.39/297.13 586.39/297.13 Computation stopped due to timeout after 24.0 seconds. 586.39/297.13 586.39/297.13 3) 'Best' failed due to the following reason: 586.39/297.13 586.39/297.13 None of the processors succeeded. 586.39/297.13 586.39/297.13 Details of failed attempt(s): 586.39/297.13 ----------------------------- 586.39/297.13 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 586.39/297.13 following reason: 586.39/297.13 586.39/297.13 The processor is inapplicable, reason: 586.39/297.13 Processor only applicable for innermost runtime complexity analysis 586.39/297.13 586.39/297.13 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 586.39/297.13 to the following reason: 586.39/297.13 586.39/297.13 The processor is inapplicable, reason: 586.39/297.13 Processor only applicable for innermost runtime complexity analysis 586.39/297.13 586.39/297.13 586.39/297.13 586.39/297.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 586.39/297.13 the following reason: 586.39/297.13 586.39/297.13 We add the following weak dependency pairs: 586.39/297.13 586.39/297.13 Strict DPs: 586.39/297.13 { active^#(f(X, X)) -> c_1(f^#(a(), b())) 586.39/297.13 , active^#(f(X1, X2)) -> c_2(f^#(active(X1), X2)) 586.39/297.13 , active^#(b()) -> c_3() 586.39/297.13 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 , proper^#(f(X1, X2)) -> c_6(f^#(proper(X1), proper(X2))) 586.39/297.13 , proper^#(a()) -> c_7() 586.39/297.13 , proper^#(b()) -> c_8() 586.39/297.13 , top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 , top^#(ok(X)) -> c_10(top^#(active(X))) } 586.39/297.13 586.39/297.13 and mark the set of starting terms. 586.39/297.13 586.39/297.13 We are left with following problem, upon which TcT provides the 586.39/297.13 certificate MAYBE. 586.39/297.13 586.39/297.13 Strict DPs: 586.39/297.13 { active^#(f(X, X)) -> c_1(f^#(a(), b())) 586.39/297.13 , active^#(f(X1, X2)) -> c_2(f^#(active(X1), X2)) 586.39/297.13 , active^#(b()) -> c_3() 586.39/297.13 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 , proper^#(f(X1, X2)) -> c_6(f^#(proper(X1), proper(X2))) 586.39/297.13 , proper^#(a()) -> c_7() 586.39/297.13 , proper^#(b()) -> c_8() 586.39/297.13 , top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 , top^#(ok(X)) -> c_10(top^#(active(X))) } 586.39/297.13 Strict Trs: 586.39/297.13 { active(f(X, X)) -> mark(f(a(), b())) 586.39/297.13 , active(f(X1, X2)) -> f(active(X1), X2) 586.39/297.13 , active(b()) -> mark(a()) 586.39/297.13 , f(mark(X1), X2) -> mark(f(X1, X2)) 586.39/297.13 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 586.39/297.13 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 586.39/297.13 , proper(a()) -> ok(a()) 586.39/297.13 , proper(b()) -> ok(b()) 586.39/297.13 , top(mark(X)) -> top(proper(X)) 586.39/297.13 , top(ok(X)) -> top(active(X)) } 586.39/297.13 Obligation: 586.39/297.13 runtime complexity 586.39/297.13 Answer: 586.39/297.13 MAYBE 586.39/297.13 586.39/297.13 Consider the dependency graph: 586.39/297.13 586.39/297.13 1: active^#(f(X, X)) -> c_1(f^#(a(), b())) 586.39/297.13 586.39/297.13 2: active^#(f(X1, X2)) -> c_2(f^#(active(X1), X2)) 586.39/297.13 -->_1 f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) :5 586.39/297.13 -->_1 f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) :4 586.39/297.13 586.39/297.13 3: active^#(b()) -> c_3() 586.39/297.13 586.39/297.13 4: f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 -->_1 f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) :5 586.39/297.13 -->_1 f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) :4 586.39/297.13 586.39/297.13 5: f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 -->_1 f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) :5 586.39/297.13 -->_1 f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) :4 586.39/297.13 586.39/297.13 6: proper^#(f(X1, X2)) -> c_6(f^#(proper(X1), proper(X2))) 586.39/297.13 -->_1 f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) :5 586.39/297.13 -->_1 f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) :4 586.39/297.13 586.39/297.13 7: proper^#(a()) -> c_7() 586.39/297.13 586.39/297.13 8: proper^#(b()) -> c_8() 586.39/297.13 586.39/297.13 9: top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 -->_1 top^#(ok(X)) -> c_10(top^#(active(X))) :10 586.39/297.13 -->_1 top^#(mark(X)) -> c_9(top^#(proper(X))) :9 586.39/297.13 586.39/297.13 10: top^#(ok(X)) -> c_10(top^#(active(X))) 586.39/297.13 -->_1 top^#(ok(X)) -> c_10(top^#(active(X))) :10 586.39/297.13 -->_1 top^#(mark(X)) -> c_9(top^#(proper(X))) :9 586.39/297.13 586.39/297.13 586.39/297.13 Only the nodes {3,4,5,7,8,9,10} are reachable from nodes 586.39/297.13 {3,4,5,7,8,9,10} that start derivation from marked basic terms. The 586.39/297.13 nodes not reachable are removed from the problem. 586.39/297.13 586.39/297.13 We are left with following problem, upon which TcT provides the 586.39/297.13 certificate MAYBE. 586.39/297.13 586.39/297.13 Strict DPs: 586.39/297.13 { active^#(b()) -> c_3() 586.39/297.13 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 , proper^#(a()) -> c_7() 586.39/297.13 , proper^#(b()) -> c_8() 586.39/297.13 , top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 , top^#(ok(X)) -> c_10(top^#(active(X))) } 586.39/297.13 Strict Trs: 586.39/297.13 { active(f(X, X)) -> mark(f(a(), b())) 586.39/297.13 , active(f(X1, X2)) -> f(active(X1), X2) 586.39/297.13 , active(b()) -> mark(a()) 586.39/297.13 , f(mark(X1), X2) -> mark(f(X1, X2)) 586.39/297.13 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 586.39/297.13 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 586.39/297.13 , proper(a()) -> ok(a()) 586.39/297.13 , proper(b()) -> ok(b()) 586.39/297.13 , top(mark(X)) -> top(proper(X)) 586.39/297.13 , top(ok(X)) -> top(active(X)) } 586.39/297.13 Obligation: 586.39/297.13 runtime complexity 586.39/297.13 Answer: 586.39/297.13 MAYBE 586.39/297.13 586.39/297.13 We estimate the number of application of {1,4,5} by applications of 586.39/297.13 Pre({1,4,5}) = {}. Here rules are labeled as follows: 586.39/297.13 586.39/297.13 DPs: 586.39/297.13 { 1: active^#(b()) -> c_3() 586.39/297.13 , 2: f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 , 3: f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 , 4: proper^#(a()) -> c_7() 586.39/297.13 , 5: proper^#(b()) -> c_8() 586.39/297.13 , 6: top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 , 7: top^#(ok(X)) -> c_10(top^#(active(X))) } 586.39/297.13 586.39/297.13 We are left with following problem, upon which TcT provides the 586.39/297.13 certificate MAYBE. 586.39/297.13 586.39/297.13 Strict DPs: 586.39/297.13 { f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 586.39/297.13 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 586.39/297.13 , top^#(mark(X)) -> c_9(top^#(proper(X))) 586.39/297.13 , top^#(ok(X)) -> c_10(top^#(active(X))) } 586.39/297.13 Strict Trs: 586.39/297.13 { active(f(X, X)) -> mark(f(a(), b())) 586.39/297.13 , active(f(X1, X2)) -> f(active(X1), X2) 586.39/297.13 , active(b()) -> mark(a()) 586.39/297.13 , f(mark(X1), X2) -> mark(f(X1, X2)) 586.39/297.13 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 586.39/297.13 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 586.39/297.13 , proper(a()) -> ok(a()) 586.39/297.13 , proper(b()) -> ok(b()) 586.39/297.13 , top(mark(X)) -> top(proper(X)) 586.39/297.13 , top(ok(X)) -> top(active(X)) } 586.39/297.13 Weak DPs: 586.39/297.13 { active^#(b()) -> c_3() 586.39/297.13 , proper^#(a()) -> c_7() 586.39/297.13 , proper^#(b()) -> c_8() } 586.39/297.13 Obligation: 586.39/297.13 runtime complexity 586.39/297.13 Answer: 586.39/297.13 MAYBE 586.39/297.13 586.39/297.13 Empty strict component of the problem is NOT empty. 586.39/297.13 586.39/297.13 586.39/297.13 Arrrr.. 586.39/297.14 EOF