MAYBE 587.06/297.04 MAYBE 587.06/297.04 587.06/297.04 We are left with following problem, upon which TcT provides the 587.06/297.04 certificate MAYBE. 587.06/297.04 587.06/297.04 Strict Trs: 587.06/297.04 { plus(x, y) -> ifPlus(isZero(x), x, inc(y)) 587.06/297.04 , ifPlus(true(), x, y) -> p(y) 587.06/297.04 , ifPlus(false(), x, y) -> plus(p(x), y) 587.06/297.04 , isZero(0()) -> true() 587.06/297.04 , isZero(s(0())) -> false() 587.06/297.04 , isZero(s(s(x))) -> isZero(s(x)) 587.06/297.04 , inc(x) -> s(x) 587.06/297.04 , inc(0()) -> s(0()) 587.06/297.04 , inc(s(x)) -> s(inc(x)) 587.06/297.04 , p(0()) -> 0() 587.06/297.04 , p(s(x)) -> x 587.06/297.04 , p(s(s(x))) -> s(p(s(x))) 587.06/297.04 , times(x, y) -> timesIter(0(), x, y, 0()) 587.06/297.04 , timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z) 587.06/297.04 , ifTimes(true(), i, x, y, z) -> z 587.06/297.04 , ifTimes(false(), i, x, y, z) -> 587.06/297.04 timesIter(inc(i), x, y, plus(z, y)) 587.06/297.04 , ge(x, 0()) -> true() 587.06/297.04 , ge(0(), s(y)) -> false() 587.06/297.04 , ge(s(x), s(y)) -> ge(x, y) 587.06/297.04 , f0(x, y, z) -> d() 587.06/297.04 , f0(0(), y, x) -> f1(x, y, x) 587.06/297.04 , f1(x, y, z) -> f2(x, y, z) 587.06/297.04 , f1(x, y, z) -> c() 587.06/297.04 , f2(x, 1(), z) -> f0(x, z, z) } 587.06/297.04 Obligation: 587.06/297.04 runtime complexity 587.06/297.04 Answer: 587.06/297.04 MAYBE 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 587.06/297.04 following reason: 587.06/297.04 587.06/297.04 Computation stopped due to timeout after 297.0 seconds. 587.06/297.04 587.06/297.04 2) 'Best' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 587.06/297.04 seconds)' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'Fastest' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'empty' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 2) 'With Problem ...' failed due to the following reason: 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 2) 'Best' failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 587.06/297.04 to the following reason: 587.06/297.04 587.06/297.04 The processor is inapplicable, reason: 587.06/297.04 Processor only applicable for innermost runtime complexity analysis 587.06/297.04 587.06/297.04 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 587.06/297.04 following reason: 587.06/297.04 587.06/297.04 The processor is inapplicable, reason: 587.06/297.04 Processor only applicable for innermost runtime complexity analysis 587.06/297.04 587.06/297.04 587.06/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 587.06/297.04 failed due to the following reason: 587.06/297.04 587.06/297.04 None of the processors succeeded. 587.06/297.04 587.06/297.04 Details of failed attempt(s): 587.06/297.04 ----------------------------- 587.06/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 587.06/297.04 failed due to the following reason: 587.06/297.04 587.06/297.04 match-boundness of the problem could not be verified. 587.06/297.04 587.06/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 587.06/297.04 failed due to the following reason: 587.06/297.04 587.06/297.04 match-boundness of the problem could not be verified. 587.06/297.04 587.06/297.04 587.06/297.04 587.06/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 587.06/297.04 the following reason: 587.06/297.04 587.06/297.04 We add the following weak dependency pairs: 587.06/297.04 587.06/297.04 Strict DPs: 587.06/297.04 { plus^#(x, y) -> c_1(ifPlus^#(isZero(x), x, inc(y))) 587.06/297.04 , ifPlus^#(true(), x, y) -> c_2(p^#(y)) 587.06/297.04 , ifPlus^#(false(), x, y) -> c_3(plus^#(p(x), y)) 587.06/297.04 , p^#(0()) -> c_10() 587.06/297.04 , p^#(s(x)) -> c_11(x) 587.06/297.04 , p^#(s(s(x))) -> c_12(p^#(s(x))) 587.06/297.04 , isZero^#(0()) -> c_4() 587.06/297.04 , isZero^#(s(0())) -> c_5() 587.06/297.04 , isZero^#(s(s(x))) -> c_6(isZero^#(s(x))) 587.06/297.04 , inc^#(x) -> c_7(x) 587.06/297.04 , inc^#(0()) -> c_8() 587.06/297.04 , inc^#(s(x)) -> c_9(inc^#(x)) 587.06/297.04 , times^#(x, y) -> c_13(timesIter^#(0(), x, y, 0())) 587.06/297.04 , timesIter^#(i, x, y, z) -> c_14(ifTimes^#(ge(i, x), i, x, y, z)) 587.06/297.04 , ifTimes^#(true(), i, x, y, z) -> c_15(z) 587.06/297.04 , ifTimes^#(false(), i, x, y, z) -> 587.06/297.04 c_16(timesIter^#(inc(i), x, y, plus(z, y))) 587.06/297.04 , ge^#(x, 0()) -> c_17() 587.06/297.04 , ge^#(0(), s(y)) -> c_18() 587.06/297.04 , ge^#(s(x), s(y)) -> c_19(ge^#(x, y)) 587.06/297.04 , f0^#(x, y, z) -> c_20() 587.06/297.04 , f0^#(0(), y, x) -> c_21(f1^#(x, y, x)) 587.06/297.04 , f1^#(x, y, z) -> c_22(f2^#(x, y, z)) 587.06/297.04 , f1^#(x, y, z) -> c_23() 587.06/297.04 , f2^#(x, 1(), z) -> c_24(f0^#(x, z, z)) } 587.06/297.04 587.06/297.04 and mark the set of starting terms. 587.06/297.04 587.06/297.04 We are left with following problem, upon which TcT provides the 587.06/297.04 certificate MAYBE. 587.06/297.04 587.06/297.04 Strict DPs: 587.06/297.04 { plus^#(x, y) -> c_1(ifPlus^#(isZero(x), x, inc(y))) 587.06/297.04 , ifPlus^#(true(), x, y) -> c_2(p^#(y)) 587.06/297.04 , ifPlus^#(false(), x, y) -> c_3(plus^#(p(x), y)) 587.06/297.04 , p^#(0()) -> c_10() 587.06/297.04 , p^#(s(x)) -> c_11(x) 587.06/297.04 , p^#(s(s(x))) -> c_12(p^#(s(x))) 587.06/297.04 , isZero^#(0()) -> c_4() 587.06/297.04 , isZero^#(s(0())) -> c_5() 587.06/297.04 , isZero^#(s(s(x))) -> c_6(isZero^#(s(x))) 587.06/297.04 , inc^#(x) -> c_7(x) 587.06/297.04 , inc^#(0()) -> c_8() 587.06/297.04 , inc^#(s(x)) -> c_9(inc^#(x)) 587.06/297.04 , times^#(x, y) -> c_13(timesIter^#(0(), x, y, 0())) 587.06/297.04 , timesIter^#(i, x, y, z) -> c_14(ifTimes^#(ge(i, x), i, x, y, z)) 587.06/297.04 , ifTimes^#(true(), i, x, y, z) -> c_15(z) 587.06/297.04 , ifTimes^#(false(), i, x, y, z) -> 587.06/297.04 c_16(timesIter^#(inc(i), x, y, plus(z, y))) 587.06/297.04 , ge^#(x, 0()) -> c_17() 587.06/297.04 , ge^#(0(), s(y)) -> c_18() 587.06/297.04 , ge^#(s(x), s(y)) -> c_19(ge^#(x, y)) 587.06/297.04 , f0^#(x, y, z) -> c_20() 587.06/297.04 , f0^#(0(), y, x) -> c_21(f1^#(x, y, x)) 587.06/297.04 , f1^#(x, y, z) -> c_22(f2^#(x, y, z)) 587.06/297.04 , f1^#(x, y, z) -> c_23() 587.06/297.04 , f2^#(x, 1(), z) -> c_24(f0^#(x, z, z)) } 587.06/297.04 Strict Trs: 587.06/297.04 { plus(x, y) -> ifPlus(isZero(x), x, inc(y)) 587.06/297.04 , ifPlus(true(), x, y) -> p(y) 587.06/297.04 , ifPlus(false(), x, y) -> plus(p(x), y) 587.06/297.04 , isZero(0()) -> true() 587.06/297.04 , isZero(s(0())) -> false() 587.06/297.04 , isZero(s(s(x))) -> isZero(s(x)) 587.06/297.04 , inc(x) -> s(x) 587.06/297.04 , inc(0()) -> s(0()) 587.06/297.04 , inc(s(x)) -> s(inc(x)) 587.06/297.04 , p(0()) -> 0() 587.06/297.04 , p(s(x)) -> x 587.06/297.04 , p(s(s(x))) -> s(p(s(x))) 587.06/297.04 , times(x, y) -> timesIter(0(), x, y, 0()) 587.06/297.04 , timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z) 587.06/297.04 , ifTimes(true(), i, x, y, z) -> z 587.06/297.04 , ifTimes(false(), i, x, y, z) -> 587.06/297.04 timesIter(inc(i), x, y, plus(z, y)) 587.06/297.04 , ge(x, 0()) -> true() 587.06/297.04 , ge(0(), s(y)) -> false() 587.06/297.04 , ge(s(x), s(y)) -> ge(x, y) 587.06/297.04 , f0(x, y, z) -> d() 587.06/297.04 , f0(0(), y, x) -> f1(x, y, x) 587.06/297.04 , f1(x, y, z) -> f2(x, y, z) 587.06/297.04 , f1(x, y, z) -> c() 587.06/297.04 , f2(x, 1(), z) -> f0(x, z, z) } 587.06/297.04 Obligation: 587.06/297.04 runtime complexity 587.06/297.04 Answer: 587.06/297.04 MAYBE 587.06/297.04 587.06/297.04 We estimate the number of application of {4,7,8,11,17,18,20,23} by 587.06/297.04 applications of Pre({4,7,8,11,17,18,20,23}) = 587.06/297.04 {2,5,9,10,12,15,19,21,24}. Here rules are labeled as follows: 587.06/297.04 587.06/297.04 DPs: 587.06/297.04 { 1: plus^#(x, y) -> c_1(ifPlus^#(isZero(x), x, inc(y))) 587.06/297.04 , 2: ifPlus^#(true(), x, y) -> c_2(p^#(y)) 587.06/297.04 , 3: ifPlus^#(false(), x, y) -> c_3(plus^#(p(x), y)) 587.06/297.04 , 4: p^#(0()) -> c_10() 587.06/297.04 , 5: p^#(s(x)) -> c_11(x) 587.06/297.04 , 6: p^#(s(s(x))) -> c_12(p^#(s(x))) 587.06/297.04 , 7: isZero^#(0()) -> c_4() 587.06/297.04 , 8: isZero^#(s(0())) -> c_5() 587.06/297.04 , 9: isZero^#(s(s(x))) -> c_6(isZero^#(s(x))) 587.06/297.04 , 10: inc^#(x) -> c_7(x) 587.06/297.04 , 11: inc^#(0()) -> c_8() 587.06/297.04 , 12: inc^#(s(x)) -> c_9(inc^#(x)) 587.06/297.04 , 13: times^#(x, y) -> c_13(timesIter^#(0(), x, y, 0())) 587.06/297.04 , 14: timesIter^#(i, x, y, z) -> 587.06/297.04 c_14(ifTimes^#(ge(i, x), i, x, y, z)) 587.06/297.04 , 15: ifTimes^#(true(), i, x, y, z) -> c_15(z) 587.06/297.04 , 16: ifTimes^#(false(), i, x, y, z) -> 587.06/297.04 c_16(timesIter^#(inc(i), x, y, plus(z, y))) 587.06/297.04 , 17: ge^#(x, 0()) -> c_17() 587.06/297.04 , 18: ge^#(0(), s(y)) -> c_18() 587.06/297.04 , 19: ge^#(s(x), s(y)) -> c_19(ge^#(x, y)) 587.06/297.04 , 20: f0^#(x, y, z) -> c_20() 587.06/297.04 , 21: f0^#(0(), y, x) -> c_21(f1^#(x, y, x)) 587.06/297.04 , 22: f1^#(x, y, z) -> c_22(f2^#(x, y, z)) 587.06/297.04 , 23: f1^#(x, y, z) -> c_23() 587.06/297.04 , 24: f2^#(x, 1(), z) -> c_24(f0^#(x, z, z)) } 587.06/297.04 587.06/297.04 We are left with following problem, upon which TcT provides the 587.06/297.04 certificate MAYBE. 587.06/297.04 587.06/297.04 Strict DPs: 587.06/297.04 { plus^#(x, y) -> c_1(ifPlus^#(isZero(x), x, inc(y))) 587.06/297.04 , ifPlus^#(true(), x, y) -> c_2(p^#(y)) 587.06/297.04 , ifPlus^#(false(), x, y) -> c_3(plus^#(p(x), y)) 587.06/297.04 , p^#(s(x)) -> c_11(x) 587.06/297.04 , p^#(s(s(x))) -> c_12(p^#(s(x))) 587.06/297.04 , isZero^#(s(s(x))) -> c_6(isZero^#(s(x))) 587.06/297.04 , inc^#(x) -> c_7(x) 587.06/297.04 , inc^#(s(x)) -> c_9(inc^#(x)) 587.06/297.04 , times^#(x, y) -> c_13(timesIter^#(0(), x, y, 0())) 587.06/297.04 , timesIter^#(i, x, y, z) -> c_14(ifTimes^#(ge(i, x), i, x, y, z)) 587.06/297.04 , ifTimes^#(true(), i, x, y, z) -> c_15(z) 587.06/297.04 , ifTimes^#(false(), i, x, y, z) -> 587.06/297.04 c_16(timesIter^#(inc(i), x, y, plus(z, y))) 587.06/297.04 , ge^#(s(x), s(y)) -> c_19(ge^#(x, y)) 587.06/297.04 , f0^#(0(), y, x) -> c_21(f1^#(x, y, x)) 587.06/297.04 , f1^#(x, y, z) -> c_22(f2^#(x, y, z)) 587.06/297.04 , f2^#(x, 1(), z) -> c_24(f0^#(x, z, z)) } 587.06/297.04 Strict Trs: 587.06/297.04 { plus(x, y) -> ifPlus(isZero(x), x, inc(y)) 587.06/297.04 , ifPlus(true(), x, y) -> p(y) 587.06/297.04 , ifPlus(false(), x, y) -> plus(p(x), y) 587.06/297.04 , isZero(0()) -> true() 587.06/297.04 , isZero(s(0())) -> false() 587.06/297.04 , isZero(s(s(x))) -> isZero(s(x)) 587.06/297.04 , inc(x) -> s(x) 587.06/297.04 , inc(0()) -> s(0()) 587.06/297.04 , inc(s(x)) -> s(inc(x)) 587.06/297.04 , p(0()) -> 0() 587.06/297.04 , p(s(x)) -> x 587.06/297.04 , p(s(s(x))) -> s(p(s(x))) 587.06/297.04 , times(x, y) -> timesIter(0(), x, y, 0()) 587.06/297.04 , timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z) 587.06/297.04 , ifTimes(true(), i, x, y, z) -> z 587.06/297.04 , ifTimes(false(), i, x, y, z) -> 587.06/297.04 timesIter(inc(i), x, y, plus(z, y)) 587.06/297.04 , ge(x, 0()) -> true() 587.06/297.04 , ge(0(), s(y)) -> false() 587.06/297.04 , ge(s(x), s(y)) -> ge(x, y) 587.06/297.04 , f0(x, y, z) -> d() 587.06/297.04 , f0(0(), y, x) -> f1(x, y, x) 587.06/297.04 , f1(x, y, z) -> f2(x, y, z) 587.06/297.04 , f1(x, y, z) -> c() 587.06/297.04 , f2(x, 1(), z) -> f0(x, z, z) } 587.06/297.04 Weak DPs: 587.06/297.04 { p^#(0()) -> c_10() 587.06/297.04 , isZero^#(0()) -> c_4() 587.06/297.04 , isZero^#(s(0())) -> c_5() 587.06/297.04 , inc^#(0()) -> c_8() 587.06/297.04 , ge^#(x, 0()) -> c_17() 587.06/297.04 , ge^#(0(), s(y)) -> c_18() 587.06/297.04 , f0^#(x, y, z) -> c_20() 587.06/297.04 , f1^#(x, y, z) -> c_23() } 587.06/297.04 Obligation: 587.06/297.04 runtime complexity 587.06/297.04 Answer: 587.06/297.04 MAYBE 587.06/297.04 587.06/297.04 Empty strict component of the problem is NOT empty. 587.06/297.04 587.06/297.04 587.06/297.04 Arrrr.. 587.39/297.33 EOF