MAYBE
837.34/297.03	MAYBE
837.34/297.03	
837.34/297.03	We are left with following problem, upon which TcT provides the
837.34/297.03	certificate MAYBE.
837.34/297.03	
837.34/297.03	Strict Trs:
837.34/297.03	  { eq(0(), 0()) -> true()
837.34/297.03	  , eq(0(), s(x)) -> false()
837.34/297.03	  , eq(s(x), 0()) -> false()
837.34/297.03	  , eq(s(x), s(y)) -> eq(x, y)
837.34/297.03	  , le(0(), y) -> true()
837.34/297.03	  , le(s(x), 0()) -> false()
837.34/297.03	  , le(s(x), s(y)) -> le(x, y)
837.34/297.03	  , app(nil(), y) -> y
837.34/297.03	  , app(add(n, x), y) -> add(n, app(x, y))
837.34/297.03	  , min(nil()) -> 0()
837.34/297.03	  , min(add(n, x)) -> minIter(add(n, x), add(n, x), 0())
837.34/297.03	  , minIter(nil(), add(n, y), m) ->
837.34/297.03	    minIter(add(n, y), add(n, y), s(m))
837.34/297.03	  , minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m)
837.34/297.03	  , if_min(true(), x, y, m) -> m
837.34/297.03	  , if_min(false(), x, y, m) -> minIter(x, y, m)
837.34/297.03	  , head(add(n, x)) -> n
837.34/297.03	  , tail(nil()) -> nil()
837.34/297.03	  , tail(add(n, x)) -> x
837.34/297.03	  , null(nil()) -> true()
837.34/297.03	  , null(add(n, x)) -> false()
837.34/297.03	  , rm(n, nil()) -> nil()
837.34/297.03	  , rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
837.34/297.03	  , if_rm(true(), n, add(m, x)) -> rm(n, x)
837.34/297.03	  , if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
837.34/297.03	  , minsort(nil(), nil()) -> nil()
837.34/297.03	  , minsort(add(n, x), y) ->
837.34/297.03	    if_minsort(eq(n, min(add(n, x))), add(n, x), y)
837.34/297.03	  , if_minsort(true(), add(n, x), y) ->
837.34/297.03	    add(n, minsort(app(rm(n, x), y), nil()))
837.34/297.03	  , if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) }
837.34/297.03	Obligation:
837.34/297.03	  runtime complexity
837.34/297.03	Answer:
837.34/297.03	  MAYBE
837.34/297.03	
837.34/297.03	None of the processors succeeded.
837.34/297.03	
837.34/297.03	Details of failed attempt(s):
837.34/297.03	-----------------------------
837.34/297.03	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
837.34/297.03	   following reason:
837.34/297.03	   
837.34/297.03	   Computation stopped due to timeout after 297.0 seconds.
837.34/297.03	
837.34/297.03	2) 'Best' failed due to the following reason:
837.34/297.03	   
837.34/297.03	   None of the processors succeeded.
837.34/297.03	   
837.34/297.03	   Details of failed attempt(s):
837.34/297.03	   -----------------------------
837.34/297.03	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
837.34/297.03	      seconds)' failed due to the following reason:
837.34/297.03	      
837.34/297.03	      Computation stopped due to timeout after 148.0 seconds.
837.34/297.03	   
837.34/297.03	   2) 'Best' failed due to the following reason:
837.34/297.03	      
837.34/297.03	      None of the processors succeeded.
837.34/297.03	      
837.34/297.03	      Details of failed attempt(s):
837.34/297.03	      -----------------------------
837.34/297.03	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
837.34/297.03	         following reason:
837.34/297.03	         
837.34/297.03	         The processor is inapplicable, reason:
837.34/297.03	           Processor only applicable for innermost runtime complexity analysis
837.34/297.03	      
837.34/297.03	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
837.34/297.03	         to the following reason:
837.34/297.03	         
837.34/297.03	         The processor is inapplicable, reason:
837.34/297.03	           Processor only applicable for innermost runtime complexity analysis
837.34/297.03	      
837.34/297.03	   
837.34/297.03	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
837.34/297.03	      failed due to the following reason:
837.34/297.03	      
837.34/297.03	      None of the processors succeeded.
837.34/297.03	      
837.34/297.03	      Details of failed attempt(s):
837.34/297.03	      -----------------------------
837.34/297.03	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
837.34/297.03	         failed due to the following reason:
837.34/297.03	         
837.34/297.03	         match-boundness of the problem could not be verified.
837.34/297.03	      
837.34/297.03	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
837.34/297.03	         failed due to the following reason:
837.34/297.03	         
837.34/297.03	         match-boundness of the problem could not be verified.
837.34/297.03	      
837.34/297.03	   
837.34/297.03	
837.34/297.03	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
837.34/297.03	   the following reason:
837.34/297.03	   
837.34/297.03	   We add the following weak dependency pairs:
837.34/297.03	   
837.34/297.03	   Strict DPs:
837.34/297.03	     { eq^#(0(), 0()) -> c_1()
837.34/297.03	     , eq^#(0(), s(x)) -> c_2()
837.34/297.03	     , eq^#(s(x), 0()) -> c_3()
837.34/297.03	     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
837.34/297.03	     , le^#(0(), y) -> c_5()
837.34/297.03	     , le^#(s(x), 0()) -> c_6()
837.34/297.03	     , le^#(s(x), s(y)) -> c_7(le^#(x, y))
837.34/297.03	     , app^#(nil(), y) -> c_8(y)
837.34/297.03	     , app^#(add(n, x), y) -> c_9(n, app^#(x, y))
837.34/297.03	     , min^#(nil()) -> c_10()
837.34/297.03	     , min^#(add(n, x)) -> c_11(minIter^#(add(n, x), add(n, x), 0()))
837.34/297.03	     , minIter^#(nil(), add(n, y), m) ->
837.34/297.03	       c_12(minIter^#(add(n, y), add(n, y), s(m)))
837.34/297.03	     , minIter^#(add(n, x), y, m) -> c_13(if_min^#(le(n, m), x, y, m))
837.34/297.03	     , if_min^#(true(), x, y, m) -> c_14(m)
837.34/297.03	     , if_min^#(false(), x, y, m) -> c_15(minIter^#(x, y, m))
837.34/297.03	     , head^#(add(n, x)) -> c_16(n)
837.34/297.03	     , tail^#(nil()) -> c_17()
837.34/297.03	     , tail^#(add(n, x)) -> c_18(x)
837.34/297.03	     , null^#(nil()) -> c_19()
837.34/297.03	     , null^#(add(n, x)) -> c_20()
837.34/297.03	     , rm^#(n, nil()) -> c_21()
837.34/297.03	     , rm^#(n, add(m, x)) -> c_22(if_rm^#(eq(n, m), n, add(m, x)))
837.34/297.03	     , if_rm^#(true(), n, add(m, x)) -> c_23(rm^#(n, x))
837.34/297.03	     , if_rm^#(false(), n, add(m, x)) -> c_24(m, rm^#(n, x))
837.34/297.03	     , minsort^#(nil(), nil()) -> c_25()
837.34/297.03	     , minsort^#(add(n, x), y) ->
837.34/297.03	       c_26(if_minsort^#(eq(n, min(add(n, x))), add(n, x), y))
837.34/297.03	     , if_minsort^#(true(), add(n, x), y) ->
837.34/297.03	       c_27(n, minsort^#(app(rm(n, x), y), nil()))
837.34/297.03	     , if_minsort^#(false(), add(n, x), y) ->
837.34/297.03	       c_28(minsort^#(x, add(n, y))) }
837.34/297.03	   
837.34/297.03	   and mark the set of starting terms.
837.34/297.03	   
837.34/297.03	   We are left with following problem, upon which TcT provides the
837.34/297.03	   certificate MAYBE.
837.34/297.03	   
837.34/297.03	   Strict DPs:
837.34/297.03	     { eq^#(0(), 0()) -> c_1()
837.34/297.03	     , eq^#(0(), s(x)) -> c_2()
837.34/297.03	     , eq^#(s(x), 0()) -> c_3()
837.34/297.03	     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
837.34/297.03	     , le^#(0(), y) -> c_5()
837.34/297.03	     , le^#(s(x), 0()) -> c_6()
837.34/297.03	     , le^#(s(x), s(y)) -> c_7(le^#(x, y))
837.34/297.03	     , app^#(nil(), y) -> c_8(y)
837.34/297.03	     , app^#(add(n, x), y) -> c_9(n, app^#(x, y))
837.34/297.03	     , min^#(nil()) -> c_10()
837.34/297.03	     , min^#(add(n, x)) -> c_11(minIter^#(add(n, x), add(n, x), 0()))
837.34/297.03	     , minIter^#(nil(), add(n, y), m) ->
837.34/297.03	       c_12(minIter^#(add(n, y), add(n, y), s(m)))
837.34/297.03	     , minIter^#(add(n, x), y, m) -> c_13(if_min^#(le(n, m), x, y, m))
837.34/297.03	     , if_min^#(true(), x, y, m) -> c_14(m)
837.34/297.03	     , if_min^#(false(), x, y, m) -> c_15(minIter^#(x, y, m))
837.34/297.03	     , head^#(add(n, x)) -> c_16(n)
837.34/297.03	     , tail^#(nil()) -> c_17()
837.34/297.03	     , tail^#(add(n, x)) -> c_18(x)
837.34/297.03	     , null^#(nil()) -> c_19()
837.34/297.03	     , null^#(add(n, x)) -> c_20()
837.34/297.03	     , rm^#(n, nil()) -> c_21()
837.34/297.03	     , rm^#(n, add(m, x)) -> c_22(if_rm^#(eq(n, m), n, add(m, x)))
837.34/297.03	     , if_rm^#(true(), n, add(m, x)) -> c_23(rm^#(n, x))
837.34/297.03	     , if_rm^#(false(), n, add(m, x)) -> c_24(m, rm^#(n, x))
837.34/297.03	     , minsort^#(nil(), nil()) -> c_25()
837.34/297.03	     , minsort^#(add(n, x), y) ->
837.34/297.03	       c_26(if_minsort^#(eq(n, min(add(n, x))), add(n, x), y))
837.34/297.03	     , if_minsort^#(true(), add(n, x), y) ->
837.34/297.03	       c_27(n, minsort^#(app(rm(n, x), y), nil()))
837.34/297.03	     , if_minsort^#(false(), add(n, x), y) ->
837.34/297.03	       c_28(minsort^#(x, add(n, y))) }
837.34/297.03	   Strict Trs:
837.34/297.03	     { eq(0(), 0()) -> true()
837.34/297.03	     , eq(0(), s(x)) -> false()
837.34/297.03	     , eq(s(x), 0()) -> false()
837.34/297.03	     , eq(s(x), s(y)) -> eq(x, y)
837.34/297.03	     , le(0(), y) -> true()
837.34/297.03	     , le(s(x), 0()) -> false()
837.34/297.03	     , le(s(x), s(y)) -> le(x, y)
837.34/297.03	     , app(nil(), y) -> y
837.34/297.03	     , app(add(n, x), y) -> add(n, app(x, y))
837.34/297.03	     , min(nil()) -> 0()
837.34/297.03	     , min(add(n, x)) -> minIter(add(n, x), add(n, x), 0())
837.34/297.03	     , minIter(nil(), add(n, y), m) ->
837.34/297.03	       minIter(add(n, y), add(n, y), s(m))
837.34/297.03	     , minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m)
837.34/297.03	     , if_min(true(), x, y, m) -> m
837.34/297.03	     , if_min(false(), x, y, m) -> minIter(x, y, m)
837.34/297.03	     , head(add(n, x)) -> n
837.34/297.03	     , tail(nil()) -> nil()
837.34/297.03	     , tail(add(n, x)) -> x
837.34/297.03	     , null(nil()) -> true()
837.34/297.03	     , null(add(n, x)) -> false()
837.34/297.03	     , rm(n, nil()) -> nil()
837.34/297.03	     , rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
837.34/297.03	     , if_rm(true(), n, add(m, x)) -> rm(n, x)
837.34/297.03	     , if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
837.34/297.03	     , minsort(nil(), nil()) -> nil()
837.34/297.03	     , minsort(add(n, x), y) ->
837.34/297.03	       if_minsort(eq(n, min(add(n, x))), add(n, x), y)
837.34/297.03	     , if_minsort(true(), add(n, x), y) ->
837.34/297.03	       add(n, minsort(app(rm(n, x), y), nil()))
837.34/297.03	     , if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) }
837.34/297.03	   Obligation:
837.34/297.03	     runtime complexity
837.34/297.03	   Answer:
837.34/297.03	     MAYBE
837.34/297.03	   
837.34/297.03	   We estimate the number of application of
837.34/297.03	   {1,2,3,5,6,10,17,19,20,21,25} by applications of
837.34/297.03	   Pre({1,2,3,5,6,10,17,19,20,21,25}) = {4,7,8,9,14,16,18,23,24,27}.
837.34/297.03	   Here rules are labeled as follows:
837.34/297.03	   
837.34/297.03	     DPs:
837.34/297.03	       { 1: eq^#(0(), 0()) -> c_1()
837.34/297.03	       , 2: eq^#(0(), s(x)) -> c_2()
837.34/297.03	       , 3: eq^#(s(x), 0()) -> c_3()
837.34/297.03	       , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
837.34/297.03	       , 5: le^#(0(), y) -> c_5()
837.34/297.03	       , 6: le^#(s(x), 0()) -> c_6()
837.34/297.03	       , 7: le^#(s(x), s(y)) -> c_7(le^#(x, y))
837.34/297.04	       , 8: app^#(nil(), y) -> c_8(y)
837.34/297.04	       , 9: app^#(add(n, x), y) -> c_9(n, app^#(x, y))
837.34/297.04	       , 10: min^#(nil()) -> c_10()
837.34/297.04	       , 11: min^#(add(n, x)) ->
837.34/297.04	             c_11(minIter^#(add(n, x), add(n, x), 0()))
837.34/297.04	       , 12: minIter^#(nil(), add(n, y), m) ->
837.34/297.04	             c_12(minIter^#(add(n, y), add(n, y), s(m)))
837.34/297.04	       , 13: minIter^#(add(n, x), y, m) ->
837.34/297.04	             c_13(if_min^#(le(n, m), x, y, m))
837.34/297.04	       , 14: if_min^#(true(), x, y, m) -> c_14(m)
837.34/297.04	       , 15: if_min^#(false(), x, y, m) -> c_15(minIter^#(x, y, m))
837.34/297.04	       , 16: head^#(add(n, x)) -> c_16(n)
837.34/297.04	       , 17: tail^#(nil()) -> c_17()
837.34/297.04	       , 18: tail^#(add(n, x)) -> c_18(x)
837.34/297.04	       , 19: null^#(nil()) -> c_19()
837.34/297.04	       , 20: null^#(add(n, x)) -> c_20()
837.34/297.04	       , 21: rm^#(n, nil()) -> c_21()
837.34/297.04	       , 22: rm^#(n, add(m, x)) -> c_22(if_rm^#(eq(n, m), n, add(m, x)))
837.34/297.04	       , 23: if_rm^#(true(), n, add(m, x)) -> c_23(rm^#(n, x))
837.34/297.04	       , 24: if_rm^#(false(), n, add(m, x)) -> c_24(m, rm^#(n, x))
837.34/297.04	       , 25: minsort^#(nil(), nil()) -> c_25()
837.34/297.04	       , 26: minsort^#(add(n, x), y) ->
837.34/297.04	             c_26(if_minsort^#(eq(n, min(add(n, x))), add(n, x), y))
837.34/297.04	       , 27: if_minsort^#(true(), add(n, x), y) ->
837.34/297.04	             c_27(n, minsort^#(app(rm(n, x), y), nil()))
837.34/297.04	       , 28: if_minsort^#(false(), add(n, x), y) ->
837.34/297.04	             c_28(minsort^#(x, add(n, y))) }
837.34/297.04	   
837.34/297.04	   We are left with following problem, upon which TcT provides the
837.34/297.04	   certificate MAYBE.
837.34/297.04	   
837.34/297.04	   Strict DPs:
837.34/297.04	     { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
837.34/297.04	     , le^#(s(x), s(y)) -> c_7(le^#(x, y))
837.34/297.04	     , app^#(nil(), y) -> c_8(y)
837.34/297.04	     , app^#(add(n, x), y) -> c_9(n, app^#(x, y))
837.34/297.04	     , min^#(add(n, x)) -> c_11(minIter^#(add(n, x), add(n, x), 0()))
837.34/297.04	     , minIter^#(nil(), add(n, y), m) ->
837.34/297.04	       c_12(minIter^#(add(n, y), add(n, y), s(m)))
837.34/297.04	     , minIter^#(add(n, x), y, m) -> c_13(if_min^#(le(n, m), x, y, m))
837.34/297.04	     , if_min^#(true(), x, y, m) -> c_14(m)
837.34/297.04	     , if_min^#(false(), x, y, m) -> c_15(minIter^#(x, y, m))
837.34/297.04	     , head^#(add(n, x)) -> c_16(n)
837.34/297.04	     , tail^#(add(n, x)) -> c_18(x)
837.34/297.04	     , rm^#(n, add(m, x)) -> c_22(if_rm^#(eq(n, m), n, add(m, x)))
837.34/297.04	     , if_rm^#(true(), n, add(m, x)) -> c_23(rm^#(n, x))
837.34/297.04	     , if_rm^#(false(), n, add(m, x)) -> c_24(m, rm^#(n, x))
837.34/297.04	     , minsort^#(add(n, x), y) ->
837.34/297.04	       c_26(if_minsort^#(eq(n, min(add(n, x))), add(n, x), y))
837.34/297.04	     , if_minsort^#(true(), add(n, x), y) ->
837.34/297.04	       c_27(n, minsort^#(app(rm(n, x), y), nil()))
837.34/297.04	     , if_minsort^#(false(), add(n, x), y) ->
837.34/297.04	       c_28(minsort^#(x, add(n, y))) }
837.34/297.04	   Strict Trs:
837.34/297.04	     { eq(0(), 0()) -> true()
837.34/297.04	     , eq(0(), s(x)) -> false()
837.34/297.04	     , eq(s(x), 0()) -> false()
837.34/297.04	     , eq(s(x), s(y)) -> eq(x, y)
837.34/297.04	     , le(0(), y) -> true()
837.34/297.04	     , le(s(x), 0()) -> false()
837.34/297.04	     , le(s(x), s(y)) -> le(x, y)
837.34/297.04	     , app(nil(), y) -> y
837.34/297.04	     , app(add(n, x), y) -> add(n, app(x, y))
837.34/297.04	     , min(nil()) -> 0()
837.34/297.04	     , min(add(n, x)) -> minIter(add(n, x), add(n, x), 0())
837.34/297.04	     , minIter(nil(), add(n, y), m) ->
837.34/297.04	       minIter(add(n, y), add(n, y), s(m))
837.34/297.04	     , minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m)
837.34/297.04	     , if_min(true(), x, y, m) -> m
837.34/297.04	     , if_min(false(), x, y, m) -> minIter(x, y, m)
837.34/297.04	     , head(add(n, x)) -> n
837.34/297.04	     , tail(nil()) -> nil()
837.34/297.04	     , tail(add(n, x)) -> x
837.34/297.04	     , null(nil()) -> true()
837.34/297.04	     , null(add(n, x)) -> false()
837.34/297.04	     , rm(n, nil()) -> nil()
837.34/297.04	     , rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
837.34/297.04	     , if_rm(true(), n, add(m, x)) -> rm(n, x)
837.34/297.04	     , if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
837.34/297.04	     , minsort(nil(), nil()) -> nil()
837.34/297.04	     , minsort(add(n, x), y) ->
837.34/297.04	       if_minsort(eq(n, min(add(n, x))), add(n, x), y)
837.34/297.04	     , if_minsort(true(), add(n, x), y) ->
837.34/297.04	       add(n, minsort(app(rm(n, x), y), nil()))
837.34/297.04	     , if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) }
837.34/297.04	   Weak DPs:
837.34/297.04	     { eq^#(0(), 0()) -> c_1()
837.34/297.04	     , eq^#(0(), s(x)) -> c_2()
837.34/297.04	     , eq^#(s(x), 0()) -> c_3()
837.34/297.04	     , le^#(0(), y) -> c_5()
837.34/297.04	     , le^#(s(x), 0()) -> c_6()
837.34/297.04	     , min^#(nil()) -> c_10()
837.34/297.04	     , tail^#(nil()) -> c_17()
837.34/297.04	     , null^#(nil()) -> c_19()
837.34/297.04	     , null^#(add(n, x)) -> c_20()
837.34/297.04	     , rm^#(n, nil()) -> c_21()
837.34/297.04	     , minsort^#(nil(), nil()) -> c_25() }
837.34/297.04	   Obligation:
837.34/297.04	     runtime complexity
837.34/297.04	   Answer:
837.34/297.04	     MAYBE
837.34/297.04	   
837.34/297.04	   Empty strict component of the problem is NOT empty.
837.34/297.04	
837.34/297.04	
837.34/297.04	Arrrr..
837.46/297.18	EOF