MAYBE
Time: 0.075741
TRS:
 {                 from X -> cons(X, n__from n__s X),
                   from X -> n__from X,
           after(0(), XS) -> XS,
  after(s N, cons(X, XS)) -> after(N, activate XS),
               activate X -> X,
       activate n__from X -> from activate X,
          activate n__s X -> s activate X,
                      s X -> n__s X}
 DP:
  DP:
   {after#(s N, cons(X, XS)) -> after#(N, activate XS),
    after#(s N, cons(X, XS)) -> activate# XS,
         activate# n__from X -> from# activate X,
         activate# n__from X -> activate# X,
            activate# n__s X -> activate# X,
            activate# n__s X -> s# activate X}
  TRS:
  {                 from X -> cons(X, n__from n__s X),
                    from X -> n__from X,
            after(0(), XS) -> XS,
   after(s N, cons(X, XS)) -> after(N, activate XS),
                activate X -> X,
        activate n__from X -> from activate X,
           activate n__s X -> s activate X,
                       s X -> n__s X}
  UR:
   {            from X -> cons(X, n__from n__s X),
                from X -> n__from X,
            activate X -> X,
    activate n__from X -> from activate X,
       activate n__s X -> s activate X,
                   s X -> n__s X,
               a(x, y) -> x,
               a(x, y) -> y}
   EDG:
    {(after#(s N, cons(X, XS)) -> after#(N, activate XS), after#(s N, cons(X, XS)) -> activate# XS)
     (after#(s N, cons(X, XS)) -> after#(N, activate XS), after#(s N, cons(X, XS)) -> after#(N, activate XS))
     (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 -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# 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__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (after#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# activate X)
     (after#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> activate# X)
     (after#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> activate# X)
     (after#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> s# activate X)}
    STATUS:
     arrows: 0.611111
     SCCS (2):
      Scc:
       {after#(s N, cons(X, XS)) -> after#(N, activate XS)}
      Scc:
       {activate# n__from X -> activate# X,
           activate# n__s X -> activate# X}
      
      SCC (1):
       Strict:
        {after#(s N, cons(X, XS)) -> after#(N, activate XS)}
       Weak:
       {                 from X -> cons(X, n__from n__s X),
                         from X -> n__from X,
                 after(0(), XS) -> XS,
        after(s N, cons(X, XS)) -> after(N, activate XS),
                     activate X -> X,
             activate n__from X -> from activate X,
                activate n__s X -> s activate X,
                            s X -> n__s X}
       Open
      
      SCC (2):
       Strict:
        {activate# n__from X -> activate# X,
            activate# n__s X -> activate# X}
       Weak:
       {                 from X -> cons(X, n__from n__s X),
                         from X -> n__from X,
                 after(0(), XS) -> XS,
        after(s N, cons(X, XS)) -> after(N, activate XS),
                     activate X -> X,
             activate n__from X -> from activate X,
                activate n__s X -> s activate X,
                            s X -> n__s X}
       Open