MAYBE
Time: 0.002036
TRS:
 {                activate X -> X,
    activate n__cons(X1, X2) -> cons(activate X1, X2),
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
  2nd cons(X, n__cons(Y, Z)) -> activate Y,
                cons(X1, X2) -> n__cons(X1, X2),
                      from X -> cons(X, n__from n__s X),
                      from X -> n__from X,
                         s X -> n__s X}
 DP:
  DP:
   {  activate# n__cons(X1, X2) -> activate# X1,
      activate# n__cons(X1, X2) -> cons#(activate X1, X2),
            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,
    2nd# cons(X, n__cons(Y, Z)) -> activate# Y,
                        from# X -> cons#(X, n__from n__s X)}
  TRS:
  {                activate X -> X,
     activate n__cons(X1, X2) -> cons(activate X1, X2),
           activate n__from X -> from activate X,
              activate n__s X -> s activate X,
   2nd cons(X, n__cons(Y, Z)) -> activate Y,
                 cons(X1, X2) -> n__cons(X1, X2),
                       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__cons(X1, X2) -> cons(activate X1, X2),
          activate n__from X -> from activate X,
             activate n__s X -> s activate X,
                cons(X1, X2) -> n__cons(X1, X2),
                      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:
    {(2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__s X -> s# activate X)
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__s X -> activate# X)
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__from X -> from# activate X)
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__from X -> activate# X)
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> activate# X, activate# n__s X -> 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__cons(X1, X2) -> cons#(activate X1, X2))
     (activate# n__from X -> activate# X, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2))
     (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__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> from# activate X, from# X -> cons#(X, n__from n__s X))}
    STATUS:
     arrows: 0.609375
     SCCS (1):
      Scc:
       {activate# n__cons(X1, X2) -> activate# X1,
              activate# n__from X -> activate# X,
                 activate# n__s X -> activate# X}
      
      
      SCC (3):
       Strict:
        {activate# n__cons(X1, X2) -> activate# X1,
               activate# n__from X -> activate# X,
                  activate# n__s X -> activate# X}
       Weak:
       {                activate X -> X,
          activate n__cons(X1, X2) -> cons(activate X1, X2),
                activate n__from X -> from activate X,
                   activate n__s X -> s activate X,
        2nd cons(X, n__cons(Y, Z)) -> activate Y,
                      cons(X1, X2) -> n__cons(X1, X2),
                            from X -> cons(X, n__from n__s X),
                            from X -> n__from X,
                               s X -> n__s X}
       Open