2.70/2.03	MAYBE
2.70/2.03	
2.70/2.03	Proof:
2.70/2.03	ConCon could not decide confluence of the system.
2.70/2.03	\cite{GNG13}, Theorem 9 does not apply.
2.70/2.03	This system is of type 3 or smaller.
2.70/2.03	This system is deterministic.
2.70/2.03	This system is weakly left-linear.
2.70/2.03	This system is non-confluent.
2.70/2.03	Call external tool:
2.70/2.03	./csi.sh
2.70/2.03	Input:
2.70/2.03	(VAR x)
2.70/2.03	(RULES
2.70/2.03	  even(0) -> true
2.70/2.03	  odd(s(x)) -> ?1(eq(even(x), true), x)
2.70/2.03	  ?1(eq(T, T), x) -> true
2.70/2.03	  even(s(x)) -> ?3(eq(odd(x), true), x)
2.70/2.03	  ?3(eq(T, T), x) -> true
2.70/2.03	  odd(0) -> false
2.70/2.03	  eq(x, x) -> eq(T, T)
2.70/2.03	  even(s(x)) -> ?4(eq(odd(x), false), x)
2.70/2.03	  ?4(eq(T, T), x) -> false
2.70/2.03	  odd(s(x)) -> ?2(eq(even(x), false), x)
2.70/2.03	  ?2(eq(T, T), x) -> false
2.70/2.03	)
2.70/2.03	
2.70/2.03	 Nonconfluence Processor:
2.70/2.03	  terms: ?1(eq(even(x),true()),x) *<- odd(s(x)) ->* ?2(eq(even(x),false()),x)
2.70/2.03	  Qed
2.70/2.03	
2.70/2.06	EOF