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