YES
Time: 0.005857
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:
   DP:
    {      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)}
   TRS:
   {      i div(X, Y) -> div(Y, X),
    div(div(X, Y), Z) -> div(Y, div(i X, Z))}
   EDG:
    {(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) -> div#(i X, Z))
     (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) -> i# X)
     (div#(div(X, Y), Z) -> div#(Y, 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#(Y, 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) -> div#(i X, Z), div#(div(X, Y), Z) -> i# X)
     (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) -> div#(i X, Z))}
    SCCS (1):
     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 (4):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [div](x0, x1) = x0 + x1 + 1,
        
        [i](x0) = x0,
        
        [div#](x0, x1) = x0 + x1 + 1,
        
        [i#](x0) = x0 + 1
       Strict:
        div#(div(X, Y), Z) -> div#(i X, Z)
        2 + 1X + 1Y + 1Z >= 1 + 1X + 1Z
        div#(div(X, Y), Z) -> div#(Y, div(i X, Z))
        2 + 1X + 1Y + 1Z >= 2 + 1X + 1Y + 1Z
        div#(div(X, Y), Z) -> i# X
        2 + 1X + 1Y + 1Z >= 1 + 1X
        i# div(X, Y) -> div#(Y, X)
        2 + 1X + 1Y >= 1 + 1X + 1Y
       Weak:
        
      EDG:
       {(div#(div(X, Y), Z) -> div#(Y, div(i X, Z)), div#(div(X, Y), Z) -> div#(Y, div(i X, Z)))}
       SCCS (1):
        Scc:
         {div#(div(X, Y), Z) -> div#(Y, div(i X, Z))}
        SCC (1):
         Strict:
          {div#(div(X, Y), Z) -> div#(Y, div(i X, Z))}
         Weak:
         {      i div(X, Y) -> div(Y, X),
          div(div(X, Y), Z) -> div(Y, div(i X, Z))}
         SPSC:
          Simple Projection:
           pi(div#) = 0
          Strict:
           {}
          Qed