T307
(=> (and (= y x) (= z y)) (= x z))
Proof Trace