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:
  ssp(nil, 0) -> nil
  ?3(xs, y, ys', v) -> xs
  ssp(cons(y, ys'), v) -> ?3(ssp(ys', v), y, ys', v)
  ?2(xs', y, ys', v, w) -> cons(y, xs')
  ?1(w, y, ys', v) -> ?2(ssp(ys', w), y, ys', v, w)
  ssp(cons(y, ys'), v) -> ?1(sub(v, y), y, ys', v)
  sub(z, 0) -> z
  ?4(z, v, w) -> z
  sub(s(v), s(w)) -> ?4(sub(v, w), v, w)

 DP Processor:
  DPs:
   ssp#(cons(y,ys'),v) -> ssp#(ys',v)
   ssp#(cons(y,ys'),v) -> ?3#(ssp(ys',v),y,ys',v)
   ?1#(w,y,ys',v) -> ssp#(ys',w)
   ?1#(w,y,ys',v) -> ?2#(ssp(ys',w),y,ys',v,w)
   ssp#(cons(y,ys'),v) -> sub#(v,y)
   ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v)
   sub#(s(v),s(w)) -> sub#(v,w)
   sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
  TRS:
   ssp(nil(),0()) -> nil()
   ?3(xs,y,ys',v) -> xs
   ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
   ?2(xs',y,ys',v,w) -> cons(y,xs')
   ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
   ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
   sub(z,0()) -> z
   ?4(z,v,w) -> z
   sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
  TDG Processor:
   DPs:
    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
    ssp#(cons(y,ys'),v) -> ?3#(ssp(ys',v),y,ys',v)
    ?1#(w,y,ys',v) -> ssp#(ys',w)
    ?1#(w,y,ys',v) -> ?2#(ssp(ys',w),y,ys',v,w)
    ssp#(cons(y,ys'),v) -> sub#(v,y)
    ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v)
    sub#(s(v),s(w)) -> sub#(v,w)
    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
   TRS:
    ssp(nil(),0()) -> nil()
    ?3(xs,y,ys',v) -> xs
    ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
    ?2(xs',y,ys',v,w) -> cons(y,xs')
    ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
    ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
    sub(z,0()) -> z
    ?4(z,v,w) -> z
    sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
   graph:
    sub#(s(v),s(w)) -> sub#(v,w) ->
    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
    sub#(s(v),s(w)) -> sub#(v,w) -> sub#(s(v),s(w)) -> sub#(v,w)
    ?1#(w,y,ys',v) -> ssp#(ys',w) ->
    ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v)
    ?1#(w,y,ys',v) -> ssp#(ys',w) -> ssp#(cons(y,ys'),v) -> sub#(v,y)
    ?1#(w,y,ys',v) -> ssp#(ys',w) ->
    ssp#(cons(y,ys'),v) -> ?3#(ssp(ys',v),y,ys',v)
    ?1#(w,y,ys',v) -> ssp#(ys',w) ->
    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
    ssp#(cons(y,ys'),v) -> sub#(v,y) ->
    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
    ssp#(cons(y,ys'),v) -> sub#(v,y) ->
    sub#(s(v),s(w)) -> sub#(v,w)
    ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v) ->
    ?1#(w,y,ys',v) -> ?2#(ssp(ys',w),y,ys',v,w)
    ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v) ->
    ?1#(w,y,ys',v) -> ssp#(ys',w)
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
    ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v)
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
    ssp#(cons(y,ys'),v) -> sub#(v,y)
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
    ssp#(cons(y,ys'),v) -> ?3#(ssp(ys',v),y,ys',v)
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) -> ssp#(cons(y,ys'),v) -> ssp#(ys',v)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 14/64
    DPs:
     ?1#(w,y,ys',v) -> ssp#(ys',w)
     ssp#(cons(y,ys'),v) -> ssp#(ys',v)
     ssp#(cons(y,ys'),v) -> ?1#(sub(v,y),y,ys',v)
    TRS:
     ssp(nil(),0()) -> nil()
     ?3(xs,y,ys',v) -> xs
     ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
     ?2(xs',y,ys',v,w) -> cons(y,xs')
     ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
     ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
     sub(z,0()) -> z
     ?4(z,v,w) -> z
     sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
    Subterm Criterion Processor:
     simple projection:
      pi(ssp#) = 0
      pi(?1#) = 2
     problem:
      DPs:
       ?1#(w,y,ys',v) -> ssp#(ys',w)
      TRS:
       ssp(nil(),0()) -> nil()
       ?3(xs,y,ys',v) -> xs
       ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
       ?2(xs',y,ys',v,w) -> cons(y,xs')
       ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
       ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
       sub(z,0()) -> z
       ?4(z,v,w) -> z
       sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 5/1
      
    
    DPs:
     sub#(s(v),s(w)) -> sub#(v,w)
    TRS:
     ssp(nil(),0()) -> nil()
     ?3(xs,y,ys',v) -> xs
     ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
     ?2(xs',y,ys',v,w) -> cons(y,xs')
     ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
     ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
     sub(z,0()) -> z
     ?4(z,v,w) -> z
     sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
    Subterm Criterion Processor:
     simple projection:
      pi(sub#) = 0
     problem:
      DPs:
       
      TRS:
       ssp(nil(),0()) -> nil()
       ?3(xs,y,ys',v) -> xs
       ssp(cons(y,ys'),v) -> ?3(ssp(ys',v),y,ys',v)
       ?2(xs',y,ys',v,w) -> cons(y,xs')
       ?1(w,y,ys',v) -> ?2(ssp(ys',w),y,ys',v,w)
       ssp(cons(y,ys'),v) -> ?1(sub(v,y),y,ys',v)
       sub(z,0()) -> z
       ?4(z,v,w) -> z
       sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
     Qed