(set-option :smt.MBQI false)
(set-option :auto_config false)
(set-option :smt.QI.EAGER_THRESHOLD 100)

(declare-sort T)
(declare-sort U)

(declare-const x1 U)
(declare-const x2 U)
(declare-const x3 U)

(declare-const a T)
(declare-const b T)
(declare-const c T)
(declare-const d T)
(declare-const e T)

(declare-fun sel (U T T) Bool)
(declare-fun store (U T T T) U)

(assert (= x1 (store x2 a b c)))
(assert (= x2 (store x3 a b d)))

(check-sat)

(assert (forall ((q1 U) (q2 T) (q3 T) (q4 T) (q5 T) (q6 T))
    (! (or (= q3 q6) (= (sel (store q1 q2 q3 q4) q5 q6) (sel q1 q5 q6)))
        :pattern ((sel (store q1 q2 q3 q4) q5 q6))
        :qid main
    )))

(assert (sel (store x1 a b c) d e))

(check-sat)