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))
  TDG 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) -> div#(Y,div(i(X),Z))
    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) -> i#(X)
    i#(div(X,Y)) -> div#(Y,X) -> div#(X,e()) -> i#(X)
    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) -> 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) -> div#(i(X),Z) -> div#(div(X,Y),Z) -> i#(X)
    div#(div(X,Y),Z) -> div#(i(X),Z) -> div#(X,e()) -> 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#(Y,div(i(X),Z)) ->
    div#(div(X,Y),Z) -> i#(X)
    div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) -> div#(X,e()) -> i#(X)
    div#(X,e()) -> i#(X) -> i#(div(X,Y)) -> div#(Y,X)
   EDG 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#(X,e()) -> i#(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#(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#(X,e()) -> i#(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)
    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) -> div#(Y,div(i(X),Z))
      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) -> i#(X)
      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) -> 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) -> 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#(Y,div(i(X),Z)) -> div#(div(X,Y),Z) -> i#(X)
      div#(X,e()) -> i#(X) -> i#(div(X,Y)) -> div#(Y,X)
     SCC Processor:
      #sccs: 1
      #rules: 4
      #arcs: 11/25
      DPs:
       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))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [i#](x0) = x0,
        
        [div#](x0, x1) = x0,
        
        [i](x0) = 1x0 + 3,
        
        [div](x0, x1) = 1x0 + x1 + 4,
        
        [e] = 6
       orientation:
        i#(div(X,Y)) = 1X + Y + 4 >= Y = div#(Y,X)
        
        div#(div(X,Y),Z) = 1X + Y + 4 >= X = i#(X)
        
        div#(div(X,Y),Z) = 1X + Y + 4 >= 1X + 3 = div#(i(X),Z)
        
        div#(div(X,Y),Z) = 1X + Y + 4 >= Y = div#(Y,div(i(X),Z))
        
        div(X,e()) = 1X + 6 >= 1X + 3 = i(X)
        
        i(div(X,Y)) = 2X + 1Y + 5 >= X + 1Y + 4 = div(Y,X)
        
        div(div(X,Y),Z) = 2X + 1Y + Z + 5 >= 2X + 1Y + Z + 4 = div(Y,div(i(X),Z))
       problem:
        DPs:
         i#(div(X,Y)) -> div#(Y,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: 2
        #arcs: 10/9
        DPs:
         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))
        KBO Processor:
         argument filtering:
          pi(e) = []
          pi(div) = [0,1]
          pi(i) = [0]
          pi(div#) = 0
         weight function:
          w0 = 1
          w(div#) = w(e) = 1
          w(i) = w(div) = 0
         precedence:
          i > div# ~ div ~ e
         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