- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] natsFrom(N) -> cons(N,n__natsFrom(s(N)))
[2] fst(pair(XS,YS)) -> XS
[3] snd(pair(XS,YS)) -> YS
[4] splitAt(0,XS) -> pair(nil,XS)
[5] splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS))
[6] u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS)
[7] head(cons(N,XS)) -> N
[8] tail(cons(N,XS)) -> activate(XS)
[9] sel(N,XS) -> head(afterNth(N,XS))
[10] take(N,XS) -> fst(splitAt(N,XS))
[11] afterNth(N,XS) -> snd(splitAt(N,XS))
[12] natsFrom(X) -> n__natsFrom(X)
[13] activate(n__natsFrom(X)) -> natsFrom(X)
[14] activate(X) -> X


Sub problem: 
guided: 

DP termination of:
<Marked_splitAt(s(N),cons(X,XS)) , Marked_u(splitAt(N,activate(XS)),N,
                                    X,activate(XS))>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_splitAt(N,activate(XS))>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_activate(XS)>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_activate(XS)>
<Marked_u(pair(YS,ZS),N,X,XS) , Marked_activate(X)>
<Marked_tail(cons(N,XS)) , Marked_activate(XS)>
<Marked_sel(N,XS) , Marked_head(afterNth(N,XS))>
<Marked_sel(N,XS) , Marked_afterNth(N,XS)>
<Marked_take(N,XS) , Marked_fst(splitAt(N,XS))>
<Marked_take(N,XS) , Marked_splitAt(N,XS)>
<Marked_afterNth(N,XS) , Marked_snd(splitAt(N,XS))>
<Marked_afterNth(N,XS) , Marked_splitAt(N,XS)>
<Marked_activate(n__natsFrom(X)) , Marked_natsFrom(X)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_splitAt(s(N),cons(X,XS)) , Marked_splitAt(N,activate(XS))> 
      --> <Marked_splitAt(s(N),cons(X,XS)) , Marked_splitAt(N,activate(XS))>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_splitAt -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] natsFrom(N) -> cons(N,n__natsFrom(s(N)))
[2] fst(pair(XS,YS)) -> XS
[3] snd(pair(XS,YS)) -> YS
[4] splitAt(0,XS) -> pair(nil,XS)
[5] splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS))
[6] u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS)
[7] head(cons(N,XS)) -> N
[8] tail(cons(N,XS)) -> activate(XS)
[9] sel(N,XS) -> head(afterNth(N,XS))
[10] take(N,XS) -> fst(splitAt(N,XS))
[11] afterNth(N,XS) -> snd(splitAt(N,XS))
[12] natsFrom(X) -> n__natsFrom(X)
[13] activate(n__natsFrom(X)) -> natsFrom(X)
[14] activate(X) -> X
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_splitAt(s(N),cons(X,XS)) , Marked_u(splitAt(N,activate(XS)),
                                         N,X,activate(XS))>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_splitAt(N,activate(XS))>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_activate(XS)>
<Marked_splitAt(s(N),cons(X,XS)) , Marked_activate(XS)>
<Marked_u(pair(YS,ZS),N,X,XS) , Marked_activate(X)>
<Marked_tail(cons(N,XS)) , Marked_activate(XS)>
<Marked_sel(N,XS) , Marked_head(afterNth(N,XS))>
<Marked_sel(N,XS) , Marked_afterNth(N,XS)>
<Marked_take(N,XS) , Marked_fst(splitAt(N,XS))>
<Marked_take(N,XS) , Marked_splitAt(N,XS)>
<Marked_afterNth(N,XS) , Marked_snd(splitAt(N,XS))>
<Marked_afterNth(N,XS) , Marked_splitAt(N,XS)>
<Marked_activate(n__natsFrom(X)) , Marked_natsFrom(X)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_splitAt(s(N),cons(X,XS)) , Marked_splitAt(N,activate(XS))>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

Cime worked for 0.007640 seconds (real time)
Cime Exit Status: 0