117.04/30.79	MAYBE
117.04/30.79	
117.04/30.79	Proof:
117.04/30.79	ConCon could not decide confluence of the system.
117.04/30.79	\cite{ALS94}, Theorem 4.1 does not apply.
117.04/30.79	This system is of type 3 or smaller.
117.04/30.79	This system is strongly deterministic.
117.04/30.79	This system is of type 3 or smaller.
117.04/30.79	This system is deterministic.
117.04/30.79	ConCon could not decide if this system is quasi-decreasing.
117.04/30.79	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
117.04/30.79	This system is of type 3 or smaller.
117.04/30.79	This system is deterministic.
117.04/30.79	System R transformed to U(R).
117.04/30.79	The external tool could not decide termination of the system.
117.04/30.79	Call external tool:
117.04/30.79	./ttt2.sh
117.04/30.79	Input:
117.04/30.79	(VAR a b c)
117.04/30.79	(RULES
117.04/30.79	  ?3(I, a, b, c) -> App(App(a, c), App(b, c))
117.04/30.79	  ?2(I, a, b, c) -> ?3(c, a, b, c)
117.04/30.79	  ?1(I, a, b, c) -> ?2(b, a, b, c)
117.04/30.79	  App(App(App(S, a), b), c) -> ?1(a, a, b, c)
117.04/30.79	  ?5(I, a, b) -> a
117.04/30.79	  ?4(I, a, b) -> ?5(b, a, b)
117.04/30.79	  App(App(K, a), b) -> ?4(a, a, b)
117.04/30.79	  ?6(I, a) -> a
117.04/30.79	  App(I, a) -> ?6(a, a)
117.04/30.79	)
117.04/30.79	
117.04/30.79	
117.04/30.80	EOF