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