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