YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  s(p(x)) -> x
  p(s(x)) -> x
  pos(0) -> false
  pos(s(0)) -> true
  ?2(true, x) -> true
  pos(s(x)) -> ?2(pos(x), x)
  ?1(false, x) -> false
  pos(p(x)) -> ?1(pos(x), x)

 DP Processor:
  DPs:
   pos#(s(x)) -> pos#(x)
   pos#(s(x)) -> ?2#(pos(x),x)
   pos#(p(x)) -> pos#(x)
   pos#(p(x)) -> ?1#(pos(x),x)
  TRS:
   s(p(x)) -> x
   p(s(x)) -> x
   pos(0()) -> false()
   pos(s(0())) -> true()
   ?2(true(),x) -> true()
   pos(s(x)) -> ?2(pos(x),x)
   ?1(false(),x) -> false()
   pos(p(x)) -> ?1(pos(x),x)
  TDG Processor:
   DPs:
    pos#(s(x)) -> pos#(x)
    pos#(s(x)) -> ?2#(pos(x),x)
    pos#(p(x)) -> pos#(x)
    pos#(p(x)) -> ?1#(pos(x),x)
   TRS:
    s(p(x)) -> x
    p(s(x)) -> x
    pos(0()) -> false()
    pos(s(0())) -> true()
    ?2(true(),x) -> true()
    pos(s(x)) -> ?2(pos(x),x)
    ?1(false(),x) -> false()
    pos(p(x)) -> ?1(pos(x),x)
   graph:
    pos#(s(x)) -> pos#(x) -> pos#(p(x)) -> ?1#(pos(x),x)
    pos#(s(x)) -> pos#(x) -> pos#(p(x)) -> pos#(x)
    pos#(s(x)) -> pos#(x) -> pos#(s(x)) -> ?2#(pos(x),x)
    pos#(s(x)) -> pos#(x) -> pos#(s(x)) -> pos#(x)
    pos#(p(x)) -> pos#(x) -> pos#(p(x)) -> ?1#(pos(x),x)
    pos#(p(x)) -> pos#(x) -> pos#(p(x)) -> pos#(x)
    pos#(p(x)) -> pos#(x) -> pos#(s(x)) -> ?2#(pos(x),x)
    pos#(p(x)) -> pos#(x) -> pos#(s(x)) -> pos#(x)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 8/16
    DPs:
     pos#(s(x)) -> pos#(x)
     pos#(p(x)) -> pos#(x)
    TRS:
     s(p(x)) -> x
     p(s(x)) -> x
     pos(0()) -> false()
     pos(s(0())) -> true()
     ?2(true(),x) -> true()
     pos(s(x)) -> ?2(pos(x),x)
     ?1(false(),x) -> false()
     pos(p(x)) -> ?1(pos(x),x)
    Subterm Criterion Processor:
     simple projection:
      pi(pos#) = 0
     problem:
      DPs:
       
      TRS:
       s(p(x)) -> x
       p(s(x)) -> x
       pos(0()) -> false()
       pos(s(0())) -> true()
       ?2(true(),x) -> true()
       pos(s(x)) -> ?2(pos(x),x)
       ?1(false(),x) -> false()
       pos(p(x)) -> ?1(pos(x),x)
     Qed