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