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))
      KBO Processor:
       argument filtering:
        pi(e) = []
        pi(div) = [0,1]
        pi(i) = [0]
        pi(div#) = [0]
        pi(i#) = 0
       weight function:
        w0 = 1
        w(i#) = w(div#) = w(div) = w(e) = 1
        w(i) = 0
       precedence:
        i# ~ div# ~ i ~ e > div
       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