MAYBE
TRS:
 {    -(x, 0()) -> x,
  -(s(x), s(y)) -> -(x, y),
        p(s(x)) -> x,
     f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))),
     f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))}
 DP:
  Strict:
   {-#(s(x), s(y)) -> -#(x, y),
       f#(x, s(y)) -> -#(x, s(y)),
       f#(x, s(y)) -> -#(s(y), x),
       f#(x, s(y)) -> p#(-(x, s(y))),
       f#(x, s(y)) -> p#(-(s(y), x)),
       f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))),
       f#(s(x), y) -> -#(y, s(x)),
       f#(s(x), y) -> -#(s(x), y),
       f#(s(x), y) -> p#(-(y, s(x))),
       f#(s(x), y) -> p#(-(s(x), y)),
       f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x))))}
  Weak:
  {    -(x, 0()) -> x,
   -(s(x), s(y)) -> -(x, y),
         p(s(x)) -> x,
      f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))),
      f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))}
  EDG:
   {(f#(x, s(y)) -> -#(s(y), x), -#(s(x), s(y)) -> -#(x, y))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(s(x), y) -> p#(-(s(x), y)))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(s(x), y) -> p#(-(y, s(x))))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(s(x), y) -> -#(s(x), y))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(s(x), y) -> -#(y, s(x)))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(x, s(y)) -> p#(-(s(y), x)))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(x, s(y)) -> p#(-(x, s(y))))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(x, s(y)) -> -#(s(y), x))
    (f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))), f#(x, s(y)) -> -#(x, s(y)))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(x, s(y)) -> -#(x, s(y)))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(x, s(y)) -> -#(s(y), x))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(x, s(y)) -> p#(-(x, s(y))))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(x, s(y)) -> p#(-(s(y), x)))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(s(x), y) -> -#(y, s(x)))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(s(x), y) -> -#(s(x), y))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(s(x), y) -> p#(-(y, s(x))))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(s(x), y) -> p#(-(s(x), y)))
    (f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))), f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x)))))
    (f#(s(x), y) -> -#(s(x), y), -#(s(x), s(y)) -> -#(x, y))
    (f#(s(x), y) -> -#(y, s(x)), -#(s(x), s(y)) -> -#(x, y))
    (f#(x, s(y)) -> -#(x, s(y)), -#(s(x), s(y)) -> -#(x, y))}
   SCCS:
    Scc:
     {f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))),
      f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x))))}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    SCC:
     Strict:
      {f#(x, s(y)) -> f#(p(-(x, s(y))), p(-(s(y), x))),
       f#(s(x), y) -> f#(p(-(s(x), y)), p(-(y, s(x))))}
     Weak:
     {    -(x, 0()) -> x,
      -(s(x), s(y)) -> -(x, y),
            p(s(x)) -> x,
         f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))),
         f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))}
     Fail
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {    -(x, 0()) -> x,
      -(s(x), s(y)) -> -(x, y),
            p(s(x)) -> x,
         f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))),
         f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed