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