MAYBE
948.32/297.12	MAYBE
948.32/297.12	
948.32/297.12	We are left with following problem, upon which TcT provides the
948.32/297.12	certificate MAYBE.
948.32/297.12	
948.32/297.12	Strict Trs:
948.32/297.12	  { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
948.32/297.12	  , fst(X) -> n__fst(X)
948.32/297.12	  , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X)
948.32/297.12	  , splitAt(X1, X2) -> n__splitAt(X1, X2)
948.32/297.12	  , splitAt(s(N), cons(X, XS)) ->
948.32/297.12	    U81(and(isNatural(N),
948.32/297.12	            n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.12	        N,
948.32/297.12	        X,
948.32/297.12	        activate(XS))
948.32/297.12	  , splitAt(0(), XS) -> U71(isLNat(XS), XS)
948.32/297.12	  , activate(X) -> X
948.32/297.12	  , activate(n__natsFrom(X)) -> natsFrom(X)
948.32/297.12	  , activate(n__isLNat(X)) -> isLNat(X)
948.32/297.12	  , activate(n__nil()) -> nil()
948.32/297.12	  , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
948.32/297.12	  , activate(n__cons(X1, X2)) -> cons(X1, X2)
948.32/297.12	  , activate(n__fst(X)) -> fst(X)
948.32/297.12	  , activate(n__snd(X)) -> snd(X)
948.32/297.12	  , activate(n__tail(X)) -> tail(X)
948.32/297.12	  , activate(n__take(X1, X2)) -> take(X1, X2)
948.32/297.12	  , activate(n__0()) -> 0()
948.32/297.12	  , activate(n__head(X)) -> head(X)
948.32/297.12	  , activate(n__s(X)) -> s(X)
948.32/297.12	  , activate(n__sel(X1, X2)) -> sel(X1, X2)
948.32/297.13	  , activate(n__pair(X1, X2)) -> pair(X1, X2)
948.32/297.13	  , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
948.32/297.13	  , activate(n__and(X1, X2)) -> and(X1, X2)
948.32/297.13	  , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
948.32/297.13	  , snd(X) -> n__snd(X)
948.32/297.13	  , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y)
948.32/297.13	  , U21(tt(), X) -> activate(X)
948.32/297.13	  , U31(tt(), N) -> activate(N)
948.32/297.13	  , U41(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
948.32/297.13	  , cons(X1, X2) -> n__cons(X1, X2)
948.32/297.13	  , s(X) -> n__s(X)
948.32/297.13	  , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
948.32/297.13	  , head(X) -> n__head(X)
948.32/297.13	  , head(cons(N, XS)) ->
948.32/297.13	    U31(and(isNatural(N), n__isLNat(activate(XS))), N)
948.32/297.13	  , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	  , afterNth(X1, X2) -> n__afterNth(X1, X2)
948.32/297.13	  , U61(tt(), Y) -> activate(Y)
948.32/297.13	  , U71(tt(), XS) -> pair(nil(), activate(XS))
948.32/297.13	  , pair(X1, X2) -> n__pair(X1, X2)
948.32/297.13	  , nil() -> n__nil()
948.32/297.13	  , U81(tt(), N, X, XS) ->
948.32/297.13	    U82(splitAt(activate(N), activate(XS)), activate(X))
948.32/297.13	  , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
948.32/297.13	  , U91(tt(), XS) -> activate(XS)
948.32/297.13	  , and(X1, X2) -> n__and(X1, X2)
948.32/297.13	  , and(tt(), X) -> activate(X)
948.32/297.13	  , isNatural(n__0()) -> tt()
948.32/297.13	  , isNatural(n__head(V1)) -> isLNat(activate(V1))
948.32/297.13	  , isNatural(n__s(V1)) -> isNatural(activate(V1))
948.32/297.13	  , isNatural(n__sel(V1, V2)) ->
948.32/297.13	    and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , isLNat(X) -> n__isLNat(X)
948.32/297.13	  , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1))
948.32/297.13	  , isLNat(n__nil()) -> tt()
948.32/297.13	  , isLNat(n__afterNth(V1, V2)) ->
948.32/297.13	    and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , isLNat(n__cons(V1, V2)) ->
948.32/297.13	    and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , isLNat(n__fst(V1)) -> isPLNat(activate(V1))
948.32/297.13	  , isLNat(n__snd(V1)) -> isPLNat(activate(V1))
948.32/297.13	  , isLNat(n__tail(V1)) -> isLNat(activate(V1))
948.32/297.13	  , isLNat(n__take(V1, V2)) ->
948.32/297.13	    and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , isPLNat(n__pair(V1, V2)) ->
948.32/297.13	    and(isLNat(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , isPLNat(n__splitAt(V1, V2)) ->
948.32/297.13	    and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	  , natsFrom(N) -> U41(isNatural(N), N)
948.32/297.13	  , natsFrom(X) -> n__natsFrom(X)
948.32/297.13	  , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	  , sel(X1, X2) -> n__sel(X1, X2)
948.32/297.13	  , 0() -> n__0()
948.32/297.13	  , tail(X) -> n__tail(X)
948.32/297.13	  , tail(cons(N, XS)) ->
948.32/297.13	    U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
948.32/297.13	  , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	  , take(X1, X2) -> n__take(X1, X2) }
948.32/297.13	Obligation:
948.32/297.13	  runtime complexity
948.32/297.13	Answer:
948.32/297.13	  MAYBE
948.32/297.13	
948.32/297.13	None of the processors succeeded.
948.32/297.13	
948.32/297.13	Details of failed attempt(s):
948.32/297.13	-----------------------------
948.32/297.13	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
948.32/297.13	   following reason:
948.32/297.13	   
948.32/297.13	   Computation stopped due to timeout after 297.0 seconds.
948.32/297.13	
948.32/297.13	2) 'Best' failed due to the following reason:
948.32/297.13	   
948.32/297.13	   None of the processors succeeded.
948.32/297.13	   
948.32/297.13	   Details of failed attempt(s):
948.32/297.13	   -----------------------------
948.32/297.13	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
948.32/297.13	      seconds)' failed due to the following reason:
948.32/297.13	      
948.32/297.13	      Computation stopped due to timeout after 148.0 seconds.
948.32/297.13	   
948.32/297.13	   2) 'Best' failed due to the following reason:
948.32/297.13	      
948.32/297.13	      None of the processors succeeded.
948.32/297.13	      
948.32/297.13	      Details of failed attempt(s):
948.32/297.13	      -----------------------------
948.32/297.13	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
948.32/297.13	         following reason:
948.32/297.13	         
948.32/297.13	         The processor is inapplicable, reason:
948.32/297.13	           Processor only applicable for innermost runtime complexity analysis
948.32/297.13	      
948.32/297.13	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
948.32/297.13	         to the following reason:
948.32/297.13	         
948.32/297.13	         The processor is inapplicable, reason:
948.32/297.13	           Processor only applicable for innermost runtime complexity analysis
948.32/297.13	      
948.32/297.13	   
948.32/297.13	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
948.32/297.13	      failed due to the following reason:
948.32/297.13	      
948.32/297.13	      None of the processors succeeded.
948.32/297.13	      
948.32/297.13	      Details of failed attempt(s):
948.32/297.13	      -----------------------------
948.32/297.13	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
948.32/297.13	         failed due to the following reason:
948.32/297.13	         
948.32/297.13	         match-boundness of the problem could not be verified.
948.32/297.13	      
948.32/297.13	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
948.32/297.13	         failed due to the following reason:
948.32/297.13	         
948.32/297.13	         match-boundness of the problem could not be verified.
948.32/297.13	      
948.32/297.13	   
948.32/297.13	
948.32/297.13	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
948.32/297.13	   the following reason:
948.32/297.13	   
948.32/297.13	   We add the following weak dependency pairs:
948.32/297.13	   
948.32/297.13	   Strict DPs:
948.32/297.13	     { U101^#(tt(), N, XS) ->
948.32/297.13	       c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.13	     , fst^#(X) -> c_2(X)
948.32/297.13	     , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.13	     , U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.13	     , splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.13	     , splitAt^#(s(N), cons(X, XS)) ->
948.32/297.13	       c_5(U81^#(and(isNatural(N),
948.32/297.13	                     n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.13	                 N,
948.32/297.13	                 X,
948.32/297.13	                 activate(XS)))
948.32/297.13	     , splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.13	     , U81^#(tt(), N, X, XS) ->
948.32/297.13	       c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.13	     , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.13	     , activate^#(X) -> c_7(X)
948.32/297.13	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.13	     , activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.13	     , activate^#(n__nil()) -> c_10(nil^#())
948.32/297.13	     , activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.13	     , activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.13	     , activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.13	     , activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.13	     , activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.13	     , activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.13	     , activate^#(n__0()) -> c_17(0^#())
948.32/297.13	     , activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.13	     , activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.13	     , activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.13	     , activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.13	     , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.13	     , activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.13	     , natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.13	     , natsFrom^#(X) -> c_62(X)
948.32/297.13	     , isLNat^#(X) -> c_50(X)
948.32/297.13	     , isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__nil()) -> c_52()
948.32/297.13	     , isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.13	       c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isLNat^#(n__cons(V1, V2)) ->
948.32/297.13	       c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__take(V1, V2)) ->
948.32/297.13	       c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , nil^#() -> c_40()
948.32/297.13	     , afterNth^#(N, XS) ->
948.32/297.13	       c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.13	     , cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.13	     , snd^#(X) -> c_25(X)
948.32/297.13	     , snd^#(pair(X, Y)) -> c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.13	     , tail^#(X) -> c_66(X)
948.32/297.13	     , tail^#(cons(N, XS)) ->
948.32/297.13	       c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.13	                  activate(XS)))
948.32/297.13	     , take^#(N, XS) ->
948.32/297.13	       c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , take^#(X1, X2) -> c_69(X1, X2)
948.32/297.13	     , 0^#() -> c_65()
948.32/297.13	     , head^#(X) -> c_33(X)
948.32/297.13	     , head^#(cons(N, XS)) ->
948.32/297.13	       c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.13	     , s^#(X) -> c_31(X)
948.32/297.13	     , sel^#(N, XS) ->
948.32/297.13	       c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.13	     , pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.13	     , and^#(X1, X2) -> c_44(X1, X2)
948.32/297.13	     , and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.13	     , U11^#(tt(), N, XS) ->
948.32/297.13	       c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.13	     , U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.13	     , U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.13	     , U41^#(tt(), N) ->
948.32/297.13	       c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.13	     , U51^#(tt(), N, XS) ->
948.32/297.13	       c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.13	     , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.13	     , U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.13	     , isNatural^#(n__0()) -> c_46()
948.32/297.13	     , isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.13	     , isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.13	     , isNatural^#(n__sel(V1, V2)) ->
948.32/297.13	       c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isPLNat^#(n__pair(V1, V2)) ->
948.32/297.13	       c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.13	       c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) }
948.32/297.13	   
948.32/297.13	   and mark the set of starting terms.
948.32/297.13	   
948.32/297.13	   We are left with following problem, upon which TcT provides the
948.32/297.13	   certificate MAYBE.
948.32/297.13	   
948.32/297.13	   Strict DPs:
948.32/297.13	     { U101^#(tt(), N, XS) ->
948.32/297.13	       c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.13	     , fst^#(X) -> c_2(X)
948.32/297.13	     , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.13	     , U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.13	     , splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.13	     , splitAt^#(s(N), cons(X, XS)) ->
948.32/297.13	       c_5(U81^#(and(isNatural(N),
948.32/297.13	                     n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.13	                 N,
948.32/297.13	                 X,
948.32/297.13	                 activate(XS)))
948.32/297.13	     , splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.13	     , U81^#(tt(), N, X, XS) ->
948.32/297.13	       c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.13	     , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.13	     , activate^#(X) -> c_7(X)
948.32/297.13	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.13	     , activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.13	     , activate^#(n__nil()) -> c_10(nil^#())
948.32/297.13	     , activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.13	     , activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.13	     , activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.13	     , activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.13	     , activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.13	     , activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.13	     , activate^#(n__0()) -> c_17(0^#())
948.32/297.13	     , activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.13	     , activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.13	     , activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.13	     , activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.13	     , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.13	     , activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.13	     , natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.13	     , natsFrom^#(X) -> c_62(X)
948.32/297.13	     , isLNat^#(X) -> c_50(X)
948.32/297.13	     , isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__nil()) -> c_52()
948.32/297.13	     , isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.13	       c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isLNat^#(n__cons(V1, V2)) ->
948.32/297.13	       c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.13	     , isLNat^#(n__take(V1, V2)) ->
948.32/297.13	       c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , nil^#() -> c_40()
948.32/297.13	     , afterNth^#(N, XS) ->
948.32/297.13	       c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.13	     , cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.13	     , snd^#(X) -> c_25(X)
948.32/297.13	     , snd^#(pair(X, Y)) -> c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.13	     , tail^#(X) -> c_66(X)
948.32/297.13	     , tail^#(cons(N, XS)) ->
948.32/297.13	       c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.13	                  activate(XS)))
948.32/297.13	     , take^#(N, XS) ->
948.32/297.13	       c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , take^#(X1, X2) -> c_69(X1, X2)
948.32/297.13	     , 0^#() -> c_65()
948.32/297.13	     , head^#(X) -> c_33(X)
948.32/297.13	     , head^#(cons(N, XS)) ->
948.32/297.13	       c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.13	     , s^#(X) -> c_31(X)
948.32/297.13	     , sel^#(N, XS) ->
948.32/297.13	       c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	     , sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.13	     , pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.13	     , and^#(X1, X2) -> c_44(X1, X2)
948.32/297.13	     , and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.13	     , U11^#(tt(), N, XS) ->
948.32/297.13	       c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.13	     , U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.13	     , U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.13	     , U41^#(tt(), N) ->
948.32/297.13	       c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.13	     , U51^#(tt(), N, XS) ->
948.32/297.13	       c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.13	     , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.13	     , U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.13	     , isNatural^#(n__0()) -> c_46()
948.32/297.13	     , isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.13	     , isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.13	     , isNatural^#(n__sel(V1, V2)) ->
948.32/297.13	       c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isPLNat^#(n__pair(V1, V2)) ->
948.32/297.13	       c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	     , isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.13	       c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) }
948.32/297.13	   Strict Trs:
948.32/297.13	     { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
948.32/297.13	     , fst(X) -> n__fst(X)
948.32/297.13	     , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X)
948.32/297.13	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
948.32/297.13	     , splitAt(s(N), cons(X, XS)) ->
948.32/297.13	       U81(and(isNatural(N),
948.32/297.13	               n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.13	           N,
948.32/297.13	           X,
948.32/297.13	           activate(XS))
948.32/297.13	     , splitAt(0(), XS) -> U71(isLNat(XS), XS)
948.32/297.13	     , activate(X) -> X
948.32/297.13	     , activate(n__natsFrom(X)) -> natsFrom(X)
948.32/297.13	     , activate(n__isLNat(X)) -> isLNat(X)
948.32/297.13	     , activate(n__nil()) -> nil()
948.32/297.13	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
948.32/297.13	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
948.32/297.13	     , activate(n__fst(X)) -> fst(X)
948.32/297.13	     , activate(n__snd(X)) -> snd(X)
948.32/297.13	     , activate(n__tail(X)) -> tail(X)
948.32/297.13	     , activate(n__take(X1, X2)) -> take(X1, X2)
948.32/297.13	     , activate(n__0()) -> 0()
948.32/297.13	     , activate(n__head(X)) -> head(X)
948.32/297.13	     , activate(n__s(X)) -> s(X)
948.32/297.13	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
948.32/297.13	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
948.32/297.13	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
948.32/297.13	     , activate(n__and(X1, X2)) -> and(X1, X2)
948.32/297.13	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
948.32/297.13	     , snd(X) -> n__snd(X)
948.32/297.13	     , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y)
948.32/297.13	     , U21(tt(), X) -> activate(X)
948.32/297.13	     , U31(tt(), N) -> activate(N)
948.32/297.13	     , U41(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
948.32/297.13	     , cons(X1, X2) -> n__cons(X1, X2)
948.32/297.13	     , s(X) -> n__s(X)
948.32/297.13	     , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
948.32/297.13	     , head(X) -> n__head(X)
948.32/297.13	     , head(cons(N, XS)) ->
948.32/297.13	       U31(and(isNatural(N), n__isLNat(activate(XS))), N)
948.32/297.13	     , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
948.32/297.13	     , U61(tt(), Y) -> activate(Y)
948.32/297.13	     , U71(tt(), XS) -> pair(nil(), activate(XS))
948.32/297.13	     , pair(X1, X2) -> n__pair(X1, X2)
948.32/297.13	     , nil() -> n__nil()
948.32/297.13	     , U81(tt(), N, X, XS) ->
948.32/297.13	       U82(splitAt(activate(N), activate(XS)), activate(X))
948.32/297.13	     , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
948.32/297.13	     , U91(tt(), XS) -> activate(XS)
948.32/297.13	     , and(X1, X2) -> n__and(X1, X2)
948.32/297.13	     , and(tt(), X) -> activate(X)
948.32/297.13	     , isNatural(n__0()) -> tt()
948.32/297.13	     , isNatural(n__head(V1)) -> isLNat(activate(V1))
948.32/297.13	     , isNatural(n__s(V1)) -> isNatural(activate(V1))
948.32/297.13	     , isNatural(n__sel(V1, V2)) ->
948.32/297.13	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , isLNat(X) -> n__isLNat(X)
948.32/297.13	     , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1))
948.32/297.13	     , isLNat(n__nil()) -> tt()
948.32/297.13	     , isLNat(n__afterNth(V1, V2)) ->
948.32/297.13	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , isLNat(n__cons(V1, V2)) ->
948.32/297.13	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , isLNat(n__fst(V1)) -> isPLNat(activate(V1))
948.32/297.13	     , isLNat(n__snd(V1)) -> isPLNat(activate(V1))
948.32/297.13	     , isLNat(n__tail(V1)) -> isLNat(activate(V1))
948.32/297.13	     , isLNat(n__take(V1, V2)) ->
948.32/297.13	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , isPLNat(n__pair(V1, V2)) ->
948.32/297.13	       and(isLNat(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , isPLNat(n__splitAt(V1, V2)) ->
948.32/297.13	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.13	     , natsFrom(N) -> U41(isNatural(N), N)
948.32/297.13	     , natsFrom(X) -> n__natsFrom(X)
948.32/297.13	     , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	     , sel(X1, X2) -> n__sel(X1, X2)
948.32/297.13	     , 0() -> n__0()
948.32/297.13	     , tail(X) -> n__tail(X)
948.32/297.13	     , tail(cons(N, XS)) ->
948.32/297.13	       U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
948.32/297.13	     , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.13	     , take(X1, X2) -> n__take(X1, X2) }
948.32/297.13	   Obligation:
948.32/297.13	     runtime complexity
948.32/297.13	   Answer:
948.32/297.13	     MAYBE
948.32/297.13	   
948.32/297.13	   We estimate the number of application of {31,38,48,64} by
948.32/297.13	   applications of Pre({31,38,48,64}) =
948.32/297.13	   {2,5,10,12,13,20,28,29,30,36,40,41,42,44,47,49,51,53,54,55,65,66}.
948.32/297.13	   Here rules are labeled as follows:
948.32/297.13	   
948.32/297.13	     DPs:
948.32/297.13	       { 1: U101^#(tt(), N, XS) ->
948.32/297.13	            c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.13	       , 2: fst^#(X) -> c_2(X)
948.32/297.13	       , 3: fst^#(pair(X, Y)) ->
948.32/297.13	            c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.13	       , 4: U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.13	       , 5: splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.13	       , 6: splitAt^#(s(N), cons(X, XS)) ->
948.32/297.13	            c_5(U81^#(and(isNatural(N),
948.32/297.13	                          n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.13	                      N,
948.32/297.13	                      X,
948.32/297.13	                      activate(XS)))
948.32/297.13	       , 7: splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.13	       , 8: U81^#(tt(), N, X, XS) ->
948.32/297.13	            c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.13	       , 9: U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.13	       , 10: activate^#(X) -> c_7(X)
948.32/297.13	       , 11: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.13	       , 12: activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.13	       , 13: activate^#(n__nil()) -> c_10(nil^#())
948.32/297.13	       , 14: activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.13	       , 15: activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.13	       , 16: activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.13	       , 17: activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.13	       , 18: activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.13	       , 19: activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.13	       , 20: activate^#(n__0()) -> c_17(0^#())
948.32/297.13	       , 21: activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.13	       , 22: activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.13	       , 23: activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.13	       , 24: activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.13	       , 25: activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.13	       , 26: activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.13	       , 27: natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.13	       , 28: natsFrom^#(X) -> c_62(X)
948.32/297.13	       , 29: isLNat^#(X) -> c_50(X)
948.32/297.13	       , 30: isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.13	       , 31: isLNat^#(n__nil()) -> c_52()
948.32/297.13	       , 32: isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.13	             c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	       , 33: isLNat^#(n__cons(V1, V2)) ->
948.32/297.13	             c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	       , 34: isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.13	       , 35: isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.13	       , 36: isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.13	       , 37: isLNat^#(n__take(V1, V2)) ->
948.32/297.13	             c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	       , 38: nil^#() -> c_40()
948.32/297.13	       , 39: afterNth^#(N, XS) ->
948.32/297.13	             c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	       , 40: afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.13	       , 41: cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.13	       , 42: snd^#(X) -> c_25(X)
948.32/297.13	       , 43: snd^#(pair(X, Y)) ->
948.32/297.13	             c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.13	       , 44: tail^#(X) -> c_66(X)
948.32/297.13	       , 45: tail^#(cons(N, XS)) ->
948.32/297.13	             c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.13	                        activate(XS)))
948.32/297.13	       , 46: take^#(N, XS) ->
948.32/297.13	             c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	       , 47: take^#(X1, X2) -> c_69(X1, X2)
948.32/297.13	       , 48: 0^#() -> c_65()
948.32/297.13	       , 49: head^#(X) -> c_33(X)
948.32/297.13	       , 50: head^#(cons(N, XS)) ->
948.32/297.13	             c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.13	       , 51: s^#(X) -> c_31(X)
948.32/297.13	       , 52: sel^#(N, XS) ->
948.32/297.13	             c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.13	       , 53: sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.13	       , 54: pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.13	       , 55: and^#(X1, X2) -> c_44(X1, X2)
948.32/297.13	       , 56: and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.13	       , 57: U11^#(tt(), N, XS) ->
948.32/297.13	             c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.13	       , 58: U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.13	       , 59: U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.13	       , 60: U41^#(tt(), N) ->
948.32/297.13	             c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.13	       , 61: U51^#(tt(), N, XS) ->
948.32/297.13	             c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.13	       , 62: U82^#(pair(YS, ZS), X) ->
948.32/297.13	             c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.13	       , 63: U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.13	       , 64: isNatural^#(n__0()) -> c_46()
948.32/297.13	       , 65: isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.13	       , 66: isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.13	       , 67: isNatural^#(n__sel(V1, V2)) ->
948.32/297.13	             c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	       , 68: isPLNat^#(n__pair(V1, V2)) ->
948.32/297.13	             c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.13	       , 69: isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.13	             c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) }
948.32/297.13	   
948.32/297.13	   We are left with following problem, upon which TcT provides the
948.32/297.13	   certificate MAYBE.
948.32/297.13	   
948.32/297.13	   Strict DPs:
948.32/297.13	     { U101^#(tt(), N, XS) ->
948.32/297.13	       c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.13	     , fst^#(X) -> c_2(X)
948.32/297.13	     , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.13	     , U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.13	     , splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.13	     , splitAt^#(s(N), cons(X, XS)) ->
948.32/297.13	       c_5(U81^#(and(isNatural(N),
948.32/297.13	                     n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.13	                 N,
948.32/297.13	                 X,
948.32/297.13	                 activate(XS)))
948.32/297.13	     , splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.13	     , U81^#(tt(), N, X, XS) ->
948.32/297.13	       c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.13	     , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.13	     , activate^#(X) -> c_7(X)
948.32/297.13	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.13	     , activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.13	     , activate^#(n__nil()) -> c_10(nil^#())
948.32/297.13	     , activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.13	     , activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.13	     , activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.13	     , activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.13	     , activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.13	     , activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.14	     , activate^#(n__0()) -> c_17(0^#())
948.32/297.14	     , activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.14	     , activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.14	     , activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.14	     , activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.14	     , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.14	     , activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.14	     , natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.14	     , natsFrom^#(X) -> c_62(X)
948.32/297.14	     , isLNat^#(X) -> c_50(X)
948.32/297.14	     , isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.14	       c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isLNat^#(n__cons(V1, V2)) ->
948.32/297.14	       c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__take(V1, V2)) ->
948.32/297.14	       c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , afterNth^#(N, XS) ->
948.32/297.14	       c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.14	     , cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.14	     , snd^#(X) -> c_25(X)
948.32/297.14	     , snd^#(pair(X, Y)) -> c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.14	     , tail^#(X) -> c_66(X)
948.32/297.14	     , tail^#(cons(N, XS)) ->
948.32/297.14	       c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.14	                  activate(XS)))
948.32/297.14	     , take^#(N, XS) ->
948.32/297.14	       c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , take^#(X1, X2) -> c_69(X1, X2)
948.32/297.14	     , head^#(X) -> c_33(X)
948.32/297.14	     , head^#(cons(N, XS)) ->
948.32/297.14	       c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.14	     , s^#(X) -> c_31(X)
948.32/297.14	     , sel^#(N, XS) ->
948.32/297.14	       c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.14	     , pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.14	     , and^#(X1, X2) -> c_44(X1, X2)
948.32/297.14	     , and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.14	     , U11^#(tt(), N, XS) ->
948.32/297.14	       c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.14	     , U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.14	     , U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.14	     , U41^#(tt(), N) ->
948.32/297.14	       c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.14	     , U51^#(tt(), N, XS) ->
948.32/297.14	       c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.14	     , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.14	     , U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.14	     , isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.14	     , isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.14	     , isNatural^#(n__sel(V1, V2)) ->
948.32/297.14	       c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isPLNat^#(n__pair(V1, V2)) ->
948.32/297.14	       c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.14	       c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) }
948.32/297.14	   Strict Trs:
948.32/297.14	     { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
948.32/297.14	     , fst(X) -> n__fst(X)
948.32/297.14	     , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X)
948.32/297.14	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
948.32/297.14	     , splitAt(s(N), cons(X, XS)) ->
948.32/297.14	       U81(and(isNatural(N),
948.32/297.14	               n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.14	           N,
948.32/297.14	           X,
948.32/297.14	           activate(XS))
948.32/297.14	     , splitAt(0(), XS) -> U71(isLNat(XS), XS)
948.32/297.14	     , activate(X) -> X
948.32/297.14	     , activate(n__natsFrom(X)) -> natsFrom(X)
948.32/297.14	     , activate(n__isLNat(X)) -> isLNat(X)
948.32/297.14	     , activate(n__nil()) -> nil()
948.32/297.14	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
948.32/297.14	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
948.32/297.14	     , activate(n__fst(X)) -> fst(X)
948.32/297.14	     , activate(n__snd(X)) -> snd(X)
948.32/297.14	     , activate(n__tail(X)) -> tail(X)
948.32/297.14	     , activate(n__take(X1, X2)) -> take(X1, X2)
948.32/297.14	     , activate(n__0()) -> 0()
948.32/297.14	     , activate(n__head(X)) -> head(X)
948.32/297.14	     , activate(n__s(X)) -> s(X)
948.32/297.14	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
948.32/297.14	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
948.32/297.14	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
948.32/297.14	     , activate(n__and(X1, X2)) -> and(X1, X2)
948.32/297.14	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
948.32/297.14	     , snd(X) -> n__snd(X)
948.32/297.14	     , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y)
948.32/297.14	     , U21(tt(), X) -> activate(X)
948.32/297.14	     , U31(tt(), N) -> activate(N)
948.32/297.14	     , U41(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
948.32/297.14	     , cons(X1, X2) -> n__cons(X1, X2)
948.32/297.14	     , s(X) -> n__s(X)
948.32/297.14	     , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
948.32/297.14	     , head(X) -> n__head(X)
948.32/297.14	     , head(cons(N, XS)) ->
948.32/297.14	       U31(and(isNatural(N), n__isLNat(activate(XS))), N)
948.32/297.14	     , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
948.32/297.14	     , U61(tt(), Y) -> activate(Y)
948.32/297.14	     , U71(tt(), XS) -> pair(nil(), activate(XS))
948.32/297.14	     , pair(X1, X2) -> n__pair(X1, X2)
948.32/297.14	     , nil() -> n__nil()
948.32/297.14	     , U81(tt(), N, X, XS) ->
948.32/297.14	       U82(splitAt(activate(N), activate(XS)), activate(X))
948.32/297.14	     , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
948.32/297.14	     , U91(tt(), XS) -> activate(XS)
948.32/297.14	     , and(X1, X2) -> n__and(X1, X2)
948.32/297.14	     , and(tt(), X) -> activate(X)
948.32/297.14	     , isNatural(n__0()) -> tt()
948.32/297.14	     , isNatural(n__head(V1)) -> isLNat(activate(V1))
948.32/297.14	     , isNatural(n__s(V1)) -> isNatural(activate(V1))
948.32/297.14	     , isNatural(n__sel(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(X) -> n__isLNat(X)
948.32/297.14	     , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1))
948.32/297.14	     , isLNat(n__nil()) -> tt()
948.32/297.14	     , isLNat(n__afterNth(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(n__cons(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(n__fst(V1)) -> isPLNat(activate(V1))
948.32/297.14	     , isLNat(n__snd(V1)) -> isPLNat(activate(V1))
948.32/297.14	     , isLNat(n__tail(V1)) -> isLNat(activate(V1))
948.32/297.14	     , isLNat(n__take(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isPLNat(n__pair(V1, V2)) ->
948.32/297.14	       and(isLNat(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isPLNat(n__splitAt(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , natsFrom(N) -> U41(isNatural(N), N)
948.32/297.14	     , natsFrom(X) -> n__natsFrom(X)
948.32/297.14	     , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , sel(X1, X2) -> n__sel(X1, X2)
948.32/297.14	     , 0() -> n__0()
948.32/297.14	     , tail(X) -> n__tail(X)
948.32/297.14	     , tail(cons(N, XS)) ->
948.32/297.14	       U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
948.32/297.14	     , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , take(X1, X2) -> n__take(X1, X2) }
948.32/297.14	   Weak DPs:
948.32/297.14	     { isLNat^#(n__nil()) -> c_52()
948.32/297.14	     , nil^#() -> c_40()
948.32/297.14	     , 0^#() -> c_65()
948.32/297.14	     , isNatural^#(n__0()) -> c_46() }
948.32/297.14	   Obligation:
948.32/297.14	     runtime complexity
948.32/297.14	   Answer:
948.32/297.14	     MAYBE
948.32/297.14	   
948.32/297.14	   We estimate the number of application of {13,20} by applications of
948.32/297.14	   Pre({13,20}) =
948.32/297.14	   {2,4,5,10,28,29,38,39,40,42,45,46,48,50,51,52,53,55,56,60}. Here
948.32/297.14	   rules are labeled as follows:
948.32/297.14	   
948.32/297.14	     DPs:
948.32/297.14	       { 1: U101^#(tt(), N, XS) ->
948.32/297.14	            c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.14	       , 2: fst^#(X) -> c_2(X)
948.32/297.14	       , 3: fst^#(pair(X, Y)) ->
948.32/297.14	            c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.14	       , 4: U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.14	       , 5: splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.14	       , 6: splitAt^#(s(N), cons(X, XS)) ->
948.32/297.14	            c_5(U81^#(and(isNatural(N),
948.32/297.14	                          n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.14	                      N,
948.32/297.14	                      X,
948.32/297.14	                      activate(XS)))
948.32/297.14	       , 7: splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.14	       , 8: U81^#(tt(), N, X, XS) ->
948.32/297.14	            c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.14	       , 9: U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.14	       , 10: activate^#(X) -> c_7(X)
948.32/297.14	       , 11: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.14	       , 12: activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.14	       , 13: activate^#(n__nil()) -> c_10(nil^#())
948.32/297.14	       , 14: activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.14	       , 15: activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.14	       , 16: activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.14	       , 17: activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.14	       , 18: activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.14	       , 19: activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.14	       , 20: activate^#(n__0()) -> c_17(0^#())
948.32/297.14	       , 21: activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.14	       , 22: activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.14	       , 23: activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.14	       , 24: activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.14	       , 25: activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.14	       , 26: activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.14	       , 27: natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.14	       , 28: natsFrom^#(X) -> c_62(X)
948.32/297.14	       , 29: isLNat^#(X) -> c_50(X)
948.32/297.14	       , 30: isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.14	       , 31: isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.14	             c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 32: isLNat^#(n__cons(V1, V2)) ->
948.32/297.14	             c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 33: isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.14	       , 34: isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.14	       , 35: isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.14	       , 36: isLNat^#(n__take(V1, V2)) ->
948.32/297.14	             c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 37: afterNth^#(N, XS) ->
948.32/297.14	             c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	       , 38: afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.14	       , 39: cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.14	       , 40: snd^#(X) -> c_25(X)
948.32/297.14	       , 41: snd^#(pair(X, Y)) ->
948.32/297.14	             c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.14	       , 42: tail^#(X) -> c_66(X)
948.32/297.14	       , 43: tail^#(cons(N, XS)) ->
948.32/297.14	             c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.14	                        activate(XS)))
948.32/297.14	       , 44: take^#(N, XS) ->
948.32/297.14	             c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	       , 45: take^#(X1, X2) -> c_69(X1, X2)
948.32/297.14	       , 46: head^#(X) -> c_33(X)
948.32/297.14	       , 47: head^#(cons(N, XS)) ->
948.32/297.14	             c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.14	       , 48: s^#(X) -> c_31(X)
948.32/297.14	       , 49: sel^#(N, XS) ->
948.32/297.14	             c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	       , 50: sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.14	       , 51: pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.14	       , 52: and^#(X1, X2) -> c_44(X1, X2)
948.32/297.14	       , 53: and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.14	       , 54: U11^#(tt(), N, XS) ->
948.32/297.14	             c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.14	       , 55: U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.14	       , 56: U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.14	       , 57: U41^#(tt(), N) ->
948.32/297.14	             c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.14	       , 58: U51^#(tt(), N, XS) ->
948.32/297.14	             c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.14	       , 59: U82^#(pair(YS, ZS), X) ->
948.32/297.14	             c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.14	       , 60: U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.14	       , 61: isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.14	       , 62: isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.14	       , 63: isNatural^#(n__sel(V1, V2)) ->
948.32/297.14	             c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 64: isPLNat^#(n__pair(V1, V2)) ->
948.32/297.14	             c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 65: isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.14	             c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	       , 66: isLNat^#(n__nil()) -> c_52()
948.32/297.14	       , 67: nil^#() -> c_40()
948.32/297.14	       , 68: 0^#() -> c_65()
948.32/297.14	       , 69: isNatural^#(n__0()) -> c_46() }
948.32/297.14	   
948.32/297.14	   We are left with following problem, upon which TcT provides the
948.32/297.14	   certificate MAYBE.
948.32/297.14	   
948.32/297.14	   Strict DPs:
948.32/297.14	     { U101^#(tt(), N, XS) ->
948.32/297.14	       c_1(fst^#(splitAt(activate(N), activate(XS))))
948.32/297.14	     , fst^#(X) -> c_2(X)
948.32/297.14	     , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X))
948.32/297.14	     , U21^#(tt(), X) -> c_27(activate^#(X))
948.32/297.14	     , splitAt^#(X1, X2) -> c_4(X1, X2)
948.32/297.14	     , splitAt^#(s(N), cons(X, XS)) ->
948.32/297.14	       c_5(U81^#(and(isNatural(N),
948.32/297.14	                     n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.14	                 N,
948.32/297.14	                 X,
948.32/297.14	                 activate(XS)))
948.32/297.14	     , splitAt^#(0(), XS) -> c_6(U71^#(isLNat(XS), XS))
948.32/297.14	     , U81^#(tt(), N, X, XS) ->
948.32/297.14	       c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X)))
948.32/297.14	     , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS)))
948.32/297.14	     , activate^#(X) -> c_7(X)
948.32/297.14	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
948.32/297.14	     , activate^#(n__isLNat(X)) -> c_9(isLNat^#(X))
948.32/297.14	     , activate^#(n__afterNth(X1, X2)) -> c_11(afterNth^#(X1, X2))
948.32/297.14	     , activate^#(n__cons(X1, X2)) -> c_12(cons^#(X1, X2))
948.32/297.14	     , activate^#(n__fst(X)) -> c_13(fst^#(X))
948.32/297.14	     , activate^#(n__snd(X)) -> c_14(snd^#(X))
948.32/297.14	     , activate^#(n__tail(X)) -> c_15(tail^#(X))
948.32/297.14	     , activate^#(n__take(X1, X2)) -> c_16(take^#(X1, X2))
948.32/297.14	     , activate^#(n__head(X)) -> c_18(head^#(X))
948.32/297.14	     , activate^#(n__s(X)) -> c_19(s^#(X))
948.32/297.14	     , activate^#(n__sel(X1, X2)) -> c_20(sel^#(X1, X2))
948.32/297.14	     , activate^#(n__pair(X1, X2)) -> c_21(pair^#(X1, X2))
948.32/297.14	     , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(X1, X2))
948.32/297.14	     , activate^#(n__and(X1, X2)) -> c_23(and^#(X1, X2))
948.32/297.14	     , natsFrom^#(N) -> c_61(U41^#(isNatural(N), N))
948.32/297.14	     , natsFrom^#(X) -> c_62(X)
948.32/297.14	     , isLNat^#(X) -> c_50(X)
948.32/297.14	     , isLNat^#(n__natsFrom(V1)) -> c_51(isNatural^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__afterNth(V1, V2)) ->
948.32/297.14	       c_53(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isLNat^#(n__cons(V1, V2)) ->
948.32/297.14	       c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isLNat^#(n__fst(V1)) -> c_55(isPLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__snd(V1)) -> c_56(isPLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__tail(V1)) -> c_57(isLNat^#(activate(V1)))
948.32/297.14	     , isLNat^#(n__take(V1, V2)) ->
948.32/297.14	       c_58(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , afterNth^#(N, XS) ->
948.32/297.14	       c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , afterNth^#(X1, X2) -> c_36(X1, X2)
948.32/297.14	     , cons^#(X1, X2) -> c_30(X1, X2)
948.32/297.14	     , snd^#(X) -> c_25(X)
948.32/297.14	     , snd^#(pair(X, Y)) -> c_26(U61^#(and(isLNat(X), n__isLNat(Y)), Y))
948.32/297.14	     , tail^#(X) -> c_66(X)
948.32/297.14	     , tail^#(cons(N, XS)) ->
948.32/297.14	       c_67(U91^#(and(isNatural(N), n__isLNat(activate(XS))),
948.32/297.14	                  activate(XS)))
948.32/297.14	     , take^#(N, XS) ->
948.32/297.14	       c_68(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , take^#(X1, X2) -> c_69(X1, X2)
948.32/297.14	     , head^#(X) -> c_33(X)
948.32/297.14	     , head^#(cons(N, XS)) ->
948.32/297.14	       c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N))
948.32/297.14	     , s^#(X) -> c_31(X)
948.32/297.14	     , sel^#(N, XS) ->
948.32/297.14	       c_63(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS))
948.32/297.14	     , sel^#(X1, X2) -> c_64(X1, X2)
948.32/297.14	     , pair^#(X1, X2) -> c_39(X1, X2)
948.32/297.14	     , and^#(X1, X2) -> c_44(X1, X2)
948.32/297.14	     , and^#(tt(), X) -> c_45(activate^#(X))
948.32/297.14	     , U11^#(tt(), N, XS) ->
948.32/297.14	       c_24(snd^#(splitAt(activate(N), activate(XS))))
948.32/297.14	     , U61^#(tt(), Y) -> c_37(activate^#(Y))
948.32/297.14	     , U31^#(tt(), N) -> c_28(activate^#(N))
948.32/297.14	     , U41^#(tt(), N) ->
948.32/297.14	       c_29(cons^#(activate(N), n__natsFrom(s(activate(N)))))
948.32/297.14	     , U51^#(tt(), N, XS) ->
948.32/297.14	       c_32(head^#(afterNth(activate(N), activate(XS))))
948.32/297.14	     , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS))
948.32/297.14	     , U91^#(tt(), XS) -> c_43(activate^#(XS))
948.32/297.14	     , isNatural^#(n__head(V1)) -> c_47(isLNat^#(activate(V1)))
948.32/297.14	     , isNatural^#(n__s(V1)) -> c_48(isNatural^#(activate(V1)))
948.32/297.14	     , isNatural^#(n__sel(V1, V2)) ->
948.32/297.14	       c_49(and^#(isNatural(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isPLNat^#(n__pair(V1, V2)) ->
948.32/297.14	       c_59(and^#(isLNat(activate(V1)), n__isLNat(activate(V2))))
948.32/297.14	     , isPLNat^#(n__splitAt(V1, V2)) ->
948.32/297.14	       c_60(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) }
948.32/297.14	   Strict Trs:
948.32/297.14	     { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
948.32/297.14	     , fst(X) -> n__fst(X)
948.32/297.14	     , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X)
948.32/297.14	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
948.32/297.14	     , splitAt(s(N), cons(X, XS)) ->
948.32/297.14	       U81(and(isNatural(N),
948.32/297.14	               n__and(isNatural(X), n__isLNat(activate(XS)))),
948.32/297.14	           N,
948.32/297.14	           X,
948.32/297.14	           activate(XS))
948.32/297.14	     , splitAt(0(), XS) -> U71(isLNat(XS), XS)
948.32/297.14	     , activate(X) -> X
948.32/297.14	     , activate(n__natsFrom(X)) -> natsFrom(X)
948.32/297.14	     , activate(n__isLNat(X)) -> isLNat(X)
948.32/297.14	     , activate(n__nil()) -> nil()
948.32/297.14	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
948.32/297.14	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
948.32/297.14	     , activate(n__fst(X)) -> fst(X)
948.32/297.14	     , activate(n__snd(X)) -> snd(X)
948.32/297.14	     , activate(n__tail(X)) -> tail(X)
948.32/297.14	     , activate(n__take(X1, X2)) -> take(X1, X2)
948.32/297.14	     , activate(n__0()) -> 0()
948.32/297.14	     , activate(n__head(X)) -> head(X)
948.32/297.14	     , activate(n__s(X)) -> s(X)
948.32/297.14	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
948.32/297.14	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
948.32/297.14	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
948.32/297.14	     , activate(n__and(X1, X2)) -> and(X1, X2)
948.32/297.14	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
948.32/297.14	     , snd(X) -> n__snd(X)
948.32/297.14	     , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y)
948.32/297.14	     , U21(tt(), X) -> activate(X)
948.32/297.14	     , U31(tt(), N) -> activate(N)
948.32/297.14	     , U41(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
948.32/297.14	     , cons(X1, X2) -> n__cons(X1, X2)
948.32/297.14	     , s(X) -> n__s(X)
948.32/297.14	     , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
948.32/297.14	     , head(X) -> n__head(X)
948.32/297.14	     , head(cons(N, XS)) ->
948.32/297.14	       U31(and(isNatural(N), n__isLNat(activate(XS))), N)
948.32/297.14	     , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
948.32/297.14	     , U61(tt(), Y) -> activate(Y)
948.32/297.14	     , U71(tt(), XS) -> pair(nil(), activate(XS))
948.32/297.14	     , pair(X1, X2) -> n__pair(X1, X2)
948.32/297.14	     , nil() -> n__nil()
948.32/297.14	     , U81(tt(), N, X, XS) ->
948.32/297.14	       U82(splitAt(activate(N), activate(XS)), activate(X))
948.32/297.14	     , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
948.32/297.14	     , U91(tt(), XS) -> activate(XS)
948.32/297.14	     , and(X1, X2) -> n__and(X1, X2)
948.32/297.14	     , and(tt(), X) -> activate(X)
948.32/297.14	     , isNatural(n__0()) -> tt()
948.32/297.14	     , isNatural(n__head(V1)) -> isLNat(activate(V1))
948.32/297.14	     , isNatural(n__s(V1)) -> isNatural(activate(V1))
948.32/297.14	     , isNatural(n__sel(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(X) -> n__isLNat(X)
948.32/297.14	     , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1))
948.32/297.14	     , isLNat(n__nil()) -> tt()
948.32/297.14	     , isLNat(n__afterNth(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(n__cons(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isLNat(n__fst(V1)) -> isPLNat(activate(V1))
948.32/297.14	     , isLNat(n__snd(V1)) -> isPLNat(activate(V1))
948.32/297.14	     , isLNat(n__tail(V1)) -> isLNat(activate(V1))
948.32/297.14	     , isLNat(n__take(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isPLNat(n__pair(V1, V2)) ->
948.32/297.14	       and(isLNat(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , isPLNat(n__splitAt(V1, V2)) ->
948.32/297.14	       and(isNatural(activate(V1)), n__isLNat(activate(V2)))
948.32/297.14	     , natsFrom(N) -> U41(isNatural(N), N)
948.32/297.14	     , natsFrom(X) -> n__natsFrom(X)
948.32/297.14	     , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , sel(X1, X2) -> n__sel(X1, X2)
948.32/297.14	     , 0() -> n__0()
948.32/297.14	     , tail(X) -> n__tail(X)
948.32/297.14	     , tail(cons(N, XS)) ->
948.32/297.14	       U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
948.32/297.14	     , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS)
948.32/297.14	     , take(X1, X2) -> n__take(X1, X2) }
948.32/297.14	   Weak DPs:
948.32/297.14	     { activate^#(n__nil()) -> c_10(nil^#())
948.32/297.14	     , activate^#(n__0()) -> c_17(0^#())
948.32/297.14	     , isLNat^#(n__nil()) -> c_52()
948.32/297.14	     , nil^#() -> c_40()
948.32/297.14	     , 0^#() -> c_65()
948.32/297.14	     , isNatural^#(n__0()) -> c_46() }
948.32/297.14	   Obligation:
948.32/297.14	     runtime complexity
948.32/297.14	   Answer:
948.32/297.14	     MAYBE
948.32/297.14	   
948.32/297.14	   Empty strict component of the problem is NOT empty.
948.32/297.14	
948.32/297.14	
948.32/297.14	Arrrr..
948.32/297.15	EOF