MAYBE
Time: 2.404579
TRS:
 {  mark cons(X1, X2) -> active cons(mark X1, X2),
             mark 0() -> active 0(),
             mark f X -> active f mark X,
             mark s X -> active s mark X,
             mark p X -> active p mark X,
    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),
             f mark X -> f X,
           f active X -> f X,
             s mark X -> s X,
           s active X -> s X,
         active f 0() -> mark cons(0(), f s 0()),
       active f s 0() -> mark f p s 0(),
         active p s X -> mark X,
             p mark X -> p X,
           p active X -> p X}
 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# 0() -> active# 0(),
               mark# f X -> mark# X,
               mark# f X -> f# mark X,
               mark# f X -> active# f mark X,
               mark# s X -> mark# X,
               mark# s X -> s# mark X,
               mark# s X -> active# s mark X,
               mark# p X -> mark# X,
               mark# p X -> active# p mark X,
               mark# p X -> p# mark X,
      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),
               f# mark X -> f# X,
             f# active X -> f# X,
               s# mark X -> s# X,
             s# active X -> s# X,
           active# f 0() -> mark# cons(0(), f s 0()),
           active# f 0() -> cons#(0(), f s 0()),
           active# f 0() -> f# s 0(),
           active# f 0() -> s# 0(),
         active# f s 0() -> mark# f p s 0(),
         active# f s 0() -> f# p s 0(),
         active# f s 0() -> p# s 0(),
           active# p s X -> mark# X,
               p# mark X -> p# X,
             p# active X -> p# X}
  TRS:
  {  mark cons(X1, X2) -> active cons(mark X1, X2),
              mark 0() -> active 0(),
              mark f X -> active f mark X,
              mark s X -> active s mark X,
              mark p X -> active p mark X,
     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),
              f mark X -> f X,
            f active X -> f X,
              s mark X -> s X,
            s active X -> s X,
          active f 0() -> mark cons(0(), f s 0()),
        active f s 0() -> mark f p s 0(),
          active p s X -> mark X,
              p mark X -> p X,
            p active X -> p X}
  EDG:
   {(active# f s 0() -> mark# f p s 0(), mark# f X -> active# f mark X)
    (active# f s 0() -> mark# f p s 0(), mark# f X -> f# mark X)
    (active# f s 0() -> mark# f p s 0(), mark# f X -> mark# X)
    (mark# f X -> active# f mark X, active# f s 0() -> p# s 0())
    (mark# f X -> active# f mark X, active# f s 0() -> f# p s 0())
    (mark# f X -> active# f mark X, active# f s 0() -> mark# f p s 0())
    (mark# f X -> active# f mark X, active# f 0() -> s# 0())
    (mark# f X -> active# f mark X, active# f 0() -> f# s 0())
    (mark# f X -> active# f mark X, active# f 0() -> cons#(0(), f s 0()))
    (mark# f X -> active# f mark X, active# f 0() -> mark# cons(0(), f s 0()))
    (mark# p X -> active# p mark X, active# p s X -> mark# X)
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (active# f 0() -> mark# cons(0(), f s 0()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# f 0() -> mark# cons(0(), f s 0()), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# f 0() -> mark# cons(0(), f s 0()), mark# cons(X1, X2) -> mark# X1)
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (mark# s X -> mark# X, mark# p X -> p# mark X)
    (mark# s X -> mark# X, mark# p X -> active# p mark X)
    (mark# s X -> mark# X, mark# p X -> mark# X)
    (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# f X -> active# f mark X)
    (mark# s X -> mark# X, mark# f X -> f# mark X)
    (mark# s X -> mark# X, mark# f X -> mark# X)
    (mark# s X -> mark# X, mark# 0() -> active# 0())
    (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)
    (f# mark X -> f# X, f# active X -> f# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (active# p s X -> mark# X, mark# p X -> p# mark X)
    (active# p s X -> mark# X, mark# p X -> active# p mark X)
    (active# p s X -> mark# X, mark# p X -> mark# X)
    (active# p s X -> mark# X, mark# s X -> active# s mark X)
    (active# p s X -> mark# X, mark# s X -> s# mark X)
    (active# p s X -> mark# X, mark# s X -> mark# X)
    (active# p s X -> mark# X, mark# f X -> active# f mark X)
    (active# p s X -> mark# X, mark# f X -> f# mark X)
    (active# p s X -> mark# X, mark# f X -> mark# X)
    (active# p s X -> mark# X, mark# 0() -> active# 0())
    (active# p s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# p s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# p s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (p# active X -> p# X, p# active X -> p# X)
    (p# active X -> p# X, p# mark X -> p# X)
    (mark# s X -> s# mark X, s# active X -> s# X)
    (mark# s X -> s# mark X, s# mark X -> s# X)
    (mark# p X -> p# mark X, p# mark X -> p# X)
    (mark# p X -> p# mark X, p# active X -> p# X)
    (mark# f X -> f# mark X, f# mark X -> f# X)
    (mark# f X -> f# mark X, f# active X -> f# X)
    (p# mark X -> p# X, p# mark X -> p# X)
    (p# mark X -> p# X, p# active X -> p# X)
    (s# active X -> s# X, s# mark X -> s# X)
    (s# active X -> s# X, s# active X -> s# X)
    (f# active X -> f# X, f# mark X -> f# X)
    (f# active X -> f# X, f# active X -> f# X)
    (mark# p X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# p X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# p X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# p X -> mark# X, mark# 0() -> active# 0())
    (mark# p X -> mark# X, mark# f X -> mark# X)
    (mark# p X -> mark# X, mark# f X -> f# mark X)
    (mark# p X -> mark# X, mark# f X -> active# f mark X)
    (mark# p X -> mark# X, mark# s X -> mark# X)
    (mark# p X -> mark# X, mark# s X -> s# mark X)
    (mark# p X -> mark# X, mark# s X -> active# s mark X)
    (mark# p X -> mark# X, mark# p X -> mark# X)
    (mark# p X -> mark# X, mark# p X -> active# p mark X)
    (mark# p X -> mark# X, mark# p X -> p# mark X)
    (mark# f X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# f X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# f X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# f X -> mark# X, mark# 0() -> active# 0())
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> f# mark X)
    (mark# f X -> mark# X, mark# f X -> active# f mark X)
    (mark# f X -> mark# X, mark# s X -> mark# X)
    (mark# f X -> mark# X, mark# s X -> s# mark X)
    (mark# f X -> mark# X, mark# s X -> active# s mark X)
    (mark# f X -> mark# X, mark# p X -> mark# X)
    (mark# f X -> mark# X, mark# p X -> active# p mark X)
    (mark# f X -> mark# X, mark# p X -> p# mark X)
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(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# 0() -> active# 0())
    (mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# f X -> f# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# f X -> active# f 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# p X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# p X -> active# p mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# p X -> p# mark X)}
   STATUS:
    arrows: 0.878252
    SCCS (5):
     Scc:
      {mark# cons(X1, X2) -> mark# X1,
                mark# f X -> mark# X,
                mark# f X -> active# f mark X,
                mark# s X -> mark# X,
                mark# p X -> mark# X,
                mark# p X -> active# p mark X,
            active# f 0() -> mark# cons(0(), f s 0()),
          active# f s 0() -> mark# f p s 0(),
            active# p s X -> mark# X}
     Scc:
      {  p# mark X -> p# X,
       p# active X -> p# X}
     Scc:
      {  s# mark X -> s# X,
       s# active X -> s# X}
     Scc:
      {  f# mark X -> f# X,
       f# active X -> f# 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 (9):
      Strict:
       {mark# cons(X1, X2) -> mark# X1,
                 mark# f X -> mark# X,
                 mark# f X -> active# f mark X,
                 mark# s X -> mark# X,
                 mark# p X -> mark# X,
                 mark# p X -> active# p mark X,
             active# f 0() -> mark# cons(0(), f s 0()),
           active# f s 0() -> mark# f p s 0(),
             active# p s X -> mark# X}
      Weak:
      {  mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
                  mark f X -> active f mark X,
                  mark s X -> active s mark X,
                  mark p X -> active p mark X,
         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),
                  f mark X -> f X,
                f active X -> f X,
                  s mark X -> s X,
                s active X -> s X,
              active f 0() -> mark cons(0(), f s 0()),
            active f s 0() -> mark f p s 0(),
              active p s X -> mark X,
                  p mark X -> p X,
                p active X -> p X}
      Open
     
     SCC (2):
      Strict:
       {  p# mark X -> p# X,
        p# active X -> p# X}
      Weak:
      {  mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
                  mark f X -> active f mark X,
                  mark s X -> active s mark X,
                  mark p X -> active p mark X,
         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),
                  f mark X -> f X,
                f active X -> f X,
                  s mark X -> s X,
                s active X -> s X,
              active f 0() -> mark cons(0(), f s 0()),
            active f s 0() -> mark f p s 0(),
              active p s X -> mark X,
                  p mark X -> p X,
                p active X -> p X}
      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 0() -> active 0(),
                  mark f X -> active f mark X,
                  mark s X -> active s mark X,
                  mark p X -> active p mark X,
         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),
                  f mark X -> f X,
                f active X -> f X,
                  s mark X -> s X,
                s active X -> s X,
              active f 0() -> mark cons(0(), f s 0()),
            active f s 0() -> mark f p s 0(),
              active p s X -> mark X,
                  p mark X -> p X,
                p active X -> p X}
      Open
     
     
     
     
     
     SCC (2):
      Strict:
       {  f# mark X -> f# X,
        f# active X -> f# X}
      Weak:
      {  mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
                  mark f X -> active f mark X,
                  mark s X -> active s mark X,
                  mark p X -> active p mark X,
         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),
                  f mark X -> f X,
                f active X -> f X,
                  s mark X -> s X,
                s active X -> s X,
              active f 0() -> mark cons(0(), f s 0()),
            active f s 0() -> mark f p s 0(),
              active p s X -> mark X,
                  p mark X -> p X,
                p active X -> p X}
      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 0() -> active 0(),
                  mark f X -> active f mark X,
                  mark s X -> active s mark X,
                  mark p X -> active p mark X,
         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),
                  f mark X -> f X,
                f active X -> f X,
                  s mark X -> s X,
                s active X -> s X,
              active f 0() -> mark cons(0(), f s 0()),
            active f s 0() -> mark f p s 0(),
              active p s X -> mark X,
                  p mark X -> p X,
                p active X -> p X}
      Open