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