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