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