MAYBE
Time: 0.001121
TRS:
 {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
        times(X, s Y) -> plus(X, times(Y, X))}
 DP:
  DP:
   {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
    plus#(plus(X, Y), Z) -> plus#(Y, Z),
          times#(X, s Y) -> plus#(X, times(Y, X)),
          times#(X, s Y) -> times#(Y, X)}
  TRS:
  {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
         times(X, s Y) -> plus(X, times(Y, X))}
  UR:
   {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
          times(X, s Y) -> plus(X, times(Y, X)),
                a(x, y) -> x,
                a(x, y) -> y}
   EDG:
    {(plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(Y, Z))
     (plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
     (times#(X, s Y) -> times#(Y, X), times#(X, s Y) -> times#(Y, X))
     (times#(X, s Y) -> times#(Y, X), times#(X, s Y) -> plus#(X, times(Y, X)))
     (times#(X, s Y) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
     (times#(X, s Y) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(Y, Z))
     (plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
     (plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(Y, Z))}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {times#(X, s Y) -> times#(Y, X)}
      Scc:
       {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
        plus#(plus(X, Y), Z) -> plus#(Y, Z)}
      
      SCC (1):
       Strict:
        {times#(X, s Y) -> times#(Y, X)}
       Weak:
       {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
              times(X, s Y) -> plus(X, times(Y, X))}
       Open
      
      SCC (2):
       Strict:
        {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
         plus#(plus(X, Y), Z) -> plus#(Y, Z)}
       Weak:
       {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
              times(X, s Y) -> plus(X, times(Y, X))}
       Open