5.21/1.72	YES
5.21/1.72	
5.21/1.72	Problem:
5.21/1.72	pin(a()) -> pout(b())
5.21/1.72	pin(b()) -> pout(c())
5.21/1.72	tc(x) -> x
5.21/1.72	tc(x) -> y <= pin(x) = pout(z()), tc(z()) = y
5.21/1.72	
5.21/1.72	Proof:
5.21/1.72	This system is confluent.
5.21/1.72	By \cite{SMI95}, Corollary 4.7 or 5.3.
5.21/1.72	This system is oriented.
5.21/1.72	This system is of type 3 or smaller.
5.21/1.72	This system is right-stable.
5.21/1.72	This system is properly oriented.
5.21/1.72	This is an overlay system.
5.21/1.72	This system is left-linear.
5.21/1.72	All 2 critical pairs are trivial or infeasible.
5.21/1.72	CP: x = y <= pin(x) = pout(z()), tc(z()) = y:
5.21/1.72	This critical pair is infeasible.
5.21/1.72	This critical pair is conditional.
5.21/1.72	This critical pair has some non-trivial conditions.
5.21/1.72	'[\Sigma(REN(conds(pout(z()), y)))](->^*_R^-1_\alpha) \cap \Sigma(conds(pin(x), tc(z())))' is empty.
5.21/1.72	CP: x = z <= pin(z) = pout(z()), tc(z()) = x:
5.21/1.72	This critical pair is infeasible.
5.21/1.72	This critical pair is conditional.
5.21/1.72	This critical pair has some non-trivial conditions.
5.21/1.72	'[\Sigma(REN(conds(pout(z()), x)))](->^*_R^-1_\alpha) \cap \Sigma(conds(pin(z), tc(z())))' is empty.
5.21/1.72	
5.33/2.12	EOF