4.36/1.94	YES
4.36/1.94	
4.36/1.94	Proof:
4.36/1.94	This system is confluent.
4.36/1.94	By \cite{SMI95}, Corollary 4.7 or 5.3.
4.36/1.94	This system is oriented.
4.36/1.94	This system is of type 3 or smaller.
4.36/1.94	This system is right-stable.
4.36/1.94	This system is properly oriented.
4.36/1.94	This is an overlay system.
4.36/1.94	This system is left-linear.
4.36/1.94	All 2 critical pairs are trivial or infeasible.
4.36/1.94	Overlap: (rule1: g(y, a) -> d <= f(y, b) = b, rule2: g(a, z) -> c <= f(z, a) = a, pos: ε, mgu: {(y,a), (z,a)})
4.36/1.94	CP: c = d <= f(a, b) = b, f(a, a) = a
4.36/1.94	This critical pair is infeasible.
4.36/1.94	This critical pair is conditional.
4.36/1.94	This critical pair has some non-trivial conditions.
4.36/1.94	Call external tool:
4.36/1.94	./waldmeister
4.36/1.94	Input:
4.36/1.94	  f(a, x) -> a
4.36/1.94	  f(b, x) -> b
4.36/1.94	  g(a, x) -> c <= f(x, a) = a
4.36/1.94	  g(x, a) -> d <= f(x, b) = b
4.36/1.94	  c -> c
4.36/1.94	
4.36/1.94	By Waldmeister.
4.36/1.94	Overlap: (rule1: g(a, y) -> c <= f(y, a) = a, rule2: g(z, a) -> d <= f(z, b) = b, pos: ε, mgu: {(z,a), (y,a)})
4.36/1.94	CP: d = c <= f(a, a) = a, f(a, b) = b
4.36/1.94	This critical pair is infeasible.
4.36/1.94	This critical pair is conditional.
4.36/1.94	This critical pair has some non-trivial conditions.
4.36/1.94	'\Sigma(b) \cap (->^*_R^_1)[\Sigma(REN(f(a, b)))]' is empty by ETAC.
4.36/1.94	
4.49/2.14	EOF