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