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