3.23/1.96	MAYBE
3.23/1.96	
3.23/1.96	Proof:
3.23/1.96	ConCon could not decide confluence of the system.
3.23/1.96	\cite{GNG13}, Theorem 9 does not apply.
3.23/1.96	This system is of type 3 or smaller.
3.23/1.96	This system is deterministic.
3.23/1.96	This system is weakly left-linear.
3.23/1.96	This system is non-confluent.
3.23/1.96	Call external tool:
3.23/1.96	./csi.sh
3.23/1.96	Input:
3.23/1.96	(VAR x z)
3.23/1.96	(RULES
3.23/1.96	  a -> c
3.23/1.96	  g(a) -> h(b)
3.23/1.96	  h(b) -> g(c)
3.23/1.96	  f(x) -> ?1(g(x), x)
3.23/1.96	  ?1(h(z), x) -> z
3.23/1.96	)
3.23/1.96	
3.23/1.96	 Nonconfluence Processor:
3.23/1.96	  terms: ?1(g(c()),x) *<- ?1(h(b()),x) ->* b()
3.23/1.96	  Qed
3.23/1.96	
3.26/1.99	EOF