MAYBE

Problem:
 from(X) -> cons(X,from(s(X)))
 head(cons(X,XS)) -> X
 2nd(cons(X,XS)) -> head(XS)
 take(0(),XS) -> nil()
 take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
 sel(0(),cons(X,XS)) -> X
 sel(s(N),cons(X,XS)) -> sel(N,XS)

Proof:
 DP Processor:
  DPs:
   from#(X) -> from#(s(X))
   2nd#(cons(X,XS)) -> head#(XS)
   take#(s(N),cons(X,XS)) -> take#(N,XS)
   sel#(s(N),cons(X,XS)) -> sel#(N,XS)
  TRS:
   from(X) -> cons(X,from(s(X)))
   head(cons(X,XS)) -> X
   2nd(cons(X,XS)) -> head(XS)
   take(0(),XS) -> nil()
   take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
   sel(0(),cons(X,XS)) -> X
   sel(s(N),cons(X,XS)) -> sel(N,XS)
  Usable Rule Processor:
   DPs:
    from#(X) -> from#(s(X))
    2nd#(cons(X,XS)) -> head#(XS)
    take#(s(N),cons(X,XS)) -> take#(N,XS)
    sel#(s(N),cons(X,XS)) -> sel#(N,XS)
   TRS:
    
   EDG Processor:
    DPs:
     from#(X) -> from#(s(X))
     2nd#(cons(X,XS)) -> head#(XS)
     take#(s(N),cons(X,XS)) -> take#(N,XS)
     sel#(s(N),cons(X,XS)) -> sel#(N,XS)
    TRS:
     
    graph:
     sel#(s(N),cons(X,XS)) -> sel#(N,XS) ->
     sel#(s(N),cons(X,XS)) -> sel#(N,XS)
     take#(s(N),cons(X,XS)) -> take#(N,XS) ->
     take#(s(N),cons(X,XS)) -> take#(N,XS)
     from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    Restore Modifier:
     DPs:
      from#(X) -> from#(s(X))
      2nd#(cons(X,XS)) -> head#(XS)
      take#(s(N),cons(X,XS)) -> take#(N,XS)
      sel#(s(N),cons(X,XS)) -> sel#(N,XS)
     TRS:
      from(X) -> cons(X,from(s(X)))
      head(cons(X,XS)) -> X
      2nd(cons(X,XS)) -> head(XS)
      take(0(),XS) -> nil()
      take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
      sel(0(),cons(X,XS)) -> X
      sel(s(N),cons(X,XS)) -> sel(N,XS)
     SCC Processor:
      #sccs: 3
      #rules: 3
      #arcs: 3/16
      DPs:
       from#(X) -> from#(s(X))
      TRS:
       from(X) -> cons(X,from(s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(XS)
       take(0(),XS) -> nil()
       take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
       sel(0(),cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,XS)
      Open
      
      DPs:
       take#(s(N),cons(X,XS)) -> take#(N,XS)
      TRS:
       from(X) -> cons(X,from(s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(XS)
       take(0(),XS) -> nil()
       take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
       sel(0(),cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,XS)
      Open
      
      DPs:
       sel#(s(N),cons(X,XS)) -> sel#(N,XS)
      TRS:
       from(X) -> cons(X,from(s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(XS)
       take(0(),XS) -> nil()
       take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
       sel(0(),cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,XS)
      Open