(set-option :incremental false)
(set-info :status sat)
(set-info :status unknown)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v4 () Index)
(declare-fun v2 () Index)
(declare-fun v3 () Index)
(declare-fun v1 () (Array Index Element))
(declare-fun v6 () Element)
(declare-fun v0 () (Array Index Element))
(declare-fun v5 () Element)
(check-sat-assuming ( (let ((_let_0 (distinct (store v1 v3 v6) v0))) (let ((_let_1 (store v1 v4 v6))) (let ((_let_2 (select _let_1 v2))) (let ((_let_3 (select v1 v3))) (or (and (= v6 (ite _let_0 (ite (= v4 v2) (ite true _let_2 v6) _let_3) (ite (distinct _let_3 _let_3) v6 _let_2))) (distinct _let_1 (ite (distinct _let_3 v5) v1 (ite _let_0 v1 v0)))) (distinct (ite (distinct v0 _let_1) v2 v4) (ite (= v3 v2) v3 (ite (= v0 v0) (ite (= v6 _let_3) v3 (ite false v4 (ite (= _let_2 _let_3) v3 v2))) v4)))))))) ))