MAYBE
Time: 0.000662
TRS:
 {       +(X, 0()) -> X,
         +(X, s Y) -> s +(X, Y),
  f(0(), s 0(), X) -> f(X, +(X, X), X),
           g(X, Y) -> X,
           g(X, Y) -> Y}
 DP:
  DP:
   {       +#(X, s Y) -> +#(X, Y),
    f#(0(), s 0(), X) -> +#(X, X),
    f#(0(), s 0(), X) -> f#(X, +(X, X), X)}
  TRS:
  {       +(X, 0()) -> X,
          +(X, s Y) -> s +(X, Y),
   f(0(), s 0(), X) -> f(X, +(X, X), X),
            g(X, Y) -> X,
            g(X, Y) -> Y}
  UR:
   {+(X, 0()) -> X,
    +(X, s Y) -> s +(X, Y)}
   EDG:
    {(f#(0(), s 0(), X) -> f#(X, +(X, X), X), f#(0(), s 0(), X) -> f#(X, +(X, X), X))
     (f#(0(), s 0(), X) -> f#(X, +(X, X), X), f#(0(), s 0(), X) -> +#(X, X))
     (f#(0(), s 0(), X) -> +#(X, X), +#(X, s Y) -> +#(X, Y))
     (+#(X, s Y) -> +#(X, Y), +#(X, s Y) -> +#(X, Y))}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {f#(0(), s 0(), X) -> f#(X, +(X, X), X)}
      Scc:
       {+#(X, s Y) -> +#(X, Y)}
      
      SCC (1):
       Strict:
        {f#(0(), s 0(), X) -> f#(X, +(X, X), X)}
       Weak:
       {       +(X, 0()) -> X,
               +(X, s Y) -> s +(X, Y),
        f(0(), s 0(), X) -> f(X, +(X, X), X),
                 g(X, Y) -> X,
                 g(X, Y) -> Y}
       Open
      
      SCC (1):
       Strict:
        {+#(X, s Y) -> +#(X, Y)}
       Weak:
       {       +(X, 0()) -> X,
               +(X, s Y) -> s +(X, Y),
        f(0(), s 0(), X) -> f(X, +(X, X), X),
                 g(X, Y) -> X,
                 g(X, Y) -> Y}
       Open