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