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