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