1.46/1.21	NO
1.46/1.22	
1.46/1.22	Proof:
1.46/1.22	This system is not confluent.
1.46/1.22	For the unconditional CP y = up(s(y)) the left- and right-hand sides are not joinable wrt R_u.
1.46/1.22	Call external tool:
1.46/1.22	./csi.sh
1.46/1.22	Input:
1.46/1.22	  up(x) -> x
1.46/1.22	  down(x) -> x
1.46/1.22	  up(x) -> up(s(x))
1.46/1.22	  down(s(x)) -> down(x)
1.46/1.22	  between(x, y, z) -> true
1.46/1.22	
1.46/1.22	 Nonconfluence Processor:
1.46/1.22	  terms: f5() *<- f5() ->* up(s(f5()))
1.46/1.22	  Qed
1.46/1.22	  
1.46/1.22	  first automaton:
1.46/1.22	   final states: {1}
1.46/1.22	   transitions:
1.46/1.22	    f5() -> 1*
1.46/1.22	  
1.46/1.22	  second automaton:
1.46/1.22	   final states: {2}
1.46/1.22	   transitions:
1.46/1.22	    up(4) -> 2*
1.46/1.22	    s(4) -> 4*
1.46/1.22	    s(3) -> 4*
1.46/1.22	    f5() -> 3*
1.46/1.22	    4 -> 2*
1.46/1.22	
3.32/1.52	EOF