; EXPECT: unsat (set-option :incremental false) (set-logic ALL) (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun a () Int) (declare-fun z () (Tuple Int Int)) (assert (= z (mkTuple 1 2))) (declare-fun zt () (Tuple Int Int)) (assert (= zt (mkTuple 2 1))) (assert (member z x)) (assert (not (member zt (transpose x)))) (assert (= y (transpose x))) (check-sat)