MAYBE
Time: 0.014204
TRS:
 {      mark cons(X1, X2) -> active cons(mark X1, X2),
                 mark 0() -> active 0(),
             mark zeros() -> active zeros(),
              mark tail X -> active tail 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),
           active zeros() -> mark cons(0(), zeros()),
  active tail cons(X, XS) -> mark XS,
              tail mark X -> tail X,
            tail active X -> tail 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# zeros() -> active# zeros(),
                mark# tail X -> mark# X,
                mark# tail X -> active# tail mark X,
                mark# tail X -> tail# 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),
             active# zeros() -> mark# cons(0(), zeros()),
             active# zeros() -> cons#(0(), zeros()),
    active# tail cons(X, XS) -> mark# XS,
                tail# mark X -> tail# X,
              tail# active X -> tail# X}
  TRS:
  {      mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
              mark zeros() -> active zeros(),
               mark tail X -> active tail 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),
            active zeros() -> mark cons(0(), zeros()),
   active tail cons(X, XS) -> mark XS,
               tail mark X -> tail X,
             tail active X -> tail X}
  UR:
   {      mark cons(X1, X2) -> active cons(mark X1, X2),
                   mark 0() -> active 0(),
               mark zeros() -> active zeros(),
                mark tail X -> active tail 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),
             active zeros() -> mark cons(0(), zeros()),
    active tail cons(X, XS) -> mark XS,
                tail mark X -> tail X,
              tail active X -> tail X}
   EDG:
    {(mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
     (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# tail X -> tail# mark X, tail# active X -> tail# X)
     (mark# tail X -> tail# mark X, tail# mark X -> tail# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# tail X -> tail# mark X)
     (mark# tail X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# zeros() -> active# zeros())
     (mark# tail X -> mark# X, mark# 0() -> active# 0())
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (tail# active X -> tail# X, tail# active X -> tail# X)
     (tail# active X -> tail# X, tail# mark X -> tail# X)
     (mark# tail X -> active# tail mark X, active# tail cons(X, XS) -> mark# XS)
     (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# cons(X1, X2) -> active# cons(mark X1, X2), active# tail cons(X, XS) -> mark# XS)
     (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))
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# tail cons(X, XS) -> mark# XS, mark# 0() -> active# 0())
     (active# tail cons(X, XS) -> mark# XS, mark# zeros() -> active# zeros())
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> mark# X)
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> active# tail mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> tail# mark X)
     (tail# mark X -> tail# X, tail# mark X -> tail# X)
     (tail# mark X -> tail# X, tail# active X -> tail# X)
     (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# zeros() -> active# zeros())
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X)
     (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))}
    STATUS:
     arrows: 0.809689
     SCCS (3):
      Scc:
       {      mark# cons(X1, X2) -> mark# X1,
              mark# cons(X1, X2) -> active# cons(mark X1, X2),
                   mark# zeros() -> active# zeros(),
                    mark# tail X -> mark# X,
                    mark# tail X -> active# tail mark X,
                 active# zeros() -> mark# cons(0(), zeros()),
        active# tail cons(X, XS) -> mark# XS}
      Scc:
       {  tail# mark X -> tail# X,
        tail# active X -> tail# 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 (7):
       Strict:
        {      mark# cons(X1, X2) -> mark# X1,
               mark# cons(X1, X2) -> active# cons(mark X1, X2),
                    mark# zeros() -> active# zeros(),
                     mark# tail X -> mark# X,
                     mark# tail X -> active# tail mark X,
                  active# zeros() -> mark# cons(0(), zeros()),
         active# tail cons(X, XS) -> mark# XS}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
                    mark tail X -> active tail 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),
                 active zeros() -> mark cons(0(), zeros()),
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      
      SCC (2):
       Strict:
        {  tail# mark X -> tail# X,
         tail# active X -> tail# X}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
                    mark tail X -> active tail 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),
                 active zeros() -> mark cons(0(), zeros()),
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> tail X,
                  tail active X -> tail 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 zeros() -> active zeros(),
                    mark tail X -> active tail 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),
                 active zeros() -> mark cons(0(), zeros()),
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open