MAYBE
Time: 0.001265
TRS:
 {              from X -> cons(X, n__from n__s X),
                from X -> n__from X,
  sel(0(), cons(X, Y)) -> X,
  sel(s X, cons(Y, Z)) -> sel(X, activate Z),
            activate X -> X,
    activate n__from X -> from activate X,
       activate n__s X -> s activate X,
                   s X -> n__s X}
 DP:
  DP:
   {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z),
    sel#(s X, cons(Y, Z)) -> activate# Z,
      activate# n__from X -> from# activate X,
      activate# n__from X -> activate# X,
         activate# n__s X -> activate# X,
         activate# n__s X -> s# activate X}
  TRS:
  {              from X -> cons(X, n__from n__s X),
                 from X -> n__from X,
   sel(0(), cons(X, Y)) -> X,
   sel(s X, cons(Y, Z)) -> sel(X, activate Z),
             activate X -> X,
     activate n__from X -> from activate X,
        activate n__s X -> s activate X,
                    s X -> n__s X}
  UR:
   {            from X -> cons(X, n__from n__s X),
                from X -> n__from X,
            activate X -> X,
    activate n__from X -> from activate X,
       activate n__s X -> s activate X,
                   s X -> n__s X,
               a(x, y) -> x,
               a(x, y) -> y}
   EDG:
    {(sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# activate X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X)
     (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(X, activate Z))
     (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z)}
    STATUS:
     arrows: 0.611111
     SCCS (2):
      Scc:
       {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
      Scc:
       {activate# n__from X -> activate# X,
           activate# n__s X -> activate# X}
      
      SCC (1):
       Strict:
        {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
       Weak:
       {              from X -> cons(X, n__from n__s X),
                      from X -> n__from X,
        sel(0(), cons(X, Y)) -> X,
        sel(s X, cons(Y, Z)) -> sel(X, activate Z),
                  activate X -> X,
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
                         s X -> n__s X}
       Open
      
      SCC (2):
       Strict:
        {activate# n__from X -> activate# X,
            activate# n__s X -> activate# X}
       Weak:
       {              from X -> cons(X, n__from n__s X),
                      from X -> n__from X,
        sel(0(), cons(X, Y)) -> X,
        sel(s X, cons(Y, Z)) -> sel(X, activate Z),
                  activate X -> X,
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
                         s X -> n__s X}
       Open