MAYBE 1019.63/298.63 MAYBE 1019.63/298.63 1019.63/298.63 We are left with following problem, upon which TcT provides the 1019.63/298.63 certificate MAYBE. 1019.63/298.63 1019.63/298.63 Strict Trs: 1019.63/298.63 { h(e(x), y) -> h(d(x, y), s(y)) 1019.63/298.63 , d(g(x, y), z) -> g(d(x, z), e(y)) 1019.63/298.63 , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z)) 1019.63/298.63 , d(g(g(0(), x), y), 0()) -> e(y) 1019.63/298.63 , d(g(0(), x), y) -> e(x) 1019.63/298.63 , g(e(x), e(y)) -> e(g(x, y)) } 1019.63/298.63 Obligation: 1019.63/298.63 runtime complexity 1019.63/298.63 Answer: 1019.63/298.63 MAYBE 1019.63/298.63 1019.63/298.63 None of the processors succeeded. 1019.63/298.63 1019.63/298.63 Details of failed attempt(s): 1019.63/298.63 ----------------------------- 1019.63/298.63 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1019.63/298.63 following reason: 1019.63/298.63 1019.63/298.63 Computation stopped due to timeout after 297.0 seconds. 1019.63/298.63 1019.63/298.63 2) 'Best' failed due to the following reason: 1019.63/298.63 1019.63/298.63 None of the processors succeeded. 1019.63/298.63 1019.63/298.63 Details of failed attempt(s): 1019.63/298.63 ----------------------------- 1019.63/298.63 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1019.63/298.63 seconds)' failed due to the following reason: 1019.63/298.63 1019.63/298.63 Computation stopped due to timeout after 148.0 seconds. 1019.63/298.63 1019.63/298.63 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1019.63/298.63 failed due to the following reason: 1019.63/298.63 1019.63/298.63 None of the processors succeeded. 1019.63/298.63 1019.63/298.63 Details of failed attempt(s): 1019.63/298.63 ----------------------------- 1019.63/298.63 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1019.63/298.63 failed due to the following reason: 1019.63/298.63 1019.63/298.63 match-boundness of the problem could not be verified. 1019.63/298.63 1019.63/298.63 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1019.63/298.63 failed due to the following reason: 1019.63/298.63 1019.63/298.63 match-boundness of the problem could not be verified. 1019.63/298.63 1019.63/298.63 1019.63/298.63 3) 'Best' failed due to the following reason: 1019.63/298.63 1019.63/298.63 None of the processors succeeded. 1019.63/298.63 1019.63/298.63 Details of failed attempt(s): 1019.63/298.63 ----------------------------- 1019.63/298.63 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1019.63/298.63 following reason: 1019.63/298.63 1019.63/298.63 The processor is inapplicable, reason: 1019.63/298.63 Processor only applicable for innermost runtime complexity analysis 1019.63/298.63 1019.63/298.63 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1019.63/298.63 to the following reason: 1019.63/298.63 1019.63/298.63 The processor is inapplicable, reason: 1019.63/298.63 Processor only applicable for innermost runtime complexity analysis 1019.63/298.63 1019.63/298.63 1019.63/298.63 1019.63/298.63 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1019.63/298.63 the following reason: 1019.63/298.63 1019.63/298.63 We add the following weak dependency pairs: 1019.63/298.63 1019.63/298.63 Strict DPs: 1019.63/298.63 { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) 1019.63/298.63 , d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) 1019.63/298.63 , d^#(g(g(0(), x), y), s(z)) -> 1019.63/298.63 c_3(g^#(e(x), d(g(g(0(), x), y), z))) 1019.63/298.63 , d^#(g(g(0(), x), y), 0()) -> c_4(y) 1019.63/298.63 , d^#(g(0(), x), y) -> c_5(x) 1019.63/298.63 , g^#(e(x), e(y)) -> c_6(g^#(x, y)) } 1019.63/298.63 1019.63/298.63 and mark the set of starting terms. 1019.63/298.63 1019.63/298.63 We are left with following problem, upon which TcT provides the 1019.63/298.63 certificate MAYBE. 1019.63/298.63 1019.63/298.63 Strict DPs: 1019.63/298.63 { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) 1019.63/298.63 , d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) 1019.63/298.63 , d^#(g(g(0(), x), y), s(z)) -> 1019.63/298.63 c_3(g^#(e(x), d(g(g(0(), x), y), z))) 1019.63/298.63 , d^#(g(g(0(), x), y), 0()) -> c_4(y) 1019.63/298.63 , d^#(g(0(), x), y) -> c_5(x) 1019.63/298.63 , g^#(e(x), e(y)) -> c_6(g^#(x, y)) } 1019.63/298.63 Strict Trs: 1019.63/298.63 { h(e(x), y) -> h(d(x, y), s(y)) 1019.63/298.63 , d(g(x, y), z) -> g(d(x, z), e(y)) 1019.63/298.63 , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z)) 1019.63/298.63 , d(g(g(0(), x), y), 0()) -> e(y) 1019.63/298.63 , d(g(0(), x), y) -> e(x) 1019.63/298.63 , g(e(x), e(y)) -> e(g(x, y)) } 1019.63/298.63 Obligation: 1019.63/298.63 runtime complexity 1019.63/298.63 Answer: 1019.63/298.63 MAYBE 1019.63/298.63 1019.63/298.63 Consider the dependency graph: 1019.63/298.63 1019.63/298.63 1: h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) 1019.63/298.63 -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1 1019.63/298.63 1019.63/298.63 2: d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) 1019.63/298.63 -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6 1019.63/298.63 1019.63/298.63 3: d^#(g(g(0(), x), y), s(z)) -> 1019.63/298.63 c_3(g^#(e(x), d(g(g(0(), x), y), z))) 1019.63/298.63 -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6 1019.63/298.63 1019.63/298.63 4: d^#(g(g(0(), x), y), 0()) -> c_4(y) 1019.63/298.63 -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6 1019.63/298.63 -->_1 d^#(g(0(), x), y) -> c_5(x) :5 1019.63/298.63 -->_1 d^#(g(g(0(), x), y), 0()) -> c_4(y) :4 1019.63/298.63 -->_1 d^#(g(g(0(), x), y), s(z)) -> 1019.63/298.63 c_3(g^#(e(x), d(g(g(0(), x), y), z))) :3 1019.63/298.63 -->_1 d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) :2 1019.63/298.63 -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1 1019.63/298.63 1019.63/298.63 5: d^#(g(0(), x), y) -> c_5(x) 1019.63/298.63 -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6 1019.63/298.63 -->_1 d^#(g(0(), x), y) -> c_5(x) :5 1019.63/298.63 -->_1 d^#(g(g(0(), x), y), 0()) -> c_4(y) :4 1019.63/298.63 -->_1 d^#(g(g(0(), x), y), s(z)) -> 1019.63/298.63 c_3(g^#(e(x), d(g(g(0(), x), y), z))) :3 1019.63/298.63 -->_1 d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) :2 1019.63/298.63 -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1 1019.63/298.63 1019.63/298.63 6: g^#(e(x), e(y)) -> c_6(g^#(x, y)) 1019.63/298.63 -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6 1019.63/298.63 1019.63/298.63 1019.63/298.63 Only the nodes {1,6} are reachable from nodes {1,6} that start 1019.63/298.63 derivation from marked basic terms. The nodes not reachable are 1019.63/298.63 removed from the problem. 1019.63/298.63 1019.63/298.63 We are left with following problem, upon which TcT provides the 1019.63/298.63 certificate MAYBE. 1019.63/298.63 1019.63/298.63 Strict DPs: 1019.63/298.63 { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) 1019.63/298.63 , g^#(e(x), e(y)) -> c_6(g^#(x, y)) } 1019.63/298.63 Strict Trs: 1019.63/298.63 { h(e(x), y) -> h(d(x, y), s(y)) 1019.63/298.63 , d(g(x, y), z) -> g(d(x, z), e(y)) 1019.63/298.63 , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z)) 1019.63/298.63 , d(g(g(0(), x), y), 0()) -> e(y) 1019.63/298.63 , d(g(0(), x), y) -> e(x) 1019.63/298.63 , g(e(x), e(y)) -> e(g(x, y)) } 1019.63/298.63 Obligation: 1019.63/298.63 runtime complexity 1019.63/298.63 Answer: 1019.63/298.63 MAYBE 1019.63/298.63 1019.63/298.63 Empty strict component of the problem is NOT empty. 1019.63/298.63 1019.63/298.63 1019.63/298.63 Arrrr.. 1020.14/299.02 EOF