3.20/1.68	NO
3.20/1.68	
3.20/1.68	Proof:
3.20/1.68	This system is not confluent.
3.20/1.68	For the unconditional CP z = up(s(z)) the left- and right-hand sides are not joinable wrt R_u.
3.20/1.68	This critical pair is non-joinable.
3.20/1.68	Call external tool:
3.20/1.68	./csi.sh
3.20/1.68	Input:
3.20/1.68	(VAR x y z)
3.20/1.68	(RULES
3.20/1.68	  up(x) -> x
3.20/1.68	  down(x) -> x
3.20/1.68	  up(x) -> up(s(x))
3.20/1.68	  down(s(x)) -> down(x)
3.20/1.68	  between(x, y, z) -> true
3.20/1.68	
3.20/1.68	  ?1 ->= up(s(?1))
3.20/1.68	)
3.20/1.68	
3.20/1.68	 Nonconfluence Processor:
3.20/1.68	  terms: ?1() *<- ?1() ->* up(s(?1()))
3.20/1.68	  Qed
3.20/1.68	  
3.20/1.68	  first automaton:
3.20/1.68	   final states: {1}
3.20/1.68	   transitions:
3.20/1.68	    ?1() -> 1*
3.20/1.68	  
3.20/1.68	  second automaton:
3.20/1.68	   final states: {2}
3.20/1.68	   transitions:
3.20/1.68	    up(4) -> 2*
3.20/1.68	    s(4) -> 4*
3.20/1.68	    s(3) -> 4*
3.20/1.68	    ?1() -> 3*
3.20/1.68	    4 -> 2*
3.20/1.68	
3.88/2.02	EOF