MAYBE 980.00/297.08 MAYBE 980.00/297.08 980.00/297.08 We are left with following problem, upon which TcT provides the 980.00/297.08 certificate MAYBE. 980.00/297.08 980.00/297.08 Strict Trs: 980.00/297.08 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.00/297.08 , cond(false(), x, y) -> 0() 980.00/297.08 , cond(true(), x, y) -> s(minus(x, s(y))) 980.00/297.08 , ge(u, 0()) -> true() 980.00/297.08 , ge(s(u), s(v)) -> ge(u, v) 980.00/297.08 , ge(0(), s(v)) -> false() } 980.00/297.08 Obligation: 980.00/297.08 runtime complexity 980.00/297.08 Answer: 980.00/297.08 MAYBE 980.00/297.08 980.00/297.08 None of the processors succeeded. 980.00/297.08 980.00/297.08 Details of failed attempt(s): 980.00/297.08 ----------------------------- 980.00/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 980.00/297.08 following reason: 980.00/297.08 980.00/297.08 Computation stopped due to timeout after 297.0 seconds. 980.00/297.08 980.00/297.08 2) 'Best' failed due to the following reason: 980.00/297.08 980.00/297.08 None of the processors succeeded. 980.00/297.08 980.00/297.08 Details of failed attempt(s): 980.00/297.08 ----------------------------- 980.00/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 980.00/297.08 seconds)' failed due to the following reason: 980.00/297.08 980.00/297.08 The weightgap principle applies (using the following nonconstant 980.00/297.08 growth matrix-interpretation) 980.00/297.08 980.00/297.08 The following argument positions are usable: 980.00/297.08 Uargs(cond) = {1}, Uargs(s) = {1} 980.00/297.08 980.00/297.08 TcT has computed the following matrix interpretation satisfying 980.00/297.08 not(EDA) and not(IDA(1)). 980.00/297.08 980.00/297.08 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 980.00/297.08 980.00/297.08 [cond](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 980.00/297.08 980.00/297.08 [ge](x1, x2) = [4] 980.00/297.08 980.00/297.08 [s](x1) = [1] x1 + [0] 980.00/297.08 980.00/297.08 [false] = [0] 980.00/297.08 980.00/297.08 [0] = [7] 980.00/297.08 980.00/297.08 [true] = [1] 980.00/297.08 980.00/297.08 The order satisfies the following ordering constraints: 980.00/297.08 980.00/297.08 [minus(x, y)] = [1] x + [1] y + [0] 980.00/297.08 ? [1] x + [1] y + [4] 980.00/297.08 = [cond(ge(x, s(y)), x, y)] 980.00/297.08 980.00/297.08 [cond(false(), x, y)] = [1] x + [1] y + [0] 980.00/297.08 ? [7] 980.00/297.08 = [0()] 980.00/297.08 980.00/297.08 [cond(true(), x, y)] = [1] x + [1] y + [1] 980.00/297.08 > [1] x + [1] y + [0] 980.00/297.08 = [s(minus(x, s(y)))] 980.00/297.08 980.00/297.08 [ge(u, 0())] = [4] 980.00/297.08 > [1] 980.00/297.08 = [true()] 980.00/297.08 980.00/297.08 [ge(s(u), s(v))] = [4] 980.00/297.08 >= [4] 980.00/297.08 = [ge(u, v)] 980.00/297.08 980.00/297.08 [ge(0(), s(v))] = [4] 980.00/297.08 > [0] 980.00/297.08 = [false()] 980.00/297.08 980.00/297.08 980.00/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 980.00/297.08 980.00/297.08 We are left with following problem, upon which TcT provides the 980.00/297.08 certificate MAYBE. 980.00/297.08 980.00/297.08 Strict Trs: 980.00/297.08 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.00/297.08 , cond(false(), x, y) -> 0() 980.00/297.08 , ge(s(u), s(v)) -> ge(u, v) } 980.00/297.08 Weak Trs: 980.00/297.08 { cond(true(), x, y) -> s(minus(x, s(y))) 980.00/297.08 , ge(u, 0()) -> true() 980.00/297.08 , ge(0(), s(v)) -> false() } 980.00/297.08 Obligation: 980.00/297.08 runtime complexity 980.00/297.08 Answer: 980.00/297.08 MAYBE 980.00/297.08 980.00/297.08 The weightgap principle applies (using the following nonconstant 980.00/297.08 growth matrix-interpretation) 980.00/297.08 980.00/297.08 The following argument positions are usable: 980.00/297.08 Uargs(cond) = {1}, Uargs(s) = {1} 980.00/297.08 980.00/297.08 TcT has computed the following matrix interpretation satisfying 980.00/297.08 not(EDA) and not(IDA(1)). 980.00/297.08 980.00/297.08 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 980.00/297.08 980.00/297.08 [cond](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 980.00/297.08 980.00/297.08 [ge](x1, x2) = [0] 980.00/297.08 980.00/297.08 [s](x1) = [1] x1 + [0] 980.00/297.08 980.00/297.08 [false] = [0] 980.00/297.08 980.00/297.08 [0] = [0] 980.00/297.08 980.00/297.08 [true] = [0] 980.00/297.08 980.00/297.08 The order satisfies the following ordering constraints: 980.00/297.08 980.00/297.08 [minus(x, y)] = [1] x + [1] y + [0] 980.00/297.08 ? [1] x + [1] y + [1] 980.00/297.08 = [cond(ge(x, s(y)), x, y)] 980.00/297.08 980.00/297.08 [cond(false(), x, y)] = [1] x + [1] y + [1] 980.00/297.08 > [0] 980.00/297.08 = [0()] 980.00/297.08 980.00/297.08 [cond(true(), x, y)] = [1] x + [1] y + [1] 980.00/297.08 > [1] x + [1] y + [0] 980.00/297.08 = [s(minus(x, s(y)))] 980.00/297.08 980.00/297.08 [ge(u, 0())] = [0] 980.00/297.08 >= [0] 980.00/297.08 = [true()] 980.00/297.08 980.00/297.08 [ge(s(u), s(v))] = [0] 980.00/297.08 >= [0] 980.00/297.08 = [ge(u, v)] 980.00/297.08 980.00/297.08 [ge(0(), s(v))] = [0] 980.00/297.08 >= [0] 980.00/297.08 = [false()] 980.00/297.08 980.00/297.08 980.00/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 980.00/297.08 980.00/297.08 We are left with following problem, upon which TcT provides the 980.00/297.08 certificate MAYBE. 980.00/297.08 980.00/297.08 Strict Trs: 980.00/297.08 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.00/297.08 , ge(s(u), s(v)) -> ge(u, v) } 980.00/297.08 Weak Trs: 980.00/297.08 { cond(false(), x, y) -> 0() 980.00/297.08 , cond(true(), x, y) -> s(minus(x, s(y))) 980.00/297.08 , ge(u, 0()) -> true() 980.00/297.08 , ge(0(), s(v)) -> false() } 980.00/297.08 Obligation: 980.00/297.08 runtime complexity 980.00/297.08 Answer: 980.00/297.08 MAYBE 980.00/297.08 980.00/297.08 None of the processors succeeded. 980.00/297.08 980.00/297.08 Details of failed attempt(s): 980.00/297.08 ----------------------------- 980.00/297.08 1) 'empty' failed due to the following reason: 980.00/297.08 980.00/297.08 Empty strict component of the problem is NOT empty. 980.00/297.08 980.00/297.08 2) 'With Problem ...' failed due to the following reason: 980.00/297.08 980.00/297.08 None of the processors succeeded. 980.00/297.08 980.00/297.08 Details of failed attempt(s): 980.00/297.08 ----------------------------- 980.00/297.08 1) 'empty' failed due to the following reason: 980.00/297.08 980.00/297.08 Empty strict component of the problem is NOT empty. 980.00/297.08 980.00/297.08 2) 'Fastest' failed due to the following reason: 980.00/297.08 980.00/297.08 None of the processors succeeded. 980.00/297.08 980.00/297.08 Details of failed attempt(s): 980.00/297.08 ----------------------------- 980.00/297.08 1) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.00/297.09 ----------------------------- 980.00/297.09 1) 'empty' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 2) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 980.00/297.09 2) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.00/297.09 ----------------------------- 980.00/297.09 1) 'empty' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 2) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 The weightgap principle applies (using the following nonconstant 980.00/297.09 growth matrix-interpretation) 980.00/297.09 980.00/297.09 The following argument positions are usable: 980.00/297.09 Uargs(cond) = {1}, Uargs(s) = {1} 980.00/297.09 980.00/297.09 TcT has computed the following matrix interpretation satisfying 980.00/297.09 not(EDA) and not(IDA(1)). 980.00/297.09 980.00/297.09 [minus](x1, x2) = [1 4] x2 + [5] 980.00/297.09 [0 0] [4] 980.00/297.09 980.00/297.09 [cond](x1, x2, x3) = [1 4] x1 + [1 4] x3 + [0] 980.00/297.09 [0 0] [0 0] [4] 980.00/297.09 980.00/297.09 [ge](x1, x2) = [0 0] x2 + [4] 980.00/297.09 [0 1] [0] 980.00/297.09 980.00/297.09 [s](x1) = [1 0] x1 + [4] 980.00/297.09 [0 0] [0] 980.00/297.09 980.00/297.09 [false] = [0] 980.00/297.09 [0] 980.00/297.09 980.00/297.09 [0] = [0] 980.00/297.09 [4] 980.00/297.09 980.00/297.09 [true] = [1] 980.00/297.09 [3] 980.00/297.09 980.00/297.09 The order satisfies the following ordering constraints: 980.00/297.09 980.00/297.09 [minus(x, y)] = [1 4] y + [5] 980.00/297.09 [0 0] [4] 980.00/297.09 > [1 4] y + [4] 980.00/297.09 [0 0] [4] 980.00/297.09 = [cond(ge(x, s(y)), x, y)] 980.00/297.09 980.00/297.09 [cond(false(), x, y)] = [1 4] y + [0] 980.00/297.09 [0 0] [4] 980.00/297.09 >= [0] 980.00/297.09 [4] 980.00/297.09 = [0()] 980.00/297.09 980.00/297.09 [cond(true(), x, y)] = [1 4] y + [13] 980.00/297.09 [0 0] [4] 980.00/297.09 >= [1 0] y + [13] 980.00/297.09 [0 0] [0] 980.00/297.09 = [s(minus(x, s(y)))] 980.00/297.09 980.00/297.09 [ge(u, 0())] = [4] 980.00/297.09 [4] 980.00/297.09 > [1] 980.00/297.09 [3] 980.00/297.09 = [true()] 980.00/297.09 980.00/297.09 [ge(s(u), s(v))] = [4] 980.00/297.09 [0] 980.00/297.09 ? [0 0] v + [4] 980.00/297.09 [0 1] [0] 980.00/297.09 = [ge(u, v)] 980.00/297.09 980.00/297.09 [ge(0(), s(v))] = [4] 980.00/297.09 [0] 980.00/297.09 > [0] 980.00/297.09 [0] 980.00/297.09 = [false()] 980.00/297.09 980.00/297.09 980.00/297.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 980.00/297.09 980.00/297.09 We are left with following problem, upon which TcT provides the 980.00/297.09 certificate MAYBE. 980.00/297.09 980.00/297.09 Strict Trs: { ge(s(u), s(v)) -> ge(u, v) } 980.00/297.09 Weak Trs: 980.00/297.09 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.00/297.09 , cond(false(), x, y) -> 0() 980.00/297.09 , cond(true(), x, y) -> s(minus(x, s(y))) 980.00/297.09 , ge(u, 0()) -> true() 980.00/297.09 , ge(0(), s(v)) -> false() } 980.00/297.09 Obligation: 980.00/297.09 runtime complexity 980.00/297.09 Answer: 980.00/297.09 MAYBE 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.00/297.09 ----------------------------- 980.00/297.09 1) 'empty' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 2) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.00/297.09 ----------------------------- 980.00/297.09 1) 'empty' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 2) 'With Problem ...' failed due to the following reason: 980.00/297.09 980.00/297.09 Empty strict component of the problem is NOT empty. 980.00/297.09 980.00/297.09 980.00/297.09 980.00/297.09 980.00/297.09 980.00/297.09 980.00/297.09 980.00/297.09 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 980.00/297.09 failed due to the following reason: 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.00/297.09 ----------------------------- 980.00/297.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 980.00/297.09 failed due to the following reason: 980.00/297.09 980.00/297.09 match-boundness of the problem could not be verified. 980.00/297.09 980.00/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 980.00/297.09 failed due to the following reason: 980.00/297.09 980.00/297.09 match-boundness of the problem could not be verified. 980.00/297.09 980.00/297.09 980.00/297.09 3) 'Best' failed due to the following reason: 980.00/297.09 980.00/297.09 None of the processors succeeded. 980.00/297.09 980.00/297.09 Details of failed attempt(s): 980.33/297.10 ----------------------------- 980.33/297.10 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 980.33/297.10 to the following reason: 980.33/297.10 980.33/297.10 The processor is inapplicable, reason: 980.33/297.10 Processor only applicable for innermost runtime complexity analysis 980.33/297.10 980.33/297.10 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 980.33/297.10 following reason: 980.33/297.10 980.33/297.10 The processor is inapplicable, reason: 980.33/297.10 Processor only applicable for innermost runtime complexity analysis 980.33/297.10 980.33/297.10 980.33/297.10 980.33/297.10 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 980.33/297.10 the following reason: 980.33/297.10 980.33/297.10 We add the following weak dependency pairs: 980.33/297.10 980.33/297.10 Strict DPs: 980.33/297.10 { minus^#(x, y) -> c_1(cond^#(ge(x, s(y)), x, y)) 980.33/297.10 , cond^#(false(), x, y) -> c_2() 980.33/297.10 , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) 980.33/297.10 , ge^#(u, 0()) -> c_4() 980.33/297.10 , ge^#(s(u), s(v)) -> c_5(ge^#(u, v)) 980.33/297.10 , ge^#(0(), s(v)) -> c_6() } 980.33/297.10 980.33/297.10 and mark the set of starting terms. 980.33/297.10 980.33/297.10 We are left with following problem, upon which TcT provides the 980.33/297.10 certificate MAYBE. 980.33/297.10 980.33/297.10 Strict DPs: 980.33/297.10 { minus^#(x, y) -> c_1(cond^#(ge(x, s(y)), x, y)) 980.33/297.10 , cond^#(false(), x, y) -> c_2() 980.33/297.10 , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) 980.33/297.10 , ge^#(u, 0()) -> c_4() 980.33/297.10 , ge^#(s(u), s(v)) -> c_5(ge^#(u, v)) 980.33/297.10 , ge^#(0(), s(v)) -> c_6() } 980.33/297.10 Strict Trs: 980.33/297.10 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.33/297.10 , cond(false(), x, y) -> 0() 980.33/297.10 , cond(true(), x, y) -> s(minus(x, s(y))) 980.33/297.10 , ge(u, 0()) -> true() 980.33/297.10 , ge(s(u), s(v)) -> ge(u, v) 980.33/297.10 , ge(0(), s(v)) -> false() } 980.33/297.10 Obligation: 980.33/297.10 runtime complexity 980.33/297.10 Answer: 980.33/297.10 MAYBE 980.33/297.10 980.33/297.10 We estimate the number of application of {2,4,6} by applications of 980.33/297.10 Pre({2,4,6}) = {1,5}. Here rules are labeled as follows: 980.33/297.10 980.33/297.10 DPs: 980.33/297.10 { 1: minus^#(x, y) -> c_1(cond^#(ge(x, s(y)), x, y)) 980.33/297.10 , 2: cond^#(false(), x, y) -> c_2() 980.33/297.10 , 3: cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) 980.33/297.10 , 4: ge^#(u, 0()) -> c_4() 980.33/297.10 , 5: ge^#(s(u), s(v)) -> c_5(ge^#(u, v)) 980.33/297.10 , 6: ge^#(0(), s(v)) -> c_6() } 980.33/297.10 980.33/297.10 We are left with following problem, upon which TcT provides the 980.33/297.10 certificate MAYBE. 980.33/297.10 980.33/297.10 Strict DPs: 980.33/297.10 { minus^#(x, y) -> c_1(cond^#(ge(x, s(y)), x, y)) 980.33/297.10 , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) 980.33/297.10 , ge^#(s(u), s(v)) -> c_5(ge^#(u, v)) } 980.33/297.10 Strict Trs: 980.33/297.10 { minus(x, y) -> cond(ge(x, s(y)), x, y) 980.33/297.10 , cond(false(), x, y) -> 0() 980.33/297.10 , cond(true(), x, y) -> s(minus(x, s(y))) 980.33/297.10 , ge(u, 0()) -> true() 980.33/297.10 , ge(s(u), s(v)) -> ge(u, v) 980.33/297.10 , ge(0(), s(v)) -> false() } 980.33/297.10 Weak DPs: 980.33/297.10 { cond^#(false(), x, y) -> c_2() 980.33/297.10 , ge^#(u, 0()) -> c_4() 980.33/297.10 , ge^#(0(), s(v)) -> c_6() } 980.33/297.10 Obligation: 980.33/297.10 runtime complexity 980.33/297.10 Answer: 980.33/297.10 MAYBE 980.33/297.10 980.33/297.10 Empty strict component of the problem is NOT empty. 980.33/297.10 980.33/297.10 980.33/297.10 Arrrr.. 981.25/298.03 EOF