YES
Time: 0.000977
TRS:
 {2nd cons1(X, cons(Y, Z)) -> Y,
           2nd cons(X, X1) -> 2nd cons1(X, activate X1),
                activate X -> X,
        activate n__from X -> from X,
                    from X -> cons(X, n__from s X),
                    from X -> n__from X}
 DP:
  DP:
   {   2nd# cons(X, X1) -> 2nd# cons1(X, activate X1),
       2nd# cons(X, X1) -> activate# X1,
    activate# n__from X -> from# X}
  TRS:
  {2nd cons1(X, cons(Y, Z)) -> Y,
            2nd cons(X, X1) -> 2nd cons1(X, activate X1),
                 activate X -> X,
         activate n__from X -> from X,
                     from X -> cons(X, n__from s X),
                     from X -> n__from X}
  EDG:
   {(2nd# cons(X, X1) -> activate# X1, activate# n__from X -> from# X)
    (2nd# cons(X, X1) -> 2nd# cons1(X, activate X1), 2nd# cons(X, X1) -> 2nd# cons1(X, activate X1))
    (2nd# cons(X, X1) -> 2nd# cons1(X, activate X1), 2nd# cons(X, X1) -> activate# X1)}
   EDG:
    {(2nd# cons(X, X1) -> activate# X1, activate# n__from X -> from# X)}
    EDG:
     {(2nd# cons(X, X1) -> activate# X1, activate# n__from X -> from# X)}
     EDG:
      {(2nd# cons(X, X1) -> activate# X1, activate# n__from X -> from# X)}
      STATUS:
       arrows: 0.888889
       SCCS (0):