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