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