- : 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 (Choosing graph)
Trying to solve the following constraints:
{
  natsFrom(N) >= cons(N,n__natsFrom(s(N))) ;
  natsFrom(X) >= n__natsFrom(X) ;
  fst(pair(XS,YS)) >= XS ;
  snd(pair(XS,YS)) >= YS ;
  splitAt(s(N),cons(X,XS)) >= u(splitAt(N,activate(XS)),N,X,activate(XS)) ;
  splitAt(0,XS) >= pair(nil,XS) ;
  u(pair(YS,ZS),N,X,XS) >= pair(cons(activate(X),YS),ZS) ;
  activate(n__natsFrom(X)) >= natsFrom(X) ;
  activate(X) >= X ;
  head(cons(N,XS)) >= N ;
  tail(cons(N,XS)) >= activate(XS) ;
  afterNth(N,XS) >= snd(splitAt(N,XS)) ;
  sel(N,XS) >= head(afterNth(N,XS)) ;
  take(N,XS) >= fst(splitAt(N,XS)) ;
  Marked_splitAt(s(N),cons(X,XS)) >= Marked_splitAt(N,activate(XS)) ;
 }
 + Disjunctions:{ 
{
  Marked_splitAt(s(N),cons(X,XS)) > Marked_splitAt(N,activate(XS)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== STOPING TIMER virtual ===
constraint: natsFrom(N) >= cons(N,n__natsFrom(s(N)))
constraint: natsFrom(X) >= n__natsFrom(X)
constraint: fst(pair(XS,YS)) >= XS
constraint: snd(pair(XS,YS)) >= YS
constraint: splitAt(s(N),cons(X,XS)) >= u(splitAt(N,activate(XS)),N,X,
                                         activate(XS))
constraint: splitAt(0,XS) >= pair(nil,XS)
constraint: u(pair(YS,ZS),N,X,XS) >= pair(cons(activate(X),YS),ZS)
constraint: activate(n__natsFrom(X)) >= natsFrom(X)
constraint: activate(X) >= X
constraint: head(cons(N,XS)) >= N
constraint: tail(cons(N,XS)) >= activate(XS)
constraint: afterNth(N,XS) >= snd(splitAt(N,XS))
constraint: sel(N,XS) >= head(afterNth(N,XS))
constraint: take(N,XS) >= fst(splitAt(N,XS))
constraint: Marked_splitAt(s(N),cons(X,XS)) >= Marked_splitAt(N,activate(XS))
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: ORD
 [ 
     Solution found:
     RPO with AFS = AFS: 
     and precedence:
     prec (All symbols are Lex.): { cons  <  natsFrom ; cons  <  splitAt ;
                                   cons  <  u ; cons  <  activate ;
                                   cons  <  tail ; cons  <  afterNth ;
                                   cons  <  sel ; cons  <  take ;
                                   cons  <  Marked_splitAt ;
                                   n__natsFrom  <  natsFrom ;
                                   n__natsFrom  <  splitAt ;
                                   n__natsFrom  <  u ;
                                   n__natsFrom  <  activate ;
                                   n__natsFrom  <  tail ;
                                   n__natsFrom  <  afterNth ;
                                   n__natsFrom  <  sel ; n__natsFrom  <  take ;
                                   n__natsFrom  <  Marked_splitAt ;
                                   s  <  natsFrom ; s  <  splitAt ; s  <  u ;
                                   s  <  activate ; s  <  tail ;
                                   s  <  afterNth ; s  <  sel ; s  <  take ;
                                   s  <  Marked_splitAt ; natsFrom  >  cons ;
                                   natsFrom  >  n__natsFrom ; natsFrom  >  s ;
                                   natsFrom  <  splitAt ; natsFrom  <  u ;
                                   natsFrom  <  activate ; natsFrom  <  tail ;
                                   natsFrom  <  afterNth ; natsFrom  <  sel ;
                                   natsFrom  <  take ;
                                   natsFrom  <  Marked_splitAt ; fst  <  take ;
                                   pair  <  splitAt ; pair  <  u ;
                                   pair  <  afterNth ; pair  <  sel ;
                                   pair  <  take ; snd  <  afterNth ;
                                   snd  <  sel ; nil  <  splitAt ;
                                   nil  <  afterNth ; nil  <  sel ;
                                   nil  <  take ; splitAt  >  cons ;
                                   splitAt  >  n__natsFrom ; splitAt  >  s ;
                                   splitAt  >  natsFrom ; splitAt  >  pair ;
                                   splitAt  >  nil ; splitAt  >  u ;
                                   splitAt  >  activate ;
                                   splitAt  <  afterNth ; splitAt  <  sel ;
                                   splitAt  <  take ; u  >  cons ;
                                   u  >  n__natsFrom ; u  >  s ;
                                   u  >  natsFrom ; u  >  pair ;
                                   u  <  splitAt ; u  >  activate ;
                                   u  <  afterNth ; u  <  sel ; u  <  take ;
                                   activate  >  cons ;
                                   activate  >  n__natsFrom ; activate  >  s ;
                                   activate  >  natsFrom ;
                                   activate  <  splitAt ; activate  <  u ;
                                   activate  <  tail ; activate  <  afterNth ;
                                   activate  <  sel ; activate  <  take ;
                                   activate  <  Marked_splitAt ; head  <  sel ;
                                   tail  >  cons ; tail  >  n__natsFrom ;
                                   tail  >  s ; tail  >  natsFrom ;
                                   tail  >  activate ; afterNth  >  cons ;
                                   afterNth  >  n__natsFrom ; afterNth  >  s ;
                                   afterNth  >  natsFrom ; afterNth  >  pair ;
                                   afterNth  >  snd ; afterNth  >  nil ;
                                   afterNth  >  splitAt ; afterNth  >  u ;
                                   afterNth  >  activate ; afterNth  <  sel ;
                                   sel  >  cons ; sel  >  n__natsFrom ;
                                   sel  >  s ; sel  >  natsFrom ;
                                   sel  >  pair ; sel  >  snd ; sel  >  nil ;
                                   sel  >  splitAt ; sel  >  u ;
                                   sel  >  activate ; sel  >  head ;
                                   sel  >  afterNth ; take  >  cons ;
                                   take  >  n__natsFrom ; take  >  s ;
                                   take  >  natsFrom ; take  >  fst ;
                                   take  >  pair ; take  >  nil ;
                                   take  >  splitAt ; take  >  u ;
                                   take  >  activate ;
                                   Marked_splitAt  >  cons ;
                                   Marked_splitAt  >  n__natsFrom ;
                                   Marked_splitAt  >  s ;
                                   Marked_splitAt  >  natsFrom ;
                                   Marked_splitAt  >  activate ; }

 ]} 
 ]} 
 ]} 

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