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