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