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