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