MAYBE
Time: 0.001096
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 activate X,
           activate n__s X -> s activate X,
                    from X -> cons(X, n__from n__s X),
                    from X -> n__from X,
                       s X -> n__s X}
 DP:
  DP:
   {   2nd# cons(X, X1) -> 2nd# cons1(X, activate X1),
       2nd# cons(X, X1) -> activate# X1,
    activate# n__from X -> activate# X,
    activate# n__from X -> from# activate X,
       activate# n__s X -> activate# X,
       activate# n__s X -> s# activate 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 activate X,
            activate n__s X -> s activate X,
                     from X -> cons(X, n__from n__s X),
                     from X -> n__from X,
                        s X -> n__s X}
  UR:
   {        activate X -> X,
    activate n__from X -> from activate X,
       activate n__s X -> s activate X,
                from X -> cons(X, n__from n__s X),
                from X -> n__from X,
                   s X -> n__s X,
               a(x, y) -> x,
               a(x, y) -> y}
   EDG:
    {(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 -> from# activate X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (2nd# cons(X, X1) -> activate# X1, activate# n__s X -> s# activate X)
     (2nd# cons(X, X1) -> activate# X1, activate# n__s X -> activate# X)
     (2nd# cons(X, X1) -> activate# X1, activate# n__from X -> from# activate X)
     (2nd# cons(X, X1) -> activate# X1, activate# n__from X -> activate# 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)
     (activate# n__from X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__from X -> from# 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)}
    STATUS:
     arrows: 0.611111
     SCCS (2):
      Scc:
       {2nd# cons(X, X1) -> 2nd# cons1(X, activate X1)}
      Scc:
       {activate# n__from X -> activate# X,
           activate# n__s X -> activate# X}
      
      SCC (1):
       Strict:
        {2nd# cons(X, X1) -> 2nd# cons1(X, activate X1)}
       Weak:
       {2nd cons1(X, cons(Y, Z)) -> Y,
                 2nd cons(X, X1) -> 2nd cons1(X, activate X1),
                      activate X -> X,
              activate n__from X -> from activate X,
                 activate n__s X -> s activate X,
                          from X -> cons(X, n__from n__s X),
                          from X -> n__from X,
                             s X -> n__s X}
       Open
      
      SCC (2):
       Strict:
        {activate# n__from X -> activate# X,
            activate# n__s X -> activate# X}
       Weak:
       {2nd cons1(X, cons(Y, Z)) -> Y,
                 2nd cons(X, X1) -> 2nd cons1(X, activate X1),
                      activate X -> X,
              activate n__from X -> from activate X,
                 activate n__s X -> s activate X,
                          from X -> cons(X, n__from n__s X),
                          from X -> n__from X,
                             s X -> n__s X}
       Open