MAYBE
859.58/297.03 MAYBE
859.58/297.03
859.58/297.03 We are left with following problem, upon which TcT provides the
859.58/297.03 certificate MAYBE.
859.58/297.03
859.58/297.03 Strict Trs:
859.58/297.03 { lt(0(), s(X)) -> true()
859.58/297.03 , lt(s(X), 0()) -> false()
859.58/297.03 , lt(s(X), s(Y)) -> lt(X, Y)
859.58/297.03 , append(nil(), Y) -> Y
859.58/297.03 , append(add(N, X), Y) -> add(N, append(X, Y))
859.58/297.03 , split(N, nil()) -> pair(nil(), nil())
859.58/297.03 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
859.58/297.03 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
859.58/297.03 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
859.58/297.03 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
859.58/297.03 , qsort(nil()) -> nil()
859.58/297.03 , qsort(add(N, X)) -> f_3(split(N, X), N, X)
859.58/297.03 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
859.58/297.03 Obligation:
859.58/297.03 runtime complexity
859.58/297.03 Answer:
859.58/297.03 MAYBE
859.58/297.03
859.58/297.03 None of the processors succeeded.
859.58/297.03
859.58/297.03 Details of failed attempt(s):
859.58/297.03 -----------------------------
859.58/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the
859.58/297.03 following reason:
859.58/297.03
859.58/297.03 Computation stopped due to timeout after 297.0 seconds.
859.58/297.03
859.58/297.03 2) 'Best' failed due to the following reason:
859.58/297.03
859.58/297.03 None of the processors succeeded.
859.58/297.03
859.58/297.03 Details of failed attempt(s):
859.58/297.03 -----------------------------
859.58/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
859.58/297.03 seconds)' failed due to the following reason:
859.58/297.03
859.58/297.03 Computation stopped due to timeout after 148.0 seconds.
859.58/297.03
859.58/297.03 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
859.58/297.03 failed due to the following reason:
859.58/297.03
859.58/297.03 None of the processors succeeded.
859.58/297.03
859.58/297.03 Details of failed attempt(s):
859.58/297.03 -----------------------------
859.58/297.03 1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
859.58/297.03 failed due to the following reason:
859.58/297.03
859.58/297.03 match-boundness of the problem could not be verified.
859.58/297.03
859.58/297.03 2) 'Bounds with minimal-enrichment and initial automaton 'match''
859.58/297.03 failed due to the following reason:
859.58/297.03
859.58/297.03 match-boundness of the problem could not be verified.
859.58/297.03
859.58/297.03
859.58/297.03 3) 'Best' failed due to the following reason:
859.58/297.03
859.58/297.03 None of the processors succeeded.
859.58/297.03
859.58/297.03 Details of failed attempt(s):
859.58/297.03 -----------------------------
859.58/297.03 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
859.58/297.03 to the following reason:
859.58/297.03
859.58/297.03 The processor is inapplicable, reason:
859.58/297.03 Processor only applicable for innermost runtime complexity analysis
859.58/297.03
859.58/297.03 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
859.58/297.03 following reason:
859.58/297.03
859.58/297.03 The processor is inapplicable, reason:
859.58/297.03 Processor only applicable for innermost runtime complexity analysis
859.58/297.03
859.58/297.03
859.58/297.03
859.58/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
859.58/297.03 the following reason:
859.58/297.03
859.58/297.03 We add the following weak dependency pairs:
859.58/297.03
859.58/297.03 Strict DPs:
859.58/297.03 { lt^#(0(), s(X)) -> c_1()
859.58/297.03 , lt^#(s(X), 0()) -> c_2()
859.58/297.03 , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
859.58/297.03 , append^#(nil(), Y) -> c_4(Y)
859.58/297.03 , append^#(add(N, X), Y) -> c_5(N, append^#(X, Y))
859.58/297.03 , split^#(N, nil()) -> c_6()
859.58/297.03 , split^#(N, add(M, Y)) -> c_7(f_1^#(split(N, Y), N, M, Y))
859.58/297.03 , f_1^#(pair(X, Z), N, M, Y) -> c_8(f_2^#(lt(N, M), N, M, Y, X, Z))
859.58/297.03 , f_2^#(true(), N, M, Y, X, Z) -> c_9(X, M, Z)
859.58/297.03 , f_2^#(false(), N, M, Y, X, Z) -> c_10(M, X, Z)
859.58/297.03 , qsort^#(nil()) -> c_11()
859.58/297.03 , qsort^#(add(N, X)) -> c_12(f_3^#(split(N, X), N, X))
859.58/297.03 , f_3^#(pair(Y, Z), N, X) ->
859.58/297.03 c_13(append^#(qsort(Y), add(X, qsort(Z)))) }
859.58/297.03
859.58/297.03 and mark the set of starting terms.
859.58/297.03
859.58/297.03 We are left with following problem, upon which TcT provides the
859.58/297.03 certificate MAYBE.
859.58/297.03
859.58/297.03 Strict DPs:
859.58/297.03 { lt^#(0(), s(X)) -> c_1()
859.58/297.03 , lt^#(s(X), 0()) -> c_2()
859.58/297.03 , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
859.58/297.03 , append^#(nil(), Y) -> c_4(Y)
859.58/297.03 , append^#(add(N, X), Y) -> c_5(N, append^#(X, Y))
859.58/297.03 , split^#(N, nil()) -> c_6()
859.58/297.03 , split^#(N, add(M, Y)) -> c_7(f_1^#(split(N, Y), N, M, Y))
859.58/297.03 , f_1^#(pair(X, Z), N, M, Y) -> c_8(f_2^#(lt(N, M), N, M, Y, X, Z))
859.58/297.03 , f_2^#(true(), N, M, Y, X, Z) -> c_9(X, M, Z)
859.58/297.03 , f_2^#(false(), N, M, Y, X, Z) -> c_10(M, X, Z)
859.58/297.03 , qsort^#(nil()) -> c_11()
859.58/297.03 , qsort^#(add(N, X)) -> c_12(f_3^#(split(N, X), N, X))
859.58/297.03 , f_3^#(pair(Y, Z), N, X) ->
859.58/297.03 c_13(append^#(qsort(Y), add(X, qsort(Z)))) }
859.58/297.03 Strict Trs:
859.58/297.03 { lt(0(), s(X)) -> true()
859.58/297.03 , lt(s(X), 0()) -> false()
859.58/297.03 , lt(s(X), s(Y)) -> lt(X, Y)
859.58/297.03 , append(nil(), Y) -> Y
859.58/297.03 , append(add(N, X), Y) -> add(N, append(X, Y))
859.58/297.03 , split(N, nil()) -> pair(nil(), nil())
859.58/297.03 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
859.58/297.03 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
859.58/297.03 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
859.58/297.03 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
859.58/297.03 , qsort(nil()) -> nil()
859.58/297.03 , qsort(add(N, X)) -> f_3(split(N, X), N, X)
859.58/297.03 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
859.58/297.03 Obligation:
859.58/297.03 runtime complexity
859.58/297.03 Answer:
859.58/297.03 MAYBE
859.58/297.03
859.58/297.03 We estimate the number of application of {1,2,6,11} by applications
859.58/297.03 of Pre({1,2,6,11}) = {3,4,5,9,10}. Here rules are labeled as
859.58/297.03 follows:
859.58/297.03
859.58/297.03 DPs:
859.58/297.03 { 1: lt^#(0(), s(X)) -> c_1()
859.58/297.03 , 2: lt^#(s(X), 0()) -> c_2()
859.58/297.03 , 3: lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
859.58/297.03 , 4: append^#(nil(), Y) -> c_4(Y)
859.58/297.03 , 5: append^#(add(N, X), Y) -> c_5(N, append^#(X, Y))
859.58/297.03 , 6: split^#(N, nil()) -> c_6()
859.58/297.03 , 7: split^#(N, add(M, Y)) -> c_7(f_1^#(split(N, Y), N, M, Y))
859.58/297.03 , 8: f_1^#(pair(X, Z), N, M, Y) ->
859.58/297.03 c_8(f_2^#(lt(N, M), N, M, Y, X, Z))
859.58/297.03 , 9: f_2^#(true(), N, M, Y, X, Z) -> c_9(X, M, Z)
859.58/297.03 , 10: f_2^#(false(), N, M, Y, X, Z) -> c_10(M, X, Z)
859.58/297.03 , 11: qsort^#(nil()) -> c_11()
859.58/297.03 , 12: qsort^#(add(N, X)) -> c_12(f_3^#(split(N, X), N, X))
859.58/297.03 , 13: f_3^#(pair(Y, Z), N, X) ->
859.58/297.03 c_13(append^#(qsort(Y), add(X, qsort(Z)))) }
859.58/297.03
859.58/297.03 We are left with following problem, upon which TcT provides the
859.58/297.03 certificate MAYBE.
859.58/297.03
859.58/297.03 Strict DPs:
859.58/297.03 { lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
859.58/297.03 , append^#(nil(), Y) -> c_4(Y)
859.58/297.03 , append^#(add(N, X), Y) -> c_5(N, append^#(X, Y))
859.58/297.03 , split^#(N, add(M, Y)) -> c_7(f_1^#(split(N, Y), N, M, Y))
859.58/297.03 , f_1^#(pair(X, Z), N, M, Y) -> c_8(f_2^#(lt(N, M), N, M, Y, X, Z))
859.58/297.03 , f_2^#(true(), N, M, Y, X, Z) -> c_9(X, M, Z)
859.58/297.03 , f_2^#(false(), N, M, Y, X, Z) -> c_10(M, X, Z)
859.58/297.03 , qsort^#(add(N, X)) -> c_12(f_3^#(split(N, X), N, X))
859.58/297.03 , f_3^#(pair(Y, Z), N, X) ->
859.58/297.03 c_13(append^#(qsort(Y), add(X, qsort(Z)))) }
859.58/297.03 Strict Trs:
859.58/297.03 { lt(0(), s(X)) -> true()
859.58/297.03 , lt(s(X), 0()) -> false()
859.58/297.03 , lt(s(X), s(Y)) -> lt(X, Y)
859.58/297.03 , append(nil(), Y) -> Y
859.58/297.03 , append(add(N, X), Y) -> add(N, append(X, Y))
859.58/297.03 , split(N, nil()) -> pair(nil(), nil())
859.58/297.03 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
859.58/297.03 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
859.58/297.03 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
859.58/297.03 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
859.58/297.03 , qsort(nil()) -> nil()
859.58/297.03 , qsort(add(N, X)) -> f_3(split(N, X), N, X)
859.58/297.03 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
859.58/297.03 Weak DPs:
859.58/297.03 { lt^#(0(), s(X)) -> c_1()
859.58/297.03 , lt^#(s(X), 0()) -> c_2()
859.58/297.03 , split^#(N, nil()) -> c_6()
859.58/297.03 , qsort^#(nil()) -> c_11() }
859.58/297.03 Obligation:
859.58/297.03 runtime complexity
859.58/297.03 Answer:
859.58/297.03 MAYBE
859.58/297.03
859.58/297.03 Empty strict component of the problem is NOT empty.
859.58/297.03
859.58/297.03
859.58/297.03 Arrrr..
859.69/297.19 EOF