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:
  p(q(x)) -> p(r(x))
  q(h(x)) -> r(x)
  ?1(0, x) -> r(h(x))
  r(x) -> ?1(s(x), x)
  s(x) -> 1

 DP Processor:
  DPs:
   p#(q(x)) -> r#(x)
   p#(q(x)) -> p#(r(x))
   q#(h(x)) -> r#(x)
   ?1#(0(),x) -> r#(h(x))
   r#(x) -> s#(x)
   r#(x) -> ?1#(s(x),x)
  TRS:
   p(q(x)) -> p(r(x))
   q(h(x)) -> r(x)
   ?1(0(),x) -> r(h(x))
   r(x) -> ?1(s(x),x)
   s(x) -> 1()
  TDG Processor:
   DPs:
    p#(q(x)) -> r#(x)
    p#(q(x)) -> p#(r(x))
    q#(h(x)) -> r#(x)
    ?1#(0(),x) -> r#(h(x))
    r#(x) -> s#(x)
    r#(x) -> ?1#(s(x),x)
   TRS:
    p(q(x)) -> p(r(x))
    q(h(x)) -> r(x)
    ?1(0(),x) -> r(h(x))
    r(x) -> ?1(s(x),x)
    s(x) -> 1()
   graph:
    ?1#(0(),x) -> r#(h(x)) -> r#(x) -> ?1#(s(x),x)
    ?1#(0(),x) -> r#(h(x)) -> r#(x) -> s#(x)
    q#(h(x)) -> r#(x) -> r#(x) -> ?1#(s(x),x)
    q#(h(x)) -> r#(x) -> r#(x) -> s#(x)
    r#(x) -> ?1#(s(x),x) -> ?1#(0(),x) -> r#(h(x))
    p#(q(x)) -> r#(x) -> r#(x) -> ?1#(s(x),x)
    p#(q(x)) -> r#(x) -> r#(x) -> s#(x)
    p#(q(x)) -> p#(r(x)) -> p#(q(x)) -> p#(r(x))
    p#(q(x)) -> p#(r(x)) -> p#(q(x)) -> r#(x)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 9/36
    DPs:
     p#(q(x)) -> p#(r(x))
    TRS:
     p(q(x)) -> p(r(x))
     q(h(x)) -> r(x)
     ?1(0(),x) -> r(h(x))
     r(x) -> ?1(s(x),x)
     s(x) -> 1()
    EDG Processor:
     DPs:
      p#(q(x)) -> p#(r(x))
     TRS:
      p(q(x)) -> p(r(x))
      q(h(x)) -> r(x)
      ?1(0(),x) -> r(h(x))
      r(x) -> ?1(s(x),x)
      s(x) -> 1()
     graph:
      
     Qed
    
    DPs:
     ?1#(0(),x) -> r#(h(x))
     r#(x) -> ?1#(s(x),x)
    TRS:
     p(q(x)) -> p(r(x))
     q(h(x)) -> r(x)
     ?1(0(),x) -> r(h(x))
     r(x) -> ?1(s(x),x)
     s(x) -> 1()
    EDG Processor:
     DPs:
      ?1#(0(),x) -> r#(h(x))
      r#(x) -> ?1#(s(x),x)
     TRS:
      p(q(x)) -> p(r(x))
      q(h(x)) -> r(x)
      ?1(0(),x) -> r(h(x))
      r(x) -> ?1(s(x),x)
      s(x) -> 1()
     graph:
      ?1#(0(),x) -> r#(h(x)) -> r#(x) -> ?1#(s(x),x)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 1/4