MAYBE
1073.38/297.05	MAYBE
1073.38/297.05	
1073.38/297.05	We are left with following problem, upon which TcT provides the
1073.38/297.05	certificate MAYBE.
1073.38/297.05	
1073.38/297.05	Strict Trs:
1073.38/297.05	  { active(dbl(X)) -> dbl(active(X))
1073.38/297.05	  , active(dbl(0())) -> mark(0())
1073.38/297.05	  , active(dbl(s(X))) -> mark(s(s(dbl(X))))
1073.38/297.05	  , active(dbls(X)) -> dbls(active(X))
1073.38/297.05	  , active(dbls(nil())) -> mark(nil())
1073.38/297.05	  , active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y)))
1073.38/297.05	  , active(sel(X1, X2)) -> sel(X1, active(X2))
1073.38/297.05	  , active(sel(X1, X2)) -> sel(active(X1), X2)
1073.38/297.05	  , active(sel(0(), cons(X, Y))) -> mark(X)
1073.38/297.05	  , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z))
1073.38/297.05	  , active(indx(X1, X2)) -> indx(active(X1), X2)
1073.38/297.05	  , active(indx(nil(), X)) -> mark(nil())
1073.38/297.05	  , active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z)))
1073.38/297.05	  , active(from(X)) -> mark(cons(X, from(s(X))))
1073.38/297.05	  , dbl(mark(X)) -> mark(dbl(X))
1073.38/297.05	  , dbl(ok(X)) -> ok(dbl(X))
1073.38/297.05	  , s(ok(X)) -> ok(s(X))
1073.38/297.05	  , dbls(mark(X)) -> mark(dbls(X))
1073.38/297.05	  , dbls(ok(X)) -> ok(dbls(X))
1073.38/297.05	  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
1073.38/297.05	  , sel(X1, mark(X2)) -> mark(sel(X1, X2))
1073.38/297.05	  , sel(mark(X1), X2) -> mark(sel(X1, X2))
1073.38/297.05	  , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2))
1073.38/297.05	  , indx(mark(X1), X2) -> mark(indx(X1, X2))
1073.38/297.05	  , indx(ok(X1), ok(X2)) -> ok(indx(X1, X2))
1073.38/297.05	  , from(ok(X)) -> ok(from(X))
1073.38/297.05	  , proper(dbl(X)) -> dbl(proper(X))
1073.38/297.05	  , proper(0()) -> ok(0())
1073.38/297.05	  , proper(s(X)) -> s(proper(X))
1073.38/297.05	  , proper(dbls(X)) -> dbls(proper(X))
1073.38/297.05	  , proper(nil()) -> ok(nil())
1073.38/297.05	  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
1073.38/297.05	  , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
1073.38/297.05	  , proper(indx(X1, X2)) -> indx(proper(X1), proper(X2))
1073.38/297.05	  , proper(from(X)) -> from(proper(X))
1073.38/297.05	  , top(mark(X)) -> top(proper(X))
1073.38/297.05	  , top(ok(X)) -> top(active(X)) }
1073.38/297.05	Obligation:
1073.38/297.05	  runtime complexity
1073.38/297.05	Answer:
1073.38/297.05	  MAYBE
1073.38/297.05	
1073.38/297.05	None of the processors succeeded.
1073.38/297.05	
1073.38/297.05	Details of failed attempt(s):
1073.38/297.05	-----------------------------
1073.38/297.05	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1073.38/297.05	   following reason:
1073.38/297.05	   
1073.38/297.05	   Computation stopped due to timeout after 297.0 seconds.
1073.38/297.05	
1073.38/297.05	2) 'Best' failed due to the following reason:
1073.38/297.05	   
1073.38/297.05	   None of the processors succeeded.
1073.38/297.05	   
1073.38/297.05	   Details of failed attempt(s):
1073.38/297.05	   -----------------------------
1073.38/297.05	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1073.38/297.05	      seconds)' failed due to the following reason:
1073.38/297.05	      
1073.38/297.05	      Computation stopped due to timeout after 148.0 seconds.
1073.38/297.05	   
1073.38/297.05	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1073.38/297.05	      failed due to the following reason:
1073.38/297.05	      
1073.38/297.05	      None of the processors succeeded.
1073.38/297.05	      
1073.38/297.05	      Details of failed attempt(s):
1073.38/297.05	      -----------------------------
1073.38/297.05	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
1073.38/297.05	         failed due to the following reason:
1073.38/297.05	         
1073.38/297.05	         match-boundness of the problem could not be verified.
1073.38/297.05	      
1073.38/297.05	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1073.38/297.05	         failed due to the following reason:
1073.38/297.05	         
1073.38/297.05	         match-boundness of the problem could not be verified.
1073.38/297.05	      
1073.38/297.05	   
1073.38/297.05	   3) 'Best' failed due to the following reason:
1073.38/297.05	      
1073.38/297.05	      None of the processors succeeded.
1073.38/297.05	      
1073.38/297.05	      Details of failed attempt(s):
1073.38/297.05	      -----------------------------
1073.38/297.05	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1073.38/297.05	         following reason:
1073.38/297.05	         
1073.38/297.05	         The processor is inapplicable, reason:
1073.38/297.05	           Processor only applicable for innermost runtime complexity analysis
1073.38/297.05	      
1073.38/297.05	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1073.38/297.05	         to the following reason:
1073.38/297.05	         
1073.38/297.05	         The processor is inapplicable, reason:
1073.38/297.05	           Processor only applicable for innermost runtime complexity analysis
1073.38/297.05	      
1073.38/297.05	   
1073.38/297.05	
1073.38/297.05	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
1073.38/297.05	   the following reason:
1073.38/297.05	   
1073.38/297.05	   We add the following weak dependency pairs:
1073.38/297.05	   
1073.38/297.05	   Strict DPs:
1073.38/297.05	     { active^#(dbl(X)) -> c_1(dbl^#(active(X)))
1073.38/297.05	     , active^#(dbl(0())) -> c_2()
1073.38/297.05	     , active^#(dbl(s(X))) -> c_3(s^#(s(dbl(X))))
1073.38/297.05	     , active^#(dbls(X)) -> c_4(dbls^#(active(X)))
1073.38/297.05	     , active^#(dbls(nil())) -> c_5()
1073.38/297.05	     , active^#(dbls(cons(X, Y))) -> c_6(cons^#(dbl(X), dbls(Y)))
1073.38/297.05	     , active^#(sel(X1, X2)) -> c_7(sel^#(X1, active(X2)))
1073.38/297.05	     , active^#(sel(X1, X2)) -> c_8(sel^#(active(X1), X2))
1073.38/297.05	     , active^#(sel(0(), cons(X, Y))) -> c_9(X)
1073.38/297.05	     , active^#(sel(s(X), cons(Y, Z))) -> c_10(sel^#(X, Z))
1073.38/297.05	     , active^#(indx(X1, X2)) -> c_11(indx^#(active(X1), X2))
1073.38/297.05	     , active^#(indx(nil(), X)) -> c_12()
1073.38/297.05	     , active^#(indx(cons(X, Y), Z)) ->
1073.38/297.05	       c_13(cons^#(sel(X, Z), indx(Y, Z)))
1073.38/297.05	     , active^#(from(X)) -> c_14(cons^#(X, from(s(X))))
1073.38/297.05	     , dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.05	     , dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.05	     , s^#(ok(X)) -> c_17(s^#(X))
1073.38/297.05	     , dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.05	     , dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.05	     , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.05	     , sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.05	     , sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.05	     , sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.05	     , indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.05	     , indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.05	     , from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.05	     , proper^#(dbl(X)) -> c_27(dbl^#(proper(X)))
1073.38/297.05	     , proper^#(0()) -> c_28()
1073.38/297.05	     , proper^#(s(X)) -> c_29(s^#(proper(X)))
1073.38/297.05	     , proper^#(dbls(X)) -> c_30(dbls^#(proper(X)))
1073.38/297.05	     , proper^#(nil()) -> c_31()
1073.38/297.05	     , proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(sel(X1, X2)) -> c_33(sel^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(indx(X1, X2)) -> c_34(indx^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(from(X)) -> c_35(from^#(proper(X)))
1073.38/297.05	     , top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.05	     , top^#(ok(X)) -> c_37(top^#(active(X))) }
1073.38/297.05	   
1073.38/297.05	   and mark the set of starting terms.
1073.38/297.05	   
1073.38/297.05	   We are left with following problem, upon which TcT provides the
1073.38/297.05	   certificate MAYBE.
1073.38/297.05	   
1073.38/297.05	   Strict DPs:
1073.38/297.05	     { active^#(dbl(X)) -> c_1(dbl^#(active(X)))
1073.38/297.05	     , active^#(dbl(0())) -> c_2()
1073.38/297.05	     , active^#(dbl(s(X))) -> c_3(s^#(s(dbl(X))))
1073.38/297.05	     , active^#(dbls(X)) -> c_4(dbls^#(active(X)))
1073.38/297.05	     , active^#(dbls(nil())) -> c_5()
1073.38/297.05	     , active^#(dbls(cons(X, Y))) -> c_6(cons^#(dbl(X), dbls(Y)))
1073.38/297.05	     , active^#(sel(X1, X2)) -> c_7(sel^#(X1, active(X2)))
1073.38/297.05	     , active^#(sel(X1, X2)) -> c_8(sel^#(active(X1), X2))
1073.38/297.05	     , active^#(sel(0(), cons(X, Y))) -> c_9(X)
1073.38/297.05	     , active^#(sel(s(X), cons(Y, Z))) -> c_10(sel^#(X, Z))
1073.38/297.05	     , active^#(indx(X1, X2)) -> c_11(indx^#(active(X1), X2))
1073.38/297.05	     , active^#(indx(nil(), X)) -> c_12()
1073.38/297.05	     , active^#(indx(cons(X, Y), Z)) ->
1073.38/297.05	       c_13(cons^#(sel(X, Z), indx(Y, Z)))
1073.38/297.05	     , active^#(from(X)) -> c_14(cons^#(X, from(s(X))))
1073.38/297.05	     , dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.05	     , dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.05	     , s^#(ok(X)) -> c_17(s^#(X))
1073.38/297.05	     , dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.05	     , dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.05	     , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.05	     , sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.05	     , sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.05	     , sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.05	     , indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.05	     , indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.05	     , from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.05	     , proper^#(dbl(X)) -> c_27(dbl^#(proper(X)))
1073.38/297.05	     , proper^#(0()) -> c_28()
1073.38/297.05	     , proper^#(s(X)) -> c_29(s^#(proper(X)))
1073.38/297.05	     , proper^#(dbls(X)) -> c_30(dbls^#(proper(X)))
1073.38/297.05	     , proper^#(nil()) -> c_31()
1073.38/297.05	     , proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(sel(X1, X2)) -> c_33(sel^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(indx(X1, X2)) -> c_34(indx^#(proper(X1), proper(X2)))
1073.38/297.05	     , proper^#(from(X)) -> c_35(from^#(proper(X)))
1073.38/297.05	     , top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.05	     , top^#(ok(X)) -> c_37(top^#(active(X))) }
1073.38/297.05	   Strict Trs:
1073.38/297.05	     { active(dbl(X)) -> dbl(active(X))
1073.38/297.05	     , active(dbl(0())) -> mark(0())
1073.38/297.05	     , active(dbl(s(X))) -> mark(s(s(dbl(X))))
1073.38/297.05	     , active(dbls(X)) -> dbls(active(X))
1073.38/297.05	     , active(dbls(nil())) -> mark(nil())
1073.38/297.05	     , active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y)))
1073.38/297.05	     , active(sel(X1, X2)) -> sel(X1, active(X2))
1073.38/297.05	     , active(sel(X1, X2)) -> sel(active(X1), X2)
1073.38/297.05	     , active(sel(0(), cons(X, Y))) -> mark(X)
1073.38/297.05	     , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z))
1073.38/297.06	     , active(indx(X1, X2)) -> indx(active(X1), X2)
1073.38/297.06	     , active(indx(nil(), X)) -> mark(nil())
1073.38/297.06	     , active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z)))
1073.38/297.06	     , active(from(X)) -> mark(cons(X, from(s(X))))
1073.38/297.06	     , dbl(mark(X)) -> mark(dbl(X))
1073.38/297.06	     , dbl(ok(X)) -> ok(dbl(X))
1073.38/297.06	     , s(ok(X)) -> ok(s(X))
1073.38/297.06	     , dbls(mark(X)) -> mark(dbls(X))
1073.38/297.06	     , dbls(ok(X)) -> ok(dbls(X))
1073.38/297.06	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
1073.38/297.06	     , sel(X1, mark(X2)) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(mark(X1), X2) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2))
1073.38/297.06	     , indx(mark(X1), X2) -> mark(indx(X1, X2))
1073.38/297.06	     , indx(ok(X1), ok(X2)) -> ok(indx(X1, X2))
1073.38/297.06	     , from(ok(X)) -> ok(from(X))
1073.38/297.06	     , proper(dbl(X)) -> dbl(proper(X))
1073.38/297.06	     , proper(0()) -> ok(0())
1073.38/297.06	     , proper(s(X)) -> s(proper(X))
1073.38/297.06	     , proper(dbls(X)) -> dbls(proper(X))
1073.38/297.06	     , proper(nil()) -> ok(nil())
1073.38/297.06	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
1073.38/297.06	     , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
1073.38/297.06	     , proper(indx(X1, X2)) -> indx(proper(X1), proper(X2))
1073.38/297.06	     , proper(from(X)) -> from(proper(X))
1073.38/297.06	     , top(mark(X)) -> top(proper(X))
1073.38/297.06	     , top(ok(X)) -> top(active(X)) }
1073.38/297.06	   Obligation:
1073.38/297.06	     runtime complexity
1073.38/297.06	   Answer:
1073.38/297.06	     MAYBE
1073.38/297.06	   
1073.38/297.06	   Consider the dependency graph:
1073.38/297.06	   
1073.38/297.06	     1: active^#(dbl(X)) -> c_1(dbl^#(active(X)))
1073.38/297.06	        -->_1 dbl^#(ok(X)) -> c_16(dbl^#(X)) :16
1073.38/297.06	        -->_1 dbl^#(mark(X)) -> c_15(dbl^#(X)) :15
1073.38/297.06	     
1073.38/297.06	     2: active^#(dbl(0())) -> c_2()
1073.38/297.06	     
1073.38/297.06	     3: active^#(dbl(s(X))) -> c_3(s^#(s(dbl(X))))
1073.38/297.06	        -->_1 s^#(ok(X)) -> c_17(s^#(X)) :17
1073.38/297.06	     
1073.38/297.06	     4: active^#(dbls(X)) -> c_4(dbls^#(active(X)))
1073.38/297.06	        -->_1 dbls^#(ok(X)) -> c_19(dbls^#(X)) :19
1073.38/297.06	        -->_1 dbls^#(mark(X)) -> c_18(dbls^#(X)) :18
1073.38/297.06	     
1073.38/297.06	     5: active^#(dbls(nil())) -> c_5()
1073.38/297.06	     
1073.38/297.06	     6: active^#(dbls(cons(X, Y))) -> c_6(cons^#(dbl(X), dbls(Y)))
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	     
1073.38/297.06	     7: active^#(sel(X1, X2)) -> c_7(sel^#(X1, active(X2)))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     8: active^#(sel(X1, X2)) -> c_8(sel^#(active(X1), X2))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     9: active^#(sel(0(), cons(X, Y))) -> c_9(X)
1073.38/297.06	        -->_1 top^#(ok(X)) -> c_37(top^#(active(X))) :37
1073.38/297.06	        -->_1 top^#(mark(X)) -> c_36(top^#(proper(X))) :36
1073.38/297.06	        -->_1 proper^#(from(X)) -> c_35(from^#(proper(X))) :35
1073.38/297.06	        -->_1 proper^#(indx(X1, X2)) ->
1073.38/297.06	              c_34(indx^#(proper(X1), proper(X2))) :34
1073.38/297.06	        -->_1 proper^#(sel(X1, X2)) ->
1073.38/297.06	              c_33(sel^#(proper(X1), proper(X2))) :33
1073.38/297.06	        -->_1 proper^#(cons(X1, X2)) ->
1073.38/297.06	              c_32(cons^#(proper(X1), proper(X2))) :32
1073.38/297.06	        -->_1 proper^#(dbls(X)) -> c_30(dbls^#(proper(X))) :30
1073.38/297.06	        -->_1 proper^#(s(X)) -> c_29(s^#(proper(X))) :29
1073.38/297.06	        -->_1 proper^#(dbl(X)) -> c_27(dbl^#(proper(X))) :27
1073.38/297.06	        -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26
1073.38/297.06	        -->_1 indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2)) :25
1073.38/297.06	        -->_1 indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2)) :24
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	        -->_1 dbls^#(ok(X)) -> c_19(dbls^#(X)) :19
1073.38/297.06	        -->_1 dbls^#(mark(X)) -> c_18(dbls^#(X)) :18
1073.38/297.06	        -->_1 s^#(ok(X)) -> c_17(s^#(X)) :17
1073.38/297.06	        -->_1 dbl^#(ok(X)) -> c_16(dbl^#(X)) :16
1073.38/297.06	        -->_1 dbl^#(mark(X)) -> c_15(dbl^#(X)) :15
1073.38/297.06	        -->_1 active^#(from(X)) -> c_14(cons^#(X, from(s(X)))) :14
1073.38/297.06	        -->_1 active^#(indx(cons(X, Y), Z)) ->
1073.38/297.06	              c_13(cons^#(sel(X, Z), indx(Y, Z))) :13
1073.38/297.06	        -->_1 active^#(indx(X1, X2)) -> c_11(indx^#(active(X1), X2)) :11
1073.38/297.06	        -->_1 active^#(sel(s(X), cons(Y, Z))) -> c_10(sel^#(X, Z)) :10
1073.38/297.06	        -->_1 proper^#(nil()) -> c_31() :31
1073.38/297.06	        -->_1 proper^#(0()) -> c_28() :28
1073.38/297.06	        -->_1 active^#(indx(nil(), X)) -> c_12() :12
1073.38/297.06	        -->_1 active^#(sel(0(), cons(X, Y))) -> c_9(X) :9
1073.38/297.06	        -->_1 active^#(sel(X1, X2)) -> c_8(sel^#(active(X1), X2)) :8
1073.38/297.06	        -->_1 active^#(sel(X1, X2)) -> c_7(sel^#(X1, active(X2))) :7
1073.38/297.06	        -->_1 active^#(dbls(cons(X, Y))) -> c_6(cons^#(dbl(X), dbls(Y))) :6
1073.38/297.06	        -->_1 active^#(dbls(nil())) -> c_5() :5
1073.38/297.06	        -->_1 active^#(dbls(X)) -> c_4(dbls^#(active(X))) :4
1073.38/297.06	        -->_1 active^#(dbl(s(X))) -> c_3(s^#(s(dbl(X)))) :3
1073.38/297.06	        -->_1 active^#(dbl(0())) -> c_2() :2
1073.38/297.06	        -->_1 active^#(dbl(X)) -> c_1(dbl^#(active(X))) :1
1073.38/297.06	     
1073.38/297.06	     10: active^#(sel(s(X), cons(Y, Z))) -> c_10(sel^#(X, Z))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     11: active^#(indx(X1, X2)) -> c_11(indx^#(active(X1), X2))
1073.38/297.06	        -->_1 indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2)) :25
1073.38/297.06	        -->_1 indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2)) :24
1073.38/297.06	     
1073.38/297.06	     12: active^#(indx(nil(), X)) -> c_12()
1073.38/297.06	     
1073.38/297.06	     13: active^#(indx(cons(X, Y), Z)) ->
1073.38/297.06	         c_13(cons^#(sel(X, Z), indx(Y, Z)))
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	     
1073.38/297.06	     14: active^#(from(X)) -> c_14(cons^#(X, from(s(X))))
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	     
1073.38/297.06	     15: dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.06	        -->_1 dbl^#(ok(X)) -> c_16(dbl^#(X)) :16
1073.38/297.06	        -->_1 dbl^#(mark(X)) -> c_15(dbl^#(X)) :15
1073.38/297.06	     
1073.38/297.06	     16: dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.06	        -->_1 dbl^#(ok(X)) -> c_16(dbl^#(X)) :16
1073.38/297.06	        -->_1 dbl^#(mark(X)) -> c_15(dbl^#(X)) :15
1073.38/297.06	     
1073.38/297.06	     17: s^#(ok(X)) -> c_17(s^#(X)) -->_1 s^#(ok(X)) -> c_17(s^#(X)) :17
1073.38/297.06	     
1073.38/297.06	     18: dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.06	        -->_1 dbls^#(ok(X)) -> c_19(dbls^#(X)) :19
1073.38/297.06	        -->_1 dbls^#(mark(X)) -> c_18(dbls^#(X)) :18
1073.38/297.06	     
1073.38/297.06	     19: dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.06	        -->_1 dbls^#(ok(X)) -> c_19(dbls^#(X)) :19
1073.38/297.06	        -->_1 dbls^#(mark(X)) -> c_18(dbls^#(X)) :18
1073.38/297.06	     
1073.38/297.06	     20: cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	     
1073.38/297.06	     21: sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     22: sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     23: sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     24: indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.06	        -->_1 indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2)) :25
1073.38/297.06	        -->_1 indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2)) :24
1073.38/297.06	     
1073.38/297.06	     25: indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.06	        -->_1 indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2)) :25
1073.38/297.06	        -->_1 indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2)) :24
1073.38/297.06	     
1073.38/297.06	     26: from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.06	        -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26
1073.38/297.06	     
1073.38/297.06	     27: proper^#(dbl(X)) -> c_27(dbl^#(proper(X)))
1073.38/297.06	        -->_1 dbl^#(ok(X)) -> c_16(dbl^#(X)) :16
1073.38/297.06	        -->_1 dbl^#(mark(X)) -> c_15(dbl^#(X)) :15
1073.38/297.06	     
1073.38/297.06	     28: proper^#(0()) -> c_28()
1073.38/297.06	     
1073.38/297.06	     29: proper^#(s(X)) -> c_29(s^#(proper(X)))
1073.38/297.06	        -->_1 s^#(ok(X)) -> c_17(s^#(X)) :17
1073.38/297.06	     
1073.38/297.06	     30: proper^#(dbls(X)) -> c_30(dbls^#(proper(X)))
1073.38/297.06	        -->_1 dbls^#(ok(X)) -> c_19(dbls^#(X)) :19
1073.38/297.06	        -->_1 dbls^#(mark(X)) -> c_18(dbls^#(X)) :18
1073.38/297.06	     
1073.38/297.06	     31: proper^#(nil()) -> c_31()
1073.38/297.06	     
1073.38/297.06	     32: proper^#(cons(X1, X2)) -> c_32(cons^#(proper(X1), proper(X2)))
1073.38/297.06	        -->_1 cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2)) :20
1073.38/297.06	     
1073.38/297.06	     33: proper^#(sel(X1, X2)) -> c_33(sel^#(proper(X1), proper(X2)))
1073.38/297.06	        -->_1 sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2)) :23
1073.38/297.06	        -->_1 sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2)) :22
1073.38/297.06	        -->_1 sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2)) :21
1073.38/297.06	     
1073.38/297.06	     34: proper^#(indx(X1, X2)) -> c_34(indx^#(proper(X1), proper(X2)))
1073.38/297.06	        -->_1 indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2)) :25
1073.38/297.06	        -->_1 indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2)) :24
1073.38/297.06	     
1073.38/297.06	     35: proper^#(from(X)) -> c_35(from^#(proper(X)))
1073.38/297.06	        -->_1 from^#(ok(X)) -> c_26(from^#(X)) :26
1073.38/297.06	     
1073.38/297.06	     36: top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.06	        -->_1 top^#(ok(X)) -> c_37(top^#(active(X))) :37
1073.38/297.06	        -->_1 top^#(mark(X)) -> c_36(top^#(proper(X))) :36
1073.38/297.06	     
1073.38/297.06	     37: top^#(ok(X)) -> c_37(top^#(active(X)))
1073.38/297.06	        -->_1 top^#(ok(X)) -> c_37(top^#(active(X))) :37
1073.38/297.06	        -->_1 top^#(mark(X)) -> c_36(top^#(proper(X))) :36
1073.38/297.06	     
1073.38/297.06	   
1073.38/297.06	   Only the nodes {15,16,17,18,19,20,21,23,22,24,25,26,28,31,36,37}
1073.38/297.06	   are reachable from nodes
1073.38/297.06	   {15,16,17,18,19,20,21,22,23,24,25,26,28,31,36,37} that start
1073.38/297.06	   derivation from marked basic terms. The nodes not reachable are
1073.38/297.06	   removed from the problem.
1073.38/297.06	   
1073.38/297.06	   We are left with following problem, upon which TcT provides the
1073.38/297.06	   certificate MAYBE.
1073.38/297.06	   
1073.38/297.06	   Strict DPs:
1073.38/297.06	     { dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.06	     , dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.06	     , s^#(ok(X)) -> c_17(s^#(X))
1073.38/297.06	     , dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.06	     , dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.06	     , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.06	     , sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.06	     , sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.06	     , sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.06	     , indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.06	     , indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.06	     , from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.06	     , proper^#(0()) -> c_28()
1073.38/297.06	     , proper^#(nil()) -> c_31()
1073.38/297.06	     , top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.06	     , top^#(ok(X)) -> c_37(top^#(active(X))) }
1073.38/297.06	   Strict Trs:
1073.38/297.06	     { active(dbl(X)) -> dbl(active(X))
1073.38/297.06	     , active(dbl(0())) -> mark(0())
1073.38/297.06	     , active(dbl(s(X))) -> mark(s(s(dbl(X))))
1073.38/297.06	     , active(dbls(X)) -> dbls(active(X))
1073.38/297.06	     , active(dbls(nil())) -> mark(nil())
1073.38/297.06	     , active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y)))
1073.38/297.06	     , active(sel(X1, X2)) -> sel(X1, active(X2))
1073.38/297.06	     , active(sel(X1, X2)) -> sel(active(X1), X2)
1073.38/297.06	     , active(sel(0(), cons(X, Y))) -> mark(X)
1073.38/297.06	     , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z))
1073.38/297.06	     , active(indx(X1, X2)) -> indx(active(X1), X2)
1073.38/297.06	     , active(indx(nil(), X)) -> mark(nil())
1073.38/297.06	     , active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z)))
1073.38/297.06	     , active(from(X)) -> mark(cons(X, from(s(X))))
1073.38/297.06	     , dbl(mark(X)) -> mark(dbl(X))
1073.38/297.06	     , dbl(ok(X)) -> ok(dbl(X))
1073.38/297.06	     , s(ok(X)) -> ok(s(X))
1073.38/297.06	     , dbls(mark(X)) -> mark(dbls(X))
1073.38/297.06	     , dbls(ok(X)) -> ok(dbls(X))
1073.38/297.06	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
1073.38/297.06	     , sel(X1, mark(X2)) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(mark(X1), X2) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2))
1073.38/297.06	     , indx(mark(X1), X2) -> mark(indx(X1, X2))
1073.38/297.06	     , indx(ok(X1), ok(X2)) -> ok(indx(X1, X2))
1073.38/297.06	     , from(ok(X)) -> ok(from(X))
1073.38/297.06	     , proper(dbl(X)) -> dbl(proper(X))
1073.38/297.06	     , proper(0()) -> ok(0())
1073.38/297.06	     , proper(s(X)) -> s(proper(X))
1073.38/297.06	     , proper(dbls(X)) -> dbls(proper(X))
1073.38/297.06	     , proper(nil()) -> ok(nil())
1073.38/297.06	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
1073.38/297.06	     , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
1073.38/297.06	     , proper(indx(X1, X2)) -> indx(proper(X1), proper(X2))
1073.38/297.06	     , proper(from(X)) -> from(proper(X))
1073.38/297.06	     , top(mark(X)) -> top(proper(X))
1073.38/297.06	     , top(ok(X)) -> top(active(X)) }
1073.38/297.06	   Obligation:
1073.38/297.06	     runtime complexity
1073.38/297.06	   Answer:
1073.38/297.06	     MAYBE
1073.38/297.06	   
1073.38/297.06	   We estimate the number of application of {13,14} by applications of
1073.38/297.06	   Pre({13,14}) = {}. Here rules are labeled as follows:
1073.38/297.06	   
1073.38/297.06	     DPs:
1073.38/297.06	       { 1: dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.06	       , 2: dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.06	       , 3: s^#(ok(X)) -> c_17(s^#(X))
1073.38/297.06	       , 4: dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.06	       , 5: dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.06	       , 6: cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.06	       , 7: sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.06	       , 8: sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.06	       , 9: sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.06	       , 10: indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.06	       , 11: indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.06	       , 12: from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.06	       , 13: proper^#(0()) -> c_28()
1073.38/297.06	       , 14: proper^#(nil()) -> c_31()
1073.38/297.06	       , 15: top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.06	       , 16: top^#(ok(X)) -> c_37(top^#(active(X))) }
1073.38/297.06	   
1073.38/297.06	   We are left with following problem, upon which TcT provides the
1073.38/297.06	   certificate MAYBE.
1073.38/297.06	   
1073.38/297.06	   Strict DPs:
1073.38/297.06	     { dbl^#(mark(X)) -> c_15(dbl^#(X))
1073.38/297.06	     , dbl^#(ok(X)) -> c_16(dbl^#(X))
1073.38/297.06	     , s^#(ok(X)) -> c_17(s^#(X))
1073.38/297.06	     , dbls^#(mark(X)) -> c_18(dbls^#(X))
1073.38/297.06	     , dbls^#(ok(X)) -> c_19(dbls^#(X))
1073.38/297.06	     , cons^#(ok(X1), ok(X2)) -> c_20(cons^#(X1, X2))
1073.38/297.06	     , sel^#(X1, mark(X2)) -> c_21(sel^#(X1, X2))
1073.38/297.06	     , sel^#(mark(X1), X2) -> c_22(sel^#(X1, X2))
1073.38/297.06	     , sel^#(ok(X1), ok(X2)) -> c_23(sel^#(X1, X2))
1073.38/297.06	     , indx^#(mark(X1), X2) -> c_24(indx^#(X1, X2))
1073.38/297.06	     , indx^#(ok(X1), ok(X2)) -> c_25(indx^#(X1, X2))
1073.38/297.06	     , from^#(ok(X)) -> c_26(from^#(X))
1073.38/297.06	     , top^#(mark(X)) -> c_36(top^#(proper(X)))
1073.38/297.06	     , top^#(ok(X)) -> c_37(top^#(active(X))) }
1073.38/297.06	   Strict Trs:
1073.38/297.06	     { active(dbl(X)) -> dbl(active(X))
1073.38/297.06	     , active(dbl(0())) -> mark(0())
1073.38/297.06	     , active(dbl(s(X))) -> mark(s(s(dbl(X))))
1073.38/297.06	     , active(dbls(X)) -> dbls(active(X))
1073.38/297.06	     , active(dbls(nil())) -> mark(nil())
1073.38/297.06	     , active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y)))
1073.38/297.06	     , active(sel(X1, X2)) -> sel(X1, active(X2))
1073.38/297.06	     , active(sel(X1, X2)) -> sel(active(X1), X2)
1073.38/297.06	     , active(sel(0(), cons(X, Y))) -> mark(X)
1073.38/297.06	     , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z))
1073.38/297.06	     , active(indx(X1, X2)) -> indx(active(X1), X2)
1073.38/297.06	     , active(indx(nil(), X)) -> mark(nil())
1073.38/297.06	     , active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z)))
1073.38/297.06	     , active(from(X)) -> mark(cons(X, from(s(X))))
1073.38/297.06	     , dbl(mark(X)) -> mark(dbl(X))
1073.38/297.06	     , dbl(ok(X)) -> ok(dbl(X))
1073.38/297.06	     , s(ok(X)) -> ok(s(X))
1073.38/297.06	     , dbls(mark(X)) -> mark(dbls(X))
1073.38/297.06	     , dbls(ok(X)) -> ok(dbls(X))
1073.38/297.06	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
1073.38/297.06	     , sel(X1, mark(X2)) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(mark(X1), X2) -> mark(sel(X1, X2))
1073.38/297.06	     , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2))
1073.38/297.06	     , indx(mark(X1), X2) -> mark(indx(X1, X2))
1073.38/297.06	     , indx(ok(X1), ok(X2)) -> ok(indx(X1, X2))
1073.38/297.06	     , from(ok(X)) -> ok(from(X))
1073.38/297.06	     , proper(dbl(X)) -> dbl(proper(X))
1073.38/297.06	     , proper(0()) -> ok(0())
1073.38/297.06	     , proper(s(X)) -> s(proper(X))
1073.38/297.06	     , proper(dbls(X)) -> dbls(proper(X))
1073.38/297.06	     , proper(nil()) -> ok(nil())
1073.38/297.06	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
1073.38/297.06	     , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2))
1073.38/297.06	     , proper(indx(X1, X2)) -> indx(proper(X1), proper(X2))
1073.38/297.06	     , proper(from(X)) -> from(proper(X))
1073.38/297.06	     , top(mark(X)) -> top(proper(X))
1073.38/297.06	     , top(ok(X)) -> top(active(X)) }
1073.38/297.06	   Weak DPs:
1073.38/297.06	     { proper^#(0()) -> c_28()
1073.38/297.06	     , proper^#(nil()) -> c_31() }
1073.38/297.06	   Obligation:
1073.38/297.06	     runtime complexity
1073.38/297.06	   Answer:
1073.38/297.06	     MAYBE
1073.38/297.06	   
1073.38/297.06	   Empty strict component of the problem is NOT empty.
1073.38/297.06	
1073.38/297.06	
1073.38/297.06	Arrrr..
1073.70/297.27	EOF