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