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