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