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