MAYBE
Time: 0.005326
TRS:
 {  -(x, 0()) -> x,
  -(0(), s y) -> 0(),
  -(s x, s y) -> -(x, y),
        f 0() -> 0(),
        f s x -> -(s x, g f x),
        g 0() -> s 0(),
        g s x -> -(s x, f g x)}
 DP:
  DP:
   {-#(s x, s y) -> -#(x, y),
          f# s x -> -#(s x, g f x),
          f# s x -> f# x,
          f# s x -> g# f x,
          g# s x -> -#(s x, f g x),
          g# s x -> f# g x,
          g# s x -> g# x}
  TRS:
  {  -(x, 0()) -> x,
   -(0(), s y) -> 0(),
   -(s x, s y) -> -(x, y),
         f 0() -> 0(),
         f s x -> -(s x, g f x),
         g 0() -> s 0(),
         g s x -> -(s x, f g x)}
  EDG:
   {(g# s x -> -#(s x, f g x), -#(s x, s y) -> -#(x, y))
    (g# s x -> g# x, g# s x -> g# x)
    (g# s x -> g# x, g# s x -> f# g x)
    (g# s x -> g# x, g# s x -> -#(s x, f g x))
    (f# s x -> g# f x, g# s x -> g# x)
    (f# s x -> g# f x, g# s x -> f# g x)
    (f# s x -> g# f x, g# s x -> -#(s x, f g x))
    (g# s x -> f# g x, f# s x -> -#(s x, g f x))
    (g# s x -> f# g x, f# s x -> f# x)
    (g# s x -> f# g x, f# s x -> g# f x)
    (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
    (f# s x -> f# x, f# s x -> -#(s x, g f x))
    (f# s x -> f# x, f# s x -> f# x)
    (f# s x -> f# x, f# s x -> g# f x)
    (f# s x -> -#(s x, g f x), -#(s x, s y) -> -#(x, y))}
   EDG:
    {(g# s x -> -#(s x, f g x), -#(s x, s y) -> -#(x, y))
     (g# s x -> g# x, g# s x -> g# x)
     (g# s x -> g# x, g# s x -> f# g x)
     (g# s x -> g# x, g# s x -> -#(s x, f g x))
     (f# s x -> g# f x, g# s x -> g# x)
     (f# s x -> g# f x, g# s x -> f# g x)
     (f# s x -> g# f x, g# s x -> -#(s x, f g x))
     (g# s x -> f# g x, f# s x -> -#(s x, g f x))
     (g# s x -> f# g x, f# s x -> f# x)
     (g# s x -> f# g x, f# s x -> g# f x)
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (f# s x -> f# x, f# s x -> -#(s x, g f x))
     (f# s x -> f# x, f# s x -> f# x)
     (f# s x -> f# x, f# s x -> g# f x)
     (f# s x -> -#(s x, g f x), -#(s x, s y) -> -#(x, y))}
    EDG:
     {(g# s x -> -#(s x, f g x), -#(s x, s y) -> -#(x, y))
      (g# s x -> g# x, g# s x -> g# x)
      (g# s x -> g# x, g# s x -> f# g x)
      (g# s x -> g# x, g# s x -> -#(s x, f g x))
      (f# s x -> g# f x, g# s x -> g# x)
      (f# s x -> g# f x, g# s x -> f# g x)
      (f# s x -> g# f x, g# s x -> -#(s x, f g x))
      (g# s x -> f# g x, f# s x -> -#(s x, g f x))
      (g# s x -> f# g x, f# s x -> f# x)
      (g# s x -> f# g x, f# s x -> g# f x)
      (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
      (f# s x -> f# x, f# s x -> -#(s x, g f x))
      (f# s x -> f# x, f# s x -> f# x)
      (f# s x -> f# x, f# s x -> g# f x)
      (f# s x -> -#(s x, g f x), -#(s x, s y) -> -#(x, y))}
     EDG:
      {(g# s x -> -#(s x, f g x), -#(s x, s y) -> -#(x, y))
       (g# s x -> g# x, g# s x -> g# x)
       (g# s x -> g# x, g# s x -> f# g x)
       (g# s x -> g# x, g# s x -> -#(s x, f g x))
       (f# s x -> g# f x, g# s x -> g# x)
       (f# s x -> g# f x, g# s x -> f# g x)
       (f# s x -> g# f x, g# s x -> -#(s x, f g x))
       (g# s x -> f# g x, f# s x -> -#(s x, g f x))
       (g# s x -> f# g x, f# s x -> f# x)
       (g# s x -> f# g x, f# s x -> g# f x)
       (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
       (f# s x -> f# x, f# s x -> -#(s x, g f x))
       (f# s x -> f# x, f# s x -> f# x)
       (f# s x -> f# x, f# s x -> g# f x)
       (f# s x -> -#(s x, g f x), -#(s x, s y) -> -#(x, y))}
      STATUS:
       arrows: 0.693878
       SCCS (2):
        Scc:
         {f# s x -> f# x,
          f# s x -> g# f x,
          g# s x -> f# g x,
          g# s x -> g# x}
        Scc:
         {-#(s x, s y) -> -#(x, y)}
        
        SCC (4):
         Strict:
          {f# s x -> f# x,
           f# s x -> g# f x,
           g# s x -> f# g x,
           g# s x -> g# x}
         Weak:
         {  -(x, 0()) -> x,
          -(0(), s y) -> 0(),
          -(s x, s y) -> -(x, y),
                f 0() -> 0(),
                f s x -> -(s x, g f x),
                g 0() -> s 0(),
                g s x -> -(s x, f g x)}
         Open
        
        
        SCC (1):
         Strict:
          {-#(s x, s y) -> -#(x, y)}
         Weak:
         {  -(x, 0()) -> x,
          -(0(), s y) -> 0(),
          -(s x, s y) -> -(x, y),
                f 0() -> 0(),
                f s x -> -(s x, g f x),
                g 0() -> s 0(),
                g s x -> -(s x, f g x)}
         Open