MAYBE
Time: 0.004572
TRS:
 {           a__f X -> f X,
           a__f 0() -> cons(0(), f s 0()),
         a__f s 0() -> a__f a__p s 0(),
             a__p X -> p X,
           a__p s X -> mark X,
  mark cons(X1, X2) -> cons(mark X1, X2),
           mark 0() -> 0(),
           mark f X -> a__f mark X,
           mark s X -> s mark X,
           mark p X -> a__p mark X}
 DP:
  DP:
   {       a__f# s 0() -> a__f# a__p s 0(),
           a__f# s 0() -> a__p# s 0(),
             a__p# s X -> mark# X,
    mark# cons(X1, X2) -> mark# X1,
             mark# f X -> a__f# mark X,
             mark# f X -> mark# X,
             mark# s X -> mark# X,
             mark# p X -> a__p# mark X,
             mark# p X -> mark# X}
  TRS:
  {           a__f X -> f X,
            a__f 0() -> cons(0(), f s 0()),
          a__f s 0() -> a__f a__p s 0(),
              a__p X -> p X,
            a__p s X -> mark X,
   mark cons(X1, X2) -> cons(mark X1, X2),
            mark 0() -> 0(),
            mark f X -> a__f mark X,
            mark s X -> s mark X,
            mark p X -> a__p mark X}
  UR:
   {           a__f X -> f X,
             a__f 0() -> cons(0(), f s 0()),
           a__f s 0() -> a__f a__p s 0(),
               a__p X -> p X,
             a__p s X -> mark X,
    mark cons(X1, X2) -> cons(mark X1, X2),
             mark 0() -> 0(),
             mark f X -> a__f mark X,
             mark s X -> s mark X,
             mark p X -> a__p mark X}
   EDG:
    {(mark# f X -> mark# X, mark# p X -> mark# X)
     (mark# f X -> mark# X, mark# p X -> a__p# mark X)
     (mark# f X -> mark# X, mark# s X -> mark# X)
     (mark# f X -> mark# X, mark# f X -> mark# X)
     (mark# f X -> mark# X, mark# f X -> a__f# mark X)
     (mark# f X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# p X -> mark# X, mark# p X -> mark# X)
     (mark# p X -> mark# X, mark# p X -> a__p# mark X)
     (mark# p X -> mark# X, mark# s X -> mark# X)
     (mark# p X -> mark# X, mark# f X -> mark# X)
     (mark# p X -> mark# X, mark# f X -> a__f# mark X)
     (mark# p X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__f# s 0() -> a__p# s 0(), a__p# s X -> mark# X)
     (mark# p X -> a__p# mark X, a__p# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# f X -> a__f# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# f X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# p X -> mark# X)
     (mark# f X -> a__f# mark X, a__f# s 0() -> a__f# a__p s 0())
     (mark# f X -> a__f# mark X, a__f# s 0() -> a__p# s 0())
     (a__f# s 0() -> a__f# a__p s 0(), a__f# s 0() -> a__f# a__p s 0())
     (a__f# s 0() -> a__f# a__p s 0(), a__f# s 0() -> a__p# s 0())
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# f X -> a__f# mark X)
     (mark# s X -> mark# X, mark# f X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# p X -> a__p# mark X)
     (mark# s X -> mark# X, mark# p X -> mark# X)
     (a__p# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__p# s X -> mark# X, mark# f X -> a__f# mark X)
     (a__p# s X -> mark# X, mark# f X -> mark# X)
     (a__p# s X -> mark# X, mark# s X -> mark# X)
     (a__p# s X -> mark# X, mark# p X -> a__p# mark X)
     (a__p# s X -> mark# X, mark# p X -> mark# X)}
    STATUS:
     arrows: 0.555556
     SCCS (1):
      Scc:
       {       a__f# s 0() -> a__f# a__p s 0(),
               a__f# s 0() -> a__p# s 0(),
                 a__p# s X -> mark# X,
        mark# cons(X1, X2) -> mark# X1,
                 mark# f X -> a__f# mark X,
                 mark# f X -> mark# X,
                 mark# s X -> mark# X,
                 mark# p X -> a__p# mark X,
                 mark# p X -> mark# X}
      
      SCC (9):
       Strict:
        {       a__f# s 0() -> a__f# a__p s 0(),
                a__f# s 0() -> a__p# s 0(),
                  a__p# s X -> mark# X,
         mark# cons(X1, X2) -> mark# X1,
                  mark# f X -> a__f# mark X,
                  mark# f X -> mark# X,
                  mark# s X -> mark# X,
                  mark# p X -> a__p# mark X,
                  mark# p X -> mark# X}
       Weak:
       {           a__f X -> f X,
                 a__f 0() -> cons(0(), f s 0()),
               a__f s 0() -> a__f a__p s 0(),
                   a__p X -> p X,
                 a__p s X -> mark X,
        mark cons(X1, X2) -> cons(mark X1, X2),
                 mark 0() -> 0(),
                 mark f X -> a__f mark X,
                 mark s X -> s mark X,
                 mark p X -> a__p mark X}
       Open