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