(set-logic QF_UF) (declare-sort U 0) (declare-fun f (U) U) (declare-fun x1 () U) (declare-fun x2 () U) (declare-fun y1 () U) (declare-fun y2 () U) (declare-fun v1 () U) (declare-fun v2 () U) (declare-fun z1 () U) (declare-fun z2 () U) (declare-fun t1 () U) (declare-fun t2 () U) (declare-fun w1 () U) (declare-fun w2 () U) (declare-fun s1 () U) (declare-fun s2 () U) (declare-fun u1 () U) (declare-fun u2 () U) (assert (and (= v1 (f y1)) (= (f y2) v2) (= y1 t1) (= t2 y2) (= s1 (f w1)) (= (f w2) s2) (= w1 u1) (= u2 w2) ) ) (assert (and (= u1 u2) (= x1 v1) (= v2 x2) (= t1 (f z1)) (= (f z2) t2) (= z1 s1) (= s2 z2) (not (= x1 x2)) ) ) (check-sat)