5.27/2.33	MAYBE
5.27/2.34	
5.27/2.34	Proof:
5.27/2.34	ConCon could not decide confluence of the system.
5.27/2.34	\cite{GNG13}, Theorem 9 does not apply.
5.27/2.34	This system is of type 3 or smaller.
5.27/2.34	This system is deterministic.
5.27/2.34	This system is weakly left-linear.
5.27/2.34	This system is non-confluent.
5.27/2.34	Call external tool:
5.27/2.34	./csi.sh
5.27/2.34	Input:
5.27/2.34	(VAR x y)
5.27/2.34	(RULES
5.27/2.34	  pin(x) -> pout(g(x))
5.27/2.34	  pin(x) -> ?1(pin(x), x)
5.27/2.34	  ?1(pout(g(y)), x) -> pout(f(y))
5.27/2.34	)
5.27/2.34	
5.27/2.34	 Nonconfluence Processor:
5.27/2.34	  terms: pout(g(x)) *<- pin(x) ->* pout(f(x))
5.27/2.34	  Qed
5.27/2.34	
5.46/2.38	EOF