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