MAYBE
Time: 0.089048
TRS:
 {             mark cons(X1, X2) -> active cons(mark X1, X2),
                     mark from X -> active from mark X,
                        mark s X -> active s mark X,
              mark after(X1, X2) -> active after(mark X1, mark X2),
                        mark 0() -> active 0(),
               cons(X1, mark X2) -> cons(X1, X2),
             cons(X1, active X2) -> cons(X1, X2),
               cons(mark X1, X2) -> cons(X1, X2),
             cons(active X1, X2) -> cons(X1, X2),
                     from mark X -> from X,
                   from active X -> from X,
                        s mark X -> s X,
                      s active X -> s X,
                   active from X -> mark cons(X, from s X),
  active after(s N, cons(X, XS)) -> mark after(N, XS),
           active after(0(), XS) -> mark XS,
              after(X1, mark X2) -> after(X1, X2),
            after(X1, active X2) -> after(X1, X2),
              after(mark X1, X2) -> after(X1, X2),
            after(active X1, X2) -> after(X1, X2)}
 DP:
  DP:
   {             mark# cons(X1, X2) -> mark# X1,
                 mark# cons(X1, X2) -> cons#(mark X1, X2),
                 mark# cons(X1, X2) -> active# cons(mark X1, X2),
                       mark# from X -> mark# X,
                       mark# from X -> from# mark X,
                       mark# from X -> active# from mark X,
                          mark# s X -> mark# X,
                          mark# s X -> s# mark X,
                          mark# s X -> active# s mark X,
                mark# after(X1, X2) -> mark# X1,
                mark# after(X1, X2) -> mark# X2,
                mark# after(X1, X2) -> active# after(mark X1, mark X2),
                mark# after(X1, X2) -> after#(mark X1, mark X2),
                          mark# 0() -> active# 0(),
                 cons#(X1, mark X2) -> cons#(X1, X2),
               cons#(X1, active X2) -> cons#(X1, X2),
                 cons#(mark X1, X2) -> cons#(X1, X2),
               cons#(active X1, X2) -> cons#(X1, X2),
                       from# mark X -> from# X,
                     from# active X -> from# X,
                          s# mark X -> s# X,
                        s# active X -> s# X,
                     active# from X -> mark# cons(X, from s X),
                     active# from X -> cons#(X, from s X),
                     active# from X -> from# s X,
                     active# from X -> s# X,
    active# after(s N, cons(X, XS)) -> mark# after(N, XS),
    active# after(s N, cons(X, XS)) -> after#(N, XS),
             active# after(0(), XS) -> mark# XS,
                after#(X1, mark X2) -> after#(X1, X2),
              after#(X1, active X2) -> after#(X1, X2),
                after#(mark X1, X2) -> after#(X1, X2),
              after#(active X1, X2) -> after#(X1, X2)}
  TRS:
  {             mark cons(X1, X2) -> active cons(mark X1, X2),
                      mark from X -> active from mark X,
                         mark s X -> active s mark X,
               mark after(X1, X2) -> active after(mark X1, mark X2),
                         mark 0() -> active 0(),
                cons(X1, mark X2) -> cons(X1, X2),
              cons(X1, active X2) -> cons(X1, X2),
                cons(mark X1, X2) -> cons(X1, X2),
              cons(active X1, X2) -> cons(X1, X2),
                      from mark X -> from X,
                    from active X -> from X,
                         s mark X -> s X,
                       s active X -> s X,
                    active from X -> mark cons(X, from s X),
   active after(s N, cons(X, XS)) -> mark after(N, XS),
            active after(0(), XS) -> mark XS,
               after(X1, mark X2) -> after(X1, X2),
             after(X1, active X2) -> after(X1, X2),
               after(mark X1, X2) -> after(X1, X2),
             after(active X1, X2) -> after(X1, X2)}
  UR:
   {             mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark from X -> active from mark X,
                          mark s X -> active s mark X,
                mark after(X1, X2) -> active after(mark X1, mark X2),
                          mark 0() -> active 0(),
                 cons(X1, mark X2) -> cons(X1, X2),
               cons(X1, active X2) -> cons(X1, X2),
                 cons(mark X1, X2) -> cons(X1, X2),
               cons(active X1, X2) -> cons(X1, X2),
                       from mark X -> from X,
                     from active X -> from X,
                          s mark X -> s X,
                        s active X -> s X,
                     active from X -> mark cons(X, from s X),
    active after(s N, cons(X, XS)) -> mark after(N, XS),
             active after(0(), XS) -> mark XS,
                after(X1, mark X2) -> after(X1, X2),
              after(X1, active X2) -> after(X1, X2),
                after(mark X1, X2) -> after(X1, X2),
              after(active X1, X2) -> after(X1, X2),
                           a(x, y) -> x,
                           a(x, y) -> y}
   EDG:
    {
     (mark# s X -> active# s mark X, active# after(0(), XS) -> mark# XS)
     (mark# s X -> active# s mark X, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (mark# s X -> active# s mark X, active# after(s N, cons(X, XS)) -> mark# after(N, XS))
     (mark# s X -> active# s mark X, active# from X -> s# X)
     (mark# s X -> active# s mark X, active# from X -> from# s X)
     (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X))
     (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X))
     (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0())
     (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> after#(mark X1, mark X2))
     (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> mark# X2)
     (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> mark# X1)
     (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X)
     (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X)
     (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X)
     (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
     (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
     (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> active# from mark X)
     (mark# s X -> mark# X, mark# from X -> from# mark X)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (from# active X -> from# X, from# active X -> from# X)
     (from# active X -> from# X, from# mark X -> from# X)
     (s# active X -> s# X, s# active X -> s# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(active X1, X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(mark X1, X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, active X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, mark X2) -> after#(X1, X2))
     (mark# after(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
     (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
     (mark# after(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# after(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# after(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# after(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# after(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(active X1, X2) -> after#(X1, X2))
     (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(mark X1, X2) -> after#(X1, X2))
     (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, active X2) -> after#(X1, X2))
     (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, mark X2) -> after#(X1, X2))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(0(), XS) -> mark# XS)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
     (mark# after(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X2)
     (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X1)
     (mark# after(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# after(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# after(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# after(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
     (mark# after(X1, X2) -> mark# X2, mark# from X -> from# mark X)
     (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(active X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(active X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
     (after#(active X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(active X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
     (after#(X1, active X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(X1, active X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
     (after#(X1, active X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(X1, active X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (active# from X -> from# s X, from# mark X -> from# X)
     (active# from X -> from# s X, from# active X -> from# X)
     (mark# from X -> from# mark X, from# mark X -> from# X)
     (mark# from X -> from# mark X, from# active X -> from# X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> mark# X1)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> mark# X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> from# mark X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> active# from mark X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> mark# X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> s# mark X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> active# s mark X)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X1)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X2)
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> after#(mark X1, mark X2))
     (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# 0() -> active# 0())
     (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# after(0(), XS) -> mark# XS, mark# from X -> mark# X)
     (active# after(0(), XS) -> mark# XS, mark# from X -> from# mark X)
     (active# after(0(), XS) -> mark# XS, mark# from X -> active# from mark X)
     (active# after(0(), XS) -> mark# XS, mark# s X -> mark# X)
     (active# after(0(), XS) -> mark# XS, mark# s X -> s# mark X)
     (active# after(0(), XS) -> mark# XS, mark# s X -> active# s mark X)
     (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
     (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
     (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (active# after(0(), XS) -> mark# XS, mark# 0() -> active# 0())
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (active# from X -> s# X, s# mark X -> s# X)
     (active# from X -> s# X, s# active X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (from# mark X -> from# X, from# active X -> from# X)
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> from# mark X)
     (mark# from X -> mark# X, mark# from X -> active# from mark X)
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# s X -> s# mark X)
     (mark# from X -> mark# X, mark# s X -> active# s mark X)
     (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
     (mark# from X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# 0() -> active# 0())
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> cons#(X, from s X))
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> from# s X)
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> s# X)
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
     (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(0(), XS) -> mark# XS)
     (mark# 0() -> active# 0(), active# from X -> mark# cons(X, from s X))
     (mark# 0() -> active# 0(), active# from X -> cons#(X, from s X))
     (mark# 0() -> active# 0(), active# from X -> from# s X)
     (mark# 0() -> active# 0(), active# from X -> s# X)
     (mark# 0() -> active# 0(), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
     (mark# 0() -> active# 0(), active# after(s N, cons(X, XS)) -> after#(N, XS))
     (mark# 0() -> active# 0(), active# after(0(), XS) -> mark# XS)
     (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
     (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
     (mark# from X -> active# from mark X, active# from X -> from# s X)
     (mark# from X -> active# from mark X, active# from X -> s# X)
     (mark# from X -> active# from mark X, active# after(s N, cons(X, XS)) -> mark# after(N, XS))
     (mark# from X -> active# from mark X, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (mark# from X -> active# from mark X, active# after(0(), XS) -> mark# XS)
    }
    EDG:
     {
      (mark# s X -> active# s mark X, active# after(0(), XS) -> mark# XS)
      (mark# s X -> active# s mark X, active# after(s N, cons(X, XS)) -> after#(N, XS))
      (mark# s X -> active# s mark X, active# after(s N, cons(X, XS)) -> mark# after(N, XS))
      (mark# s X -> active# s mark X, active# from X -> s# X)
      (mark# s X -> active# s mark X, active# from X -> from# s X)
      (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X))
      (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X))
      (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2))
      (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0())
      (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> after#(mark X1, mark X2))
      (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> mark# X2)
      (active# from X -> mark# cons(X, from s X), mark# after(X1, X2) -> mark# X1)
      (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X)
      (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X)
      (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X)
      (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
      (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
      (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# 0() -> active# 0())
      (mark# s X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# s X -> active# s mark X)
      (mark# s X -> mark# X, mark# s X -> s# mark X)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# from X -> active# from mark X)
      (mark# s X -> mark# X, mark# from X -> from# mark X)
      (mark# s X -> mark# X, mark# from X -> mark# X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (from# active X -> from# X, from# active X -> from# X)
      (from# active X -> from# X, from# mark X -> from# X)
      (s# active X -> s# X, s# active X -> s# X)
      (s# active X -> s# X, s# mark X -> s# X)
      (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(active X1, X2) -> after#(X1, X2))
      (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(mark X1, X2) -> after#(X1, X2))
      (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, active X2) -> after#(X1, X2))
      (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, mark X2) -> after#(X1, X2))
      (mark# after(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
      (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
      (mark# after(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# after(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# after(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# after(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
      (mark# after(X1, X2) -> mark# X1, mark# from X -> from# mark X)
      (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(active X1, X2) -> after#(X1, X2))
      (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(mark X1, X2) -> after#(X1, X2))
      (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, active X2) -> after#(X1, X2))
      (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, mark X2) -> after#(X1, X2))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(0(), XS) -> mark# XS)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
      (mark# after(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X2)
      (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X1)
      (mark# after(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# after(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# after(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# after(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
      (mark# after(X1, X2) -> mark# X2, mark# from X -> from# mark X)
      (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
      (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> s# mark X, s# active X -> s# X)
      (mark# s X -> s# mark X, s# mark X -> s# X)
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (after#(X1, mark X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
      (after#(X1, mark X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
      (after#(X1, mark X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
      (after#(X1, mark X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
      (after#(mark X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
      (after#(mark X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
      (after#(mark X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
      (after#(mark X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
      (after#(active X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
      (after#(active X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
      (after#(active X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
      (after#(active X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
      (after#(X1, active X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
      (after#(X1, active X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
      (after#(X1, active X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
      (after#(X1, active X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (active# from X -> from# s X, from# mark X -> from# X)
      (active# from X -> from# s X, from# active X -> from# X)
      (mark# from X -> from# mark X, from# mark X -> from# X)
      (mark# from X -> from# mark X, from# active X -> from# X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> mark# X1)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> mark# X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> from# mark X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# from X -> active# from mark X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> mark# X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> s# mark X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# s X -> active# s mark X)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X1)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X2)
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> after#(mark X1, mark X2))
      (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# 0() -> active# 0())
      (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
      (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# after(0(), XS) -> mark# XS, mark# from X -> mark# X)
      (active# after(0(), XS) -> mark# XS, mark# from X -> from# mark X)
      (active# after(0(), XS) -> mark# XS, mark# from X -> active# from mark X)
      (active# after(0(), XS) -> mark# XS, mark# s X -> mark# X)
      (active# after(0(), XS) -> mark# XS, mark# s X -> s# mark X)
      (active# after(0(), XS) -> mark# XS, mark# s X -> active# s mark X)
      (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
      (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
      (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (active# after(0(), XS) -> mark# XS, mark# 0() -> active# 0())
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (active# from X -> s# X, s# mark X -> s# X)
      (active# from X -> s# X, s# active X -> s# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# active X -> s# X)
      (from# mark X -> from# X, from# mark X -> from# X)
      (from# mark X -> from# X, from# active X -> from# X)
      (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# from X -> mark# X, mark# from X -> mark# X)
      (mark# from X -> mark# X, mark# from X -> from# mark X)
      (mark# from X -> mark# X, mark# from X -> active# from mark X)
      (mark# from X -> mark# X, mark# s X -> mark# X)
      (mark# from X -> mark# X, mark# s X -> s# mark X)
      (mark# from X -> mark# X, mark# s X -> active# s mark X)
      (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X1)
      (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X2)
      (mark# from X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
      (mark# from X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
      (mark# from X -> mark# X, mark# 0() -> active# 0())
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> cons#(X, from s X))
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> from# s X)
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# from X -> s# X)
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
      (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(0(), XS) -> mark# XS)
      (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
      (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
      (mark# from X -> active# from mark X, active# from X -> from# s X)
      (mark# from X -> active# from mark X, active# from X -> s# X)
      (mark# from X -> active# from mark X, active# after(s N, cons(X, XS)) -> mark# after(N, XS))
      (mark# from X -> active# from mark X, active# after(s N, cons(X, XS)) -> after#(N, XS))
      (mark# from X -> active# from mark X, active# after(0(), XS) -> mark# XS)
     }
     EDG:
      {
       (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
       (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
       (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# 0() -> active# 0())
       (mark# s X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# s X -> active# s mark X)
       (mark# s X -> mark# X, mark# s X -> s# mark X)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# s X -> mark# X, mark# from X -> active# from mark X)
       (mark# s X -> mark# X, mark# from X -> from# mark X)
       (mark# s X -> mark# X, mark# from X -> mark# X)
       (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (from# active X -> from# X, from# active X -> from# X)
       (from# active X -> from# X, from# mark X -> from# X)
       (s# active X -> s# X, s# active X -> s# X)
       (s# active X -> s# X, s# mark X -> s# X)
       (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(active X1, X2) -> after#(X1, X2))
       (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(mark X1, X2) -> after#(X1, X2))
       (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, active X2) -> after#(X1, X2))
       (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, mark X2) -> after#(X1, X2))
       (mark# after(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
       (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
       (mark# after(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# after(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# after(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# after(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
       (mark# after(X1, X2) -> mark# X1, mark# from X -> from# mark X)
       (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(active X1, X2) -> after#(X1, X2))
       (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(mark X1, X2) -> after#(X1, X2))
       (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, active X2) -> after#(X1, X2))
       (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, mark X2) -> after#(X1, X2))
       (mark# after(X1, X2) -> mark# X2, mark# 0() -> active# 0())
       (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X2)
       (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X1)
       (mark# after(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
       (mark# after(X1, X2) -> mark# X2, mark# s X -> s# mark X)
       (mark# after(X1, X2) -> mark# X2, mark# s X -> mark# X)
       (mark# after(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
       (mark# after(X1, X2) -> mark# X2, mark# from X -> from# mark X)
       (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
       (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> s# mark X, s# active X -> s# X)
       (mark# s X -> s# mark X, s# mark X -> s# X)
       (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (after#(X1, mark X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
       (after#(X1, mark X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
       (after#(X1, mark X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
       (after#(X1, mark X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
       (after#(mark X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
       (after#(mark X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
       (after#(mark X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
       (after#(mark X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
       (after#(active X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
       (after#(active X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
       (after#(active X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
       (after#(active X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
       (after#(X1, active X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
       (after#(X1, active X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
       (after#(X1, active X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
       (after#(X1, active X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
       (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (mark# from X -> from# mark X, from# mark X -> from# X)
       (mark# from X -> from# mark X, from# active X -> from# X)
       (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X1)
       (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X2)
       (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> after#(mark X1, mark X2))
       (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
       (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (active# after(0(), XS) -> mark# XS, mark# from X -> mark# X)
       (active# after(0(), XS) -> mark# XS, mark# from X -> from# mark X)
       (active# after(0(), XS) -> mark# XS, mark# from X -> active# from mark X)
       (active# after(0(), XS) -> mark# XS, mark# s X -> mark# X)
       (active# after(0(), XS) -> mark# XS, mark# s X -> s# mark X)
       (active# after(0(), XS) -> mark# XS, mark# s X -> active# s mark X)
       (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
       (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
       (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (active# after(0(), XS) -> mark# XS, mark# 0() -> active# 0())
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (active# from X -> s# X, s# mark X -> s# X)
       (active# from X -> s# X, s# active X -> s# X)
       (s# mark X -> s# X, s# mark X -> s# X)
       (s# mark X -> s# X, s# active X -> s# X)
       (from# mark X -> from# X, from# mark X -> from# X)
       (from# mark X -> from# X, from# active X -> from# X)
       (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
       (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
       (mark# from X -> mark# X, mark# from X -> mark# X)
       (mark# from X -> mark# X, mark# from X -> from# mark X)
       (mark# from X -> mark# X, mark# from X -> active# from mark X)
       (mark# from X -> mark# X, mark# s X -> mark# X)
       (mark# from X -> mark# X, mark# s X -> s# mark X)
       (mark# from X -> mark# X, mark# s X -> active# s mark X)
       (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X1)
       (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X2)
       (mark# from X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
       (mark# from X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
       (mark# from X -> mark# X, mark# 0() -> active# 0())
       (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
       (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
       (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(0(), XS) -> mark# XS)
       (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
       (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
       (mark# from X -> active# from mark X, active# from X -> from# s X)
       (mark# from X -> active# from mark X, active# from X -> s# X)
      }
      EDG:
       {
        (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
        (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
        (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# 0() -> active# 0())
        (mark# s X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# after(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# s X -> active# s mark X)
        (mark# s X -> mark# X, mark# s X -> s# mark X)
        (mark# s X -> mark# X, mark# s X -> mark# X)
        (mark# s X -> mark# X, mark# from X -> active# from mark X)
        (mark# s X -> mark# X, mark# from X -> from# mark X)
        (mark# s X -> mark# X, mark# from X -> mark# X)
        (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (from# active X -> from# X, from# active X -> from# X)
        (from# active X -> from# X, from# mark X -> from# X)
        (s# active X -> s# X, s# active X -> s# X)
        (s# active X -> s# X, s# mark X -> s# X)
        (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(active X1, X2) -> after#(X1, X2))
        (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(mark X1, X2) -> after#(X1, X2))
        (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, active X2) -> after#(X1, X2))
        (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, mark X2) -> after#(X1, X2))
        (mark# after(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
        (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
        (mark# after(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# after(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# after(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# after(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
        (mark# after(X1, X2) -> mark# X1, mark# from X -> from# mark X)
        (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(active X1, X2) -> after#(X1, X2))
        (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(mark X1, X2) -> after#(X1, X2))
        (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, active X2) -> after#(X1, X2))
        (mark# after(X1, X2) -> after#(mark X1, mark X2), after#(X1, mark X2) -> after#(X1, X2))
        (mark# after(X1, X2) -> mark# X2, mark# 0() -> active# 0())
        (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X2)
        (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> mark# X1)
        (mark# after(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
        (mark# after(X1, X2) -> mark# X2, mark# s X -> s# mark X)
        (mark# after(X1, X2) -> mark# X2, mark# s X -> mark# X)
        (mark# after(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
        (mark# after(X1, X2) -> mark# X2, mark# from X -> from# mark X)
        (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
        (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (mark# s X -> s# mark X, s# active X -> s# X)
        (mark# s X -> s# mark X, s# mark X -> s# X)
        (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (after#(X1, mark X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
        (after#(X1, mark X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
        (after#(X1, mark X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
        (after#(X1, mark X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
        (after#(mark X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
        (after#(mark X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
        (after#(mark X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
        (after#(mark X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
        (after#(active X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
        (after#(active X1, X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
        (after#(active X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
        (after#(active X1, X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
        (after#(X1, active X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
        (after#(X1, active X2) -> after#(X1, X2), after#(X1, active X2) -> after#(X1, X2))
        (after#(X1, active X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
        (after#(X1, active X2) -> after#(X1, X2), after#(active X1, X2) -> after#(X1, X2))
        (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (mark# from X -> from# mark X, from# mark X -> from# X)
        (mark# from X -> from# mark X, from# active X -> from# X)
        (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X1)
        (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> mark# X2)
        (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (active# after(s N, cons(X, XS)) -> mark# after(N, XS), mark# after(X1, X2) -> after#(mark X1, mark X2))
        (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
        (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (active# after(0(), XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (active# after(0(), XS) -> mark# XS, mark# from X -> mark# X)
        (active# after(0(), XS) -> mark# XS, mark# from X -> from# mark X)
        (active# after(0(), XS) -> mark# XS, mark# from X -> active# from mark X)
        (active# after(0(), XS) -> mark# XS, mark# s X -> mark# X)
        (active# after(0(), XS) -> mark# XS, mark# s X -> s# mark X)
        (active# after(0(), XS) -> mark# XS, mark# s X -> active# s mark X)
        (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
        (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
        (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (active# after(0(), XS) -> mark# XS, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (active# after(0(), XS) -> mark# XS, mark# 0() -> active# 0())
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (active# from X -> s# X, s# mark X -> s# X)
        (active# from X -> s# X, s# active X -> s# X)
        (s# mark X -> s# X, s# mark X -> s# X)
        (s# mark X -> s# X, s# active X -> s# X)
        (from# mark X -> from# X, from# mark X -> from# X)
        (from# mark X -> from# X, from# active X -> from# X)
        (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
        (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
        (mark# from X -> mark# X, mark# from X -> mark# X)
        (mark# from X -> mark# X, mark# from X -> from# mark X)
        (mark# from X -> mark# X, mark# from X -> active# from mark X)
        (mark# from X -> mark# X, mark# s X -> mark# X)
        (mark# from X -> mark# X, mark# s X -> s# mark X)
        (mark# from X -> mark# X, mark# s X -> active# s mark X)
        (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X1)
        (mark# from X -> mark# X, mark# after(X1, X2) -> mark# X2)
        (mark# from X -> mark# X, mark# after(X1, X2) -> active# after(mark X1, mark X2))
        (mark# from X -> mark# X, mark# after(X1, X2) -> after#(mark X1, mark X2))
        (mark# from X -> mark# X, mark# 0() -> active# 0())
        (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> mark# after(N, XS))
        (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(s N, cons(X, XS)) -> after#(N, XS))
        (mark# after(X1, X2) -> active# after(mark X1, mark X2), active# after(0(), XS) -> mark# XS)
        (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
        (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
        (mark# from X -> active# from mark X, active# from X -> from# s X)
        (mark# from X -> active# from mark X, active# from X -> s# X)
       }
       STATUS:
        arrows: 0.854913
        SCCS (5):
         Scc:
          {             mark# cons(X1, X2) -> mark# X1,
                              mark# from X -> mark# X,
                              mark# from X -> active# from mark X,
                                 mark# s X -> mark# X,
                       mark# after(X1, X2) -> mark# X1,
                       mark# after(X1, X2) -> mark# X2,
                       mark# after(X1, X2) -> active# after(mark X1, mark X2),
                            active# from X -> mark# cons(X, from s X),
           active# after(s N, cons(X, XS)) -> mark# after(N, XS),
                    active# after(0(), XS) -> mark# XS}
         Scc:
          {  after#(X1, mark X2) -> after#(X1, X2),
           after#(X1, active X2) -> after#(X1, X2),
             after#(mark X1, X2) -> after#(X1, X2),
           after#(active X1, X2) -> after#(X1, X2)}
         Scc:
          {  s# mark X -> s# X,
           s# active X -> s# X}
         Scc:
          {  from# mark X -> from# X,
           from# active X -> from# X}
         Scc:
          {  cons#(X1, mark X2) -> cons#(X1, X2),
           cons#(X1, active X2) -> cons#(X1, X2),
             cons#(mark X1, X2) -> cons#(X1, X2),
           cons#(active X1, X2) -> cons#(X1, X2)}
         
         SCC (10):
          Strict:
           {             mark# cons(X1, X2) -> mark# X1,
                               mark# from X -> mark# X,
                               mark# from X -> active# from mark X,
                                  mark# s X -> mark# X,
                        mark# after(X1, X2) -> mark# X1,
                        mark# after(X1, X2) -> mark# X2,
                        mark# after(X1, X2) -> active# after(mark X1, mark X2),
                             active# from X -> mark# cons(X, from s X),
            active# after(s N, cons(X, XS)) -> mark# after(N, XS),
                     active# after(0(), XS) -> mark# XS}
          Weak:
          {             mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark after(X1, X2) -> active after(mark X1, mark X2),
                                 mark 0() -> active 0(),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                            active from X -> mark cons(X, from s X),
           active after(s N, cons(X, XS)) -> mark after(N, XS),
                    active after(0(), XS) -> mark XS,
                       after(X1, mark X2) -> after(X1, X2),
                     after(X1, active X2) -> after(X1, X2),
                       after(mark X1, X2) -> after(X1, X2),
                     after(active X1, X2) -> after(X1, X2)}
          Open
         
         
         
         
         
         
         SCC (4):
          Strict:
           {  after#(X1, mark X2) -> after#(X1, X2),
            after#(X1, active X2) -> after#(X1, X2),
              after#(mark X1, X2) -> after#(X1, X2),
            after#(active X1, X2) -> after#(X1, X2)}
          Weak:
          {             mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark after(X1, X2) -> active after(mark X1, mark X2),
                                 mark 0() -> active 0(),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                            active from X -> mark cons(X, from s X),
           active after(s N, cons(X, XS)) -> mark after(N, XS),
                    active after(0(), XS) -> mark XS,
                       after(X1, mark X2) -> after(X1, X2),
                     after(X1, active X2) -> after(X1, X2),
                       after(mark X1, X2) -> after(X1, X2),
                     after(active X1, X2) -> after(X1, X2)}
          Open
         
         
         SCC (2):
          Strict:
           {  s# mark X -> s# X,
            s# active X -> s# X}
          Weak:
          {             mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark after(X1, X2) -> active after(mark X1, mark X2),
                                 mark 0() -> active 0(),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                            active from X -> mark cons(X, from s X),
           active after(s N, cons(X, XS)) -> mark after(N, XS),
                    active after(0(), XS) -> mark XS,
                       after(X1, mark X2) -> after(X1, X2),
                     after(X1, active X2) -> after(X1, X2),
                       after(mark X1, X2) -> after(X1, X2),
                     after(active X1, X2) -> after(X1, X2)}
          Open
         
         SCC (2):
          Strict:
           {  from# mark X -> from# X,
            from# active X -> from# X}
          Weak:
          {             mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark after(X1, X2) -> active after(mark X1, mark X2),
                                 mark 0() -> active 0(),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                            active from X -> mark cons(X, from s X),
           active after(s N, cons(X, XS)) -> mark after(N, XS),
                    active after(0(), XS) -> mark XS,
                       after(X1, mark X2) -> after(X1, X2),
                     after(X1, active X2) -> after(X1, X2),
                       after(mark X1, X2) -> after(X1, X2),
                     after(active X1, X2) -> after(X1, X2)}
          Open
         
         
         SCC (4):
          Strict:
           {  cons#(X1, mark X2) -> cons#(X1, X2),
            cons#(X1, active X2) -> cons#(X1, X2),
              cons#(mark X1, X2) -> cons#(X1, X2),
            cons#(active X1, X2) -> cons#(X1, X2)}
          Weak:
          {             mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark after(X1, X2) -> active after(mark X1, mark X2),
                                 mark 0() -> active 0(),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                            active from X -> mark cons(X, from s X),
           active after(s N, cons(X, XS)) -> mark after(N, XS),
                    active after(0(), XS) -> mark XS,
                       after(X1, mark X2) -> after(X1, X2),
                     after(X1, active X2) -> after(X1, X2),
                       after(mark X1, X2) -> after(X1, X2),
                     after(active X1, X2) -> after(X1, X2)}
          Open