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