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:
  split(x, nil) -> tp2(nil, nil)
  ?4(true, zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
  ?3(tp2(zs1, zs2), x, y, ys) -> ?4(le(x, y), zs2, x, ys, zs1, y)
  split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys)
  ?2(false, zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
  le(0, y) -> true
  le(s(x), 0) -> false
  le(s(x), s(y)) -> le(x, y)

 DP Processor:
  DPs:
   ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
   ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
   split#(x,cons(y,ys)) -> split#(x,ys)
   split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
   le#(s(x),s(y)) -> le#(x,y)
  TRS:
   split(x,nil()) -> tp2(nil(),nil())
   ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
   ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
   split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
  TDG Processor:
   DPs:
    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
    split#(x,cons(y,ys)) -> split#(x,ys)
    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
    le#(s(x),s(y)) -> le#(x,y)
   TRS:
    split(x,nil()) -> tp2(nil(),nil())
    ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
    ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
    split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
   graph:
    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
    split#(x,cons(y,ys)) -> split#(x,ys) ->
    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
    split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 10/64
    DPs:
     split#(x,cons(y,ys)) -> split#(x,ys)
    TRS:
     split(x,nil()) -> tp2(nil(),nil())
     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(split#) = 1
     problem:
      DPs:
       
      TRS:
       split(x,nil()) -> tp2(nil(),nil())
       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     split(x,nil()) -> tp2(nil(),nil())
     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 0
     problem:
      DPs:
       
      TRS:
       split(x,nil()) -> tp2(nil(),nil())
       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
     Qed