YES
Time: 0.048878
TRS:
 {                   from X -> cons(X, n__from s X),
                     from X -> n__from X,
              first(X1, X2) -> n__first(X1, X2),
     first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
              first(0(), Z) -> nil(),
                 activate X -> X,
         activate n__from X -> from X,
  activate n__first(X1, X2) -> first(X1, X2),
       sel(s X, cons(Y, Z)) -> sel(X, activate Z),
       sel(0(), cons(X, Z)) -> X}
 DP:
  DP:
   {   first#(s X, cons(Y, Z)) -> activate# Z,
           activate# n__from X -> from# X,
    activate# n__first(X1, X2) -> first#(X1, X2),
         sel#(s X, cons(Y, Z)) -> activate# Z,
         sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
  TRS:
  {                   from X -> cons(X, n__from s X),
                      from X -> n__from X,
               first(X1, X2) -> n__first(X1, X2),
      first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
               first(0(), Z) -> nil(),
                  activate X -> X,
          activate n__from X -> from X,
   activate n__first(X1, X2) -> first(X1, X2),
        sel(s X, cons(Y, Z)) -> sel(X, activate Z),
        sel(0(), cons(X, Z)) -> X}
  EDG:
   {(sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))
    (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
    (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)
    (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z)
    (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(X, activate Z))
    (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
    (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))}
   STATUS:
    arrows: 0.720000
    SCCS (2):
     Scc:
      {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
     Scc:
      {   first#(s X, cons(Y, Z)) -> activate# Z,
       activate# n__first(X1, X2) -> first#(X1, X2)}
     
     SCC (1):
      Strict:
       {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)}
      Weak:
      {                   from X -> cons(X, n__from s X),
                          from X -> n__from X,
                   first(X1, X2) -> n__first(X1, X2),
          first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                   first(0(), Z) -> nil(),
                      activate X -> X,
              activate n__from X -> from X,
       activate n__first(X1, X2) -> first(X1, X2),
            sel(s X, cons(Y, Z)) -> sel(X, activate Z),
            sel(0(), cons(X, Z)) -> X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = 0,
        
        [first](x0, x1) = x0 + 1,
        
        [n__first](x0, x1) = 0,
        
        [sel](x0, x1) = 0,
        
        [n__from](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [from](x0) = 0,
        
        [activate](x0) = 0,
        
        [nil] = 0,
        
        [0] = 1,
        
        [sel#](x0, x1) = x0
       Strict:
        sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)
        1 + 1X + 0Z + 0Y >= 0 + 1X + 0Z
       Weak:
        sel(0(), cons(X, Z)) -> X
        0 + 0X + 0Z >= 1X
        sel(s X, cons(Y, Z)) -> sel(X, activate Z)
        0 + 0X + 0Z + 0Y >= 0 + 0X + 0Z
        activate n__first(X1, X2) -> first(X1, X2)
        0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
        activate n__from X -> from X
        0 + 0X >= 0 + 0X
        activate X -> X
        0 + 0X >= 1X
        first(0(), Z) -> nil()
        2 + 0Z >= 0
        first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z))
        2 + 1X + 0Z + 0Y >= 0 + 0X + 0Z + 0Y
        first(X1, X2) -> n__first(X1, X2)
        1 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
        from X -> n__from X
        0 + 0X >= 0 + 0X
        from X -> cons(X, n__from s X)
        0 + 0X >= 0 + 0X
      Qed
    
    SCC (2):
     Strict:
      {   first#(s X, cons(Y, Z)) -> activate# Z,
       activate# n__first(X1, X2) -> first#(X1, X2)}
     Weak:
     {                   from X -> cons(X, n__from s X),
                         from X -> n__from X,
                  first(X1, X2) -> n__first(X1, X2),
         first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                  first(0(), Z) -> nil(),
                     activate X -> X,
             activate n__from X -> from X,
      activate n__first(X1, X2) -> first(X1, X2),
           sel(s X, cons(Y, Z)) -> sel(X, activate Z),
           sel(0(), cons(X, Z)) -> X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = x0 + 1,
       
       [first](x0, x1) = x0 + 1,
       
       [n__first](x0, x1) = x0 + x1 + 1,
       
       [sel](x0, x1) = 0,
       
       [n__from](x0) = 0,
       
       [s](x0) = 1,
       
       [from](x0) = 0,
       
       [activate](x0) = 1,
       
       [nil] = 0,
       
       [0] = 0,
       
       [first#](x0, x1) = x0 + x1,
       
       [activate#](x0) = x0
      Strict:
       activate# n__first(X1, X2) -> first#(X1, X2)
       1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
       first#(s X, cons(Y, Z)) -> activate# Z
       2 + 0X + 1Z + 0Y >= 0 + 1Z
      Weak:
       sel(0(), cons(X, Z)) -> X
       0 + 0X + 0Z >= 1X
       sel(s X, cons(Y, Z)) -> sel(X, activate Z)
       0 + 0X + 0Z + 0Y >= 0 + 0X + 0Z
       activate n__first(X1, X2) -> first(X1, X2)
       1 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
       activate n__from X -> from X
       1 + 0X >= 0 + 0X
       activate X -> X
       1 + 0X >= 1X
       first(0(), Z) -> nil()
       1 + 1Z >= 0
       first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z))
       2 + 0X + 1Z + 0Y >= 3 + 1X + 0Z + 0Y
       first(X1, X2) -> n__first(X1, X2)
       1 + 0X1 + 1X2 >= 1 + 1X1 + 1X2
       from X -> n__from X
       0 + 0X >= 0 + 0X
       from X -> cons(X, n__from s X)
       0 + 0X >= 1 + 0X
     Qed