MAYBE 879.92/297.03 MAYBE 879.92/297.03 879.92/297.03 We are left with following problem, upon which TcT provides the 879.92/297.03 certificate MAYBE. 879.92/297.03 879.92/297.03 Strict Trs: 879.92/297.03 { sort(nil()) -> nil() 879.92/297.03 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.03 , insert(x, nil()) -> cons(x, nil()) 879.92/297.03 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.03 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.03 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 879.92/297.03 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.03 choose(x, cons(v, w), y, z) } 879.92/297.03 Obligation: 879.92/297.03 runtime complexity 879.92/297.03 Answer: 879.92/297.03 MAYBE 879.92/297.03 879.92/297.03 None of the processors succeeded. 879.92/297.03 879.92/297.03 Details of failed attempt(s): 879.92/297.03 ----------------------------- 879.92/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 879.92/297.03 following reason: 879.92/297.03 879.92/297.03 Computation stopped due to timeout after 297.0 seconds. 879.92/297.03 879.92/297.03 2) 'Best' failed due to the following reason: 879.92/297.03 879.92/297.03 None of the processors succeeded. 879.92/297.03 879.92/297.03 Details of failed attempt(s): 879.92/297.03 ----------------------------- 879.92/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 879.92/297.03 seconds)' failed due to the following reason: 879.92/297.03 879.92/297.03 The weightgap principle applies (using the following nonconstant 879.92/297.03 growth matrix-interpretation) 879.92/297.03 879.92/297.03 The following argument positions are usable: 879.92/297.03 Uargs(cons) = {2}, Uargs(insert) = {2}, Uargs(choose) = {2} 879.92/297.03 879.92/297.03 TcT has computed the following matrix interpretation satisfying 879.92/297.03 not(EDA) and not(IDA(1)). 879.92/297.03 879.92/297.03 [sort](x1) = [0] 879.92/297.03 879.92/297.03 [nil] = [0] 879.92/297.03 879.92/297.03 [cons](x1, x2) = [1] x2 + [0] 879.92/297.03 879.92/297.03 [insert](x1, x2) = [1] x2 + [0] 879.92/297.03 879.92/297.03 [choose](x1, x2, x3, x4) = [1] x2 + [1] 879.92/297.03 879.92/297.03 [0] = [7] 879.92/297.03 879.92/297.03 [s](x1) = [1] x1 + [7] 879.92/297.03 879.92/297.03 The order satisfies the following ordering constraints: 879.92/297.03 879.92/297.03 [sort(nil())] = [0] 879.92/297.03 >= [0] 879.92/297.03 = [nil()] 879.92/297.03 879.92/297.03 [sort(cons(x, y))] = [0] 879.92/297.03 >= [0] 879.92/297.03 = [insert(x, sort(y))] 879.92/297.03 879.92/297.03 [insert(x, nil())] = [0] 879.92/297.03 >= [0] 879.92/297.03 = [cons(x, nil())] 879.92/297.03 879.92/297.03 [insert(x, cons(v, w))] = [1] w + [0] 879.92/297.03 ? [1] w + [1] 879.92/297.03 = [choose(x, cons(v, w), x, v)] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), y, 0())] = [1] w + [1] 879.92/297.03 > [1] w + [0] 879.92/297.03 = [cons(x, cons(v, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), 0(), s(z))] = [1] w + [1] 879.92/297.03 > [1] w + [0] 879.92/297.03 = [cons(v, insert(x, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), s(y), s(z))] = [1] w + [1] 879.92/297.03 >= [1] w + [1] 879.92/297.03 = [choose(x, cons(v, w), y, z)] 879.92/297.03 879.92/297.03 879.92/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.92/297.03 879.92/297.03 We are left with following problem, upon which TcT provides the 879.92/297.03 certificate MAYBE. 879.92/297.03 879.92/297.03 Strict Trs: 879.92/297.03 { sort(nil()) -> nil() 879.92/297.03 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.03 , insert(x, nil()) -> cons(x, nil()) 879.92/297.03 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.03 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.03 choose(x, cons(v, w), y, z) } 879.92/297.03 Weak Trs: 879.92/297.03 { choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.03 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 879.92/297.03 Obligation: 879.92/297.03 runtime complexity 879.92/297.03 Answer: 879.92/297.03 MAYBE 879.92/297.03 879.92/297.03 The weightgap principle applies (using the following nonconstant 879.92/297.03 growth matrix-interpretation) 879.92/297.03 879.92/297.03 The following argument positions are usable: 879.92/297.03 Uargs(cons) = {2}, Uargs(insert) = {2}, Uargs(choose) = {2} 879.92/297.03 879.92/297.03 TcT has computed the following matrix interpretation satisfying 879.92/297.03 not(EDA) and not(IDA(1)). 879.92/297.03 879.92/297.03 [sort](x1) = [1] x1 + [0] 879.92/297.03 879.92/297.03 [nil] = [0] 879.92/297.03 879.92/297.03 [cons](x1, x2) = [1] x1 + [1] x2 + [4] 879.92/297.03 879.92/297.03 [insert](x1, x2) = [1] x1 + [1] x2 + [0] 879.92/297.03 879.92/297.03 [choose](x1, x2, x3, x4) = [1] x1 + [1] x2 + [4] 879.92/297.03 879.92/297.03 [0] = [7] 879.92/297.03 879.92/297.03 [s](x1) = [1] x1 + [7] 879.92/297.03 879.92/297.03 The order satisfies the following ordering constraints: 879.92/297.03 879.92/297.03 [sort(nil())] = [0] 879.92/297.03 >= [0] 879.92/297.03 = [nil()] 879.92/297.03 879.92/297.03 [sort(cons(x, y))] = [1] x + [1] y + [4] 879.92/297.03 > [1] x + [1] y + [0] 879.92/297.03 = [insert(x, sort(y))] 879.92/297.03 879.92/297.03 [insert(x, nil())] = [1] x + [0] 879.92/297.03 ? [1] x + [4] 879.92/297.03 = [cons(x, nil())] 879.92/297.03 879.92/297.03 [insert(x, cons(v, w))] = [1] x + [1] v + [1] w + [4] 879.92/297.03 ? [1] x + [1] v + [1] w + [8] 879.92/297.03 = [choose(x, cons(v, w), x, v)] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), y, 0())] = [1] x + [1] v + [1] w + [8] 879.92/297.03 >= [1] x + [1] v + [1] w + [8] 879.92/297.03 = [cons(x, cons(v, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), 0(), s(z))] = [1] x + [1] v + [1] w + [8] 879.92/297.03 > [1] x + [1] v + [1] w + [4] 879.92/297.03 = [cons(v, insert(x, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), s(y), s(z))] = [1] x + [1] v + [1] w + [8] 879.92/297.03 >= [1] x + [1] v + [1] w + [8] 879.92/297.03 = [choose(x, cons(v, w), y, z)] 879.92/297.03 879.92/297.03 879.92/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.92/297.03 879.92/297.03 We are left with following problem, upon which TcT provides the 879.92/297.03 certificate MAYBE. 879.92/297.03 879.92/297.03 Strict Trs: 879.92/297.03 { sort(nil()) -> nil() 879.92/297.03 , insert(x, nil()) -> cons(x, nil()) 879.92/297.03 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.03 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.03 choose(x, cons(v, w), y, z) } 879.92/297.03 Weak Trs: 879.92/297.03 { sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.03 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.03 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 879.92/297.03 Obligation: 879.92/297.03 runtime complexity 879.92/297.03 Answer: 879.92/297.03 MAYBE 879.92/297.03 879.92/297.03 The weightgap principle applies (using the following nonconstant 879.92/297.03 growth matrix-interpretation) 879.92/297.03 879.92/297.03 The following argument positions are usable: 879.92/297.03 Uargs(cons) = {2}, Uargs(insert) = {2}, Uargs(choose) = {2} 879.92/297.03 879.92/297.03 TcT has computed the following matrix interpretation satisfying 879.92/297.03 not(EDA) and not(IDA(1)). 879.92/297.03 879.92/297.03 [sort](x1) = [1] 879.92/297.03 879.92/297.03 [nil] = [0] 879.92/297.03 879.92/297.03 [cons](x1, x2) = [1] x2 + [0] 879.92/297.03 879.92/297.03 [insert](x1, x2) = [1] x2 + [0] 879.92/297.03 879.92/297.03 [choose](x1, x2, x3, x4) = [1] x2 + [0] 879.92/297.03 879.92/297.03 [0] = [7] 879.92/297.03 879.92/297.03 [s](x1) = [1] x1 + [7] 879.92/297.03 879.92/297.03 The order satisfies the following ordering constraints: 879.92/297.03 879.92/297.03 [sort(nil())] = [1] 879.92/297.03 > [0] 879.92/297.03 = [nil()] 879.92/297.03 879.92/297.03 [sort(cons(x, y))] = [1] 879.92/297.03 >= [1] 879.92/297.03 = [insert(x, sort(y))] 879.92/297.03 879.92/297.03 [insert(x, nil())] = [0] 879.92/297.03 >= [0] 879.92/297.03 = [cons(x, nil())] 879.92/297.03 879.92/297.03 [insert(x, cons(v, w))] = [1] w + [0] 879.92/297.03 >= [1] w + [0] 879.92/297.03 = [choose(x, cons(v, w), x, v)] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), y, 0())] = [1] w + [0] 879.92/297.03 >= [1] w + [0] 879.92/297.03 = [cons(x, cons(v, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), 0(), s(z))] = [1] w + [0] 879.92/297.03 >= [1] w + [0] 879.92/297.03 = [cons(v, insert(x, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), s(y), s(z))] = [1] w + [0] 879.92/297.03 >= [1] w + [0] 879.92/297.03 = [choose(x, cons(v, w), y, z)] 879.92/297.03 879.92/297.03 879.92/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 879.92/297.03 879.92/297.03 We are left with following problem, upon which TcT provides the 879.92/297.03 certificate MAYBE. 879.92/297.03 879.92/297.03 Strict Trs: 879.92/297.03 { insert(x, nil()) -> cons(x, nil()) 879.92/297.03 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.03 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.03 choose(x, cons(v, w), y, z) } 879.92/297.03 Weak Trs: 879.92/297.03 { sort(nil()) -> nil() 879.92/297.03 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.03 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.03 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 879.92/297.03 Obligation: 879.92/297.03 runtime complexity 879.92/297.03 Answer: 879.92/297.03 MAYBE 879.92/297.03 879.92/297.03 We use the processor 'matrix interpretation of dimension 1' to 879.92/297.03 orient following rules strictly. 879.92/297.03 879.92/297.03 Trs: { insert(x, nil()) -> cons(x, nil()) } 879.92/297.03 879.92/297.03 The induced complexity on above rules (modulo remaining rules) is 879.92/297.03 YES(?,O(n^1)) . These rules are moved into the corresponding weak 879.92/297.03 component(s). 879.92/297.03 879.92/297.03 Sub-proof: 879.92/297.03 ---------- 879.92/297.03 The following argument positions are usable: 879.92/297.03 Uargs(cons) = {2}, Uargs(insert) = {2}, Uargs(choose) = {2} 879.92/297.03 879.92/297.03 TcT has computed the following constructor-based matrix 879.92/297.03 interpretation satisfying not(EDA). 879.92/297.03 879.92/297.03 [sort](x1) = [3] x1 + [0] 879.92/297.03 879.92/297.03 [nil] = [5] 879.92/297.03 879.92/297.03 [cons](x1, x2) = [1] x2 + [1] 879.92/297.03 879.92/297.03 [insert](x1, x2) = [1] x2 + [3] 879.92/297.03 879.92/297.03 [choose](x1, x2, x3, x4) = [1] x2 + [3] 879.92/297.03 879.92/297.03 [0] = [0] 879.92/297.03 879.92/297.03 [s](x1) = [1] x1 + [0] 879.92/297.03 879.92/297.03 The order satisfies the following ordering constraints: 879.92/297.03 879.92/297.03 [sort(nil())] = [15] 879.92/297.03 > [5] 879.92/297.03 = [nil()] 879.92/297.03 879.92/297.03 [sort(cons(x, y))] = [3] y + [3] 879.92/297.03 >= [3] y + [3] 879.92/297.03 = [insert(x, sort(y))] 879.92/297.03 879.92/297.03 [insert(x, nil())] = [8] 879.92/297.03 > [6] 879.92/297.03 = [cons(x, nil())] 879.92/297.03 879.92/297.03 [insert(x, cons(v, w))] = [1] w + [4] 879.92/297.03 >= [1] w + [4] 879.92/297.03 = [choose(x, cons(v, w), x, v)] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), y, 0())] = [1] w + [4] 879.92/297.03 > [1] w + [2] 879.92/297.03 = [cons(x, cons(v, w))] 879.92/297.03 879.92/297.03 [choose(x, cons(v, w), 0(), s(z))] = [1] w + [4] 879.92/297.03 >= [1] w + [4] 879.92/297.03 = [cons(v, insert(x, w))] 879.92/297.03 879.92/297.04 [choose(x, cons(v, w), s(y), s(z))] = [1] w + [4] 879.92/297.04 >= [1] w + [4] 879.92/297.04 = [choose(x, cons(v, w), y, z)] 879.92/297.04 879.92/297.04 879.92/297.04 We return to the main proof. 879.92/297.04 879.92/297.04 We are left with following problem, upon which TcT provides the 879.92/297.04 certificate MAYBE. 879.92/297.04 879.92/297.04 Strict Trs: 879.92/297.04 { insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.04 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 choose(x, cons(v, w), y, z) } 879.92/297.04 Weak Trs: 879.92/297.04 { sort(nil()) -> nil() 879.92/297.04 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.04 , insert(x, nil()) -> cons(x, nil()) 879.92/297.04 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.04 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 879.92/297.04 Obligation: 879.92/297.04 runtime complexity 879.92/297.04 Answer: 879.92/297.04 MAYBE 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'Fastest' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 We use the processor 'matrix interpretation of dimension 2' to 879.92/297.04 orient following rules strictly. 879.92/297.04 879.92/297.04 Trs: { insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) } 879.92/297.04 879.92/297.04 The induced complexity on above rules (modulo remaining rules) is 879.92/297.04 YES(?,O(n^2)) . These rules are moved into the corresponding weak 879.92/297.04 component(s). 879.92/297.04 879.92/297.04 Sub-proof: 879.92/297.04 ---------- 879.92/297.04 The following argument positions are usable: 879.92/297.04 Uargs(cons) = {2}, Uargs(insert) = {2}, Uargs(choose) = {2} 879.92/297.04 879.92/297.04 TcT has computed the following constructor-based matrix 879.92/297.04 interpretation satisfying not(EDA). 879.92/297.04 879.92/297.04 [sort](x1) = [4 0] x1 + [0] 879.92/297.04 [0 1] [0] 879.92/297.04 879.92/297.04 [nil] = [0] 879.92/297.04 [0] 879.92/297.04 879.92/297.04 [cons](x1, x2) = [1 1] x2 + [1] 879.92/297.04 [0 1] [2] 879.92/297.04 879.92/297.04 [insert](x1, x2) = [1 4] x2 + [2] 879.92/297.04 [0 1] [2] 879.92/297.04 879.92/297.04 [choose](x1, x2, x3, x4) = [1 4] x2 + [0] 879.92/297.04 [0 1] [2] 879.92/297.04 879.92/297.04 [0] = [0] 879.92/297.04 [0] 879.92/297.04 879.92/297.04 [s](x1) = [0] 879.92/297.04 [0] 879.92/297.04 879.92/297.04 The order satisfies the following ordering constraints: 879.92/297.04 879.92/297.04 [sort(nil())] = [0] 879.92/297.04 [0] 879.92/297.04 >= [0] 879.92/297.04 [0] 879.92/297.04 = [nil()] 879.92/297.04 879.92/297.04 [sort(cons(x, y))] = [4 4] y + [4] 879.92/297.04 [0 1] [2] 879.92/297.04 > [4 4] y + [2] 879.92/297.04 [0 1] [2] 879.92/297.04 = [insert(x, sort(y))] 879.92/297.04 879.92/297.04 [insert(x, nil())] = [2] 879.92/297.04 [2] 879.92/297.04 > [1] 879.92/297.04 [2] 879.92/297.04 = [cons(x, nil())] 879.92/297.04 879.92/297.04 [insert(x, cons(v, w))] = [1 5] w + [11] 879.92/297.04 [0 1] [4] 879.92/297.04 > [1 5] w + [9] 879.92/297.04 [0 1] [4] 879.92/297.04 = [choose(x, cons(v, w), x, v)] 879.92/297.04 879.92/297.04 [choose(x, cons(v, w), y, 0())] = [1 5] w + [9] 879.92/297.04 [0 1] [4] 879.92/297.04 > [1 2] w + [4] 879.92/297.04 [0 1] [4] 879.92/297.04 = [cons(x, cons(v, w))] 879.92/297.04 879.92/297.04 [choose(x, cons(v, w), 0(), s(z))] = [1 5] w + [9] 879.92/297.04 [0 1] [4] 879.92/297.04 > [1 5] w + [5] 879.92/297.04 [0 1] [4] 879.92/297.04 = [cons(v, insert(x, w))] 879.92/297.04 879.92/297.04 [choose(x, cons(v, w), s(y), s(z))] = [1 5] w + [9] 879.92/297.04 [0 1] [4] 879.92/297.04 >= [1 5] w + [9] 879.92/297.04 [0 1] [4] 879.92/297.04 = [choose(x, cons(v, w), y, z)] 879.92/297.04 879.92/297.04 879.92/297.04 We return to the main proof. 879.92/297.04 879.92/297.04 We are left with following problem, upon which TcT provides the 879.92/297.04 certificate MAYBE. 879.92/297.04 879.92/297.04 Strict Trs: 879.92/297.04 { choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 choose(x, cons(v, w), y, z) } 879.92/297.04 Weak Trs: 879.92/297.04 { sort(nil()) -> nil() 879.92/297.04 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.04 , insert(x, nil()) -> cons(x, nil()) 879.92/297.04 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.04 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.04 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 879.92/297.04 Obligation: 879.92/297.04 runtime complexity 879.92/297.04 Answer: 879.92/297.04 MAYBE 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'empty' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 2) 'With Problem ...' failed due to the following reason: 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 2) 'Best' failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 879.92/297.04 following reason: 879.92/297.04 879.92/297.04 The processor is inapplicable, reason: 879.92/297.04 Processor only applicable for innermost runtime complexity analysis 879.92/297.04 879.92/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 879.92/297.04 to the following reason: 879.92/297.04 879.92/297.04 The processor is inapplicable, reason: 879.92/297.04 Processor only applicable for innermost runtime complexity analysis 879.92/297.04 879.92/297.04 879.92/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 879.92/297.04 failed due to the following reason: 879.92/297.04 879.92/297.04 None of the processors succeeded. 879.92/297.04 879.92/297.04 Details of failed attempt(s): 879.92/297.04 ----------------------------- 879.92/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 879.92/297.04 failed due to the following reason: 879.92/297.04 879.92/297.04 match-boundness of the problem could not be verified. 879.92/297.04 879.92/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 879.92/297.04 failed due to the following reason: 879.92/297.04 879.92/297.04 match-boundness of the problem could not be verified. 879.92/297.04 879.92/297.04 879.92/297.04 879.92/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 879.92/297.04 the following reason: 879.92/297.04 879.92/297.04 We add the following weak dependency pairs: 879.92/297.04 879.92/297.04 Strict DPs: 879.92/297.04 { sort^#(nil()) -> c_1() 879.92/297.04 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y))) 879.92/297.04 , insert^#(x, nil()) -> c_3(x) 879.92/297.04 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 879.92/297.04 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w) 879.92/297.04 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w)) 879.92/297.04 , choose^#(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 c_7(choose^#(x, cons(v, w), y, z)) } 879.92/297.04 879.92/297.04 and mark the set of starting terms. 879.92/297.04 879.92/297.04 We are left with following problem, upon which TcT provides the 879.92/297.04 certificate MAYBE. 879.92/297.04 879.92/297.04 Strict DPs: 879.92/297.04 { sort^#(nil()) -> c_1() 879.92/297.04 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y))) 879.92/297.04 , insert^#(x, nil()) -> c_3(x) 879.92/297.04 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 879.92/297.04 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w) 879.92/297.04 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w)) 879.92/297.04 , choose^#(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 c_7(choose^#(x, cons(v, w), y, z)) } 879.92/297.04 Strict Trs: 879.92/297.04 { sort(nil()) -> nil() 879.92/297.04 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.04 , insert(x, nil()) -> cons(x, nil()) 879.92/297.04 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.04 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.04 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 879.92/297.04 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 choose(x, cons(v, w), y, z) } 879.92/297.04 Obligation: 879.92/297.04 runtime complexity 879.92/297.04 Answer: 879.92/297.04 MAYBE 879.92/297.04 879.92/297.04 We estimate the number of application of {1} by applications of 879.92/297.04 Pre({1}) = {3,5,6}. Here rules are labeled as follows: 879.92/297.04 879.92/297.04 DPs: 879.92/297.04 { 1: sort^#(nil()) -> c_1() 879.92/297.04 , 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y))) 879.92/297.04 , 3: insert^#(x, nil()) -> c_3(x) 879.92/297.04 , 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 879.92/297.04 , 5: choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w) 879.92/297.04 , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w)) 879.92/297.04 , 7: choose^#(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 c_7(choose^#(x, cons(v, w), y, z)) } 879.92/297.04 879.92/297.04 We are left with following problem, upon which TcT provides the 879.92/297.04 certificate MAYBE. 879.92/297.04 879.92/297.04 Strict DPs: 879.92/297.04 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y))) 879.92/297.04 , insert^#(x, nil()) -> c_3(x) 879.92/297.04 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 879.92/297.04 , choose^#(x, cons(v, w), y, 0()) -> c_5(x, v, w) 879.92/297.04 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(v, insert^#(x, w)) 879.92/297.04 , choose^#(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 c_7(choose^#(x, cons(v, w), y, z)) } 879.92/297.04 Strict Trs: 879.92/297.04 { sort(nil()) -> nil() 879.92/297.04 , sort(cons(x, y)) -> insert(x, sort(y)) 879.92/297.04 , insert(x, nil()) -> cons(x, nil()) 879.92/297.04 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 879.92/297.04 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 879.92/297.04 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 879.92/297.04 , choose(x, cons(v, w), s(y), s(z)) -> 879.92/297.04 choose(x, cons(v, w), y, z) } 879.92/297.04 Weak DPs: { sort^#(nil()) -> c_1() } 879.92/297.04 Obligation: 879.92/297.04 runtime complexity 879.92/297.04 Answer: 879.92/297.04 MAYBE 879.92/297.04 879.92/297.04 Empty strict component of the problem is NOT empty. 879.92/297.04 879.92/297.04 879.92/297.04 Arrrr.. 880.15/297.26 EOF