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