MAYBE
Time: 0.001341
TRS:
 {  minus(x, 0()) -> x,
  minus(s x, s y) -> minus(x, y),
            f 0() -> s 0(),
            f s x -> minus(s x, g f x),
            g 0() -> 0(),
            g s x -> minus(s x, f g x)}
 DP:
  DP:
   {minus#(s x, s y) -> minus#(x, y),
              f# s x -> minus#(s x, g f x),
              f# s x -> f# x,
              f# s x -> g# f x,
              g# s x -> minus#(s x, f g x),
              g# s x -> f# g x,
              g# s x -> g# x}
  TRS:
  {  minus(x, 0()) -> x,
   minus(s x, s y) -> minus(x, y),
             f 0() -> s 0(),
             f s x -> minus(s x, g f x),
             g 0() -> 0(),
             g s x -> minus(s x, f g x)}
  UR:
   {  minus(x, 0()) -> x,
    minus(s x, s y) -> minus(x, y),
              f 0() -> s 0(),
              f s x -> minus(s x, g f x),
              g 0() -> 0(),
              g s x -> minus(s x, f g x),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(g# s x -> minus#(s x, f g x), minus#(s x, s y) -> minus#(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 -> minus#(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 -> minus#(s x, f g x))
     (g# s x -> f# g x, f# s x -> minus#(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)
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (f# s x -> f# x, f# s x -> minus#(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 -> minus#(s x, g f x), minus#(s x, s y) -> minus#(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:
       {minus#(s x, s y) -> minus#(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:
       {  minus(x, 0()) -> x,
        minus(s x, s y) -> minus(x, y),
                  f 0() -> s 0(),
                  f s x -> minus(s x, g f x),
                  g 0() -> 0(),
                  g s x -> minus(s x, f g x)}
       Open
      
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {  minus(x, 0()) -> x,
        minus(s x, s y) -> minus(x, y),
                  f 0() -> s 0(),
                  f s x -> minus(s x, g f x),
                  g 0() -> 0(),
                  g s x -> minus(s x, f g x)}
       Open