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