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