MAYBE
Time: 0.006356
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))}
    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))}
     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))}
      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))}
          Open
         
         
         
         
         
         
         
         
         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))}
          Open