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