MAYBE 470.63/297.12 MAYBE 470.63/297.12 470.63/297.12 We are left with following problem, upon which TcT provides the 470.63/297.12 certificate MAYBE. 470.63/297.12 470.63/297.12 Strict Trs: 470.63/297.12 { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) 470.63/297.12 , gt(s(u), s(v)) -> gt(u, v) 470.63/297.12 , gt(s(u), 0()) -> true() 470.63/297.12 , gt(0(), v) -> false() 470.63/297.12 , trunc(s(s(x))) -> s(s(trunc(x))) 470.63/297.12 , trunc(s(0())) -> 0() 470.63/297.12 , trunc(0()) -> 0() } 470.63/297.12 Obligation: 470.63/297.12 innermost runtime complexity 470.63/297.12 Answer: 470.63/297.12 MAYBE 470.63/297.12 470.63/297.12 None of the processors succeeded. 470.63/297.12 470.63/297.12 Details of failed attempt(s): 470.63/297.12 ----------------------------- 470.63/297.12 1) 'empty' failed due to the following reason: 470.63/297.12 470.63/297.12 Empty strict component of the problem is NOT empty. 470.63/297.12 470.63/297.12 2) 'Best' failed due to the following reason: 470.63/297.12 470.63/297.12 None of the processors succeeded. 470.63/297.12 470.63/297.12 Details of failed attempt(s): 470.63/297.12 ----------------------------- 470.63/297.12 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 470.63/297.12 following reason: 470.63/297.12 470.63/297.12 Computation stopped due to timeout after 297.0 seconds. 470.63/297.12 470.63/297.12 2) 'Best' failed due to the following reason: 470.63/297.12 470.63/297.12 None of the processors succeeded. 470.63/297.12 470.63/297.12 Details of failed attempt(s): 470.63/297.12 ----------------------------- 470.63/297.12 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 470.63/297.12 seconds)' failed due to the following reason: 470.63/297.12 470.63/297.12 The weightgap principle applies (using the following nonconstant 470.63/297.12 growth matrix-interpretation) 470.63/297.12 470.63/297.12 The following argument positions are usable: 470.63/297.12 Uargs(f) = {1, 2}, Uargs(s) = {1} 470.63/297.12 470.63/297.12 TcT has computed the following matrix interpretation satisfying 470.63/297.12 not(EDA) and not(IDA(1)). 470.63/297.12 470.63/297.12 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 470.63/297.12 470.63/297.12 [true] = [5] 470.63/297.12 470.63/297.12 [gt](x1, x2) = [0] 470.63/297.12 470.63/297.12 [trunc](x1) = [0] 470.63/297.12 470.63/297.12 [s](x1) = [1] x1 + [0] 470.63/297.12 470.63/297.12 [0] = [0] 470.63/297.12 470.63/297.12 [false] = [7] 470.63/297.12 470.63/297.12 The order satisfies the following ordering constraints: 470.63/297.12 470.63/297.12 [f(true(), x, y)] = [1] x + [1] y + [5] 470.63/297.12 > [1] y + [0] 470.63/297.12 = [f(gt(x, y), trunc(x), s(y))] 470.63/297.12 470.63/297.12 [gt(s(u), s(v))] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [gt(u, v)] 470.63/297.12 470.63/297.12 [gt(s(u), 0())] = [0] 470.63/297.12 ? [5] 470.63/297.12 = [true()] 470.63/297.12 470.63/297.12 [gt(0(), v)] = [0] 470.63/297.12 ? [7] 470.63/297.12 = [false()] 470.63/297.12 470.63/297.12 [trunc(s(s(x)))] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [s(s(trunc(x)))] 470.63/297.12 470.63/297.12 [trunc(s(0()))] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [0()] 470.63/297.12 470.63/297.12 [trunc(0())] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [0()] 470.63/297.12 470.63/297.12 470.63/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 470.63/297.12 470.63/297.12 We are left with following problem, upon which TcT provides the 470.63/297.12 certificate MAYBE. 470.63/297.12 470.63/297.12 Strict Trs: 470.63/297.12 { gt(s(u), s(v)) -> gt(u, v) 470.63/297.12 , gt(s(u), 0()) -> true() 470.63/297.12 , gt(0(), v) -> false() 470.63/297.12 , trunc(s(s(x))) -> s(s(trunc(x))) 470.63/297.12 , trunc(s(0())) -> 0() 470.63/297.12 , trunc(0()) -> 0() } 470.63/297.12 Weak Trs: { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) } 470.63/297.12 Obligation: 470.63/297.12 innermost runtime complexity 470.63/297.12 Answer: 470.63/297.12 MAYBE 470.63/297.12 470.63/297.12 The weightgap principle applies (using the following nonconstant 470.63/297.12 growth matrix-interpretation) 470.63/297.12 470.63/297.12 The following argument positions are usable: 470.63/297.12 Uargs(f) = {1, 2}, Uargs(s) = {1} 470.63/297.12 470.63/297.12 TcT has computed the following matrix interpretation satisfying 470.63/297.12 not(EDA) and not(IDA(1)). 470.63/297.12 470.63/297.12 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 470.63/297.12 470.63/297.12 [true] = [7] 470.63/297.12 470.63/297.12 [gt](x1, x2) = [1] 470.63/297.12 470.63/297.12 [trunc](x1) = [0] 470.63/297.12 470.63/297.12 [s](x1) = [1] x1 + [0] 470.63/297.12 470.63/297.12 [0] = [0] 470.63/297.12 470.63/297.12 [false] = [0] 470.63/297.12 470.63/297.12 The order satisfies the following ordering constraints: 470.63/297.12 470.63/297.12 [f(true(), x, y)] = [1] x + [1] y + [8] 470.63/297.12 > [1] y + [2] 470.63/297.12 = [f(gt(x, y), trunc(x), s(y))] 470.63/297.12 470.63/297.12 [gt(s(u), s(v))] = [1] 470.63/297.12 >= [1] 470.63/297.12 = [gt(u, v)] 470.63/297.12 470.63/297.12 [gt(s(u), 0())] = [1] 470.63/297.12 ? [7] 470.63/297.12 = [true()] 470.63/297.12 470.63/297.12 [gt(0(), v)] = [1] 470.63/297.12 > [0] 470.63/297.12 = [false()] 470.63/297.12 470.63/297.12 [trunc(s(s(x)))] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [s(s(trunc(x)))] 470.63/297.12 470.63/297.12 [trunc(s(0()))] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [0()] 470.63/297.12 470.63/297.12 [trunc(0())] = [0] 470.63/297.12 >= [0] 470.63/297.12 = [0()] 470.63/297.12 470.63/297.12 470.63/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 470.63/297.12 470.63/297.12 We are left with following problem, upon which TcT provides the 470.63/297.12 certificate MAYBE. 470.63/297.12 470.63/297.12 Strict Trs: 470.63/297.12 { gt(s(u), s(v)) -> gt(u, v) 470.63/297.12 , gt(s(u), 0()) -> true() 470.63/297.13 , trunc(s(s(x))) -> s(s(trunc(x))) 470.63/297.13 , trunc(s(0())) -> 0() 470.63/297.13 , trunc(0()) -> 0() } 470.63/297.13 Weak Trs: 470.63/297.13 { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) 470.63/297.13 , gt(0(), v) -> false() } 470.63/297.13 Obligation: 470.63/297.13 innermost runtime complexity 470.63/297.13 Answer: 470.63/297.13 MAYBE 470.63/297.13 470.63/297.13 The weightgap principle applies (using the following nonconstant 470.63/297.13 growth matrix-interpretation) 470.63/297.13 470.63/297.13 The following argument positions are usable: 470.63/297.13 Uargs(f) = {1, 2}, Uargs(s) = {1} 470.63/297.13 470.63/297.13 TcT has computed the following matrix interpretation satisfying 470.63/297.13 not(EDA) and not(IDA(1)). 470.63/297.13 470.63/297.13 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] 470.63/297.13 470.63/297.13 [true] = [0] 470.63/297.13 470.63/297.13 [gt](x1, x2) = [1] x1 + [0] 470.63/297.13 470.63/297.13 [trunc](x1) = [0] 470.63/297.13 470.63/297.13 [s](x1) = [1] x1 + [4] 470.63/297.13 470.63/297.13 [0] = [0] 470.63/297.13 470.63/297.13 [false] = [0] 470.63/297.13 470.63/297.13 The order satisfies the following ordering constraints: 470.63/297.13 470.63/297.13 [f(true(), x, y)] = [1] x + [1] 470.63/297.13 >= [1] x + [1] 470.63/297.13 = [f(gt(x, y), trunc(x), s(y))] 470.63/297.13 470.63/297.13 [gt(s(u), s(v))] = [1] u + [4] 470.63/297.13 > [1] u + [0] 470.63/297.13 = [gt(u, v)] 470.63/297.13 470.63/297.13 [gt(s(u), 0())] = [1] u + [4] 470.63/297.13 > [0] 470.63/297.13 = [true()] 470.63/297.13 470.63/297.13 [gt(0(), v)] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [false()] 470.63/297.13 470.63/297.13 [trunc(s(s(x)))] = [0] 470.63/297.13 ? [8] 470.63/297.13 = [s(s(trunc(x)))] 470.63/297.13 470.63/297.13 [trunc(s(0()))] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 [trunc(0())] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 470.63/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 470.63/297.13 470.63/297.13 We are left with following problem, upon which TcT provides the 470.63/297.13 certificate MAYBE. 470.63/297.13 470.63/297.13 Strict Trs: 470.63/297.13 { trunc(s(s(x))) -> s(s(trunc(x))) 470.63/297.13 , trunc(s(0())) -> 0() 470.63/297.13 , trunc(0()) -> 0() } 470.63/297.13 Weak Trs: 470.63/297.13 { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) 470.63/297.13 , gt(s(u), s(v)) -> gt(u, v) 470.63/297.13 , gt(s(u), 0()) -> true() 470.63/297.13 , gt(0(), v) -> false() } 470.63/297.13 Obligation: 470.63/297.13 innermost runtime complexity 470.63/297.13 Answer: 470.63/297.13 MAYBE 470.63/297.13 470.63/297.13 The weightgap principle applies (using the following nonconstant 470.63/297.13 growth matrix-interpretation) 470.63/297.13 470.63/297.13 The following argument positions are usable: 470.63/297.13 Uargs(f) = {1, 2}, Uargs(s) = {1} 470.63/297.13 470.63/297.13 TcT has computed the following matrix interpretation satisfying 470.63/297.13 not(EDA) and not(IDA(1)). 470.63/297.13 470.63/297.13 [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] 470.63/297.13 470.63/297.13 [true] = [0] 470.63/297.13 470.63/297.13 [gt](x1, x2) = [0] 470.63/297.13 470.63/297.13 [trunc](x1) = [1] x1 + [0] 470.63/297.13 470.63/297.13 [s](x1) = [1] x1 + [4] 470.63/297.13 470.63/297.13 [0] = [0] 470.63/297.13 470.63/297.13 [false] = [0] 470.63/297.13 470.63/297.13 The order satisfies the following ordering constraints: 470.63/297.13 470.63/297.13 [f(true(), x, y)] = [1] x + [1] 470.63/297.13 >= [1] x + [1] 470.63/297.13 = [f(gt(x, y), trunc(x), s(y))] 470.63/297.13 470.63/297.13 [gt(s(u), s(v))] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [gt(u, v)] 470.63/297.13 470.63/297.13 [gt(s(u), 0())] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [true()] 470.63/297.13 470.63/297.13 [gt(0(), v)] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [false()] 470.63/297.13 470.63/297.13 [trunc(s(s(x)))] = [1] x + [8] 470.63/297.13 >= [1] x + [8] 470.63/297.13 = [s(s(trunc(x)))] 470.63/297.13 470.63/297.13 [trunc(s(0()))] = [4] 470.63/297.13 > [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 [trunc(0())] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 470.63/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 470.63/297.13 470.63/297.13 We are left with following problem, upon which TcT provides the 470.63/297.13 certificate MAYBE. 470.63/297.13 470.63/297.13 Strict Trs: 470.63/297.13 { trunc(s(s(x))) -> s(s(trunc(x))) 470.63/297.13 , trunc(0()) -> 0() } 470.63/297.13 Weak Trs: 470.63/297.13 { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) 470.63/297.13 , gt(s(u), s(v)) -> gt(u, v) 470.63/297.13 , gt(s(u), 0()) -> true() 470.63/297.13 , gt(0(), v) -> false() 470.63/297.13 , trunc(s(0())) -> 0() } 470.63/297.13 Obligation: 470.63/297.13 innermost runtime complexity 470.63/297.13 Answer: 470.63/297.13 MAYBE 470.63/297.13 470.63/297.13 The weightgap principle applies (using the following nonconstant 470.63/297.13 growth matrix-interpretation) 470.63/297.13 470.63/297.13 The following argument positions are usable: 470.63/297.13 Uargs(f) = {1, 2}, Uargs(s) = {1} 470.63/297.13 470.63/297.13 TcT has computed the following matrix interpretation satisfying 470.63/297.13 not(EDA) and not(IDA(1)). 470.63/297.13 470.63/297.13 [f](x1, x2, x3) = [1] x1 + [1] x2 + [0] 470.63/297.13 470.63/297.13 [true] = [1] 470.63/297.13 470.63/297.13 [gt](x1, x2) = [1] x1 + [0] 470.63/297.13 470.63/297.13 [trunc](x1) = [1] 470.63/297.13 470.63/297.13 [s](x1) = [1] x1 + [4] 470.63/297.13 470.63/297.13 [0] = [0] 470.63/297.13 470.63/297.13 [false] = [0] 470.63/297.13 470.63/297.13 The order satisfies the following ordering constraints: 470.63/297.13 470.63/297.13 [f(true(), x, y)] = [1] x + [1] 470.63/297.13 >= [1] x + [1] 470.63/297.13 = [f(gt(x, y), trunc(x), s(y))] 470.63/297.13 470.63/297.13 [gt(s(u), s(v))] = [1] u + [4] 470.63/297.13 > [1] u + [0] 470.63/297.13 = [gt(u, v)] 470.63/297.13 470.63/297.13 [gt(s(u), 0())] = [1] u + [4] 470.63/297.13 > [1] 470.63/297.13 = [true()] 470.63/297.13 470.63/297.13 [gt(0(), v)] = [0] 470.63/297.13 >= [0] 470.63/297.13 = [false()] 470.63/297.13 470.63/297.13 [trunc(s(s(x)))] = [1] 470.63/297.13 ? [9] 470.63/297.13 = [s(s(trunc(x)))] 470.63/297.13 470.63/297.13 [trunc(s(0()))] = [1] 470.63/297.13 > [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 [trunc(0())] = [1] 470.63/297.13 > [0] 470.63/297.13 = [0()] 470.63/297.13 470.63/297.13 470.63/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 470.63/297.13 470.63/297.13 We are left with following problem, upon which TcT provides the 470.63/297.13 certificate MAYBE. 470.63/297.13 470.63/297.13 Strict Trs: { trunc(s(s(x))) -> s(s(trunc(x))) } 470.63/297.13 Weak Trs: 470.63/297.13 { f(true(), x, y) -> f(gt(x, y), trunc(x), s(y)) 470.63/297.13 , gt(s(u), s(v)) -> gt(u, v) 470.63/297.13 , gt(s(u), 0()) -> true() 470.63/297.13 , gt(0(), v) -> false() 470.63/297.13 , trunc(s(0())) -> 0() 470.63/297.13 , trunc(0()) -> 0() } 470.63/297.13 Obligation: 470.63/297.13 innermost runtime complexity 470.63/297.13 Answer: 470.63/297.13 MAYBE 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'Fastest' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'empty' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 2) 'With Problem ...' failed due to the following reason: 470.63/297.13 470.63/297.13 Empty strict component of the problem is NOT empty. 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 2) 'Best' failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 470.63/297.13 to the following reason: 470.63/297.13 470.63/297.13 The input cannot be shown compatible 470.63/297.13 470.63/297.13 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 470.63/297.13 following reason: 470.63/297.13 470.63/297.13 The input cannot be shown compatible 470.63/297.13 470.63/297.13 470.63/297.13 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 470.63/297.13 failed due to the following reason: 470.63/297.13 470.63/297.13 None of the processors succeeded. 470.63/297.13 470.63/297.13 Details of failed attempt(s): 470.63/297.13 ----------------------------- 470.63/297.13 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 470.63/297.13 failed due to the following reason: 470.63/297.13 470.63/297.13 match-boundness of the problem could not be verified. 470.63/297.13 470.63/297.13 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 470.63/297.13 failed due to the following reason: 470.63/297.13 470.63/297.13 match-boundness of the problem could not be verified. 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 470.63/297.13 Arrrr.. 470.63/297.13 EOF