MAYBE 1167.53/299.98 MAYBE 1167.53/299.98 1167.53/299.98 We are left with following problem, upon which TcT provides the 1167.53/299.98 certificate MAYBE. 1167.53/299.98 1167.53/299.98 Strict Trs: 1167.53/299.98 { f(0()) -> 0() 1167.53/299.98 , f(s(0())) -> s(0()) 1167.53/299.98 , f(s(s(x))) -> p(h(g(x))) 1167.53/299.98 , f(s(s(x))) -> +(p(g(x)), q(g(x))) 1167.53/299.98 , p(pair(x, y)) -> x 1167.53/299.98 , h(x) -> pair(+(p(x), q(x)), p(x)) 1167.53/299.98 , g(0()) -> pair(s(0()), s(0())) 1167.53/299.98 , g(s(x)) -> h(g(x)) 1167.53/299.98 , g(s(x)) -> pair(+(p(g(x)), q(g(x))), p(g(x))) 1167.53/299.98 , +(x, 0()) -> x 1167.53/299.98 , +(x, s(y)) -> s(+(x, y)) 1167.53/299.98 , q(pair(x, y)) -> y } 1167.53/299.98 Obligation: 1167.53/299.98 runtime complexity 1167.53/299.98 Answer: 1167.53/299.98 MAYBE 1167.53/299.98 1167.53/299.98 None of the processors succeeded. 1167.53/299.98 1167.53/299.98 Details of failed attempt(s): 1167.53/299.98 ----------------------------- 1167.53/299.98 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1167.53/299.98 following reason: 1167.53/299.98 1167.53/299.98 Computation stopped due to timeout after 297.0 seconds. 1167.53/299.98 1167.53/299.98 2) 'Best' failed due to the following reason: 1167.53/299.98 1167.53/299.98 None of the processors succeeded. 1167.53/299.98 1167.53/299.98 Details of failed attempt(s): 1167.53/299.98 ----------------------------- 1167.53/299.98 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1167.53/299.98 seconds)' failed due to the following reason: 1167.53/299.98 1167.53/299.98 Computation stopped due to timeout after 148.0 seconds. 1167.53/299.98 1167.53/299.98 2) 'Best' failed due to the following reason: 1167.53/299.98 1167.53/299.98 None of the processors succeeded. 1167.53/299.98 1167.53/299.98 Details of failed attempt(s): 1167.53/299.98 ----------------------------- 1167.53/299.98 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1167.53/299.98 to the following reason: 1167.53/299.98 1167.53/299.98 The processor is inapplicable, reason: 1167.53/299.98 Processor only applicable for innermost runtime complexity analysis 1167.53/299.98 1167.53/299.98 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1167.53/299.98 following reason: 1167.53/299.98 1167.53/299.98 The processor is inapplicable, reason: 1167.53/299.98 Processor only applicable for innermost runtime complexity analysis 1167.53/299.98 1167.53/299.98 1167.53/299.98 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1167.53/299.98 failed due to the following reason: 1167.53/299.98 1167.53/299.98 None of the processors succeeded. 1167.53/299.98 1167.53/299.98 Details of failed attempt(s): 1167.53/299.98 ----------------------------- 1167.53/299.98 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1167.53/299.98 failed due to the following reason: 1167.53/299.98 1167.53/299.98 match-boundness of the problem could not be verified. 1167.53/299.98 1167.53/299.98 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1167.53/299.98 failed due to the following reason: 1167.53/299.98 1167.53/299.98 match-boundness of the problem could not be verified. 1167.53/299.98 1167.53/299.98 1167.53/299.98 1167.53/299.98 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1167.53/299.98 the following reason: 1167.53/299.98 1167.53/299.98 We add the following weak dependency pairs: 1167.53/299.98 1167.53/299.98 Strict DPs: 1167.53/299.98 { f^#(0()) -> c_1() 1167.53/299.98 , f^#(s(0())) -> c_2() 1167.53/299.98 , f^#(s(s(x))) -> c_3(p^#(h(g(x)))) 1167.53/299.98 , f^#(s(s(x))) -> c_4(+^#(p(g(x)), q(g(x)))) 1167.53/299.98 , p^#(pair(x, y)) -> c_5(x) 1167.53/299.98 , +^#(x, 0()) -> c_10(x) 1167.53/299.98 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1167.53/299.98 , h^#(x) -> c_6(+^#(p(x), q(x)), p^#(x)) 1167.53/299.98 , g^#(0()) -> c_7() 1167.53/299.98 , g^#(s(x)) -> c_8(h^#(g(x))) 1167.53/299.98 , g^#(s(x)) -> c_9(+^#(p(g(x)), q(g(x))), p^#(g(x))) 1167.53/299.98 , q^#(pair(x, y)) -> c_12(y) } 1167.53/299.98 1167.53/299.98 and mark the set of starting terms. 1167.53/299.98 1167.53/299.98 We are left with following problem, upon which TcT provides the 1167.53/299.98 certificate MAYBE. 1167.53/299.98 1167.53/299.98 Strict DPs: 1167.53/299.98 { f^#(0()) -> c_1() 1167.53/299.98 , f^#(s(0())) -> c_2() 1167.53/299.98 , f^#(s(s(x))) -> c_3(p^#(h(g(x)))) 1167.53/299.98 , f^#(s(s(x))) -> c_4(+^#(p(g(x)), q(g(x)))) 1167.53/299.98 , p^#(pair(x, y)) -> c_5(x) 1167.53/299.98 , +^#(x, 0()) -> c_10(x) 1167.53/299.98 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1167.53/299.98 , h^#(x) -> c_6(+^#(p(x), q(x)), p^#(x)) 1167.53/299.98 , g^#(0()) -> c_7() 1167.53/299.98 , g^#(s(x)) -> c_8(h^#(g(x))) 1167.53/299.98 , g^#(s(x)) -> c_9(+^#(p(g(x)), q(g(x))), p^#(g(x))) 1167.53/299.98 , q^#(pair(x, y)) -> c_12(y) } 1167.53/299.98 Strict Trs: 1167.53/299.98 { f(0()) -> 0() 1167.53/299.98 , f(s(0())) -> s(0()) 1167.53/299.98 , f(s(s(x))) -> p(h(g(x))) 1167.53/299.98 , f(s(s(x))) -> +(p(g(x)), q(g(x))) 1167.53/299.98 , p(pair(x, y)) -> x 1167.53/299.98 , h(x) -> pair(+(p(x), q(x)), p(x)) 1167.53/299.98 , g(0()) -> pair(s(0()), s(0())) 1167.53/299.98 , g(s(x)) -> h(g(x)) 1167.53/299.98 , g(s(x)) -> pair(+(p(g(x)), q(g(x))), p(g(x))) 1167.53/299.98 , +(x, 0()) -> x 1167.53/299.98 , +(x, s(y)) -> s(+(x, y)) 1167.53/299.98 , q(pair(x, y)) -> y } 1167.53/299.98 Obligation: 1167.53/299.98 runtime complexity 1167.53/299.98 Answer: 1167.53/299.98 MAYBE 1167.53/299.98 1167.53/299.98 We estimate the number of application of {1,2,9} by applications of 1167.53/299.99 Pre({1,2,9}) = {5,6,12}. Here rules are labeled as follows: 1167.53/299.99 1167.53/299.99 DPs: 1167.53/299.99 { 1: f^#(0()) -> c_1() 1167.53/299.99 , 2: f^#(s(0())) -> c_2() 1167.53/299.99 , 3: f^#(s(s(x))) -> c_3(p^#(h(g(x)))) 1167.53/299.99 , 4: f^#(s(s(x))) -> c_4(+^#(p(g(x)), q(g(x)))) 1167.53/299.99 , 5: p^#(pair(x, y)) -> c_5(x) 1167.53/299.99 , 6: +^#(x, 0()) -> c_10(x) 1167.53/299.99 , 7: +^#(x, s(y)) -> c_11(+^#(x, y)) 1167.53/299.99 , 8: h^#(x) -> c_6(+^#(p(x), q(x)), p^#(x)) 1167.53/299.99 , 9: g^#(0()) -> c_7() 1167.53/299.99 , 10: g^#(s(x)) -> c_8(h^#(g(x))) 1167.53/299.99 , 11: g^#(s(x)) -> c_9(+^#(p(g(x)), q(g(x))), p^#(g(x))) 1167.53/299.99 , 12: q^#(pair(x, y)) -> c_12(y) } 1167.53/299.99 1167.53/299.99 We are left with following problem, upon which TcT provides the 1167.53/299.99 certificate MAYBE. 1167.53/299.99 1167.53/299.99 Strict DPs: 1167.53/299.99 { f^#(s(s(x))) -> c_3(p^#(h(g(x)))) 1167.53/299.99 , f^#(s(s(x))) -> c_4(+^#(p(g(x)), q(g(x)))) 1167.53/299.99 , p^#(pair(x, y)) -> c_5(x) 1167.53/299.99 , +^#(x, 0()) -> c_10(x) 1167.53/299.99 , +^#(x, s(y)) -> c_11(+^#(x, y)) 1167.53/299.99 , h^#(x) -> c_6(+^#(p(x), q(x)), p^#(x)) 1167.53/299.99 , g^#(s(x)) -> c_8(h^#(g(x))) 1167.53/299.99 , g^#(s(x)) -> c_9(+^#(p(g(x)), q(g(x))), p^#(g(x))) 1167.53/299.99 , q^#(pair(x, y)) -> c_12(y) } 1167.53/299.99 Strict Trs: 1167.53/299.99 { f(0()) -> 0() 1167.53/299.99 , f(s(0())) -> s(0()) 1167.53/299.99 , f(s(s(x))) -> p(h(g(x))) 1167.53/299.99 , f(s(s(x))) -> +(p(g(x)), q(g(x))) 1167.53/299.99 , p(pair(x, y)) -> x 1167.53/299.99 , h(x) -> pair(+(p(x), q(x)), p(x)) 1167.53/299.99 , g(0()) -> pair(s(0()), s(0())) 1167.53/299.99 , g(s(x)) -> h(g(x)) 1167.53/299.99 , g(s(x)) -> pair(+(p(g(x)), q(g(x))), p(g(x))) 1167.53/299.99 , +(x, 0()) -> x 1167.53/299.99 , +(x, s(y)) -> s(+(x, y)) 1167.53/299.99 , q(pair(x, y)) -> y } 1167.53/299.99 Weak DPs: 1167.53/299.99 { f^#(0()) -> c_1() 1167.53/299.99 , f^#(s(0())) -> c_2() 1167.53/299.99 , g^#(0()) -> c_7() } 1167.53/299.99 Obligation: 1167.53/299.99 runtime complexity 1167.53/299.99 Answer: 1167.53/299.99 MAYBE 1167.53/299.99 1167.53/299.99 Empty strict component of the problem is NOT empty. 1167.53/299.99 1167.53/299.99 1167.53/299.99 Arrrr.. 1167.89/300.70 EOF