YES

Problem:
 div(X,e()) -> i(X)
 i(div(X,Y)) -> div(Y,X)
 div(div(X,Y),Z) -> div(Y,div(i(X),Z))

Proof:
 DP Processor:
  DPs:
   div#(X,e()) -> i#(X)
   i#(div(X,Y)) -> div#(Y,X)
   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))
  TRS:
   div(X,e()) -> i(X)
   i(div(X,Y)) -> div(Y,X)
   div(div(X,Y),Z) -> div(Y,div(i(X),Z))
  CDG Processor:
   DPs:
    div#(X,e()) -> i#(X)
    i#(div(X,Y)) -> div#(Y,X)
    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))
   TRS:
    div(X,e()) -> i(X)
    i(div(X,Y)) -> div(Y,X)
    div(div(X,Y),Z) -> div(Y,div(i(X),Z))
   graph:
    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#(i(X),Z)
    i#(div(X,Y)) -> div#(Y,X) -> div#(div(X,Y),Z) -> div#(Y,div(i(X),Z))
    div#(div(X,Y),Z) -> i#(X) -> i#(div(X,Y)) -> div#(Y,X)
    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#(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) -> 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#(X,e()) -> i#(X) -> i#(div(X,Y)) -> div#(Y,X)
   Restore Modifier:
    DPs:
     div#(X,e()) -> i#(X)
     i#(div(X,Y)) -> div#(Y,X)
     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))
    TRS:
     div(X,e()) -> i(X)
     i(div(X,Y)) -> div(Y,X)
     div(div(X,Y),Z) -> div(Y,div(i(X),Z))
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 11/25
     DPs:
      i#(div(X,Y)) -> div#(Y,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) -> i#(X)
     TRS:
      div(X,e()) -> i(X)
      i(div(X,Y)) -> div(Y,X)
      div(div(X,Y),Z) -> div(Y,div(i(X),Z))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [i#](x0) = x0,
       
       [div#](x0, x1) = x0 + 1,
       
       [i](x0) = x0,
       
       [div](x0, x1) = x0 + x1 + 1,
       
       [e] = 1
      orientation:
       i#(div(X,Y)) = X + Y + 1 >= Y + 1 = div#(Y,X)
       
       div#(div(X,Y),Z) = X + Y + 2 >= Y + 1 = div#(Y,div(i(X),Z))
       
       div#(div(X,Y),Z) = X + Y + 2 >= X + 1 = div#(i(X),Z)
       
       div#(div(X,Y),Z) = X + Y + 2 >= X = i#(X)
       
       div(X,e()) = X + 2 >= X = i(X)
       
       i(div(X,Y)) = X + Y + 1 >= X + Y + 1 = div(Y,X)
       
       div(div(X,Y),Z) = X + Y + Z + 2 >= X + Y + Z + 2 = div(Y,div(i(X),Z))
      problem:
       DPs:
        i#(div(X,Y)) -> div#(Y,X)
       TRS:
        div(X,e()) -> i(X)
        i(div(X,Y)) -> div(Y,X)
        div(div(X,Y),Z) -> div(Y,div(i(X),Z))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [i#](x0) = 1,
        
        [div#](x0, x1) = 0,
        
        [i](x0) = 0,
        
        [div](x0, x1) = 0,
        
        [e] = 0
       orientation:
        i#(div(X,Y)) = 1 >= 0 = div#(Y,X)
        
        div(X,e()) = 0 >= 0 = i(X)
        
        i(div(X,Y)) = 0 >= 0 = div(Y,X)
        
        div(div(X,Y),Z) = 0 >= 0 = div(Y,div(i(X),Z))
       problem:
        DPs:
         
        TRS:
         div(X,e()) -> i(X)
         i(div(X,Y)) -> div(Y,X)
         div(div(X,Y),Z) -> div(Y,div(i(X),Z))
       Qed