0.00/0.57	YES
0.00/0.57	
0.00/0.57	Problem:
0.00/0.57	App(App(App(S(), a), b), c) -> App(App(a, c), App(b, c)) <= a = I(), b = I(), c = I()
0.00/0.57	App(App(K(), a), b) -> a <= a = I(), b = I()
0.00/0.57	App(I(), a) -> a <= a = I()
0.00/0.57	
0.00/0.57	Proof:
0.00/0.57	This system is confluent.
0.00/0.58	By \cite{SMI95}, Corollary 4.7 or 5.3.
0.00/0.58	This system is oriented.
0.00/0.58	This system is of type 3 or smaller.
0.00/0.58	This system is right-stable.
0.00/0.58	This system is properly oriented.
0.00/0.58	This is an overlay system.
0.00/0.58	This system is left-linear.
0.00/0.58	All 0 critical pairs are trivial or infeasible.
0.00/0.58	
0.00/0.58	EOF