5.02/2.16	MAYBE
5.02/2.16	
5.02/2.16	Proof:
5.02/2.16	ConCon could not decide confluence of the system.
5.02/2.16	\cite{GNG13}, Theorem 9 does not apply.
5.02/2.16	This system is of type 3 or smaller.
5.02/2.16	This system is deterministic.
5.02/2.16	This system is weakly left-linear.
5.02/2.16	This system is non-confluent.
5.02/2.16	Call external tool:
5.02/2.16	./csi.sh
5.02/2.16	Input:
5.02/2.16	(VAR )
5.02/2.16	(RULES
5.02/2.16	  a -> b
5.02/2.16	  a -> c
5.02/2.16	  b -> ?1(b)
5.02/2.16	  ?1(c) -> c
5.02/2.16	)
5.02/2.16	
5.02/2.16	 Nonconfluence Processor:
5.02/2.17	  terms: b() *<- a() ->* c()
5.02/2.17	  Qed
5.02/2.17	  
5.02/2.17	  first automaton:
5.02/2.17	   final states: {2}
5.02/2.17	   transitions:
5.02/2.17	    b() -> 2*
5.02/2.17	    ?1(2) -> 2*
5.02/2.17	  
5.02/2.17	  second automaton:
5.02/2.17	   final states: {1}
5.02/2.17	   transitions:
5.02/2.17	    c() -> 1*
5.02/2.17	
5.02/2.19	EOF