MAYBE
Time: 0.256790
TRS:
 {          plus(x, s y) -> s plus(x, y),
            plus(x, 0()) -> x,
  times(x, plus(y, s z)) -> plus(times(x, plus(y, times(s z, 0()))), times(x, s z)),
           times(x, s y) -> plus(times(x, y), x),
           times(x, 0()) -> 0()}
 DP:
  DP:
   {          plus#(x, s y) -> plus#(x, y),
    times#(x, plus(y, s z)) -> plus#(y, times(s z, 0())),
    times#(x, plus(y, s z)) -> plus#(times(x, plus(y, times(s z, 0()))), times(x, s z)),
    times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))),
    times#(x, plus(y, s z)) -> times#(x, s z),
    times#(x, plus(y, s z)) -> times#(s z, 0()),
             times#(x, s y) -> plus#(times(x, y), x),
             times#(x, s y) -> times#(x, y)}
  TRS:
  {          plus(x, s y) -> s plus(x, y),
             plus(x, 0()) -> x,
   times(x, plus(y, s z)) -> plus(times(x, plus(y, times(s z, 0()))), times(x, s z)),
            times(x, s y) -> plus(times(x, y), x),
            times(x, 0()) -> 0()}
  UR:
   {          plus(x, s y) -> s plus(x, y),
              plus(x, 0()) -> x,
    times(x, plus(y, s z)) -> plus(times(x, plus(y, times(s z, 0()))), times(x, s z)),
             times(x, s y) -> plus(times(x, y), x),
             times(x, 0()) -> 0(),
                   a(w, v) -> w,
                   a(w, v) -> v}
   EDG:
    {(times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, s y) -> times#(x, y))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, s y) -> plus#(times(x, y), x))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, plus(y, s z)) -> times#(s z, 0()))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, plus(y, s z)) -> times#(x, s z))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, plus(y, s z)) -> plus#(times(x, plus(y, times(s z, 0()))), times(x, s z)))
     (times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))), times#(x, plus(y, s z)) -> plus#(y, times(s z, 0())))
     (times#(x, s y) -> times#(x, y), times#(x, s y) -> times#(x, y))
     (times#(x, s y) -> times#(x, y), times#(x, s y) -> plus#(times(x, y), x))
     (times#(x, s y) -> times#(x, y), times#(x, plus(y, s z)) -> times#(s z, 0()))
     (times#(x, s y) -> times#(x, y), times#(x, plus(y, s z)) -> times#(x, s z))
     (times#(x, s y) -> times#(x, y), times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))))
     (times#(x, s y) -> times#(x, y), times#(x, plus(y, s z)) -> plus#(times(x, plus(y, times(s z, 0()))), times(x, s z)))
     (times#(x, s y) -> times#(x, y), times#(x, plus(y, s z)) -> plus#(y, times(s z, 0())))
     (times#(x, s y) -> plus#(times(x, y), x), plus#(x, s y) -> plus#(x, y))
     (times#(x, plus(y, s z)) -> plus#(y, times(s z, 0())), plus#(x, s y) -> plus#(x, y))
     (times#(x, plus(y, s z)) -> times#(x, s z), times#(x, s y) -> plus#(times(x, y), x))
     (times#(x, plus(y, s z)) -> times#(x, s z), times#(x, s y) -> times#(x, y))
     (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(x, y))
     (times#(x, plus(y, s z)) -> plus#(times(x, plus(y, times(s z, 0()))), times(x, s z)), plus#(x, s y) -> plus#(x, y))}
    STATUS:
     arrows: 0.687500
     SCCS (2):
      Scc:
       {times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))),
        times#(x, plus(y, s z)) -> times#(x, s z),
                 times#(x, s y) -> times#(x, y)}
      Scc:
       {plus#(x, s y) -> plus#(x, y)}
      
      SCC (3):
       Strict:
        {times#(x, plus(y, s z)) -> times#(x, plus(y, times(s z, 0()))),
         times#(x, plus(y, s z)) -> times#(x, s z),
                  times#(x, s y) -> times#(x, y)}
       Weak:
       {          plus(x, s y) -> s plus(x, y),
                  plus(x, 0()) -> x,
        times(x, plus(y, s z)) -> plus(times(x, plus(y, times(s z, 0()))), times(x, s z)),
                 times(x, s y) -> plus(times(x, y), x),
                 times(x, 0()) -> 0()}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {plus#(x, s y) -> plus#(x, y)}
       Weak:
       {          plus(x, s y) -> s plus(x, y),
                  plus(x, 0()) -> x,
        times(x, plus(y, s z)) -> plus(times(x, plus(y, times(s z, 0()))), times(x, s z)),
                 times(x, s y) -> plus(times(x, y), x),
                 times(x, 0()) -> 0()}
       Open