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