MAYBE 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, nil()) -> nil() 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'Best' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'Best' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 120.93/39.84 seconds)' failed due to the following reason: 120.93/39.84 120.93/39.84 The weightgap principle applies (using the following nonconstant 120.93/39.84 growth matrix-interpretation) 120.93/39.84 120.93/39.84 The following argument positions are usable: 120.93/39.84 Uargs(qsort) = {1}, Uargs(.) = {2}, Uargs(++) = {1, 2}, 120.93/39.84 Uargs(if) = {2, 3} 120.93/39.84 120.93/39.84 TcT has computed the following matrix interpretation satisfying 120.93/39.84 not(EDA) and not(IDA(1)). 120.93/39.84 120.93/39.84 [qsort](x1) = [1] x1 + [0] 120.93/39.84 120.93/39.84 [nil] = [1] 120.93/39.84 120.93/39.84 [.](x1, x2) = [1] x2 + [0] 120.93/39.84 120.93/39.84 [++](x1, x2) = [1] x1 + [1] x2 + [7] 120.93/39.84 120.93/39.84 [lowers](x1, x2) = [0] 120.93/39.84 120.93/39.84 [greaters](x1, x2) = [4] 120.93/39.84 120.93/39.84 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 120.93/39.84 120.93/39.84 [<=](x1, x2) = [0] 120.93/39.84 120.93/39.84 The order satisfies the following ordering constraints: 120.93/39.84 120.93/39.84 [qsort(nil())] = [1] 120.93/39.84 >= [1] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [qsort(.(x, y))] = [1] y + [0] 120.93/39.84 ? [11] 120.93/39.84 = [++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))] 120.93/39.84 120.93/39.84 [lowers(x, nil())] = [0] 120.93/39.84 ? [1] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [lowers(x, .(y, z))] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))] 120.93/39.84 120.93/39.84 [greaters(x, nil())] = [4] 120.93/39.84 > [1] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [greaters(x, .(y, z))] = [4] 120.93/39.84 ? [8] 120.93/39.84 = [if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))] 120.93/39.84 120.93/39.84 120.93/39.84 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Weak Trs: { greaters(x, nil()) -> nil() } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 The weightgap principle applies (using the following nonconstant 120.93/39.84 growth matrix-interpretation) 120.93/39.84 120.93/39.84 The following argument positions are usable: 120.93/39.84 Uargs(qsort) = {1}, Uargs(.) = {2}, Uargs(++) = {1, 2}, 120.93/39.84 Uargs(if) = {2, 3} 120.93/39.84 120.93/39.84 TcT has computed the following matrix interpretation satisfying 120.93/39.84 not(EDA) and not(IDA(1)). 120.93/39.84 120.93/39.84 [qsort](x1) = [1] x1 + [0] 120.93/39.84 120.93/39.84 [nil] = [0] 120.93/39.84 120.93/39.84 [.](x1, x2) = [1] x2 + [0] 120.93/39.84 120.93/39.84 [++](x1, x2) = [1] x1 + [1] x2 + [7] 120.93/39.84 120.93/39.84 [lowers](x1, x2) = [4] 120.93/39.84 120.93/39.84 [greaters](x1, x2) = [0] 120.93/39.84 120.93/39.84 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 120.93/39.84 120.93/39.84 [<=](x1, x2) = [0] 120.93/39.84 120.93/39.84 The order satisfies the following ordering constraints: 120.93/39.84 120.93/39.84 [qsort(nil())] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [qsort(.(x, y))] = [1] y + [0] 120.93/39.84 ? [11] 120.93/39.84 = [++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))] 120.93/39.84 120.93/39.84 [lowers(x, nil())] = [4] 120.93/39.84 > [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [lowers(x, .(y, z))] = [4] 120.93/39.84 ? [8] 120.93/39.84 = [if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))] 120.93/39.84 120.93/39.84 [greaters(x, nil())] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [greaters(x, .(y, z))] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))] 120.93/39.84 120.93/39.84 120.93/39.84 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Weak Trs: 120.93/39.84 { lowers(x, nil()) -> nil() 120.93/39.84 , greaters(x, nil()) -> nil() } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 The weightgap principle applies (using the following nonconstant 120.93/39.84 growth matrix-interpretation) 120.93/39.84 120.93/39.84 The following argument positions are usable: 120.93/39.84 Uargs(qsort) = {1}, Uargs(.) = {2}, Uargs(++) = {1, 2}, 120.93/39.84 Uargs(if) = {2, 3} 120.93/39.84 120.93/39.84 TcT has computed the following matrix interpretation satisfying 120.93/39.84 not(EDA) and not(IDA(1)). 120.93/39.84 120.93/39.84 [qsort](x1) = [1] x1 + [1] 120.93/39.84 120.93/39.84 [nil] = [0] 120.93/39.84 120.93/39.84 [.](x1, x2) = [1] x2 + [0] 120.93/39.84 120.93/39.84 [++](x1, x2) = [1] x1 + [1] x2 + [5] 120.93/39.84 120.93/39.84 [lowers](x1, x2) = [0] 120.93/39.84 120.93/39.84 [greaters](x1, x2) = [0] 120.93/39.84 120.93/39.84 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 120.93/39.84 120.93/39.84 [<=](x1, x2) = [0] 120.93/39.84 120.93/39.84 The order satisfies the following ordering constraints: 120.93/39.84 120.93/39.84 [qsort(nil())] = [1] 120.93/39.84 > [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [qsort(.(x, y))] = [1] y + [1] 120.93/39.84 ? [7] 120.93/39.84 = [++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))] 120.93/39.84 120.93/39.84 [lowers(x, nil())] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [lowers(x, .(y, z))] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))] 120.93/39.84 120.93/39.84 [greaters(x, nil())] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [greaters(x, .(y, z))] = [0] 120.93/39.84 >= [0] 120.93/39.84 = [if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))] 120.93/39.84 120.93/39.84 120.93/39.84 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict Trs: 120.93/39.84 { qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , greaters(x, nil()) -> nil() } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'Fastest' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 We use the processor 'matrix interpretation of dimension 2' to 120.93/39.84 orient following rules strictly. 120.93/39.84 120.93/39.84 Trs: 120.93/39.84 { qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) } 120.93/39.84 120.93/39.84 The induced complexity on above rules (modulo remaining rules) is 120.93/39.84 YES(?,O(n^1)) . These rules are moved into the corresponding weak 120.93/39.84 component(s). 120.93/39.84 120.93/39.84 Sub-proof: 120.93/39.84 ---------- 120.93/39.84 The following argument positions are usable: 120.93/39.84 Uargs(qsort) = {1}, Uargs(.) = {2}, Uargs(++) = {1, 2}, 120.93/39.84 Uargs(if) = {2, 3} 120.93/39.84 120.93/39.84 TcT has computed the following constructor-based matrix 120.93/39.84 interpretation satisfying not(EDA) and not(IDA(1)). 120.93/39.84 120.93/39.84 [qsort](x1) = [4 2] x1 + [0] 120.93/39.84 [0 1] [1] 120.93/39.84 120.93/39.84 [nil] = [0] 120.93/39.84 [0] 120.93/39.84 120.93/39.84 [.](x1, x2) = [1 0] x2 + [0] 120.93/39.84 [0 1] [5] 120.93/39.84 120.93/39.84 [++](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 120.93/39.84 [0 0] [0 0] [3] 120.93/39.84 120.93/39.84 [lowers](x1, x2) = [0] 120.93/39.84 [0] 120.93/39.84 120.93/39.84 [greaters](x1, x2) = [0] 120.93/39.84 [1] 120.93/39.84 120.93/39.84 [if](x1, x2, x3) = [1 0] x2 + [1 0] x3 + [0] 120.93/39.84 [0 0] [0 0] [0] 120.93/39.84 120.93/39.84 [<=](x1, x2) = [7] 120.93/39.84 [0] 120.93/39.84 120.93/39.84 The order satisfies the following ordering constraints: 120.93/39.84 120.93/39.84 [qsort(nil())] = [0] 120.93/39.84 [1] 120.93/39.84 >= [0] 120.93/39.84 [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [qsort(.(x, y))] = [4 2] y + [10] 120.93/39.84 [0 1] [6] 120.93/39.84 > [9] 120.93/39.84 [3] 120.93/39.84 = [++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))] 120.93/39.84 120.93/39.84 [lowers(x, nil())] = [0] 120.93/39.84 [0] 120.93/39.84 >= [0] 120.93/39.84 [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [lowers(x, .(y, z))] = [0] 120.93/39.84 [0] 120.93/39.84 >= [0] 120.93/39.84 [0] 120.93/39.84 = [if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))] 120.93/39.84 120.93/39.84 [greaters(x, nil())] = [0] 120.93/39.84 [1] 120.93/39.84 >= [0] 120.93/39.84 [0] 120.93/39.84 = [nil()] 120.93/39.84 120.93/39.84 [greaters(x, .(y, z))] = [0] 120.93/39.84 [1] 120.93/39.84 >= [0] 120.93/39.84 [0] 120.93/39.84 = [if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))] 120.93/39.84 120.93/39.84 120.93/39.84 We return to the main proof. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict Trs: 120.93/39.84 { lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , greaters(x, nil()) -> nil() } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'empty' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 2) 'With Problem ...' failed due to the following reason: 120.93/39.84 120.93/39.84 Empty strict component of the problem is NOT empty. 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 2) 'Best' failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 120.93/39.84 following reason: 120.93/39.84 120.93/39.84 The input cannot be shown compatible 120.93/39.84 120.93/39.84 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 120.93/39.84 to the following reason: 120.93/39.84 120.93/39.84 The input cannot be shown compatible 120.93/39.84 120.93/39.84 120.93/39.84 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 120.93/39.84 failed due to the following reason: 120.93/39.84 120.93/39.84 None of the processors succeeded. 120.93/39.84 120.93/39.84 Details of failed attempt(s): 120.93/39.84 ----------------------------- 120.93/39.84 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 120.93/39.84 failed due to the following reason: 120.93/39.84 120.93/39.84 match-boundness of the problem could not be verified. 120.93/39.84 120.93/39.84 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 120.93/39.84 failed due to the following reason: 120.93/39.84 120.93/39.84 match-boundness of the problem could not be verified. 120.93/39.84 120.93/39.84 120.93/39.84 120.93/39.84 2) 'With Problem ... (timeout of 297 seconds)' failed due to the 120.93/39.84 following reason: 120.93/39.84 120.93/39.84 We add the following dependency tuples: 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(nil()) -> c_1() 120.93/39.84 , qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) 120.93/39.84 , lowers^#(x, nil()) -> c_3() 120.93/39.84 , lowers^#(x, .(y, z)) -> c_4(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , greaters^#(x, nil()) -> c_5() 120.93/39.84 , greaters^#(x, .(y, z)) -> 120.93/39.84 c_6(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 120.93/39.84 and mark the set of starting terms. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(nil()) -> c_1() 120.93/39.84 , qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) 120.93/39.84 , lowers^#(x, nil()) -> c_3() 120.93/39.84 , lowers^#(x, .(y, z)) -> c_4(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , greaters^#(x, nil()) -> c_5() 120.93/39.84 , greaters^#(x, .(y, z)) -> 120.93/39.84 c_6(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, nil()) -> nil() 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 We estimate the number of application of {1,3,5} by applications of 120.93/39.84 Pre({1,3,5}) = {2,4,6}. Here rules are labeled as follows: 120.93/39.84 120.93/39.84 DPs: 120.93/39.84 { 1: qsort^#(nil()) -> c_1() 120.93/39.84 , 2: qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) 120.93/39.84 , 3: lowers^#(x, nil()) -> c_3() 120.93/39.84 , 4: lowers^#(x, .(y, z)) -> c_4(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , 5: greaters^#(x, nil()) -> c_5() 120.93/39.84 , 6: greaters^#(x, .(y, z)) -> 120.93/39.84 c_6(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) 120.93/39.84 , lowers^#(x, .(y, z)) -> c_4(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , greaters^#(x, .(y, z)) -> 120.93/39.84 c_6(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 Weak DPs: 120.93/39.84 { qsort^#(nil()) -> c_1() 120.93/39.84 , lowers^#(x, nil()) -> c_3() 120.93/39.84 , greaters^#(x, nil()) -> c_5() } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, nil()) -> nil() 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 The following weak DPs constitute a sub-graph of the DG that is 120.93/39.84 closed under successors. The DPs are removed. 120.93/39.84 120.93/39.84 { qsort^#(nil()) -> c_1() 120.93/39.84 , lowers^#(x, nil()) -> c_3() 120.93/39.84 , greaters^#(x, nil()) -> c_5() } 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) 120.93/39.84 , lowers^#(x, .(y, z)) -> c_4(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , greaters^#(x, .(y, z)) -> 120.93/39.84 c_6(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, nil()) -> nil() 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 Due to missing edges in the dependency-graph, the right-hand sides 120.93/39.84 of following rules could be simplified: 120.93/39.84 120.93/39.84 { qsort^#(.(x, y)) -> 120.93/39.84 c_2(qsort^#(lowers(x, y)), 120.93/39.84 lowers^#(x, y), 120.93/39.84 qsort^#(greaters(x, y)), 120.93/39.84 greaters^#(x, y)) } 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(.(x, y)) -> c_1(lowers^#(x, y), greaters^#(x, y)) 120.93/39.84 , lowers^#(x, .(y, z)) -> c_2(lowers^#(x, z), lowers^#(x, z)) 120.93/39.84 , greaters^#(x, .(y, z)) -> 120.93/39.84 c_3(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.84 Weak Trs: 120.93/39.84 { qsort(nil()) -> nil() 120.93/39.84 , qsort(.(x, y)) -> 120.93/39.84 ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 120.93/39.84 , lowers(x, nil()) -> nil() 120.93/39.84 , lowers(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 120.93/39.84 , greaters(x, nil()) -> nil() 120.93/39.84 , greaters(x, .(y, z)) -> 120.93/39.84 if(<=(y, x), greaters(x, z), .(y, greaters(x, z))) } 120.93/39.84 Obligation: 120.93/39.84 innermost runtime complexity 120.93/39.84 Answer: 120.93/39.84 MAYBE 120.93/39.84 120.93/39.84 No rule is usable, rules are removed from the input problem. 120.93/39.84 120.93/39.84 We are left with following problem, upon which TcT provides the 120.93/39.84 certificate MAYBE. 120.93/39.84 120.93/39.84 Strict DPs: 120.93/39.84 { qsort^#(.(x, y)) -> c_1(lowers^#(x, y), greaters^#(x, y)) 120.93/39.85 , lowers^#(x, .(y, z)) -> c_2(lowers^#(x, z), lowers^#(x, z)) 120.93/39.85 , greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.85 Obligation: 120.93/39.85 innermost runtime complexity 120.93/39.85 Answer: 120.93/39.85 MAYBE 120.93/39.85 120.93/39.85 Consider the dependency graph 120.93/39.85 120.93/39.85 1: qsort^#(.(x, y)) -> c_1(lowers^#(x, y), greaters^#(x, y)) 120.93/39.85 -->_2 greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) :3 120.93/39.85 -->_1 lowers^#(x, .(y, z)) -> 120.93/39.85 c_2(lowers^#(x, z), lowers^#(x, z)) :2 120.93/39.85 120.93/39.85 2: lowers^#(x, .(y, z)) -> c_2(lowers^#(x, z), lowers^#(x, z)) 120.93/39.85 -->_2 lowers^#(x, .(y, z)) -> 120.93/39.85 c_2(lowers^#(x, z), lowers^#(x, z)) :2 120.93/39.85 -->_1 lowers^#(x, .(y, z)) -> 120.93/39.85 c_2(lowers^#(x, z), lowers^#(x, z)) :2 120.93/39.85 120.93/39.85 3: greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) 120.93/39.85 -->_2 greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) :3 120.93/39.85 -->_1 greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) :3 120.93/39.85 120.93/39.85 120.93/39.85 Following roots of the dependency graph are removed, as the 120.93/39.85 considered set of starting terms is closed under reduction with 120.93/39.85 respect to these rules (modulo compound contexts). 120.93/39.85 120.93/39.85 { qsort^#(.(x, y)) -> c_1(lowers^#(x, y), greaters^#(x, y)) } 120.93/39.85 120.93/39.85 120.93/39.85 We are left with following problem, upon which TcT provides the 120.93/39.85 certificate MAYBE. 120.93/39.85 120.93/39.85 Strict DPs: 120.93/39.85 { lowers^#(x, .(y, z)) -> c_2(lowers^#(x, z), lowers^#(x, z)) 120.93/39.85 , greaters^#(x, .(y, z)) -> 120.93/39.85 c_3(greaters^#(x, z), greaters^#(x, z)) } 120.93/39.85 Obligation: 120.93/39.85 innermost runtime complexity 120.93/39.85 Answer: 120.93/39.85 MAYBE 120.93/39.85 120.93/39.85 None of the processors succeeded. 120.93/39.85 120.93/39.85 Details of failed attempt(s): 120.93/39.85 ----------------------------- 120.93/39.85 1) 'empty' failed due to the following reason: 120.93/39.85 120.93/39.85 Empty strict component of the problem is NOT empty. 120.93/39.85 120.93/39.85 2) 'With Problem ...' failed due to the following reason: 120.93/39.85 120.93/39.85 None of the processors succeeded. 120.93/39.85 120.93/39.85 Details of failed attempt(s): 120.93/39.85 ----------------------------- 120.93/39.85 1) 'empty' failed due to the following reason: 120.93/39.85 120.93/39.85 Empty strict component of the problem is NOT empty. 120.93/39.85 120.93/39.85 2) 'Fastest' failed due to the following reason: 120.93/39.85 120.93/39.85 None of the processors succeeded. 120.93/39.85 120.93/39.85 Details of failed attempt(s): 120.93/39.85 ----------------------------- 120.93/39.85 1) 'With Problem ...' failed due to the following reason: 120.93/39.85 120.93/39.85 None of the processors succeeded. 120.93/39.85 120.93/39.85 Details of failed attempt(s): 120.93/39.85 ----------------------------- 120.93/39.85 1) 'empty' failed due to the following reason: 120.93/39.85 120.93/39.85 Empty strict component of the problem is NOT empty. 120.93/39.85 120.93/39.85 2) 'Polynomial Path Order (PS)' failed due to the following reason: 120.93/39.85 120.93/39.85 The input cannot be shown compatible 120.93/39.85 120.93/39.85 120.93/39.85 2) 'Fastest (timeout of 24 seconds)' failed due to the following 120.93/39.85 reason: 120.93/39.85 120.93/39.85 None of the processors succeeded. 120.93/39.85 120.93/39.85 Details of failed attempt(s): 120.93/39.85 ----------------------------- 120.93/39.85 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 120.93/39.85 failed due to the following reason: 120.93/39.85 120.93/39.85 match-boundness of the problem could not be verified. 120.93/39.85 120.93/39.85 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 120.93/39.85 failed due to the following reason: 120.93/39.85 120.93/39.85 match-boundness of the problem could not be verified. 120.93/39.85 120.93/39.85 120.93/39.85 3) 'Polynomial Path Order (PS)' failed due to the following reason: 120.93/39.85 120.93/39.85 The input cannot be shown compatible 120.93/39.85 120.93/39.85 120.93/39.85 120.93/39.85 120.93/39.85 120.93/39.85 120.93/39.85 Arrrr.. 120.93/39.87 EOF