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