blob: 5db18e6a20c32deb5495562ca558d36d4f83cc8c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(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 () Index)
(declare-fun v3 () Index)
(declare-fun v4 () Element)
(declare-fun v5 () Element)
(declare-fun v6 () Element)
(declare-fun v7 () Element)
(declare-fun v8 () Element)
(check-sat-assuming ( (let ((_let_0 (select v0 v3))) (let ((_let_1 (distinct _let_0 v5))) (let ((_let_2 (= v4 v8))) (let ((_let_3 (distinct v7 v5))) (let ((_let_4 (ite (distinct v2 v2) v1 v0))) (let ((_let_5 (ite _let_2 v0 v1))) (let ((_let_6 (ite _let_1 v1 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))))) (let ((_let_7 (ite (= _let_0 v5) _let_5 _let_6))) (let ((_let_8 (ite (= _let_0 _let_0) (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)))) (let ((_let_9 (ite _let_2 v3 v3))) (let ((_let_10 (ite (= v0 v1) (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3)))) (let ((_let_11 (ite (distinct v2 v2) (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3)) v2))) (let ((_let_12 (ite (= _let_0 v5) (ite (= v3 v2) v2 v3) _let_10))) (let ((_let_13 (ite (= _let_0 v6) (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3)) (ite (= v3 v2) v2 v3)))) (let ((_let_14 (ite _let_3 _let_13 v3))) (let ((_let_15 (ite _let_3 _let_13 v2))) (let ((_let_16 (ite (= _let_0 _let_0) _let_15 v2))) (let ((_let_17 (ite (= v8 v6) _let_15 v2))) (let ((_let_18 (ite (distinct v2 v2) v6 (ite (= v0 v1) v8 v5)))) (let ((_let_19 (ite (= v3 v2) (ite (= _let_0 _let_0) _let_0 _let_18) (ite (= _let_0 v5) v5 v6)))) (let ((_let_20 (ite _let_3 _let_0 (ite (= _let_0 _let_0) _let_0 _let_18)))) (let ((_let_21 (ite _let_2 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) _let_19))) (let ((_let_22 (ite _let_2 (ite (= v0 v1) v8 v5) _let_19))) (let ((_let_23 (distinct v2 v3))) (let ((_let_24 (not (distinct _let_10 _let_9)))) (let ((_let_25 (=> (=> (not (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (or (distinct v1 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (distinct v1 _let_4))) (not (=> _let_3 (distinct (ite (= _let_0 _let_0) v4 v4) (ite (= _let_0 v5) v5 v6))))))) (let ((_let_26 (ite (=> (ite (xor (or _let_2 (distinct v1 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (xor (= _let_11 _let_13) (= v3 _let_10))) (= _let_7 (ite (= _let_0 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (distinct v8 (ite (= v0 v1) v8 v5))) (= _let_20 _let_18)) (xor (=> (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= _let_0 _let_0) _let_0 _let_18) v5)) (=> (= _let_8 (ite _let_3 v0 v0)) (=> (= (or (distinct _let_16 (ite (= v3 v2) v2 v3)) (distinct _let_22 (ite (= v0 v1) v8 v5))) (ite (distinct _let_22 _let_18) (distinct _let_11 _let_16) (distinct (ite (= v3 v2) v2 v3) _let_17))) (distinct _let_16 _let_17)))) (xor (= (= v1 _let_6) (or (distinct _let_8 _let_7) (= _let_0 v6))) _let_2)))) (let ((_let_27 (= (xor (=> (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18))))) (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18)))))) (=> (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18))))) (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18))))))) (xor (=> (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18))))) (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18)))))) (=> (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18))))) (or (=> (xor (not (ite (distinct v7 v4) (distinct _let_8 _let_5) (distinct _let_11 v3))) (xor (distinct _let_13 _let_17) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 v0 v0)))) (ite (not (and (distinct v1 v0) (= v4 v6))) (not (and (= _let_11 _let_13) (or (= (ite (= _let_0 _let_0) _let_0 _let_18) _let_19) (distinct (ite (= _let_0 v5) v5 v6) (ite (= _let_0 v6) (ite (= _let_0 v5) v5 v6) _let_0))))) (=> (not (= (distinct _let_8 _let_7) (= (ite (distinct v2 v2) v6 v7) _let_18))) (= (and (= (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_22 (ite (= _let_0 v5) v5 v6))) (distinct v4 v5))))) (ite (or (distinct _let_15 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))) (or (or (= (ite (= v8 v6) _let_18 (ite (distinct v2 v2) v6 v7)) _let_22) (distinct v8 v6)) (= (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) v1))) (or (xor (distinct v8 _let_21) (not (and (=> (ite (xor (= (distinct _let_21 (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4))) (= _let_6 _let_5)) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) (ite _let_3 v0 v0))) (= (xor (= _let_9 _let_16) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_6)) (distinct _let_12 _let_10)) (= _let_0 _let_0)) (=> (=> _let_1 _let_1) (= (ite (= v0 v1) v8 v5) (ite (= _let_0 _let_0) v4 v4)))) (ite (=> (not (distinct _let_10 _let_13)) (distinct _let_16 _let_11)) (ite (or (= (= (distinct _let_10 _let_16) (= _let_15 _let_14)) (= v0 v1)) (= v1 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4))) (or (not (= v3 v2)) (and (distinct _let_17 (ite _let_2 _let_12 _let_9)) (= (select _let_4 _let_12) (select _let_4 _let_12)))) (xor (= _let_0 v5) (distinct (ite (= v3 v2) v2 v3) _let_12))) (xor (and (distinct _let_22 (ite (= v0 v1) v8 v5)) (= (ite (= v3 v2) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) _let_6) v0)) (xor (not (or (= _let_10 v3) (= (distinct (ite _let_3 v0 v0) v0) _let_23))) (distinct (ite _let_3 v0 v0) (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))))))) (=> (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))) (not (and (distinct _let_6 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))) (or (distinct (ite _let_1 v6 (ite (= _let_0 _let_0) v4 v4)) (ite (distinct v2 v2) v6 v7)) (= v3 _let_11)))))) (= (or (=> (=> (or (= v2 _let_16) (distinct (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_6)) (= (ite (= v0 v1) v8 v5) v4)) (and (distinct v0 (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (=> (distinct _let_7 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct _let_15 _let_13)))) (and (= (distinct v2 v2) (distinct (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4) _let_4)) (distinct _let_17 (ite _let_1 (ite (= v3 v2) v2 v3) (ite (= v3 v2) v2 v3))))) (ite _let_23 (and (and (or (= _let_12 _let_9) (not (= _let_9 _let_11))) (distinct v1 (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0))) (= (=> (= (= (distinct _let_20 v7) (distinct _let_14 _let_13)) (or (distinct _let_15 _let_10) (= (distinct _let_6 (ite (= v0 v1) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) _let_4)) (distinct (ite (= v8 v6) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0) (ite _let_2 (ite _let_2 (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0))) v0)) (ite _let_3 (ite _let_3 v0 v0) (ite _let_3 v0 v0)))))) (not (= v8 v6))) (= (xor (distinct v4 (ite (= _let_0 v5) v5 v6)) (distinct _let_0 v7)) (= (ite (= v0 v1) v8 v5) _let_20)))) (= v7 _let_18)))))))))) (xor (and _let_24 _let_24) (= (ite (xor (=> _let_26 _let_26) (= _let_12 v3)) _let_27 _let_27) (= _let_25 _let_25))))))))))))))))))))))))))))))) ))
|
