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