YES
Time: 2.384889
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 0() -> mark 0(),
             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 0() -> mark# 0(),
               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 0() -> mark 0(),
              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 0() -> mark# 0())
    (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))
    (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))
    (mark# f X -> mark# X, mark# p X -> p# mark X)
    (mark# f X -> mark# X, mark# p X -> active# p mark X)
    (mark# f X -> mark# X, mark# p X -> mark# X)
    (mark# f X -> mark# X, mark# s X -> active# s mark X)
    (mark# f X -> mark# X, mark# s X -> s# mark X)
    (mark# f X -> mark# X, mark# s X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> active# f mark X)
    (mark# f X -> mark# X, mark# f X -> f# mark X)
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# 0() -> active# 0())
    (mark# f X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# f X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# f X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# p X -> mark# X, mark# p X -> p# mark X)
    (mark# p X -> mark# X, mark# p X -> active# p mark X)
    (mark# p X -> mark# X, mark# p X -> mark# X)
    (mark# p X -> mark# X, mark# s X -> active# s mark X)
    (mark# p X -> mark# X, mark# s X -> s# mark X)
    (mark# p X -> mark# X, mark# s X -> mark# X)
    (mark# p X -> mark# X, mark# f X -> active# f mark X)
    (mark# p X -> mark# X, mark# f X -> f# mark X)
    (mark# p X -> mark# X, mark# f X -> mark# X)
    (mark# p X -> mark# X, mark# 0() -> active# 0())
    (mark# p X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# p X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# p X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (f# active X -> f# X, f# active X -> f# X)
    (f# active X -> f# X, f# mark X -> f# X)
    (s# active X -> s# X, s# active X -> s# X)
    (s# active X -> s# X, s# mark X -> s# X)
    (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# mark X -> s# X, s# mark X -> s# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (f# mark X -> f# X, f# active X -> f# X)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# s X -> mark# X, mark# 0() -> active# 0())
    (mark# s X -> mark# X, mark# f X -> mark# X)
    (mark# s X -> mark# X, mark# f X -> f# mark X)
    (mark# s X -> mark# X, mark# f X -> active# f mark X)
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# s X -> s# mark X)
    (mark# s X -> mark# X, mark# s X -> active# s mark X)
    (mark# s X -> mark# X, mark# p X -> mark# X)
    (mark# s X -> mark# X, mark# p X -> active# p mark X)
    (mark# s X -> mark# X, mark# p X -> p# mark X)
    (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# f 0() -> mark# cons(0(), f s 0()), mark# cons(X1, X2) -> mark# X1)
    (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) -> active# cons(mark X1, X2))
    (active# p s 0() -> mark# 0(), mark# 0() -> active# 0())
    (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.890739
    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,
            active# f 0() -> mark# cons(0(), f s 0()),
          active# f s 0() -> mark# f p s 0()}
     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 (7):
      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,
             active# f 0() -> mark# cons(0(), f s 0()),
           active# f s 0() -> mark# f p s 0()}
      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 0() -> mark 0(),
                  p mark X -> p X,
                p active X -> p X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = x0,
        
        [mark](x0) = x0,
        
        [f](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [active](x0) = x0,
        
        [p](x0) = x0,
        
        [0] = 0,
        
        [mark#](x0) = x0,
        
        [active#](x0) = x0
       Strict:
        active# f s 0() -> mark# f p s 0()
        1 >= 1
        active# f 0() -> mark# cons(0(), f s 0())
        0 >= 0
        mark# p X -> mark# X
        0 + 1X >= 0 + 1X
        mark# s X -> mark# X
        1 + 1X >= 0 + 1X
        mark# f X -> active# f mark X
        0 + 1X >= 0 + 1X
        mark# f X -> mark# X
        0 + 1X >= 0 + 1X
        mark# cons(X1, X2) -> mark# X1
        0 + 1X1 + 0X2 >= 0 + 1X1
       Weak:
        p active X -> p X
        0 + 1X >= 0 + 1X
        p mark X -> p X
        0 + 1X >= 0 + 1X
        active p s 0() -> mark 0()
        1 >= 0
        active f s 0() -> mark f p s 0()
        1 >= 1
        active f 0() -> mark cons(0(), f s 0())
        0 >= 0
        s active X -> s X
        1 + 1X >= 1 + 1X
        s mark X -> s X
        1 + 1X >= 1 + 1X
        f active X -> f X
        0 + 1X >= 0 + 1X
        f mark X -> f X
        0 + 1X >= 0 + 1X
        cons(active X1, X2) -> cons(X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
        cons(mark X1, X2) -> cons(X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
        cons(X1, active X2) -> cons(X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
        cons(X1, mark X2) -> cons(X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
        mark p X -> active p mark X
        0 + 1X >= 0 + 1X
        mark s X -> active s mark X
        1 + 1X >= 1 + 1X
        mark f X -> active f mark X
        0 + 1X >= 0 + 1X
        mark 0() -> active 0()
        0 >= 0
        mark cons(X1, X2) -> active cons(mark X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
      SCCS (1):
       Scc:
        {mark# cons(X1, X2) -> mark# X1,
                  mark# f X -> mark# X,
                  mark# f X -> active# f mark X,
                  mark# p X -> mark# X,
              active# f 0() -> mark# cons(0(), f s 0()),
            active# f s 0() -> mark# f p s 0()}
       
       SCC (6):
        Strict:
         {mark# cons(X1, X2) -> mark# X1,
                   mark# f X -> mark# X,
                   mark# f X -> active# f mark X,
                   mark# p X -> mark# X,
               active# f 0() -> mark# cons(0(), f s 0()),
             active# f s 0() -> mark# f p s 0()}
        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 0() -> mark 0(),
                    p mark X -> p X,
                  p active X -> p X}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [cons](x0, x1) = x0,
          
          [mark](x0) = x0 + 1,
          
          [f](x0) = x0 + 1,
          
          [s](x0) = x0,
          
          [active](x0) = x0,
          
          [p](x0) = x0,
          
          [0] = 0,
          
          [mark#](x0) = x0,
          
          [active#](x0) = 1
         Strict:
          active# f s 0() -> mark# f p s 0()
          1 >= 1
          active# f 0() -> mark# cons(0(), f s 0())
          1 >= 0
          mark# p X -> mark# X
          0 + 1X >= 0 + 1X
          mark# f X -> active# f mark X
          1 + 1X >= 1 + 0X
          mark# f X -> mark# X
          1 + 1X >= 0 + 1X
          mark# cons(X1, X2) -> mark# X1
          0 + 1X1 + 0X2 >= 0 + 1X1
         Weak:
          p active X -> p X
          0 + 1X >= 0 + 1X
          p mark X -> p X
          1 + 1X >= 0 + 1X
          active p s 0() -> mark 0()
          0 >= 1
          active f s 0() -> mark f p s 0()
          1 >= 2
          active f 0() -> mark cons(0(), f s 0())
          1 >= 1
          s active X -> s X
          0 + 1X >= 0 + 1X
          s mark X -> s X
          1 + 1X >= 0 + 1X
          f active X -> f X
          1 + 1X >= 1 + 1X
          f mark X -> f X
          2 + 1X >= 1 + 1X
          cons(active X1, X2) -> cons(X1, X2)
          0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
          cons(mark X1, X2) -> cons(X1, X2)
          1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
          cons(X1, active X2) -> cons(X1, X2)
          0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
          cons(X1, mark X2) -> cons(X1, X2)
          0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
          mark p X -> active p mark X
          1 + 1X >= 1 + 1X
          mark s X -> active s mark X
          1 + 1X >= 1 + 1X
          mark f X -> active f mark X
          2 + 1X >= 2 + 1X
          mark 0() -> active 0()
          1 >= 0
          mark cons(X1, X2) -> active cons(mark X1, X2)
          1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        SCCS (2):
         Scc:
          {mark# cons(X1, X2) -> mark# X1,
                    mark# p X -> mark# X}
         Scc:
          {      mark# f X -> active# f mark X,
           active# f s 0() -> mark# f p s 0()}
         
         SCC (2):
          Strict:
           {mark# cons(X1, X2) -> mark# X1,
                     mark# p 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 0() -> mark 0(),
                      p mark X -> p X,
                    p active X -> p X}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [cons](x0, x1) = x0 + x1 + 1,
            
            [mark](x0) = x0 + 1,
            
            [f](x0) = 0,
            
            [s](x0) = x0 + 1,
            
            [active](x0) = x0,
            
            [p](x0) = x0,
            
            [0] = 0,
            
            [mark#](x0) = x0
           Strict:
            mark# p X -> mark# X
            0 + 1X >= 0 + 1X
            mark# cons(X1, X2) -> mark# X1
            1 + 1X1 + 1X2 >= 0 + 1X1
           Weak:
            p active X -> p X
            0 + 1X >= 0 + 1X
            p mark X -> p X
            1 + 1X >= 0 + 1X
            active p s 0() -> mark 0()
            1 >= 1
            active f s 0() -> mark f p s 0()
            0 >= 1
            active f 0() -> mark cons(0(), f s 0())
            0 >= 2
            s active X -> s X
            1 + 1X >= 1 + 1X
            s mark X -> s X
            2 + 1X >= 1 + 1X
            f active X -> f X
            0 + 0X >= 0 + 0X
            f mark X -> f X
            0 + 0X >= 0 + 0X
            cons(active X1, X2) -> cons(X1, X2)
            1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
            cons(mark X1, X2) -> cons(X1, X2)
            2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
            cons(X1, active X2) -> cons(X1, X2)
            1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
            cons(X1, mark X2) -> cons(X1, X2)
            2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
            mark p X -> active p mark X
            1 + 1X >= 1 + 1X
            mark s X -> active s mark X
            2 + 1X >= 2 + 1X
            mark f X -> active f mark X
            1 + 0X >= 0 + 0X
            mark 0() -> active 0()
            1 >= 0
            mark cons(X1, X2) -> active cons(mark X1, X2)
            2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
          SCCS (1):
           Scc:
            {mark# p X -> mark# X}
           
           SCC (1):
            Strict:
             {mark# p 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 0() -> mark 0(),
                        p mark X -> p X,
                      p active X -> p X}
            POLY:
             Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
             Interpretation:
              [cons](x0, x1) = x0 + x1 + 1,
              
              [mark](x0) = x0 + 1,
              
              [f](x0) = x0 + 1,
              
              [s](x0) = x0 + 1,
              
              [active](x0) = x0,
              
              [p](x0) = x0 + 1,
              
              [0] = 0,
              
              [mark#](x0) = x0 + 1
             Strict:
              mark# p X -> mark# X
              2 + 1X >= 1 + 1X
             Weak:
              p active X -> p X
              1 + 1X >= 1 + 1X
              p mark X -> p X
              2 + 1X >= 1 + 1X
              active p s 0() -> mark 0()
              2 >= 1
              active f s 0() -> mark f p s 0()
              2 >= 4
              active f 0() -> mark cons(0(), f s 0())
              1 >= 4
              s active X -> s X
              1 + 1X >= 1 + 1X
              s mark X -> s X
              2 + 1X >= 1 + 1X
              f active X -> f X
              1 + 1X >= 1 + 1X
              f mark X -> f X
              2 + 1X >= 1 + 1X
              cons(active X1, X2) -> cons(X1, X2)
              1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
              cons(mark X1, X2) -> cons(X1, X2)
              2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
              cons(X1, active X2) -> cons(X1, X2)
              1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
              cons(X1, mark X2) -> cons(X1, X2)
              2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
              mark p X -> active p mark X
              2 + 1X >= 2 + 1X
              mark s X -> active s mark X
              2 + 1X >= 2 + 1X
              mark f X -> active f mark X
              2 + 1X >= 2 + 1X
              mark 0() -> active 0()
              1 >= 0
              mark cons(X1, X2) -> active cons(mark X1, X2)
              2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
            Qed
        SCC (2):
         Strict:
          {      mark# f X -> active# f mark X,
           active# f s 0() -> mark# f p s 0()}
         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 0() -> mark 0(),
                     p mark X -> p X,
                   p active X -> p X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [cons](x0, x1) = 0,
           
           [mark](x0) = x0,
           
           [f](x0) = x0,
           
           [s](x0) = 1,
           
           [active](x0) = x0,
           
           [p](x0) = 0,
           
           [0] = 0,
           
           [mark#](x0) = x0,
           
           [active#](x0) = x0
          Strict:
           active# f s 0() -> mark# f p s 0()
           1 >= 0
           mark# f X -> active# f mark X
           0 + 1X >= 0 + 1X
          Weak:
           p active X -> p X
           0 + 0X >= 0 + 0X
           p mark X -> p X
           0 + 0X >= 0 + 0X
           active p s 0() -> mark 0()
           0 >= 0
           active f s 0() -> mark f p s 0()
           1 >= 0
           active f 0() -> mark cons(0(), f s 0())
           0 >= 0
           s active X -> s X
           1 + 0X >= 1 + 0X
           s mark X -> s X
           1 + 0X >= 1 + 0X
           f active X -> f X
           0 + 1X >= 0 + 1X
           f mark X -> f X
           0 + 1X >= 0 + 1X
           cons(active X1, X2) -> cons(X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           cons(mark X1, X2) -> cons(X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           cons(X1, active X2) -> cons(X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           cons(X1, mark X2) -> cons(X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           mark p X -> active p mark X
           0 + 0X >= 0 + 0X
           mark s X -> active s mark X
           1 + 0X >= 1 + 0X
           mark f X -> active f mark X
           0 + 1X >= 0 + 1X
           mark 0() -> active 0()
           0 >= 0
           mark cons(X1, X2) -> active cons(mark X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         SCCS (0):
          
          
  
  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 0() -> mark 0(),
               p mark X -> p X,
             p active X -> p X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [cons](x0, x1) = x0 + x1 + 1,
     
     [mark](x0) = x0 + 1,
     
     [f](x0) = 0,
     
     [s](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [p](x0) = 0,
     
     [0] = 1,
     
     [p#](x0) = x0 + 1
    Strict:
     p# active X -> p# X
     2 + 1X >= 1 + 1X
     p# mark X -> p# X
     2 + 1X >= 1 + 1X
    Weak:
     p active X -> p X
     0 + 0X >= 0 + 0X
     p mark X -> p X
     0 + 0X >= 0 + 0X
     active p s 0() -> mark 0()
     1 >= 2
     active f s 0() -> mark f p s 0()
     1 >= 1
     active f 0() -> mark cons(0(), f s 0())
     1 >= 3
     s active X -> s X
     2 + 1X >= 1 + 1X
     s mark X -> s X
     2 + 1X >= 1 + 1X
     f active X -> f X
     0 + 0X >= 0 + 0X
     f mark X -> f X
     0 + 0X >= 0 + 0X
     cons(active X1, X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(mark X1, X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(X1, active X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(X1, mark X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     mark p X -> active p mark X
     1 + 0X >= 1 + 0X
     mark s X -> active s mark X
     2 + 1X >= 3 + 1X
     mark f X -> active f mark X
     1 + 0X >= 1 + 0X
     mark 0() -> active 0()
     2 >= 2
     mark cons(X1, X2) -> active cons(mark X1, X2)
     2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
   Qed
  
  
  
  
  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 0() -> mark 0(),
               p mark X -> p X,
             p active X -> p X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [cons](x0, x1) = x0 + x1 + 1,
     
     [mark](x0) = x0 + 1,
     
     [f](x0) = 0,
     
     [s](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [p](x0) = 0,
     
     [0] = 1,
     
     [s#](x0) = x0 + 1
    Strict:
     s# active X -> s# X
     2 + 1X >= 1 + 1X
     s# mark X -> s# X
     2 + 1X >= 1 + 1X
    Weak:
     p active X -> p X
     0 + 0X >= 0 + 0X
     p mark X -> p X
     0 + 0X >= 0 + 0X
     active p s 0() -> mark 0()
     1 >= 2
     active f s 0() -> mark f p s 0()
     1 >= 1
     active f 0() -> mark cons(0(), f s 0())
     1 >= 3
     s active X -> s X
     2 + 1X >= 1 + 1X
     s mark X -> s X
     2 + 1X >= 1 + 1X
     f active X -> f X
     0 + 0X >= 0 + 0X
     f mark X -> f X
     0 + 0X >= 0 + 0X
     cons(active X1, X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(mark X1, X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(X1, active X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     cons(X1, mark X2) -> cons(X1, X2)
     2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
     mark p X -> active p mark X
     1 + 0X >= 1 + 0X
     mark s X -> active s mark X
     2 + 1X >= 3 + 1X
     mark f X -> active f mark X
     1 + 0X >= 1 + 0X
     mark 0() -> active 0()
     2 >= 2
     mark cons(X1, X2) -> active cons(mark X1, X2)
     2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
   Qed
 
 
 
 
 
 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 0() -> mark 0(),
              p mark X -> p X,
            p active X -> p X}
  POLY:
   Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
   Interpretation:
    [cons](x0, x1) = x0 + x1 + 1,
    
    [mark](x0) = x0 + 1,
    
    [f](x0) = 0,
    
    [s](x0) = x0 + 1,
    
    [active](x0) = x0 + 1,
    
    [p](x0) = 0,
    
    [0] = 1,
    
    [f#](x0) = x0 + 1
   Strict:
    f# active X -> f# X
    2 + 1X >= 1 + 1X
    f# mark X -> f# X
    2 + 1X >= 1 + 1X
   Weak:
    p active X -> p X
    0 + 0X >= 0 + 0X
    p mark X -> p X
    0 + 0X >= 0 + 0X
    active p s 0() -> mark 0()
    1 >= 2
    active f s 0() -> mark f p s 0()
    1 >= 1
    active f 0() -> mark cons(0(), f s 0())
    1 >= 3
    s active X -> s X
    2 + 1X >= 1 + 1X
    s mark X -> s X
    2 + 1X >= 1 + 1X
    f active X -> f X
    0 + 0X >= 0 + 0X
    f mark X -> f X
    0 + 0X >= 0 + 0X
    cons(active X1, X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(mark X1, X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(X1, active X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(X1, mark X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    mark p X -> active p mark X
    1 + 0X >= 1 + 0X
    mark s X -> active s mark X
    2 + 1X >= 3 + 1X
    mark f X -> active f mark X
    1 + 0X >= 1 + 0X
    mark 0() -> active 0()
    2 >= 2
    mark cons(X1, X2) -> active cons(mark X1, X2)
    2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
  Qed
 
 
 
 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 0() -> mark 0(),
              p mark X -> p X,
            p active X -> p X}
  POLY:
   Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
   Interpretation:
    [cons](x0, x1) = x0 + x1 + 1,
    
    [mark](x0) = x0 + 1,
    
    [f](x0) = x0 + 1,
    
    [s](x0) = x0,
    
    [active](x0) = x0 + 1,
    
    [p](x0) = 0,
    
    [0] = 1,
    
    [cons#](x0, x1) = x0 + x1 + 1
   Strict:
    cons#(active X1, X2) -> cons#(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons#(mark X1, X2) -> cons#(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons#(X1, active X2) -> cons#(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons#(X1, mark X2) -> cons#(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
   Weak:
    p active X -> p X
    0 + 0X >= 0 + 0X
    p mark X -> p X
    0 + 0X >= 0 + 0X
    active p s 0() -> mark 0()
    1 >= 2
    active f s 0() -> mark f p s 0()
    3 >= 2
    active f 0() -> mark cons(0(), f s 0())
    3 >= 5
    s active X -> s X
    1 + 1X >= 0 + 1X
    s mark X -> s X
    1 + 1X >= 0 + 1X
    f active X -> f X
    2 + 1X >= 1 + 1X
    f mark X -> f X
    2 + 1X >= 1 + 1X
    cons(active X1, X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(mark X1, X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(X1, active X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    cons(X1, mark X2) -> cons(X1, X2)
    2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
    mark p X -> active p mark X
    1 + 0X >= 1 + 0X
    mark s X -> active s mark X
    1 + 1X >= 2 + 1X
    mark f X -> active f mark X
    2 + 1X >= 3 + 1X
    mark 0() -> active 0()
    2 >= 2
    mark cons(X1, X2) -> active cons(mark X1, X2)
    2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
  Qed