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