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