(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v0 () (Array Index Element))
(declare-fun v1 () (Array Index Element))
(declare-fun v2 () (Array Index Element))
(declare-fun v3 () Index)
(declare-fun v4 () Index)
(declare-fun v5 () Element)
(check-sat-assuming ( (let ((_let_0 (store (store v1 v4 v5) v4 v5))) (let ((_let_1 (select (store v1 v4 v5) v3))) (let ((_let_2 (distinct v1 v2))) (let ((_let_3 (= _let_1 v5))) (let ((_let_4 (= (select v0 v3) (select v0 v3)))) (let ((_let_5 (ite (= v3 v3) (store v1 v4 v5) (store _let_0 v3 (select v0 v3))))) (let ((_let_6 (ite (= (select _let_0 v3) _let_1) _let_5 (ite _let_2 _let_5 (store v1 v4 v5))))) (let ((_let_7 (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) v2 v2))) (let ((_let_8 (ite _let_3 _let_0 (ite _let_2 _let_5 (store v1 v4 v5))))) (let ((_let_9 (ite (= (select _let_0 v3) v5) v0 v1))) (let ((_let_10 (ite (= v3 v3) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) v2))) (let ((_let_11 (ite (distinct v2 (store v1 v4 v5)) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_5))) (let ((_let_12 (ite (= v3 v3) _let_8 (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1)))) (let ((_let_13 (ite _let_4 (ite (distinct v2 (store v1 v4 v5)) (ite _let_2 _let_5 (store v1 v4 v5)) _let_6) v2))) (let ((_let_14 (ite (distinct v4 v3) (ite _let_3 (ite (= v3 v3) v2 v2) v2) (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3)))))) (let ((_let_15 (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_12 (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8))))) (let ((_let_16 (ite (= (store v1 v4 v5) (store v1 v4 v5)) v3 v3))) (let ((_let_17 (ite _let_2 v3 (ite (distinct v4 v3) v3 v3)))) (let ((_let_18 (ite (distinct _let_1 (select v1 v3)) (ite _let_3 v4 v4) (ite (distinct v4 v3) v3 v3)))) (let ((_let_19 (ite _let_4 _let_18 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17))))) (let ((_let_20 (ite (distinct v3 v3) (ite _let_3 v4 v4) (ite (= v3 v3) v3 _let_17)))) (let ((_let_21 (ite (distinct v2 (store v1 v4 v5)) (ite (= v3 v3) v3 _let_17) _let_19))) (let ((_let_22 (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16)))) (let ((_let_23 (ite _let_3 (select _let_0 v3) _let_1))) (let ((_let_24 (ite _let_2 (select v0 v3) v5))) (let ((_let_25 (ite _let_4 (select v0 v3) (select v1 v3)))) (let ((_let_26 (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) v5 (select v0 v3)))) (let ((_let_27 (ite (= (select _let_0 v3) v5) (select v1 v3) (select v0 v3)))) (let ((_let_28 (ite (= v0 v0) (ite (= v3 v3) _let_24 _let_1) v5))) (let ((_let_29 (select (ite (distinct v3 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) _let_8) (ite _let_4 _let_18 v3)))) (let ((_let_30 (select (store _let_0 v3 (select v0 v3)) _let_17))) (let ((_let_31 (select (ite (= (select _let_0 v3) v5) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_14) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17))))) (let ((_let_32 (= _let_5 (ite (distinct v2 (store v1 v4 v5)) (ite (distinct v4 v3) _let_12 _let_11) _let_11)))) (let ((_let_33 (= _let_19 _let_20))) (let ((_let_34 (distinct (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite (distinct v4 v3) v3 v3))))) (let ((_let_35 (distinct (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16) (ite (distinct v4 v3) v3 v3)))) (let ((_let_36 (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) v2) (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite (distinct v4 v3) v3 v3)) (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)))) (let ((_let_37 (and (xor (distinct (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite (distinct v4 v3) v3 v3))) (= _let_14 (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)))) (=> (and (distinct _let_10 (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1))) (distinct (select v0 v3) (select _let_0 v3))) (=> (= (ite (= (select _let_0 v3) v5) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_14) (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3)))) (= _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_24 (select v1 v3)))))))) (let ((_let_38 (and (distinct v2 (store v1 v4 v5)) (distinct (select (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8) v3) _let_1)))) (let ((_let_39 (=> (ite (not (or (= (select _let_0 v3) v5) (distinct _let_1 (ite (= v3 v3) _let_24 _let_1)))) (ite (and (distinct v4 v3) (distinct _let_9 (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)))) (ite (or (distinct _let_1 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (not (distinct v0 _let_15))) (distinct _let_11 (store _let_10 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) _let_25)) (distinct (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8) (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)))) (= (ite (distinct (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1) _let_7) (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) _let_10) (distinct (select v0 v3) v5)) (not _let_33))) (= (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) _let_20)) (=> (ite (ite (= (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8) _let_11) (ite (distinct (ite (= v3 v3) v3 _let_17) (ite (distinct v4 v3) v3 v3)) (= _let_19 (ite _let_4 _let_18 v3)) (distinct (ite (distinct (select v0 v3) (select v0 v3)) _let_24 _let_25) (select (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) _let_19))) (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) (ite (= v3 v3) v2 v2) (ite _let_2 _let_5 (store v1 v4 v5))) _let_13)) (= v3 v3) (not (= (store (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (= v3 v3) v2 v2)))) (xor (ite (distinct _let_30 (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (= (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_24 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3))) (=> (= (=> (distinct _let_23 (ite _let_2 _let_25 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3)))) (= (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3))) _let_11)) (=> (=> (= (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) _let_12) (= v2 _let_0)) (= (ite (= (select _let_0 v3) v5) (ite (distinct _let_1 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3)) _let_25) _let_25) (select v1 v3))))) (= (xor (distinct _let_11 (ite (distinct v4 v3) _let_12 _let_11)) (distinct (store _let_0 v3 (select v0 v3)) v2)) (ite (= (= (ite _let_4 _let_18 v3) (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (distinct (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) (ite (distinct (select v0 v3) (select v0 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_10))) (distinct (store _let_0 v3 (select v0 v3)) _let_12) (distinct (ite (= (select _let_0 v3) v5) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_14) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8))))))))) (let ((_let_40 (xor (xor (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) v2) (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite (distinct v4 v3) v3 v3)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16)) (ite (or (= (= (ite (distinct v3 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) _let_8) (store _let_13 (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (ite (= v3 v3) (select v0 v3) v5))) (= (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) _let_19)) (= _let_19 (ite _let_4 _let_18 v3))) (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) _let_13) (or (and (or (distinct (ite (= (select _let_0 v3) v5) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_14) (store _let_0 v3 (select v0 v3))) (distinct (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (distinct v4 v3) (ite (= v3 v3) _let_24 _let_1) (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))))) (distinct (ite (= (store v1 v4 v5) (store v1 v4 v5)) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17))) v4)) (or (= (store (store v2 (ite (distinct v4 v3) v3 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (ite (= (select _let_0 v3) _let_1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (select _let_0 v3) v5) v4 _let_18)) (ite (= v3 v3) _let_24 _let_1)) _let_14) (ite (= (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (select (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) _let_19)) (= (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) _let_1) (= (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (distinct v4 v3) v3 v3))))))) (distinct (ite _let_2 _let_25 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))))))) (let ((_let_41 (or (= (=> (=> (= (select v0 v3) (ite (distinct _let_1 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3)) _let_25)) (not (distinct (select _let_0 v3) (ite (distinct v4 v3) (ite (= v3 v3) _let_24 _let_1) (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))))))) (and (and (distinct (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3))) _let_6) (= v5 _let_1)) (= _let_17 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)))) (not (or (not (distinct (ite _let_4 _let_6 v1) v1)) (not (distinct (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16)))))) (= (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16)) (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16)))))) (xor (= (not (not (not (not (xor (and (ite (or (= _let_14 (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1)) (distinct (store _let_10 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) _let_25) (ite (distinct v3 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) _let_8))) (= _let_25 _let_29) (= (store (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))))) (distinct _let_8 (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)))) (distinct (ite _let_4 _let_18 v3) _let_16)))))) (not (not (and (or (=> (distinct _let_28 (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))) (distinct (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3))) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8))) (not (or (not (=> (= (ite (= (select _let_0 v3) v5) (ite (distinct _let_1 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3)) _let_25) _let_25) _let_24) (and (= (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= (select _let_0 v3) _let_1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (select _let_0 v3) v5) v4 _let_18))) (distinct (ite (distinct v2 (store v1 v4 v5)) (ite (distinct v4 v3) _let_12 _let_11) _let_11) (ite (= v3 v3) v2 v2))))) (xor (= _let_35 (distinct (select v0 v3) (select v0 v3))) (ite (= (ite (= (select _let_0 v3) v5) v4 _let_18) _let_20) (distinct (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (distinct (select v0 v3) _let_26)))))) (and (and (not (=> (= _let_18 (ite _let_3 v4 v4)) (= _let_14 (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1))))) (distinct v0 (store _let_0 v3 (select v0 v3)))) (and (=> (= (xor (distinct _let_8 (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) (distinct (ite (= (store v1 v4 v5) (store v1 v4 v5)) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17))) _let_19)) (= (store _let_0 v3 (select v0 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)))) (= (ite _let_2 _let_25 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) _let_29)) (and (or (and (= (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) (store _let_13 (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (ite (= v3 v3) (select v0 v3) v5))) (= (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) v0)) (distinct _let_25 (select v0 v3))) (ite (=> (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8))) (and (= _let_25 _let_30) (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) (ite (= v3 v3) v2 v2) (ite _let_2 _let_5 (store v1 v4 v5))) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1))))) (distinct (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3)))) (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) (store v2 (ite (distinct v4 v3) v3 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))))))))))) (or (not (and (=> (or (distinct v4 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)))) (= (distinct v1 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (or (= (ite (= v2 _let_0) _let_5 (store _let_0 v3 (select v0 v3))) (ite (distinct (select v0 v3) (select v0 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_10)) (distinct (select (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) _let_19) _let_1)))) (or (xor _let_37 _let_37) (xor (or (xor (or (or (distinct _let_27 (select v0 v3)) (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) _let_13)) (= (distinct (select (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) _let_19) (select (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8) v3)) (= (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) (ite _let_3 v4 v4)))) (and (not (xor (or _let_32 _let_32) _let_2)) (or (= (= (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) _let_17) (= (ite (distinct v4 v3) v3 v3) _let_17)) (distinct _let_18 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17))))))) (= (ite (not (= (ite (distinct (select v0 v3) (select v0 v3)) v4 (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4)) _let_21)) (or (ite (not (ite (distinct _let_5 (store _let_10 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) _let_25)) (distinct (select v1 v3) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3)))) (or (distinct _let_1 _let_28) (xor (= (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3))) _let_10) (distinct (ite _let_2 (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)) v4) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))))))) (not (ite (ite (and (= _let_23 (ite (= v3 v3) (select v0 v3) v5)) (distinct (ite (= (select _let_0 v3) _let_1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (select _let_0 v3) v5) v4 _let_18)) _let_18)) (distinct v2 (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1))) (distinct (ite (= (select _let_0 v3) v5) v4 _let_18) (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))))) (= (ite (= (select _let_0 v3) v5) (ite (distinct _let_1 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3)) _let_25) _let_25) (ite _let_2 _let_25 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (or (= (store _let_0 v3 (select v0 v3)) _let_13) (distinct _let_31 _let_28)))) (= (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) _let_18)) _let_3) (ite (= (and (= _let_22 (ite (= (select _let_0 v3) _let_1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (select _let_0 v3) v5) v4 _let_18))) (= _let_9 (store (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))))) (= (distinct (select v1 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (distinct (ite _let_4 (store v1 v4 v5) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)) (ite (distinct (select v0 v3) (select v0 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_10)))) (ite (xor (xor (distinct v4 _let_22) (= (ite _let_3 (ite (= v3 v3) v2 v2) v2) (store v1 v4 v5))) (= (select _let_0 v3) _let_1)) (=> (= (= (=> (distinct (select v0 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (distinct v3 v3)) (= _let_29 (ite (= v3 v3) _let_24 _let_1))) (= (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_24 (select v1 v3)) v5)) (xor (or (= (store (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (store _let_0 v3 (select v0 v3))) (or (= (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) (ite (distinct (select v0 v3) (select v0 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_10)) (= (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3)))) (= (ite (= (store v1 v4 v5) (store v1 v4 v5)) _let_9 v1) (ite (= (select _let_0 v3) v5) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) _let_8)))) (=> (and (= (ite (distinct v4 v3) (ite (= v3 v3) _let_24 _let_1) (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))) (ite (= v3 v3) _let_24 _let_1)) (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite _let_4 _let_18 v3))) (= (store _let_0 v3 (select v0 v3)) (ite (distinct v2 (store v1 v4 v5)) (ite _let_2 _let_5 (store v1 v4 v5)) _let_6)))) (= (select _let_0 v3) v5))) (and (=> _let_39 _let_39) (ite (xor (or (not (xor (and (= v0 v0) (= (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_0 (store _let_0 v3 (select v0 v3))) (store _let_13 (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (ite (= v3 v3) (select v0 v3) v5)))) (distinct (ite (= v3 v3) _let_24 _let_1) _let_30))) (=> (xor (or (distinct (ite (= v3 v3) (select v0 v3) v5) (select _let_0 v3)) (distinct _let_10 _let_5)) (= (distinct (ite _let_4 _let_18 v3) (ite (= (store v1 v4 v5) (store v1 v4 v5)) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) (ite (= v3 v3) v3 _let_17)))) (and (distinct _let_1 (select v1 v3)) _let_4))) (ite (=> (xor _let_34 _let_34) (distinct (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (distinct v4 v3) v3 v3))) _let_38 _let_38))) (not (= (distinct (ite (= v3 v3) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16)) _let_16) (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (= _let_23 (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))))) (xor _let_33 (= _let_20 v3)) (or (xor (= (store v2 (ite (distinct v4 v3) v3 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (store v1 v4 v5)) (distinct _let_1 _let_25)) (ite (distinct v4 _let_18) (xor (distinct (ite (= v3 v3) v2 v2) _let_15) (distinct _let_30 _let_23)) (not (= _let_26 (ite (distinct v4 v3) (ite (= v3 v3) _let_24 _let_1) (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))))))))))) (or (ite (xor (= v0 _let_6) (not (distinct (ite _let_2 _let_5 (store v1 v4 v5)) (store v1 v4 v5)))) (ite (ite (= (or (= (store v1 v4 v5) (store v1 v4 v5)) (= (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) (select v0 v3) (ite (= v3 v3) (select v0 v3) v5)) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))))) _let_35) (or (= (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) (= (ite _let_4 _let_6 v1) (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1))) _let_34) (distinct (store (store v2 (ite (distinct v4 v3) v3 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (ite (= (select _let_0 v3) _let_1) (ite (distinct (store _let_0 v3 (select v0 v3)) (store _let_0 v3 (select v0 v3))) _let_16 v3) (ite (= (select _let_0 v3) v5) v4 _let_18)) (ite (= v3 v3) _let_24 _let_1)) _let_6)) _let_4 (=> (= _let_27 (ite _let_2 _let_25 (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (distinct (ite _let_2 _let_5 (store v1 v4 v5)) (store _let_13 (ite (= v0 v0) v3 (ite (= v2 _let_0) v4 (ite (= (select _let_0 v3) v5) (ite (distinct v4 v3) v3 v3) _let_16))) (ite (= v3 v3) (select v0 v3) v5))))) (not (ite (distinct (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1) (ite (distinct _let_1 (select v1 v3)) (ite _let_2 v2 (ite (distinct _let_1 (select v1 v3)) (ite (= v3 v3) v2 v2) v1)) (store _let_0 v3 (select v0 v3)))) (= (ite (= (select _let_0 v3) v5) (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_14) (store v2 (ite (distinct v4 v3) v3 v3) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))))) (or (= v3 v3) (=> _let_36 _let_36))))) (not (or (xor (= _let_7 _let_6) (=> (= (not (distinct (ite (distinct v4 v3) v3 v3) _let_21)) (= _let_27 _let_31)) (distinct _let_25 v5))) (not (=> (not (ite (= v0 (store _let_0 v3 (select v0 v3))) (distinct (ite (= v0 v0) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3))) (ite (= (select _let_0 v3) _let_1) (ite (distinct v3 v3) _let_24 (ite (= (store v1 v4 v5) (store v1 v4 v5)) (select v0 v3) (select v1 v3))) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)))) (ite (distinct _let_1 (select v1 v3)) (ite (distinct (store _let_0 v3 (select v0 v3)) v2) _let_25 (select v0 v3)) _let_25)) (= (ite (= v2 _let_0) (ite (distinct v2 (store v1 v4 v5)) _let_24 (select v0 v3)) (ite (= v3 v3) (select v0 v3) v5)) _let_24))) (not (distinct (ite (= v0 v0) _let_9 (ite _let_4 _let_6 v1)) _let_0)))))))))) (or _let_40 _let_40))) (= _let_41 _let_41))))))))))))))))))))))))))))))))))))))))))))) ))