(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFLIA)
(declare-fun f0 (Int) Int)
(declare-fun f1 ((Array Int Int) (Array Int Int)) (Array Int Int))
(declare-fun p0 (Int) Bool)
(declare-fun p1 ((Array Int Int) (Array Int Int) (Array Int Int)) Bool)
(declare-fun v0 () Int)
(declare-fun v1 () (Array Int Int))
(check-sat-assuming ( (let ((_let_0 (ite (p0 v0) 1 0))) (let ((_let_1 (ite (p0 _let_0) 1 0))) (let ((_let_2 (f0 _let_0))) (let ((_let_3 (* _let_0 (- 0)))) (let ((_let_4 (store v1 (- _let_0) _let_3))) (let ((_let_5 (select _let_4 _let_0))) (let ((_let_6 (store _let_4 _let_3 _let_2))) (let ((_let_7 (select _let_6 _let_5))) (let ((_let_8 (f1 _let_4 (f1 _let_6 _let_6)))) (let ((_let_9 (p1 (f1 v1 (f1 _let_6 _let_6)) _let_6 _let_8))) (let ((_let_10 (p1 _let_4 _let_4 (f1 v1 (f1 _let_6 _let_6))))) (let ((_let_11 (p0 _let_2))) (let ((_let_12 (distinct _let_1 (- _let_0)))) (let ((_let_13 (<= _let_2 v0))) (let ((_let_14 (ite _let_13 _let_8 (f1 _let_6 _let_6)))) (let ((_let_15 (ite (= _let_2 _let_7) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))))) (let ((_let_16 (ite (>= _let_0 _let_3) _let_6 (ite (< _let_0 _let_2) _let_4 v1)))) (let ((_let_17 (ite (= _let_2 _let_7) (f1 v1 (f1 _let_6 _let_6)) _let_15))) (let ((_let_18 (ite _let_11 _let_16 _let_15))) (let ((_let_19 (ite (> _let_2 _let_7) _let_16 _let_4))) (let ((_let_20 (ite (>= _let_0 _let_3) (ite _let_12 (f1 _let_6 _let_6) (f1 _let_6 _let_6)) _let_16))) (let ((_let_21 (ite _let_10 (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))) (f1 _let_6 _let_6)))) (let ((_let_22 (ite _let_11 (- _let_0) _let_0))) (let ((_let_23 (ite _let_9 _let_7 _let_5))) (let ((_let_24 (ite _let_9 (ite (> _let_2 _let_7) _let_5 _let_1) _let_3))) (let ((_let_25 (ite _let_11 _let_22 _let_23))) (let ((_let_26 (ite _let_12 _let_5 (- _let_0)))) (let ((_let_27 (ite _let_10 (ite (= _let_2 _let_7) v0 _let_3) (ite (> _let_2 _let_7) _let_5 _let_1)))) (let ((_let_28 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_5 _let_0))) (let ((_let_29 (ite _let_13 _let_27 _let_7))) (let ((_let_30 (store (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)) (ite (> _let_2 _let_7) _let_5 _let_1) _let_3))) (let ((_let_31 (store (ite (> _let_2 _let_7) _let_14 _let_4) _let_25 _let_27))) (let ((_let_32 (select (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) v0))) (let ((_let_33 (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_16))) (let ((_let_34 (f1 _let_18 _let_19))) (let ((_let_35 (f1 _let_17 (f1 v1 (f1 _let_6 _let_6))))) (let ((_let_36 (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_19))) (let ((_let_37 (f1 v1 v1))) (let ((_let_38 (f1 (ite _let_12 (f1 _let_6 _let_6) (f1 _let_6 _let_6)) (ite _let_12 (f1 _let_6 _let_6) (f1 _let_6 _let_6))))) (let ((_let_39 (f1 (f1 _let_16 (f1 (ite (< _let_0 _let_2) _let_4 v1) (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))) _let_17))) (let ((_let_40 (ite (p0 _let_22) 1 0))) (let ((_let_41 (ite (p0 _let_28) 1 0))) (let ((_let_42 (* 0 _let_7))) (let ((_let_43 (- _let_27))) (let ((_let_44 (* 0 (ite (> _let_2 _let_7) _let_5 _let_1)))) (let ((_let_45 (ite (p0 (ite (<= v0 _let_0) _let_24 _let_24)) 1 0))) (let ((_let_46 (f0 _let_25))) (let ((_let_47 (* (- 0) (ite (> _let_2 _let_7) _let_0 v0)))) (let ((_let_48 (p1 (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20) (f1 (ite (< _let_0 _let_2) _let_4 v1) (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1))) _let_33))) (let ((_let_49 (and (p1 (f1 _let_6 _let_6) _let_8 v1) (<= (ite (<= v0 _let_0) _let_24 _let_24) _let_7)))) (let ((_let_50 (xor (and (or (xor (>= _let_1 (- _let_0 (ite (p0 _let_7) 1 0))) (p0 _let_41)) (=> (= (or (p1 _let_35 (ite _let_9 _let_19 _let_6) _let_8) (p1 (f1 (f1 (f1 _let_6 _let_6) _let_19) (f1 _let_6 _let_6)) _let_34 (f1 _let_30 _let_30))) _let_12) (ite (p1 (f1 _let_15 _let_15) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) (f1 _let_8 _let_8)) (not (= _let_2 _let_7)) (xor (p0 _let_5) (= (ite (p0 _let_5) 1 0) _let_0))))) (= _let_11 (ite (=> (p1 _let_30 (ite _let_11 (ite _let_9 _let_19 _let_6) (f1 _let_6 _let_6)) (f1 _let_6 (f1 v1 (f1 _let_6 _let_6)))) (p0 _let_25)) (or (<= (* 0 (ite (>= _let_0 _let_3) (ite (< _let_0 _let_2) _let_2 _let_1) _let_3)) (- _let_0 (ite (p0 _let_7) 1 0))) (p1 (ite _let_12 (f1 _let_6 _let_6) (f1 _let_6 _let_6)) _let_14 _let_18)) (not (< _let_0 _let_2))))) (ite (not (xor (> (ite (= _let_2 _let_7) v0 _let_3) _let_24) (<= v0 _let_0))) (and (= (=> (p1 _let_39 _let_39 (f1 _let_14 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))) (>= _let_28 (ite (p0 _let_7) 1 0))) (p1 (store _let_4 _let_32 (ite (> _let_2 _let_7) _let_0 v0)) _let_18 (f1 (ite (p0 _let_5) _let_14 v1) (ite (p0 _let_5) _let_14 v1)))) (p1 _let_21 (f1 _let_8 _let_8) _let_17)) (and (= (=> (p1 _let_39 _let_39 (f1 _let_14 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))) (>= _let_28 (ite (p0 _let_7) 1 0))) (p1 (store _let_4 _let_32 (ite (> _let_2 _let_7) _let_0 v0)) _let_18 (f1 (ite (p0 _let_5) _let_14 v1) (ite (p0 _let_5) _let_14 v1)))) (p1 _let_21 (f1 _let_8 _let_8) _let_17)))))) (let ((_let_51 (=> (=> (not (ite (not (p1 (f1 (ite (p0 _let_5) _let_14 v1) (ite (p0 _let_5) _let_14 v1)) _let_33 (f1 _let_30 _let_30))) (or (and (or (< (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0) (* 0 (ite (>= _let_0 _let_3) (ite (< _let_0 _let_2) _let_2 _let_1) _let_3))) _let_13) (and (or (or (p1 (ite (p0 _let_5) _let_14 v1) _let_38 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) (p1 _let_6 (store _let_4 _let_32 (ite (> _let_2 _let_7) _let_0 v0)) (ite (< _let_0 _let_2) _let_4 v1))) (>= _let_32 _let_29)) (>= _let_0 _let_3))) (not (> _let_45 _let_46))) (=> (= (not (p1 v1 _let_31 _let_21)) (p1 _let_34 _let_21 _let_36)) (= (ite (not (or (or (>= (ite (> _let_2 _let_7) _let_5 _let_1) (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0)) (distinct (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0) _let_23)) (p1 (f1 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6)) (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) _let_36 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1))))) (or (ite (= _let_42 _let_22) (p1 _let_19 _let_39 (f1 _let_17 _let_31)) (<= (f0 _let_41) _let_28)) (p1 (ite (< _let_0 _let_2) _let_4 v1) _let_36 (f1 _let_6 (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))))) (not (or (or (>= (ite (> _let_2 _let_7) _let_5 _let_1) (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0)) (distinct (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0) _let_23)) (p1 (f1 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6)) (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) _let_36 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))))) (and (ite (p0 (select _let_30 _let_26)) (p1 (f1 (f1 _let_6 _let_6) _let_19) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) (f1 v1 (f1 _let_6 _let_6))) (p1 (f1 _let_21 (ite (< _let_0 _let_2) _let_4 v1)) _let_36 (f1 _let_37 _let_31))) (=> (p1 (ite (< _let_0 _let_2) _let_4 v1) _let_37 (f1 _let_6 _let_6)) (p1 (f1 _let_6 (f1 v1 (f1 _let_6 _let_6))) (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20) (f1 _let_6 _let_6)))))))) (not (ite (not (p1 (f1 (ite (p0 _let_5) _let_14 v1) (ite (p0 _let_5) _let_14 v1)) _let_33 (f1 _let_30 _let_30))) (or (and (or (< (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0) (* 0 (ite (>= _let_0 _let_3) (ite (< _let_0 _let_2) _let_2 _let_1) _let_3))) _let_13) (and (or (or (p1 (ite (p0 _let_5) _let_14 v1) _let_38 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) (p1 _let_6 (store _let_4 _let_32 (ite (> _let_2 _let_7) _let_0 v0)) (ite (< _let_0 _let_2) _let_4 v1))) (>= _let_32 _let_29)) (>= _let_0 _let_3))) (not (> _let_45 _let_46))) (=> (= (not (p1 v1 _let_31 _let_21)) (p1 _let_34 _let_21 _let_36)) (= (ite (not (or (or (>= (ite (> _let_2 _let_7) _let_5 _let_1) (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0)) (distinct (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0) _let_23)) (p1 (f1 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6)) (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) _let_36 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1))))) (or (ite (= _let_42 _let_22) (p1 _let_19 _let_39 (f1 _let_17 _let_31)) (<= (f0 _let_41) _let_28)) (p1 (ite (< _let_0 _let_2) _let_4 v1) _let_36 (f1 _let_6 (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))))) (not (or (or (>= (ite (> _let_2 _let_7) _let_5 _let_1) (ite (p0 (- _let_0 (ite (p0 _let_7) 1 0))) 1 0)) (distinct (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0) _let_23)) (p1 (f1 (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6)) (ite (p1 (f1 _let_6 _let_6) _let_8 v1) _let_6 (f1 _let_6 _let_6))) _let_36 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))))) (and (ite (p0 (select _let_30 _let_26)) (p1 (f1 (f1 _let_6 _let_6) _let_19) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) (f1 v1 (f1 _let_6 _let_6))) (p1 (f1 _let_21 (ite (< _let_0 _let_2) _let_4 v1)) _let_36 (f1 _let_37 _let_31))) (=> (p1 (ite (< _let_0 _let_2) _let_4 v1) _let_37 (f1 _let_6 _let_6)) (p1 (f1 _let_6 (f1 v1 (f1 _let_6 _let_6))) (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20) (f1 _let_6 _let_6))))))))) (not (xor (ite (p1 _let_19 _let_38 _let_39) (>= _let_3 (- _let_0 (ite (= _let_2 _let_7) v0 _let_3))) (p1 _let_37 (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4)) _let_33)) (ite (and (= (ite (=> (p0 _let_32) (p1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))) _let_17)) _let_11 (<= _let_45 (- _let_0))) (p1 (f1 _let_4 _let_18) (ite (<= v0 _let_0) _let_8 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))))) (f1 _let_4 _let_18))) (= (ite (p0 _let_45) 1 0) _let_0)) (=> (ite (xor (< (* (- 0) (ite (> _let_2 _let_7) _let_5 _let_0)) _let_43) (p1 _let_20 (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4)) (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20))) (xor (< (* (- 0) (ite (> _let_2 _let_7) _let_5 _let_0)) _let_43) (p1 _let_20 (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4)) (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20))) (and (= _let_9 (< (* (- 0) _let_32) _let_23)) (ite (< (* _let_24 (- 0)) _let_0) (>= (- _let_29 _let_40) (* _let_5 0)) (= (= _let_46 _let_41) (> _let_2 _let_7))))) (> _let_40 _let_2)) (and (xor (not (p0 (f0 (+ v0 _let_5)))) (= _let_28 _let_43)) (and (not (p1 (f1 (ite (<= v0 _let_0) _let_8 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))))) (ite (<= v0 _let_0) _let_8 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))))) _let_39 (f1 (ite _let_11 (ite _let_9 _let_19 _let_6) (f1 _let_6 _let_6)) _let_34))) (> (- _let_26 (- _let_0)) _let_42))))))))) (= (ite _let_49 (ite (ite (=> (not (not (= _let_10 (p1 _let_31 (f1 (ite (<= v0 _let_0) _let_8 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))))) (ite (<= v0 _let_0) _let_8 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))))) _let_21)))) (or (not (and (= (ite (p0 _let_7) 1 0) (ite (> _let_2 _let_7) _let_0 v0)) (< (ite _let_11 1 0) (* (- 0) _let_32)))) (and (and (p1 (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)) v1 _let_16) (distinct (+ _let_23 _let_27) (+ v0 _let_5))) (distinct (- _let_0) _let_23)))) _let_50 _let_50) (=> (xor (<= v0 (ite (> _let_2 _let_7) _let_5 _let_0)) (ite (not (not (distinct (- (ite (< _let_0 _let_2) _let_2 _let_1)) (* _let_24 (- 0))))) (ite (xor (and (> (select _let_30 _let_26) _let_44) (>= _let_41 _let_25)) (> (* (select _let_30 _let_26) (- 0)) _let_47)) (p0 (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0)) (< _let_1 (ite (p0 (ite (p0 _let_5) _let_2 _let_25)) 1 0))) (or _let_48 _let_48))) (ite (xor (or (xor (= (p1 (ite _let_9 _let_19 _let_6) (f1 (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) _let_20) _let_38) (= (ite (= _let_2 _let_7) v0 _let_3) (ite (p0 _let_5) _let_2 _let_25))) (p1 (f1 _let_16 (f1 (ite (< _let_0 _let_2) _let_4 v1) (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))) (f1 _let_16 (f1 (ite (< _let_0 _let_2) _let_4 v1) (ite _let_10 _let_6 (ite (p0 _let_5) _let_14 v1)))) _let_18)) (=> (= (<= (- (- _let_0 (ite (p0 _let_7) 1 0))) _let_47) (p0 _let_26)) (ite (= (distinct _let_44 _let_25) (p1 (ite _let_11 (ite _let_9 _let_19 _let_6) (f1 _let_6 _let_6)) _let_36 _let_37)) (and (p1 _let_8 (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4)) (f1 v1 (f1 _let_6 _let_6))) (p1 (f1 (ite _let_9 _let_19 _let_6) (ite _let_9 _let_19 _let_6)) _let_4 _let_15)) (or (p1 (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4)) (f1 _let_37 _let_31) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))))) (p1 _let_33 (f1 (store _let_4 _let_32 (ite (> _let_2 _let_7) _let_0 v0)) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6))))) (ite _let_11 (ite _let_9 _let_19 _let_6) (f1 _let_6 _let_6))))))) (p1 _let_14 (f1 _let_4 _let_18) _let_35)) (=> (ite (< _let_5 (ite (< _let_0 _let_2) _let_2 _let_1)) (and (p1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (>= _let_0 _let_3) (f1 v1 (f1 _let_6 _let_6)) (ite (p0 _let_5) (f1 v1 (f1 _let_6 _let_6)) (f1 v1 (f1 _let_6 _let_6)))) (f1 (ite (> _let_2 _let_7) _let_14 _let_4) (ite (> _let_2 _let_7) _let_14 _let_4))) (distinct (* 0 _let_41) _let_27)) (distinct (- (f0 _let_41) _let_1) _let_41)) (p0 (ite (p0 _let_7) 1 0))) (distinct _let_0 _let_0))) (and (=> (ite (and (> (* _let_5 0) _let_5) (distinct (- _let_3) (ite (<= v0 _let_0) _let_24 _let_24))) (xor (p0 (- _let_0 (ite (= _let_2 _let_7) v0 _let_3))) (<= (ite (>= _let_0 _let_3) (ite (< _let_0 _let_2) _let_2 _let_1) _let_3) (* 0 _let_0))) (not (distinct _let_27 _let_41))) (not (> _let_32 _let_22))) (p1 (ite (> _let_2 _let_7) _let_14 _let_4) _let_17 (f1 v1 (f1 _let_6 _let_6))))) _let_49) (xor _let_51 _let_51)))))))))))))))))))))))))))))))))))))))))))))))))))))) ))