MAYBE
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:
  Strict:
   {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())}
  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()}
  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()))}
   SCCS:
    Scc:
     {times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0())))}
    SCC:
     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()}
     Fail