6.41/2.26	YES
6.41/2.26	
6.41/2.26	Proof:
6.41/2.26	This system is confluent.
6.41/2.26	By \cite{ALS94}, Theorem 4.1.
6.41/2.26	This system is of type 3 or smaller.
6.41/2.26	This system is strongly deterministic.
6.41/2.26	This system is quasi-decreasing.
6.41/2.26	By \cite{O02}, p. 214, Proposition 7.2.50.
6.41/2.26	This system is of type 3 or smaller.
6.41/2.26	This system is deterministic.
6.41/2.26	System R transformed to optimized U(R).
6.41/2.26	This system is terminating.
6.41/2.26	Call external tool:
6.41/2.26	./ttt2.sh
6.41/2.26	Input:
6.41/2.26	  le(0, y) -> true
6.41/2.26	  split(x, nil) -> tp2(nil, nil)
6.41/2.26	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
6.41/2.26	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
6.41/2.26	  ?2(true, zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
6.41/2.26	  le(s(x), s(y)) -> le(x, y)
6.41/2.26	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
6.41/2.26	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
6.41/2.26	  ?2(false, zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
6.41/2.26	  le(s(x), 0) -> false
6.41/2.26	
6.41/2.26	 DP Processor:
6.41/2.26	  DPs:
6.41/2.26	   split#(x,cons(y,ys)) -> split#(x,ys)
6.41/2.26	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
6.41/2.26	   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
6.41/2.26	   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
6.41/2.26	   le#(s(x),s(y)) -> le#(x,y)
6.41/2.26	  TRS:
6.41/2.26	   le(0(),y) -> true()
6.41/2.26	   split(x,nil()) -> tp2(nil(),nil())
6.41/2.26	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.26	   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.26	   ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.26	   le(s(x),s(y)) -> le(x,y)
6.41/2.26	   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.26	   le(s(x),0()) -> false()
6.41/2.27	  TDG Processor:
6.41/2.27	   DPs:
6.41/2.27	    split#(x,cons(y,ys)) -> split#(x,ys)
6.41/2.27	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
6.41/2.27	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
6.41/2.27	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	    le#(s(x),s(y)) -> le#(x,y)
6.41/2.27	   TRS:
6.41/2.27	    le(0(),y) -> true()
6.41/2.27	    split(x,nil()) -> tp2(nil(),nil())
6.41/2.27	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.27	    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	    ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.27	    le(s(x),s(y)) -> le(x,y)
6.41/2.27	    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.27	    le(s(x),0()) -> false()
6.41/2.27	   graph:
6.41/2.27	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
6.41/2.27	    le#(s(x),s(y)) -> le#(x,y)
6.41/2.27	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
6.41/2.27	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
6.41/2.27	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
6.41/2.27	    split#(x,cons(y,ys)) -> split#(x,ys) ->
6.41/2.27	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
6.41/2.27	    split#(x,cons(y,ys)) -> split#(x,ys) ->
6.41/2.27	    split#(x,cons(y,ys)) -> split#(x,ys)
6.41/2.27	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
6.41/2.27	   SCC Processor:
6.41/2.27	    #sccs: 2
6.41/2.27	    #rules: 2
6.41/2.27	    #arcs: 6/25
6.41/2.27	    DPs:
6.41/2.27	     split#(x,cons(y,ys)) -> split#(x,ys)
6.41/2.27	    TRS:
6.41/2.27	     le(0(),y) -> true()
6.41/2.27	     split(x,nil()) -> tp2(nil(),nil())
6.41/2.27	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.27	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.27	     le(s(x),s(y)) -> le(x,y)
6.41/2.27	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.27	     le(s(x),0()) -> false()
6.41/2.27	    Subterm Criterion Processor:
6.41/2.27	     simple projection:
6.41/2.27	      pi(split#) = 1
6.41/2.27	     problem:
6.41/2.27	      DPs:
6.41/2.27	       
6.41/2.27	      TRS:
6.41/2.27	       le(0(),y) -> true()
6.41/2.27	       split(x,nil()) -> tp2(nil(),nil())
6.41/2.27	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.27	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.27	       le(s(x),s(y)) -> le(x,y)
6.41/2.27	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.27	       le(s(x),0()) -> false()
6.41/2.27	     Qed
6.41/2.27	    
6.41/2.27	    DPs:
6.41/2.27	     le#(s(x),s(y)) -> le#(x,y)
6.41/2.27	    TRS:
6.41/2.27	     le(0(),y) -> true()
6.41/2.27	     split(x,nil()) -> tp2(nil(),nil())
6.41/2.27	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.27	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.27	     le(s(x),s(y)) -> le(x,y)
6.41/2.27	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.27	     le(s(x),0()) -> false()
6.41/2.27	    Subterm Criterion Processor:
6.41/2.27	     simple projection:
6.41/2.27	      pi(le#) = 0
6.41/2.27	     problem:
6.41/2.27	      DPs:
6.41/2.27	       
6.41/2.27	      TRS:
6.41/2.27	       le(0(),y) -> true()
6.41/2.27	       split(x,nil()) -> tp2(nil(),nil())
6.41/2.27	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
6.41/2.27	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
6.41/2.27	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
6.41/2.27	       le(s(x),s(y)) -> le(x,y)
6.41/2.27	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
6.41/2.27	       le(s(x),0()) -> false()
6.41/2.27	     Qed
6.41/2.27	All 2 critical pairs are joinable.
6.41/2.27	Overlap: (rule1: split(z', cons(x', $1)) -> tp2(cons(x', y'), z) <= split(z', $1) = tp2(y', z), le(z', x') = false, rule2: split($3, cons($6, $5)) -> tp2($4, cons($6, $2)) <= split($3, $5) = tp2($4, $2), le($3, $6) = true, pos: ε, mgu: {($3,z'), ($6,x'), ($5,$1)})
6.41/2.27	CP: tp2($4, cons(x', $2)) = tp2(cons(x', y'), z) <= split(z', $1) = tp2(y', z), le(z', x') = false, split(z', $1) = tp2($4, $2), le(z', x') = true
6.41/2.27	This critical pair is unfeasible.
6.41/2.27	Overlap: (rule1: split(z', cons(x', $1)) -> tp2(y', cons(x', z)) <= split(z', $1) = tp2(y', z), le(z', x') = true, rule2: split($3, cons($6, $5)) -> tp2(cons($6, $4), $2) <= split($3, $5) = tp2($4, $2), le($3, $6) = false, pos: ε, mgu: {($3,z'), ($6,x'), ($5,$1)})
6.41/2.27	CP: tp2(cons(x', $4), $2) = tp2(y', cons(x', z)) <= split(z', $1) = tp2(y', z), le(z', x') = true, split(z', $1) = tp2($4, $2), le(z', x') = false
6.41/2.27	This critical pair is unfeasible.
6.41/2.27	
7.19/2.44	EOF