T2-312
(=> (not (= ?X ?Y)) (not (= ?Y ?X)))
Proof Trace