MAYBE
Time: 0.002179
TRS:
 {     plus(x, 0()) -> x,
       plus(0(), y) -> y,
       plus(s x, y) -> s plus(x, y),
      times(0(), y) -> 0(),
      times(s x, y) -> plus(y, times(x, y)),
    times(s 0(), y) -> y,
          div(x, y) -> quot(x, y, y),
        div(0(), y) -> 0(),
  div(div(x, y), z) -> div(x, times(y, z)),
  quot(x, 0(), s z) -> s div(x, s z),
  quot(0(), s y, z) -> 0(),
  quot(s x, s y, z) -> quot(x, y, z)}
 DP:
  DP:
   {     plus#(s x, y) -> plus#(x, y),
        times#(s x, y) -> plus#(y, times(x, y)),
        times#(s x, y) -> times#(x, y),
            div#(x, y) -> quot#(x, y, y),
    div#(div(x, y), z) -> times#(y, z),
    div#(div(x, y), z) -> div#(x, times(y, z)),
    quot#(x, 0(), s z) -> div#(x, s z),
    quot#(s x, s y, z) -> quot#(x, y, z)}
  TRS:
  {     plus(x, 0()) -> x,
        plus(0(), y) -> y,
        plus(s x, y) -> s plus(x, y),
       times(0(), y) -> 0(),
       times(s x, y) -> plus(y, times(x, y)),
     times(s 0(), y) -> y,
           div(x, y) -> quot(x, y, y),
         div(0(), y) -> 0(),
   div(div(x, y), z) -> div(x, times(y, z)),
   quot(x, 0(), s z) -> s div(x, s z),
   quot(0(), s y, z) -> 0(),
   quot(s x, s y, z) -> quot(x, y, z)}
  EDG:
   {(times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (div#(div(x, y), z) -> times#(y, z), times#(s x, y) -> times#(x, y))
    (div#(div(x, y), z) -> times#(y, z), times#(s x, y) -> plus#(y, times(x, y)))
    (quot#(s x, s y, z) -> quot#(x, y, z), quot#(s x, s y, z) -> quot#(x, y, z))
    (quot#(s x, s y, z) -> quot#(x, y, z), quot#(x, 0(), s z) -> div#(x, s z))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(x, y) -> quot#(x, y, y))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> times#(y, z))
    (quot#(x, 0(), s z) -> div#(x, s z), div#(div(x, y), z) -> div#(x, times(y, z)))
    (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
    (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> times#(y, z))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))
    (div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s z) -> div#(x, s z))
    (div#(x, y) -> quot#(x, y, y), quot#(s x, s y, z) -> quot#(x, y, z))}
   STATUS:
    arrows: 0.750000
    SCCS (3):
     Scc:
      {        div#(x, y) -> quot#(x, y, y),
       div#(div(x, y), z) -> div#(x, times(y, z)),
       quot#(x, 0(), s z) -> div#(x, s z),
       quot#(s x, s y, z) -> quot#(x, y, z)}
     Scc:
      {times#(s x, y) -> times#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     SCC (4):
      Strict:
       {        div#(x, y) -> quot#(x, y, y),
        div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s z) -> div#(x, s z),
        quot#(s x, s y, z) -> quot#(x, y, z)}
      Weak:
      {     plus(x, 0()) -> x,
            plus(0(), y) -> y,
            plus(s x, y) -> s plus(x, y),
           times(0(), y) -> 0(),
           times(s x, y) -> plus(y, times(x, y)),
         times(s 0(), y) -> y,
               div(x, y) -> quot(x, y, y),
             div(0(), y) -> 0(),
       div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s z) -> s div(x, s z),
       quot(0(), s y, z) -> 0(),
       quot(s x, s y, z) -> quot(x, y, z)}
      Open
     
     SCC (1):
      Strict:
       {times#(s x, y) -> times#(x, y)}
      Weak:
      {     plus(x, 0()) -> x,
            plus(0(), y) -> y,
            plus(s x, y) -> s plus(x, y),
           times(0(), y) -> 0(),
           times(s x, y) -> plus(y, times(x, y)),
         times(s 0(), y) -> y,
               div(x, y) -> quot(x, y, y),
             div(0(), y) -> 0(),
       div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s z) -> s div(x, s z),
       quot(0(), s y, z) -> 0(),
       quot(s x, s y, z) -> quot(x, y, z)}
      Open
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {     plus(x, 0()) -> x,
            plus(0(), y) -> y,
            plus(s x, y) -> s plus(x, y),
           times(0(), y) -> 0(),
           times(s x, y) -> plus(y, times(x, y)),
         times(s 0(), y) -> y,
               div(x, y) -> quot(x, y, y),
             div(0(), y) -> 0(),
       div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s z) -> s div(x, s z),
       quot(0(), s y, z) -> 0(),
       quot(s x, s y, z) -> quot(x, y, z)}
      Open