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