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:
  ssp(nil, 0) -> nil
  ssp(cons(y, ys'), v) -> ssp(ys', v)
  ssp(cons(y, ys'), v) -> cons(y, ssp(ys', sub(v, y)))
  ssp(cons(y, ys'), v) -> ssp(ys', sub(v, y))
  ssp(cons(y, ys'), v) -> sub(v, y)
  sub(z, 0) -> z
  sub(s(v), s(w)) -> sub(v, w)
  s(x) -> x
  sub(x, y) -> x
  sub(x, y) -> y
  ssp(x, y) -> x
  ssp(x, y) -> y
  cons(x, y) -> x
  cons(x, y) -> y

 DP Processor:
  DPs:
   ssp#(cons(y,ys'),v) -> ssp#(ys',v)
   ssp#(cons(y,ys'),v) -> sub#(v,y)
   ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y))
   ssp#(cons(y,ys'),v) -> cons#(y,ssp(ys',sub(v,y)))
   sub#(s(v),s(w)) -> sub#(v,w)
  TRS:
   ssp(nil(),0()) -> nil()
   ssp(cons(y,ys'),v) -> ssp(ys',v)
   ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
   ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
   ssp(cons(y,ys'),v) -> sub(v,y)
   sub(z,0()) -> z
   sub(s(v),s(w)) -> sub(v,w)
   s(x) -> x
   sub(x,y) -> x
   sub(x,y) -> y
   ssp(x,y) -> x
   ssp(x,y) -> y
   cons(x,y) -> x
   cons(x,y) -> y
  TDG Processor:
   DPs:
    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
    ssp#(cons(y,ys'),v) -> sub#(v,y)
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y))
    ssp#(cons(y,ys'),v) -> cons#(y,ssp(ys',sub(v,y)))
    sub#(s(v),s(w)) -> sub#(v,w)
   TRS:
    ssp(nil(),0()) -> nil()
    ssp(cons(y,ys'),v) -> ssp(ys',v)
    ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
    ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
    ssp(cons(y,ys'),v) -> sub(v,y)
    sub(z,0()) -> z
    sub(s(v),s(w)) -> sub(v,w)
    s(x) -> x
    sub(x,y) -> x
    sub(x,y) -> y
    ssp(x,y) -> x
    ssp(x,y) -> y
    cons(x,y) -> x
    cons(x,y) -> y
   graph:
    sub#(s(v),s(w)) -> sub#(v,w) -> sub#(s(v),s(w)) -> sub#(v,w)
    ssp#(cons(y,ys'),v) -> sub#(v,y) ->
    sub#(s(v),s(w)) -> sub#(v,w)
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y)) ->
    ssp#(cons(y,ys'),v) -> cons#(y,ssp(ys',sub(v,y)))
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y)) ->
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y))
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y)) ->
    ssp#(cons(y,ys'),v) -> sub#(v,y)
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y)) ->
    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
    ssp#(cons(y,ys'),v) -> cons#(y,ssp(ys',sub(v,y)))
    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
    ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y))
    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) -> ssp#(ys',v)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 10/25
    DPs:
     ssp#(cons(y,ys'),v) -> ssp#(ys',sub(v,y))
     ssp#(cons(y,ys'),v) -> ssp#(ys',v)
    TRS:
     ssp(nil(),0()) -> nil()
     ssp(cons(y,ys'),v) -> ssp(ys',v)
     ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
     ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
     ssp(cons(y,ys'),v) -> sub(v,y)
     sub(z,0()) -> z
     sub(s(v),s(w)) -> sub(v,w)
     s(x) -> x
     sub(x,y) -> x
     sub(x,y) -> y
     ssp(x,y) -> x
     ssp(x,y) -> y
     cons(x,y) -> x
     cons(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(ssp#) = 0
     problem:
      DPs:
       
      TRS:
       ssp(nil(),0()) -> nil()
       ssp(cons(y,ys'),v) -> ssp(ys',v)
       ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
       ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
       ssp(cons(y,ys'),v) -> sub(v,y)
       sub(z,0()) -> z
       sub(s(v),s(w)) -> sub(v,w)
       s(x) -> x
       sub(x,y) -> x
       sub(x,y) -> y
       ssp(x,y) -> x
       ssp(x,y) -> y
       cons(x,y) -> x
       cons(x,y) -> y
     Qed
    
    DPs:
     sub#(s(v),s(w)) -> sub#(v,w)
    TRS:
     ssp(nil(),0()) -> nil()
     ssp(cons(y,ys'),v) -> ssp(ys',v)
     ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
     ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
     ssp(cons(y,ys'),v) -> sub(v,y)
     sub(z,0()) -> z
     sub(s(v),s(w)) -> sub(v,w)
     s(x) -> x
     sub(x,y) -> x
     sub(x,y) -> y
     ssp(x,y) -> x
     ssp(x,y) -> y
     cons(x,y) -> x
     cons(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(sub#) = 0
     problem:
      DPs:
       
      TRS:
       ssp(nil(),0()) -> nil()
       ssp(cons(y,ys'),v) -> ssp(ys',v)
       ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
       ssp(cons(y,ys'),v) -> ssp(ys',sub(v,y))
       ssp(cons(y,ys'),v) -> sub(v,y)
       sub(z,0()) -> z
       sub(s(v),s(w)) -> sub(v,w)
       s(x) -> x
       sub(x,y) -> x
       sub(x,y) -> y
       ssp(x,y) -> x
       ssp(x,y) -> y
       cons(x,y) -> x
       cons(x,y) -> y
     Qed