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