MAYBE
Time: 0.104331
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:
  DP:
   {-#(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))}
  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))}
  UR:
   {  -(x, 0()) -> x,
    -(s x, s y) -> -(x, y),
          p s x -> x,
        a(z, w) -> z,
        a(z, w) -> w}
   EDG:
    {(f#(s x, y) -> -#(y, s x), -#(s x, s y) -> -#(x, y))
     (f#(s x, y) -> -#(s 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#(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) -> -#(x, s y), -#(s x, s y) -> -#(x, y))}
    STATUS:
     arrows: 0.793388
     SCCS (2):
      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 (2):
       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 (1):
       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))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [-](x0, x1) = x0,
         
         [f](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [p](x0) = x0 + 1,
         
         [0] = 0,
         
         [-#](x0, x1) = x0
        Strict:
         -#(s x, s y) -> -#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         f(s x, y) -> f(p -(s x, y), p -(y, s x))
         2 + 1x + 0y >= 3 + 1x + 0y
         f(x, s y) -> f(p -(x, s y), p -(s y, x))
         1 + 1x + 0y >= 2 + 1x + 0y
         p s x -> x
         2 + 1x >= 1x
         -(s x, s y) -> -(x, y)
         1 + 1x + 0y >= 0 + 1x + 0y
         -(x, 0()) -> x
         0 + 1x >= 1x
       Qed