MAYBE
Time: 0.066596
TRS:
 {            0() -> n__0(),
              f X -> n__f X,
            f 0() -> cons(0(), n__f n__s n__0()),
          f s 0() -> f p s 0(),
            p s X -> X,
              s X -> n__s X,
       activate X -> X,
  activate n__f X -> f activate X,
  activate n__s X -> s activate X,
  activate n__0() -> 0()}
 DP:
  DP:
   {        f# s 0() -> f# p s 0(),
            f# s 0() -> p# s 0(),
    activate# n__f X -> f# activate X,
    activate# n__f X -> activate# X,
    activate# n__s X -> s# activate X,
    activate# n__s X -> activate# X,
    activate# n__0() -> 0#()}
  TRS:
  {            0() -> n__0(),
               f X -> n__f X,
             f 0() -> cons(0(), n__f n__s n__0()),
           f s 0() -> f p s 0(),
             p s X -> X,
               s X -> n__s X,
        activate X -> X,
   activate n__f X -> f activate X,
   activate n__s X -> s activate X,
   activate n__0() -> 0()}
  UR:
   {            0() -> n__0(),
                f X -> n__f X,
              f 0() -> cons(0(), n__f n__s n__0()),
            f s 0() -> f p s 0(),
              p s X -> X,
                s X -> n__s X,
         activate X -> X,
    activate n__f X -> f activate X,
    activate n__s X -> s activate X,
    activate n__0() -> 0()}
   EDG:
    {(activate# n__f X -> activate# X, activate# n__0() -> 0#())
     (activate# n__f X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__f X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__f X -> f# activate X)
     (f# s 0() -> f# p s 0(), f# s 0() -> f# p s 0())
     (f# s 0() -> f# p s 0(), f# s 0() -> p# s 0())
     (activate# n__f X -> f# activate X, f# s 0() -> f# p s 0())
     (activate# n__f X -> f# activate X, f# s 0() -> p# s 0())
     (activate# n__s X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__s X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__0() -> 0#())}
    STATUS:
     arrows: 0.714286
     SCCS (2):
      Scc:
       {activate# n__f X -> activate# X,
        activate# n__s X -> activate# X}
      Scc:
       {f# s 0() -> f# p s 0()}
      
      SCC (2):
       Strict:
        {activate# n__f X -> activate# X,
         activate# n__s X -> activate# X}
       Weak:
       {            0() -> n__0(),
                    f X -> n__f X,
                  f 0() -> cons(0(), n__f n__s n__0()),
                f s 0() -> f p s 0(),
                  p s X -> X,
                    s X -> n__s X,
             activate X -> X,
        activate n__f X -> f activate X,
        activate n__s X -> s activate X,
        activate n__0() -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0,
         
         [n__f](x0) = x0 + 1,
         
         [n__s](x0) = x0,
         
         [f](x0) = x0 + 1,
         
         [p](x0) = 0,
         
         [s](x0) = x0,
         
         [activate](x0) = 0,
         
         [0] = 1,
         
         [n__0] = 0,
         
         [activate#](x0) = x0
        Strict:
         activate# n__s X -> activate# X
         0 + 1X >= 0 + 1X
         activate# n__f X -> activate# X
         1 + 1X >= 0 + 1X
        Weak:
         activate n__0() -> 0()
         0 >= 1
         activate n__s X -> s activate X
         0 + 0X >= 0 + 0X
         activate n__f X -> f activate X
         0 + 0X >= 1 + 0X
         activate X -> X
         0 + 0X >= 1X
         s X -> n__s X
         0 + 1X >= 0 + 1X
         p s X -> X
         0 + 0X >= 1X
         f s 0() -> f p s 0()
         2 >= 1
         f 0() -> cons(0(), n__f n__s n__0())
         2 >= 1
         f X -> n__f X
         1 + 1X >= 1 + 1X
         0() -> n__0()
         1 >= 0
       SCCS (1):
        Scc:
         {activate# n__s X -> activate# X}
        
        SCC (1):
         Strict:
          {activate# n__s X -> activate# X}
         Weak:
         {            0() -> n__0(),
                      f X -> n__f X,
                    f 0() -> cons(0(), n__f n__s n__0()),
                  f s 0() -> f p s 0(),
                    p s X -> X,
                      s X -> n__s X,
               activate X -> X,
          activate n__f X -> f activate X,
          activate n__s X -> s activate X,
          activate n__0() -> 0()}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [cons](x0, x1) = 0,
           
           [n__f](x0) = 0,
           
           [n__s](x0) = x0 + 1,
           
           [f](x0) = x0 + 1,
           
           [p](x0) = x0,
           
           [s](x0) = x0 + 1,
           
           [activate](x0) = 0,
           
           [0] = 1,
           
           [n__0] = 1,
           
           [activate#](x0) = x0 + 1
          Strict:
           activate# n__s X -> activate# X
           2 + 1X >= 1 + 1X
          Weak:
           activate n__0() -> 0()
           0 >= 1
           activate n__s X -> s activate X
           0 + 0X >= 1 + 0X
           activate n__f X -> f activate X
           0 + 0X >= 1 + 0X
           activate X -> X
           0 + 0X >= 1X
           s X -> n__s X
           1 + 1X >= 1 + 1X
           p s X -> X
           1 + 1X >= 1X
           f s 0() -> f p s 0()
           3 >= 3
           f 0() -> cons(0(), n__f n__s n__0())
           2 >= 0
           f X -> n__f X
           1 + 1X >= 0 + 0X
           0() -> n__0()
           1 >= 1
         Qed
     
     
     
     SCC (1):
      Strict:
       {f# s 0() -> f# p s 0()}
      Weak:
      {            0() -> n__0(),
                   f X -> n__f X,
                 f 0() -> cons(0(), n__f n__s n__0()),
               f s 0() -> f p s 0(),
                 p s X -> X,
                   s X -> n__s X,
            activate X -> X,
       activate n__f X -> f activate X,
       activate n__s X -> s activate X,
       activate n__0() -> 0()}
      Fail