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