YES
Time: 0.004979
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 0() -> 0(),
              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 0() -> 0(),
               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 0() -> 0(),
                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#())}
    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#())}
     EDG:
      {(activate# n__f X -> activate# X, activate# n__0() -> 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__0() -> 0#())}
      EDG:
       {(activate# n__f X -> activate# X, activate# n__0() -> 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__0() -> 0#())}
       STATUS:
        arrows: 0.918367
        SCCS (0):