9.21/2.92	YES
9.21/2.92	
9.21/2.92	Proof:
9.21/2.92	This system is confluent.
9.21/2.92	By \cite{SMI95}, Corollary 4.7 or 5.3.
9.21/2.92	This system is oriented.
9.21/2.92	This system is of type 3 or smaller.
9.21/2.92	This system is right-stable.
9.21/2.92	This system is properly oriented.
9.21/2.92	This is an overlay system.
9.21/2.92	This system is left-linear.
9.21/2.92	All 2 critical pairs are trivial or infeasible.
9.21/2.92	Overlap: (rule1: f(c(c(c(z))), x') -> a(x') <= c(f(c(z), c(c(x')))) = c(a(a(b))), rule2: f(c(y'), c(c(z'))) -> a(a(y')) <= c(f(y', z')) = c(a(b)), pos: ε, mgu: {(y',c(c(z))), (x',c(c(z')))})
9.21/2.92	CP: a(a(c(c(z)))) = a(c(c(z'))) <= c(f(c(z), c(c(c(c(z')))))) = c(a(a(b))), c(f(c(c(z)), z')) = c(a(b))
9.21/2.93	This critical pair is infeasible.
9.21/2.93	This critical pair is conditional.
9.21/2.93	This critical pair has some non-trivial conditions.
9.21/2.93	Call external tool:
9.21/2.93	./waldmeister
9.21/2.93	Input:
9.21/2.93	  f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b))
9.21/2.93	  f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b)))
9.21/2.93	  h(b) -> b
9.21/2.93	  h(a(a(x))) -> a(b) <= h(x) = b
9.21/2.93	
9.21/2.93	By Waldmeister.
9.21/2.93	Overlap: (rule1: f(c(z), c(c(x'))) -> a(a(z)) <= c(f(z, x')) = c(a(b)), rule2: f(c(c(c(y'))), z') -> a(z') <= c(f(c(y'), c(c(z')))) = c(a(a(b))), pos: ε, mgu: {(z,c(c(y'))), (z',c(c(x')))})
9.21/2.93	CP: a(c(c(x'))) = a(a(c(c(y')))) <= c(f(c(c(y')), x')) = c(a(b)), c(f(c(y'), c(c(c(c(x')))))) = c(a(a(b)))
9.21/2.93	This critical pair is infeasible.
9.21/2.93	This critical pair is conditional.
9.21/2.93	This critical pair has some non-trivial conditions.
9.21/2.93	Call external tool:
9.21/2.93	./waldmeister
9.21/2.93	Input:
9.21/2.93	  f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b))
9.21/2.93	  f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b)))
9.21/2.93	  h(b) -> b
9.21/2.93	  h(a(a(x))) -> a(b) <= h(x) = b
9.21/2.93	
9.21/2.93	By Waldmeister.
9.21/2.93	
9.82/3.02	EOF