2.28/1.35	MAYBE
2.28/1.35	
2.28/1.35	Proof:
2.28/1.35	ConCon could not decide confluence of the system.
2.28/1.35	\cite{GNG13}, Theorem 9 does not apply.
2.28/1.35	This system is of type 3 or smaller.
2.28/1.35	This system is deterministic.
2.28/1.35	This system is weakly left-linear.
2.28/1.35	This system is non-confluent.
2.28/1.35	Call external tool:
2.28/1.35	./csi.sh
2.28/1.35	Input:
2.28/1.35	  a -> c
2.28/1.35	  g(a) -> h(b)
2.28/1.35	  h(b) -> g(c)
2.28/1.35	  f(x) -> ?1(g(x), x)
2.28/1.35	  ?1(h(z), x) -> z
2.28/1.35	
2.28/1.35	 Nonconfluence Processor:
2.28/1.35	  terms: ?1(g(c()),f7()) *<- ?1(h(b()),f7()) ->* b()
2.28/1.35	  Qed
2.28/1.35	  
2.28/1.35	  first automaton:
2.28/1.35	   final states: {1}
2.28/1.35	   transitions:
2.28/1.35	    c() -> 3*
2.28/1.35	    g(3) -> 4*
2.28/1.35	    ?1(4,2) -> 1*
2.28/1.35	    f7() -> 2*
2.28/1.35	  
2.28/1.35	  second automaton:
2.28/1.35	   final states: {5}
2.28/1.35	   transitions:
2.28/1.35	    b() -> 5*
2.28/1.35	
2.28/1.38	EOF