YES
Time: 0.032375
TRS:
 {                activate X -> X,
    activate n__cons(X1, X2) -> cons(X1, X2),
          activate n__from X -> from X,
  2nd cons(X, n__cons(Y, Z)) -> activate Y,
                cons(X1, X2) -> n__cons(X1, X2),
                      from X -> cons(X, n__from s X),
                      from X -> n__from X}
 DP:
  DP:
   {  activate# n__cons(X1, X2) -> cons#(X1, X2),
            activate# n__from X -> from# X,
    2nd# cons(X, n__cons(Y, Z)) -> activate# Y,
                        from# X -> cons#(X, n__from s X)}
  TRS:
  {                activate X -> X,
     activate n__cons(X1, X2) -> cons(X1, X2),
           activate n__from X -> from X,
   2nd cons(X, n__cons(Y, Z)) -> activate Y,
                 cons(X1, X2) -> n__cons(X1, X2),
                       from X -> cons(X, n__from s X),
                       from X -> n__from X}
  UR:
   {a(x, y) -> x,
    a(x, y) -> y}
   EDG:
    {(activate# n__from X -> from# X, from# X -> cons#(X, n__from s X))
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__from X -> from# X)}
    STATUS:
     arrows: 0.812500
     SCCS (0):