YES

Proof:
This system is quasi-decreasing.
By \cite{A14}, Theorem 11.5.9.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to V(R) + Emb.
Call external tool:
ttt2 - trs 30
Input:
  s(p(x)) -> x
  p(s(x)) -> x
  lte(s(x), y) -> lte(x, p(y))
  lte(p(x), y) -> lte(x, s(y))
  lte(0, 0) -> T
  lte(0, p(0)) -> F
  lte(0, s(x)) -> T
  lte(0, s(x)) -> lte(0, x)
  lte(0, p(x)) -> F
  lte(0, p(x)) -> lte(0, x)
  p(x) -> x
  s(x) -> x
  lte(x, y) -> x
  lte(x, y) -> y

 DP Processor:
  DPs:
   lte#(s(x),y) -> p#(y)
   lte#(s(x),y) -> lte#(x,p(y))
   lte#(p(x),y) -> s#(y)
   lte#(p(x),y) -> lte#(x,s(y))
   lte#(0(),s(x)) -> lte#(0(),x)
   lte#(0(),p(x)) -> lte#(0(),x)
  TRS:
   s(p(x)) -> x
   p(s(x)) -> x
   lte(s(x),y) -> lte(x,p(y))
   lte(p(x),y) -> lte(x,s(y))
   lte(0(),0()) -> T()
   lte(0(),p(0())) -> F()
   lte(0(),s(x)) -> T()
   lte(0(),s(x)) -> lte(0(),x)
   lte(0(),p(x)) -> F()
   lte(0(),p(x)) -> lte(0(),x)
   p(x) -> x
   s(x) -> x
   lte(x,y) -> x
   lte(x,y) -> y
  TDG Processor:
   DPs:
    lte#(s(x),y) -> p#(y)
    lte#(s(x),y) -> lte#(x,p(y))
    lte#(p(x),y) -> s#(y)
    lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> lte#(0(),x)
   TRS:
    s(p(x)) -> x
    p(s(x)) -> x
    lte(s(x),y) -> lte(x,p(y))
    lte(p(x),y) -> lte(x,s(y))
    lte(0(),0()) -> T()
    lte(0(),p(0())) -> F()
    lte(0(),s(x)) -> T()
    lte(0(),s(x)) -> lte(0(),x)
    lte(0(),p(x)) -> F()
    lte(0(),p(x)) -> lte(0(),x)
    p(x) -> x
    s(x) -> x
    lte(x,y) -> x
    lte(x,y) -> y
   graph:
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(p(x),y) -> s#(y)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(s(x),y) -> p#(y)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(p(x),y) -> s#(y)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(s(x),y) -> p#(y)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(p(x),y) -> s#(y)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(s(x),y) -> p#(y)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(p(x),y) -> s#(y)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(s(x),y) -> p#(y)
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 24/36
    DPs:
     lte#(0(),s(x)) -> lte#(0(),x)
     lte#(s(x),y) -> lte#(x,p(y))
     lte#(p(x),y) -> lte#(x,s(y))
     lte#(0(),p(x)) -> lte#(0(),x)
    TRS:
     s(p(x)) -> x
     p(s(x)) -> x
     lte(s(x),y) -> lte(x,p(y))
     lte(p(x),y) -> lte(x,s(y))
     lte(0(),0()) -> T()
     lte(0(),p(0())) -> F()
     lte(0(),s(x)) -> T()
     lte(0(),s(x)) -> lte(0(),x)
     lte(0(),p(x)) -> F()
     lte(0(),p(x)) -> lte(0(),x)
     p(x) -> x
     s(x) -> x
     lte(x,y) -> x
     lte(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(lte#) = 0
     problem:
      DPs:
       lte#(0(),s(x)) -> lte#(0(),x)
       lte#(0(),p(x)) -> lte#(0(),x)
      TRS:
       s(p(x)) -> x
       p(s(x)) -> x
       lte(s(x),y) -> lte(x,p(y))
       lte(p(x),y) -> lte(x,s(y))
       lte(0(),0()) -> T()
       lte(0(),p(0())) -> F()
       lte(0(),s(x)) -> T()
       lte(0(),s(x)) -> lte(0(),x)
       lte(0(),p(x)) -> F()
       lte(0(),p(x)) -> lte(0(),x)
       p(x) -> x
       s(x) -> x
       lte(x,y) -> x
       lte(x,y) -> y
     Subterm Criterion Processor:
      simple projection:
       pi(lte#) = 1
      problem:
       DPs:
        
       TRS:
        s(p(x)) -> x
        p(s(x)) -> x
        lte(s(x),y) -> lte(x,p(y))
        lte(p(x),y) -> lte(x,s(y))
        lte(0(),0()) -> T()
        lte(0(),p(0())) -> F()
        lte(0(),s(x)) -> T()
        lte(0(),s(x)) -> lte(0(),x)
        lte(0(),p(x)) -> F()
        lte(0(),p(x)) -> lte(0(),x)
        p(x) -> x
        s(x) -> x
        lte(x,y) -> x
        lte(x,y) -> y
      Qed