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