YES
TRS:
 {     i(div(X, Y)) -> div(Y, X),
        div(X, e()) -> i(X),
  div(div(X, Y), Z) -> div(Y, div(i(X), Z))}
 RUF:
  Strict:
   {     i(div(X, Y)) -> div(Y, X),
    div(div(X, Y), Z) -> div(Y, div(i(X), Z))}
  Weak:
   {}
  DP:
   Strict:
    {     i#(div(X, Y)) -> div#(Y, X),
     div#(div(X, Y), Z) -> i#(X),
     div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)),
     div#(div(X, Y), Z) -> div#(i(X), Z)}
   Weak:
   {     i(div(X, Y)) -> div(Y, X),
    div(div(X, Y), Z) -> div(Y, div(i(X), Z))}
   EDG:
    {(div#(div(X, Y), Z) -> div#(i(X), Z), div#(div(X, Y), Z) -> div#(i(X), Z))
     (div#(div(X, Y), Z) -> div#(i(X), Z), div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)))
     (div#(div(X, Y), Z) -> div#(i(X), Z), div#(div(X, Y), Z) -> i#(X))
     (div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)), div#(div(X, Y), Z) -> div#(i(X), Z))
     (div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)), div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)))
     (div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)), div#(div(X, Y), Z) -> i#(X))
     (div#(div(X, Y), Z) -> i#(X), i#(div(X, Y)) -> div#(Y, X))
     (i#(div(X, Y)) -> div#(Y, X), div#(div(X, Y), Z) -> i#(X))
     (i#(div(X, Y)) -> div#(Y, X), div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)))
     (i#(div(X, Y)) -> div#(Y, X), div#(div(X, Y), Z) -> div#(i(X), Z))}
    SCCS:
     Scc:
      {     i#(div(X, Y)) -> div#(Y, X),
       div#(div(X, Y), Z) -> i#(X),
       div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)),
       div#(div(X, Y), Z) -> div#(i(X), Z)}
     SCC:
      Strict:
       {     i#(div(X, Y)) -> div#(Y, X),
        div#(div(X, Y), Z) -> i#(X),
        div#(div(X, Y), Z) -> div#(Y, div(i(X), Z)),
        div#(div(X, Y), Z) -> div#(i(X), Z)}
      Weak:
      {     i(div(X, Y)) -> div(Y, X),
       div(div(X, Y), Z) -> div(Y, div(i(X), Z))}
      POLY:
       Argument Filtering:
        pi(div#) = 0, pi(div) = [0,1], pi(i#) = 0, pi(i) = 0
       Usable Rules:
        {}
       Interpretation:
        [div](x0, x1) = x0 + x1 + 1
       Strict:
        {}
       Weak:
        {     i(div(X, Y)) -> div(Y, X),
         div(div(X, Y), Z) -> div(Y, div(i(X), Z))}
       Qed