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