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