2.75/1.18	YES
2.75/1.18	
2.75/1.18	Proof:
2.75/1.18	This system is confluent.
2.75/1.18	By \cite{SMI95}, Corollary 4.7 or 5.3.
2.75/1.18	This system is oriented.
2.75/1.18	This system is of type 3 or smaller.
2.75/1.18	This system is right-stable.
2.75/1.18	This system is properly oriented.
2.75/1.18	This is an overlay system.
2.75/1.18	This system is left-linear.
2.75/1.18	All 2 critical pairs are trivial or infeasible.
2.75/1.18	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)})
2.75/1.18	CP: c = d <= f(a, b) = b, f(a, a) = a
2.75/1.18	This critical pair is infeasible.
2.75/1.18	This critical pair is conditional.
2.75/1.18	This critical pair has some non-trivial conditions.
2.75/1.18	Call external tool:
2.75/1.18	./waldmeister
2.75/1.18	Input:
2.75/1.18	  f(a, x) -> a
2.75/1.18	  f(b, x) -> b
2.75/1.18	  g(a, x) -> c <= f(x, a) = a
2.75/1.18	  g(x, a) -> d <= f(x, b) = b
2.75/1.18	  c -> c
2.75/1.18	
2.75/1.18	By Waldmeister.
2.75/1.18	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)})
2.75/1.18	CP: d = c <= f(a, a) = a, f(a, b) = b
2.75/1.18	This critical pair is infeasible.
2.75/1.18	This critical pair is conditional.
2.75/1.18	This critical pair has some non-trivial conditions.
2.75/1.18	Call external tool:
2.75/1.18	./waldmeister
2.75/1.19	Input:
2.75/1.19	  f(a, x) -> a
2.75/1.19	  f(b, x) -> b
2.75/1.19	  g(a, x) -> c <= f(x, a) = a
2.75/1.19	  g(x, a) -> d <= f(x, b) = b
2.75/1.19	  c -> c
2.75/1.19	
2.75/1.19	By Waldmeister.
2.75/1.19	
2.92/1.43	EOF