MAYBE
Time: 0.135507
TRS:
 {         mark cons(X1, X2) -> cons(mark X1, X2),
                 mark from X -> a__from mark X,
                    mark s X -> s mark X,
                    mark 0() -> 0(),
          mark after(X1, X2) -> a__after(mark X1, mark X2),
                   a__from X -> cons(mark X, from s X),
                   a__from X -> from X,
            a__after(X1, X2) -> after(X1, X2),
  a__after(s N, cons(X, XS)) -> a__after(mark N, mark XS),
           a__after(0(), XS) -> mark XS}
 DP:
  DP:
   {         mark# cons(X1, X2) -> mark# X1,
                   mark# from X -> mark# X,
                   mark# from X -> a__from# mark X,
                      mark# s X -> mark# X,
            mark# after(X1, X2) -> mark# X1,
            mark# after(X1, X2) -> mark# X2,
            mark# after(X1, X2) -> a__after#(mark X1, mark X2),
                     a__from# X -> mark# X,
    a__after#(s N, cons(X, XS)) -> mark# XS,
    a__after#(s N, cons(X, XS)) -> mark# N,
    a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS),
             a__after#(0(), XS) -> mark# XS}
  TRS:
  {         mark cons(X1, X2) -> cons(mark X1, X2),
                  mark from X -> a__from mark X,
                     mark s X -> s mark X,
                     mark 0() -> 0(),
           mark after(X1, X2) -> a__after(mark X1, mark X2),
                    a__from X -> cons(mark X, from s X),
                    a__from X -> from X,
             a__after(X1, X2) -> after(X1, X2),
   a__after(s N, cons(X, XS)) -> a__after(mark N, mark XS),
            a__after(0(), XS) -> mark XS}
  UR:
   {         mark cons(X1, X2) -> cons(mark X1, X2),
                   mark from X -> a__from mark X,
                      mark s X -> s mark X,
                      mark 0() -> 0(),
            mark after(X1, X2) -> a__after(mark X1, mark X2),
                     a__from X -> cons(mark X, from s X),
                     a__from X -> from X,
              a__after(X1, X2) -> after(X1, X2),
    a__after(s N, cons(X, XS)) -> a__after(mark N, mark XS),
             a__after(0(), XS) -> mark XS}
   EDG:
    {(a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X2)
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X1)
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# s X -> mark# X)
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> a__from# mark X)
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> mark# X)
     (a__after#(s N, cons(X, XS)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X2)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X1)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# s X -> mark# X)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> a__from# mark X)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> mark# X)
     (a__after#(s N, cons(X, XS)) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> a__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 -> mark# X)
     (mark# after(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# after(X1, X2) -> a__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 -> mark# X)
     (mark# s X -> mark# X, mark# from X -> a__from# mark X)
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__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 -> mark# X)
     (mark# after(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> a__from# mark X, a__from# X -> mark# X)
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> a__from# mark X)
     (mark# from X -> mark# X, mark# s X -> 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) -> a__after#(mark X1, mark X2))
     (a__after#(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__after#(0(), XS) -> mark# XS, mark# from X -> mark# X)
     (a__after#(0(), XS) -> mark# XS, mark# from X -> a__from# mark X)
     (a__after#(0(), XS) -> mark# XS, mark# s X -> mark# X)
     (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
     (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
     (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
     (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# XS)
     (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# N)
     (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
     (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(0(), XS) -> mark# XS)
     (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# XS)
     (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# N)
     (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
     (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(0(), XS) -> mark# XS)}
    EDG:
     {(a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X2)
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X1)
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# s X -> mark# X)
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> a__from# mark X)
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> mark# X)
      (a__after#(s N, cons(X, XS)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X2)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X1)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# s X -> mark# X)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> a__from# mark X)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> mark# X)
      (a__after#(s N, cons(X, XS)) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
      (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> a__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 -> mark# X)
      (mark# after(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
      (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
      (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# after(X1, X2) -> a__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 -> mark# X)
      (mark# s X -> mark# X, mark# from X -> a__from# mark X)
      (mark# s X -> mark# X, mark# from X -> mark# X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__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 -> mark# X)
      (mark# after(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
      (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# from X -> a__from# mark X, a__from# X -> mark# X)
      (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__from# X -> mark# X, mark# from X -> mark# X)
      (a__from# X -> mark# X, mark# from X -> a__from# mark X)
      (a__from# X -> mark# X, mark# s X -> mark# X)
      (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X1)
      (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X2)
      (a__from# X -> mark# X, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
      (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# from X -> mark# X, mark# from X -> mark# X)
      (mark# from X -> mark# X, mark# from X -> a__from# mark X)
      (mark# from X -> mark# X, mark# s X -> 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) -> a__after#(mark X1, mark X2))
      (a__after#(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
      (a__after#(0(), XS) -> mark# XS, mark# from X -> mark# X)
      (a__after#(0(), XS) -> mark# XS, mark# from X -> a__from# mark X)
      (a__after#(0(), XS) -> mark# XS, mark# s X -> mark# X)
      (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
      (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
      (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
      (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# XS)
      (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# N)
      (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
      (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(0(), XS) -> mark# XS)
      (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# XS)
      (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# N)
      (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
      (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(0(), XS) -> mark# XS)}
     EDG:
      {(a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X2)
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X1)
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# s X -> mark# X)
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> a__from# mark X)
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> mark# X)
       (a__after#(s N, cons(X, XS)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X2)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X1)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# s X -> mark# X)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> a__from# mark X)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> mark# X)
       (a__after#(s N, cons(X, XS)) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
       (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> a__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 -> mark# X)
       (mark# after(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
       (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
       (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# after(X1, X2) -> a__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 -> mark# X)
       (mark# s X -> mark# X, mark# from X -> a__from# mark X)
       (mark# s X -> mark# X, mark# from X -> mark# X)
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__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 -> mark# X)
       (mark# after(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
       (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# from X -> a__from# mark X, a__from# X -> mark# X)
       (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__from# X -> mark# X, mark# from X -> mark# X)
       (a__from# X -> mark# X, mark# from X -> a__from# mark X)
       (a__from# X -> mark# X, mark# s X -> mark# X)
       (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X1)
       (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X2)
       (a__from# X -> mark# X, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
       (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# from X -> mark# X, mark# from X -> mark# X)
       (mark# from X -> mark# X, mark# from X -> a__from# mark X)
       (mark# from X -> mark# X, mark# s X -> 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) -> a__after#(mark X1, mark X2))
       (a__after#(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
       (a__after#(0(), XS) -> mark# XS, mark# from X -> mark# X)
       (a__after#(0(), XS) -> mark# XS, mark# from X -> a__from# mark X)
       (a__after#(0(), XS) -> mark# XS, mark# s X -> mark# X)
       (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
       (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
       (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
       (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# XS)
       (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# N)
       (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
       (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(0(), XS) -> mark# XS)
       (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# XS)
       (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# N)
       (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
       (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(0(), XS) -> mark# XS)}
      EDG:
       {(a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X2)
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# after(X1, X2) -> mark# X1)
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# s X -> mark# X)
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> a__from# mark X)
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# from X -> mark# X)
        (a__after#(s N, cons(X, XS)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X2)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# after(X1, X2) -> mark# X1)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# s X -> mark# X)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> a__from# mark X)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# from X -> mark# X)
        (a__after#(s N, cons(X, XS)) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
        (mark# after(X1, X2) -> mark# X2, mark# after(X1, X2) -> a__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 -> mark# X)
        (mark# after(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
        (mark# after(X1, X2) -> mark# X2, mark# from X -> mark# X)
        (mark# after(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# after(X1, X2) -> a__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 -> mark# X)
        (mark# s X -> mark# X, mark# from X -> a__from# mark X)
        (mark# s X -> mark# X, mark# from X -> mark# X)
        (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# after(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# after(X1, X2) -> mark# X1, mark# after(X1, X2) -> a__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 -> mark# X)
        (mark# after(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
        (mark# after(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# after(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# from X -> a__from# mark X, a__from# X -> mark# X)
        (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (a__from# X -> mark# X, mark# from X -> mark# X)
        (a__from# X -> mark# X, mark# from X -> a__from# mark X)
        (a__from# X -> mark# X, mark# s X -> mark# X)
        (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X1)
        (a__from# X -> mark# X, mark# after(X1, X2) -> mark# X2)
        (a__from# X -> mark# X, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
        (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# from X -> mark# X, mark# from X -> mark# X)
        (mark# from X -> mark# X, mark# from X -> a__from# mark X)
        (mark# from X -> mark# X, mark# s X -> 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) -> a__after#(mark X1, mark X2))
        (a__after#(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
        (a__after#(0(), XS) -> mark# XS, mark# from X -> mark# X)
        (a__after#(0(), XS) -> mark# XS, mark# from X -> a__from# mark X)
        (a__after#(0(), XS) -> mark# XS, mark# s X -> mark# X)
        (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X1)
        (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> mark# X2)
        (a__after#(0(), XS) -> mark# XS, mark# after(X1, X2) -> a__after#(mark X1, mark X2))
        (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# XS)
        (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> mark# N)
        (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
        (a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS), a__after#(0(), XS) -> mark# XS)
        (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# XS)
        (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> mark# N)
        (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS))
        (mark# after(X1, X2) -> a__after#(mark X1, mark X2), a__after#(0(), XS) -> mark# XS)}
       STATUS:
        arrows: 0.500000
        SCCS (1):
         Scc:
          {         mark# cons(X1, X2) -> mark# X1,
                          mark# from X -> mark# X,
                          mark# from X -> a__from# mark X,
                             mark# s X -> mark# X,
                   mark# after(X1, X2) -> mark# X1,
                   mark# after(X1, X2) -> mark# X2,
                   mark# after(X1, X2) -> a__after#(mark X1, mark X2),
                            a__from# X -> mark# X,
           a__after#(s N, cons(X, XS)) -> mark# XS,
           a__after#(s N, cons(X, XS)) -> mark# N,
           a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS),
                    a__after#(0(), XS) -> mark# XS}
         
         SCC (12):
          Strict:
           {         mark# cons(X1, X2) -> mark# X1,
                           mark# from X -> mark# X,
                           mark# from X -> a__from# mark X,
                              mark# s X -> mark# X,
                    mark# after(X1, X2) -> mark# X1,
                    mark# after(X1, X2) -> mark# X2,
                    mark# after(X1, X2) -> a__after#(mark X1, mark X2),
                             a__from# X -> mark# X,
            a__after#(s N, cons(X, XS)) -> mark# XS,
            a__after#(s N, cons(X, XS)) -> mark# N,
            a__after#(s N, cons(X, XS)) -> a__after#(mark N, mark XS),
                     a__after#(0(), XS) -> mark# XS}
          Weak:
          {         mark cons(X1, X2) -> cons(mark X1, X2),
                          mark from X -> a__from mark X,
                             mark s X -> s mark X,
                             mark 0() -> 0(),
                   mark after(X1, X2) -> a__after(mark X1, mark X2),
                            a__from X -> cons(mark X, from s X),
                            a__from X -> from X,
                     a__after(X1, X2) -> after(X1, X2),
           a__after(s N, cons(X, XS)) -> a__after(mark N, mark XS),
                    a__after(0(), XS) -> mark XS}
          Open