YES

Problem:
 msort(nil()) -> nil()
 msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
 min(x,nil()) -> x
 min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
 del(x,nil()) -> nil()
 del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))

Proof:
 DP Processor:
  DPs:
   msort#(.(x,y)) -> del#(min(x,y),.(x,y))
   msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y)))
   msort#(.(x,y)) -> min#(x,y)
   min#(x,.(y,z)) -> min#(y,z)
   min#(x,.(y,z)) -> min#(x,z)
   del#(x,.(y,z)) -> del#(x,z)
  TRS:
   msort(nil()) -> nil()
   msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
   min(x,nil()) -> x
   min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
   del(x,nil()) -> nil()
   del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
  TDG Processor:
   DPs:
    msort#(.(x,y)) -> del#(min(x,y),.(x,y))
    msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y)))
    msort#(.(x,y)) -> min#(x,y)
    min#(x,.(y,z)) -> min#(y,z)
    min#(x,.(y,z)) -> min#(x,z)
    del#(x,.(y,z)) -> del#(x,z)
   TRS:
    msort(nil()) -> nil()
    msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
    min(x,nil()) -> x
    min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
    del(x,nil()) -> nil()
    del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
   graph:
    min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(x,z)
    min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(y,z)
    min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(x,z)
    min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(y,z)
    del#(x,.(y,z)) -> del#(x,z) -> del#(x,.(y,z)) -> del#(x,z)
    msort#(.(x,y)) -> min#(x,y) -> min#(x,.(y,z)) -> min#(x,z)
    msort#(.(x,y)) -> min#(x,y) ->
    min#(x,.(y,z)) -> min#(y,z)
    msort#(.(x,y)) -> del#(min(x,y),.(x,y)) ->
    del#(x,.(y,z)) -> del#(x,z)
    msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) ->
    msort#(.(x,y)) -> min#(x,y)
    msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) ->
    msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y)))
    msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) -> msort#(.(x,y)) -> del#(min(x,y),.(x,y))
   CDG Processor:
    DPs:
     msort#(.(x,y)) -> del#(min(x,y),.(x,y))
     msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y)))
     msort#(.(x,y)) -> min#(x,y)
     min#(x,.(y,z)) -> min#(y,z)
     min#(x,.(y,z)) -> min#(x,z)
     del#(x,.(y,z)) -> del#(x,z)
    TRS:
     msort(nil()) -> nil()
     msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
     min(x,nil()) -> x
     min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
     del(x,nil()) -> nil()
     del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
    graph:
     min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(y,z)
     min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(x,z)
     min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(y,z)
     min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(x,z)
     del#(x,.(y,z)) -> del#(x,z) -> del#(x,.(y,z)) -> del#(x,z)
     msort#(.(x,y)) -> min#(x,y) -> min#(x,.(y,z)) -> min#(y,z)
     msort#(.(x,y)) -> min#(x,y) ->
     min#(x,.(y,z)) -> min#(x,z)
     msort#(.(x,y)) -> del#(min(x,y),.(x,y)) -> del#(x,.(y,z)) -> del#(x,z)
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 8/36
     DPs:
      del#(x,.(y,z)) -> del#(x,z)
     TRS:
      msort(nil()) -> nil()
      msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
      min(x,nil()) -> x
      min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
      del(x,nil()) -> nil()
      del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
     KBO Processor:
      argument filtering:
       pi(nil) = []
       pi(msort) = [0]
       pi(.) = [0,1]
       pi(min) = [0]
       pi(del) = []
       pi(<=) = 1
       pi(if) = []
       pi(=) = 1
       pi(del#) = 1
      weight function:
       w0 = 1
       w(del#) = w(=) = w(if) = w(<=) = w(del) = w(.) = w(msort) = w(nil) = 1
       w(min) = 0
      precedence:
       = > del# ~ <= ~ del ~ min ~ msort > if ~ . ~ nil
      problem:
       DPs:
        
       TRS:
        msort(nil()) -> nil()
        msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
        min(x,nil()) -> x
        min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
        del(x,nil()) -> nil()
        del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
      Qed
     
     DPs:
      min#(x,.(y,z)) -> min#(y,z)
      min#(x,.(y,z)) -> min#(x,z)
     TRS:
      msort(nil()) -> nil()
      msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
      min(x,nil()) -> x
      min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
      del(x,nil()) -> nil()
      del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
     KBO Processor:
      argument filtering:
       pi(nil) = []
       pi(msort) = [0]
       pi(.) = [1]
       pi(min) = [0]
       pi(del) = []
       pi(<=) = 0
       pi(if) = 0
       pi(=) = []
       pi(min#) = 1
      weight function:
       w0 = 1
       w(min#) = w(=) = w(if) = w(<=) = w(del) = w(.) = w(nil) = 1
       w(min) = w(msort) = 0
      precedence:
       if ~ <= ~ min ~ msort > del > min# ~ = ~ . ~ nil
      problem:
       DPs:
        
       TRS:
        msort(nil()) -> nil()
        msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
        min(x,nil()) -> x
        min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
        del(x,nil()) -> nil()
        del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
      Qed