23.11/6.47	YES
23.11/6.47	
23.11/6.47	Proof:
24.18/6.71	This system is confluent.
24.18/6.71	By \cite{GNG13}, Theorem 9.
24.18/6.79	This system is of type 3 or smaller.
24.18/6.79	This system is deterministic.
24.18/6.79	This system is weakly left-linear.
24.18/6.79	System R transformed to optimized U(R).
24.18/6.79	This system is confluent.
24.18/6.79	Call external tool:
24.18/6.79	./csi.sh
24.18/6.79	Input:
24.18/6.79	  qsort(cons(x, xs)) -> ?3(split(x, xs), x, xs)
24.18/6.79	  ?3(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs)))
24.18/6.79	  app(cons(x, xs), ys) -> cons(x, app(xs, ys))
24.18/6.79	  le(0, x) -> true
24.18/6.79	  split(x, nil) -> pair(nil, nil)
24.18/6.79	  qsort(nil) -> nil
24.18/6.79	  le(s(x), s(y)) -> le(x, y)
24.18/6.79	  le(s(x), 0) -> false
24.18/6.79	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
24.18/6.79	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
24.18/6.79	  ?2(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs))
24.18/6.79	  app(nil, x) -> x
24.18/6.79	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
24.18/6.79	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
24.18/6.79	  ?2(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs)
24.18/6.79	
24.18/6.79	 Church Rosser Transformation Processor (no redundant rules):
24.18/6.79	  strict:
24.18/6.79	   ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
24.18/6.79	   app(nil(),x) -> x
24.18/6.79	   ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
24.18/6.79	   ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
24.18/6.79	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
24.18/6.79	   le(s(x),0()) -> false()
24.18/6.79	   le(s(x),s(y)) -> le(x,y)
24.18/6.79	   qsort(nil()) -> nil()
24.18/6.79	   split(x,nil()) -> pair(nil(),nil())
24.18/6.79	   le(0(),x) -> true()
24.18/6.79	   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
24.18/6.79	   ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
24.18/6.79	   qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
24.18/6.79	  weak:
24.18/6.79	   
24.18/6.79	  critical peaks: 0
24.18/6.79	  Closedness Processor (*feeble*):
24.18/6.79	   
24.18/6.79	   Qed
24.18/6.79	
26.86/7.46	EOF