11.42/3.55	YES
11.42/3.55	
11.42/3.55	Problem:
11.42/3.55	split(x, nil()) -> tp2(nil(), nil())
11.42/3.55	split(x, cons(y, ys)) -> tp2(zs1, cons(y, zs2)) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = true()
11.42/3.55	split(x, cons(y, ys)) -> tp2(cons(y, zs1), zs2) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = false()
11.42/3.55	le(0(), y) -> true()
11.42/3.55	le(s(x), 0()) -> false()
11.42/3.55	le(s(x), s(y)) -> le(x, y)
11.42/3.55	
11.42/3.55	Proof:
11.42/3.55	This system is confluent.
11.42/3.55	By \cite{SMI95}, Corollary 4.7 or 5.3.
11.42/3.55	This system is oriented.
11.42/3.55	This system is of type 3 or smaller.
11.42/3.55	This system is right-stable.
11.42/3.55	This system is properly oriented.
11.42/3.55	This is an overlay system.
11.42/3.55	This system is left-linear.
11.42/3.55	All 2 critical pairs are trivial or infeasible.
11.42/3.55	CP: tp2($7, cons($6, y)) = tp2(cons($6, x), $3) <= split($5, $8) = tp2(x, $3), le($5, $6) = false(), split($5, $8) = tp2($7, y), le($5, $6) = true():
11.42/3.55	This critical pair is infeasible.
11.42/3.55	This critical pair is conditional.
11.42/3.55	This critical pair has some non-trivial conditions.
11.42/3.55	This system is of type 3 or smaller.
11.42/3.55	This system is deterministic.
11.42/3.55	This system is quasi-decreasing.
11.42/3.55	By \cite{O02}, p. 214, Proposition 7.2.50.
11.42/3.55	This system is of type 3 or smaller.
11.42/3.55	This system is deterministic.
11.42/3.55	System R transformed to optimized U(R).
11.42/3.55	This system is terminating.
11.42/3.55	Call external tool:
11.42/3.55	./ttt2.sh
11.42/3.55	Input:
11.42/3.55	  split(x, nil()) -> tp2(nil(), nil())
11.42/3.55	  ?1(true(), zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
11.42/3.55	  ?2(tp2(zs1, zs2), x, y, ys) -> ?1(le(x, y), zs2, x, ys, zs1, y)
11.42/3.55	  split(x, cons(y, ys)) -> ?2(split(x, ys), x, y, ys)
11.42/3.55	  ?1(false(), zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
11.42/3.55	  le(0(), y) -> true()
11.42/3.55	  le(s(x), 0()) -> false()
11.42/3.55	  le(s(x), s(y)) -> le(x, y)
11.42/3.55	
11.42/3.55	 DP Processor:
11.42/3.55	  DPs:
11.42/3.55	   ?2#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.55	   ?2#(tp2(zs1,zs2),x,y,ys) -> ?1#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.55	   split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.55	   split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
11.42/3.55	   le#(s(x),s(y)) -> le#(x,y)
11.42/3.55	  TRS:
11.42/3.55	   split(x,nil()) -> tp2(nil(),nil())
11.42/3.55	   ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.55	   ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.55	   split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.55	   ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.55	   le(0(),y) -> true()
11.42/3.55	   le(s(x),0()) -> false()
11.42/3.55	   le(s(x),s(y)) -> le(x,y)
11.42/3.55	  TDG Processor:
11.42/3.55	   DPs:
11.42/3.55	    ?2#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.55	    ?2#(tp2(zs1,zs2),x,y,ys) -> ?1#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.55	    split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.55	    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
11.42/3.55	    le#(s(x),s(y)) -> le#(x,y)
11.42/3.55	   TRS:
11.42/3.55	    split(x,nil()) -> tp2(nil(),nil())
11.42/3.55	    ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.55	    ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.55	    split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.55	    ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.55	    le(0(),y) -> true()
11.42/3.55	    le(s(x),0()) -> false()
11.42/3.55	    le(s(x),s(y)) -> le(x,y)
11.42/3.56	   graph:
11.42/3.56	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
11.42/3.56	    ?2#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
11.42/3.56	    le#(s(x),s(y)) -> le#(x,y)
11.42/3.56	    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) ->
11.42/3.56	    ?2#(tp2(zs1,zs2),x,y,ys) -> ?1#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) ->
11.42/3.56	    ?2#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.56	    split#(x,cons(y,ys)) -> split#(x,ys) ->
11.42/3.56	    split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys)
11.42/3.56	    split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.56	   SCC Processor:
11.42/3.56	    #sccs: 2
11.42/3.56	    #rules: 2
11.42/3.56	    #arcs: 6/25
11.42/3.56	    DPs:
11.42/3.56	     split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.56	    TRS:
11.42/3.56	     split(x,nil()) -> tp2(nil(),nil())
11.42/3.56	     ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.56	     ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.56	     ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.56	     le(0(),y) -> true()
11.42/3.56	     le(s(x),0()) -> false()
11.42/3.56	     le(s(x),s(y)) -> le(x,y)
11.42/3.56	    Subterm Criterion Processor:
11.42/3.56	     simple projection:
11.42/3.56	      pi(split#) = 1
11.42/3.56	     problem:
11.42/3.56	      DPs:
11.42/3.56	       
11.42/3.56	      TRS:
11.42/3.56	       split(x,nil()) -> tp2(nil(),nil())
11.42/3.56	       ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.56	       ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.56	       ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.56	       le(0(),y) -> true()
11.42/3.56	       le(s(x),0()) -> false()
11.42/3.56	       le(s(x),s(y)) -> le(x,y)
11.42/3.56	     Qed
11.42/3.56	    
11.42/3.56	    DPs:
11.42/3.56	     le#(s(x),s(y)) -> le#(x,y)
11.42/3.56	    TRS:
11.42/3.56	     split(x,nil()) -> tp2(nil(),nil())
11.42/3.56	     ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.56	     ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	     split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.56	     ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.56	     le(0(),y) -> true()
11.42/3.56	     le(s(x),0()) -> false()
11.42/3.56	     le(s(x),s(y)) -> le(x,y)
11.42/3.56	    Subterm Criterion Processor:
11.42/3.56	     simple projection:
11.42/3.56	      pi(le#) = 0
11.42/3.56	     problem:
11.42/3.56	      DPs:
11.42/3.56	       
11.42/3.56	      TRS:
11.42/3.56	       split(x,nil()) -> tp2(nil(),nil())
11.42/3.56	       ?1(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.56	       ?2(tp2(zs1,zs2),x,y,ys) -> ?1(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	       split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys)
11.42/3.56	       ?1(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.56	       le(0(),y) -> true()
11.42/3.56	       le(s(x),0()) -> false()
11.42/3.56	       le(s(x),s(y)) -> le(x,y)
11.42/3.56	     Qed
11.42/3.56	This critical pair is unfeasible.
11.42/3.56	CP: tp2(cons($6, $7), y) = tp2(x, cons($6, $3)) <= split($5, $8) = tp2(x, $3), le($5, $6) = true(), split($5, $8) = tp2($7, y), le($5, $6) = false():
11.42/3.56	This critical pair is infeasible.
11.42/3.56	This critical pair is conditional.
11.42/3.56	This critical pair has some non-trivial conditions.
11.42/3.56	This system is of type 3 or smaller.
11.42/3.56	This system is deterministic.
11.42/3.56	This system is quasi-decreasing.
11.42/3.56	By \cite{O02}, p. 214, Proposition 7.2.50.
11.42/3.56	This system is of type 3 or smaller.
11.42/3.56	This system is deterministic.
11.42/3.56	System R transformed to U(R).
11.42/3.56	This system is terminating.
11.42/3.56	Call external tool:
11.42/3.56	./ttt2.sh
11.42/3.56	Input:
11.42/3.56	  split(x, nil()) -> tp2(nil(), nil())
11.42/3.56	  ?4(true(), zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
11.42/3.56	  ?3(tp2(zs1, zs2), x, y, ys) -> ?4(le(x, y), zs2, x, ys, zs1, y)
11.42/3.56	  split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys)
11.42/3.56	  ?2(false(), zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
11.42/3.56	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
11.42/3.56	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
11.42/3.56	  le(0(), y) -> true()
11.42/3.56	  le(s(x), 0()) -> false()
11.42/3.56	  le(s(x), s(y)) -> le(x, y)
11.42/3.56	
11.42/3.56	 DP Processor:
11.42/3.56	  DPs:
11.42/3.56	   ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.56	   ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	   split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.56	   split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.42/3.56	   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.56	   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.42/3.56	   le#(s(x),s(y)) -> le#(x,y)
11.42/3.56	  TRS:
11.42/3.56	   split(x,nil()) -> tp2(nil(),nil())
11.42/3.56	   ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.56	   ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	   split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.56	   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.56	   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.56	   le(0(),y) -> true()
11.42/3.56	   le(s(x),0()) -> false()
11.42/3.56	   le(s(x),s(y)) -> le(x,y)
11.42/3.56	  TDG Processor:
11.42/3.56	   DPs:
11.42/3.56	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.56	    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.56	    split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.56	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.42/3.56	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.56	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.42/3.59	    le#(s(x),s(y)) -> le#(x,y)
11.42/3.59	   TRS:
11.42/3.59	    split(x,nil()) -> tp2(nil(),nil())
11.42/3.59	    ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.59	    ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	    split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.59	    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.59	    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.59	    le(0(),y) -> true()
11.42/3.59	    le(s(x),0()) -> false()
11.42/3.59	    le(s(x),s(y)) -> le(x,y)
11.42/3.59	   graph:
11.42/3.59	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
11.42/3.59	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
11.42/3.59	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
11.42/3.59	    le#(s(x),s(y)) -> le#(x,y)
11.42/3.59	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
11.42/3.59	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
11.42/3.59	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.59	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
11.42/3.59	    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
11.42/3.59	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.42/3.59	    split#(x,cons(y,ys)) -> split#(x,ys) ->
11.42/3.59	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.42/3.59	    split#(x,cons(y,ys)) -> split#(x,ys) ->
11.42/3.59	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.42/3.59	    split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.59	   SCC Processor:
11.42/3.59	    #sccs: 2
11.42/3.59	    #rules: 2
11.42/3.59	    #arcs: 10/64
11.42/3.59	    DPs:
11.42/3.59	     split#(x,cons(y,ys)) -> split#(x,ys)
11.42/3.59	    TRS:
11.42/3.59	     split(x,nil()) -> tp2(nil(),nil())
11.42/3.59	     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.59	     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.59	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.59	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.59	     le(0(),y) -> true()
11.42/3.59	     le(s(x),0()) -> false()
11.42/3.59	     le(s(x),s(y)) -> le(x,y)
11.42/3.59	    Subterm Criterion Processor:
11.42/3.59	     simple projection:
11.42/3.59	      pi(split#) = 1
11.42/3.59	     problem:
11.42/3.59	      DPs:
11.42/3.59	       
11.42/3.59	      TRS:
11.42/3.59	       split(x,nil()) -> tp2(nil(),nil())
11.42/3.59	       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.59	       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.59	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.59	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.59	       le(0(),y) -> true()
11.42/3.59	       le(s(x),0()) -> false()
11.42/3.59	       le(s(x),s(y)) -> le(x,y)
11.42/3.59	     Qed
11.42/3.59	    
11.42/3.59	    DPs:
11.42/3.59	     le#(s(x),s(y)) -> le#(x,y)
11.42/3.59	    TRS:
11.42/3.59	     split(x,nil()) -> tp2(nil(),nil())
11.42/3.59	     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.59	     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.59	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.59	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.59	     le(0(),y) -> true()
11.42/3.59	     le(s(x),0()) -> false()
11.42/3.59	     le(s(x),s(y)) -> le(x,y)
11.42/3.59	    Subterm Criterion Processor:
11.42/3.59	     simple projection:
11.42/3.59	      pi(le#) = 0
11.42/3.59	     problem:
11.42/3.59	      DPs:
11.42/3.59	       
11.42/3.59	      TRS:
11.42/3.59	       split(x,nil()) -> tp2(nil(),nil())
11.42/3.59	       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.42/3.59	       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.42/3.59	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.42/3.59	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.42/3.59	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.42/3.59	       le(0(),y) -> true()
11.42/3.59	       le(s(x),0()) -> false()
11.42/3.59	       le(s(x),s(y)) -> le(x,y)
11.42/3.59	     Qed
11.42/3.59	This critical pair is unfeasible.
11.42/3.59	
12.75/3.80	EOF