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