(set-option :incremental false)
(set-info :status sat)
(set-logic QF_LIA)
(declare-fun v0 () Int)
(check-sat-assuming ( (let ((_let_0 (+ (- v0 v0) v0))) (let ((_let_1 (- (- (- v0 v0)) (- (- (- (- v0 v0))))))) (let ((_let_2 (- (- (- (- (- v0 v0))))))) (let ((_let_3 (+ (+ (- (- v0 v0)) v0) (- (- v0 v0))))) (let ((_let_4 (- _let_2))) (let ((_let_5 (+ (- (- v0 v0)) _let_1))) (let ((_let_6 (- (+ (- (- v0 v0)) v0) _let_2))) (let ((_let_7 (* _let_2 (- 5)))) (let ((_let_8 (+ _let_2 _let_6))) (let ((_let_9 (- _let_7))) (let ((_let_10 (+ _let_6 _let_0))) (let ((_let_11 (* (- (- (- v0 v0))) (- 5)))) (let ((_let_12 (* _let_0 (- 5)))) (let ((_let_13 (>= _let_8 _let_0))) (let ((_let_14 (< _let_0 _let_8))) (let ((_let_15 (distinct _let_2 _let_2))) (let ((_let_16 (< (+ (- (- v0 v0)) v0) (- (- (- (- v0 v0))))))) (let ((_let_17 (< _let_5 _let_4))) (let ((_let_18 (> (+ (- (- v0 v0)) v0) _let_3))) (let ((_let_19 (distinct _let_3 _let_10))) (let ((_let_20 (< _let_6 _let_10))) (let ((_let_21 (<= _let_8 (- (- (- v0 v0)))))) (let ((_let_22 (= _let_6 _let_2))) (let ((_let_23 (distinct (- (- (- v0 v0))) (+ (- (- v0 v0)) v0)))) (let ((_let_24 (< _let_3 _let_9))) (let ((_let_25 (ite _let_16 (- (- (- (- v0 v0)))) _let_4))) (let ((_let_26 (ite (distinct (- v0 v0) v0) (- (- (- v0 v0))) _let_11))) (let ((_let_27 (ite _let_17 _let_12 _let_7))) (let ((_let_28 (ite (<= (+ (- (- v0 v0)) v0) _let_3) _let_2 _let_12))) (let ((_let_29 (ite (> _let_5 _let_9) _let_8 _let_25))) (let ((_let_30 (ite (> _let_6 _let_12) v0 _let_25))) (let ((_let_31 (ite _let_17 _let_9 _let_26))) (let ((_let_32 (ite (< _let_11 _let_10) _let_6 _let_30))) (let ((_let_33 (ite _let_23 _let_3 _let_26))) (let ((_let_34 (ite _let_21 _let_0 _let_0))) (let ((_let_35 (ite (< _let_11 _let_10) _let_7 (+ (- (- v0 v0)) v0)))) (let ((_let_36 (ite (< _let_1 _let_4) (- (- v0 v0)) (- (- (- v0 v0)))))) (let ((_let_37 (ite _let_19 _let_12 _let_5))) (let ((_let_38 (ite _let_18 (ite _let_22 _let_1 (- (- v0 v0))) (- (- v0 v0))))) (let ((_let_39 (ite _let_24 _let_38 _let_32))) (let ((_let_40 (ite _let_16 (- v0 v0) _let_29))) (let ((_let_41 (ite _let_18 (- (- v0 v0)) (- (- (- v0 v0)))))) (let ((_let_42 (ite (> _let_6 _let_12) _let_8 _let_30))) (let ((_let_43 (ite _let_18 _let_2 (- v0 v0)))) (let ((_let_44 (ite (<= (+ (- (- v0 v0)) v0) _let_3) (- (- (- (- v0 v0)))) _let_10))) (let ((_let_45 (ite (< _let_2 _let_0) _let_27 _let_43))) (let ((_let_46 (ite _let_20 _let_39 _let_37))) (let ((_let_47 (ite (= _let_10 (- (- (- v0 v0)))) _let_1 _let_8))) (let ((_let_48 (ite _let_14 _let_45 (ite _let_13 _let_10 _let_7)))) (let ((_let_49 (ite _let_19 (- v0 v0) _let_11))) (let ((_let_50 (ite (< v0 _let_3) _let_32 _let_47))) (let ((_let_51 (ite _let_15 _let_2 _let_32))) (let ((_let_52 (ite (> _let_7 _let_5) _let_36 _let_7))) (let ((_let_53 (ite (<= (- (- v0 v0)) _let_1) _let_28 _let_26))) (let ((_let_54 (ite (> _let_6 _let_12) _let_40 _let_35))) (let ((_let_55 (ite (>= _let_0 _let_8) _let_27 _let_33))) (let ((_let_56 (ite (< v0 _let_3) _let_50 (ite (distinct _let_4 (- (- (- (- v0 v0))))) _let_10 _let_39)))) (let ((_let_57 (ite (distinct (+ (- (- v0 v0)) v0) _let_4) _let_36 _let_43))) (let ((_let_58 (ite _let_13 _let_54 _let_33))) (let ((_let_59 (ite (<= (- (- (- v0 v0))) _let_10) _let_42 (- (- (- (- v0 v0))))))) (let ((_let_60 (= _let_43 _let_53))) (let ((_let_61 (>= _let_47 (- (- (- v0 v0)))))) (let ((_let_62 (or (not (and (and (not (ite (ite _let_61 (= (or (xor (> (- (- (- (- v0 v0)))) (- (- (- (- v0 v0))))) (<= (- (- (- v0 v0))) _let_10)) (not (ite (<= _let_39 _let_46) (<= _let_36 _let_48) (= _let_11 _let_25)))) (= (not (< _let_32 _let_48)) (distinct _let_52 _let_52))) (xor (and (>= _let_0 _let_8) (<= _let_2 _let_12)) (and _let_60 (> (- v0 v0) _let_57)))) (<= _let_25 _let_50) (=> (and (< (- (- v0 v0)) _let_46) (and (= _let_58 _let_5) (> _let_7 _let_28))) (and (< (- (- v0 v0)) _let_46) (and (= _let_58 _let_5) (> _let_7 _let_28)))))) (and (and (and (ite (>= _let_46 _let_32) (= (<= _let_48 _let_48) (>= _let_36 _let_29)) (= (distinct (- (- (- v0 v0))) _let_48) (= _let_59 _let_7))) (and (ite (distinct _let_10 (- (- v0 v0))) (< v0 _let_3) (< _let_36 _let_51)) (not (or (= _let_4 _let_36) (< _let_45 _let_11))))) (not (= _let_25 _let_45))) (ite (= (< _let_7 (ite (distinct _let_4 (- (- (- (- v0 v0))))) _let_10 _let_39)) (> _let_43 v0)) (ite (and (< (- (- (- (- v0 v0)))) _let_7) (distinct (- v0 v0) _let_6)) (= (>= v0 _let_41) (< _let_4 _let_45)) (and (< (- (- (- (- v0 v0)))) _let_7) (distinct (- v0 v0) _let_6))) (and _let_17 (or (<= _let_31 _let_42) (distinct _let_55 _let_12)))))) (and (not (ite (ite _let_61 (= (or (xor (> (- (- (- (- v0 v0)))) (- (- (- (- v0 v0))))) (<= (- (- (- v0 v0))) _let_10)) (not (ite (<= _let_39 _let_46) (<= _let_36 _let_48) (= _let_11 _let_25)))) (= (not (< _let_32 _let_48)) (distinct _let_52 _let_52))) (xor (and (>= _let_0 _let_8) (<= _let_2 _let_12)) (and _let_60 (> (- v0 v0) _let_57)))) (<= _let_25 _let_50) (=> (and (< (- (- v0 v0)) _let_46) (and (= _let_58 _let_5) (> _let_7 _let_28))) (and (< (- (- v0 v0)) _let_46) (and (= _let_58 _let_5) (> _let_7 _let_28)))))) (and (and (and (ite (>= _let_46 _let_32) (= (<= _let_48 _let_48) (>= _let_36 _let_29)) (= (distinct (- (- (- v0 v0))) _let_48) (= _let_59 _let_7))) (and (ite (distinct _let_10 (- (- v0 v0))) (< v0 _let_3) (< _let_36 _let_51)) (not (or (= _let_4 _let_36) (< _let_45 _let_11))))) (not (= _let_25 _let_45))) (ite (= (< _let_7 (ite (distinct _let_4 (- (- (- (- v0 v0))))) _let_10 _let_39)) (> _let_43 v0)) (ite (and (< (- (- (- (- v0 v0)))) _let_7) (distinct (- v0 v0) _let_6)) (= (>= v0 _let_41) (< _let_4 _let_45)) (and (< (- (- (- (- v0 v0)))) _let_7) (distinct (- v0 v0) _let_6))) (and _let_17 (or (<= _let_31 _let_42) (distinct _let_55 _let_12)))))))) (xor (ite (xor (=> (not (distinct (+ (- (- v0 v0)) v0) _let_4)) (or (>= _let_10 (ite _let_13 _let_10 _let_7)) (>= (ite _let_22 _let_1 (- (- v0 v0))) _let_25))) (distinct _let_25 (- (- v0 v0)))) (not (xor (or (= (ite (= _let_29 (- v0 v0)) (>= (ite _let_13 _let_10 _let_7) _let_38) (distinct _let_4 _let_50)) (>= _let_32 _let_11)) (xor (>= _let_49 _let_49) (xor (>= _let_55 _let_34) (> _let_5 _let_9)))) (= (> _let_12 _let_50) (> _let_53 _let_41)))) (xor (=> (not (distinct (+ (- (- v0 v0)) v0) _let_4)) (or (>= _let_10 (ite _let_13 _let_10 _let_7)) (>= (ite _let_22 _let_1 (- (- v0 v0))) _let_25))) (distinct _let_25 (- (- v0 v0))))) (not (ite (ite (< _let_50 _let_58) (distinct _let_7 _let_30) (< _let_50 _let_36)) (distinct _let_5 (- (- v0 v0))) (not (>= _let_43 _let_26)))))))) (and (or (or (ite _let_62 _let_62 (> (- (- (- (- v0 v0)))) _let_32)) (= (or (and (< _let_43 _let_54) (> _let_54 _let_4)) (xor (= (and _let_20 (>= _let_51 _let_57)) (=> (>= _let_32 _let_7) (ite (> _let_3 _let_53) (= _let_41 _let_57) (<= _let_5 _let_54)))) (xor (> _let_9 _let_34) (not (not (= (>= _let_54 _let_38) (=> (> _let_7 _let_5) (>= _let_11 _let_25)))))))) (not (= (and (= (=> (or (xor (and (<= _let_6 _let_55) _let_13) (< _let_29 (- (- (- v0 v0))))) (distinct _let_38 _let_28)) (=> (or (distinct _let_12 _let_52) (>= _let_39 _let_38)) (<= _let_34 _let_30))) (and (not (> _let_7 _let_8)) (and (>= _let_56 _let_28) (< _let_42 _let_0)))) (distinct _let_11 _let_38)) (ite _let_16 (>= _let_8 _let_9) (xor (distinct _let_8 _let_12) (distinct _let_12 _let_27))))))) (xor (and (xor (< _let_43 (- v0 v0)) (= (not (not _let_60)) (< _let_41 _let_41))) (ite (>= (ite _let_13 _let_10 _let_7) (- (- (- v0 v0)))) (and (< _let_58 _let_2) (>= _let_11 _let_1)) (ite (ite (= (< _let_2 _let_25) (distinct _let_28 _let_57)) (= (or (> _let_33 _let_38) (< v0 _let_58)) (= (and (<= _let_48 (+ (- (- v0 v0)) v0)) _let_15) (<= _let_34 _let_47))) (distinct _let_59 _let_57)) (= (and (and (= _let_8 _let_33) (>= _let_9 v0)) (>= _let_59 _let_39)) (> _let_9 _let_11)) (or (<= _let_31 _let_26) (> _let_7 (- (- (- v0 v0)))))))) (not (xor (not (ite (< _let_12 _let_41) (or (<= _let_8 _let_45) (ite (< _let_2 _let_0) (< _let_38 _let_4) (=> (distinct _let_3 _let_54) (or (> _let_2 _let_39) (> (- (- (- v0 v0))) (- (- (- v0 v0)))))))) (<= (+ (- (- v0 v0)) v0) _let_3))) (=> (ite (= (= (>= _let_52 _let_55) (<= _let_27 _let_58)) (>= (- (- (- (- v0 v0)))) v0)) (xor (ite (= (= _let_39 _let_31) (< _let_26 _let_1)) (> _let_2 _let_54) (or (distinct _let_38 _let_11) (=> (distinct _let_4 (- (- (- (- v0 v0))))) (= _let_10 (- (- (- v0 v0))))))) (not (=> (<= v0 _let_0) (not (> _let_36 _let_0))))) (= _let_11 _let_44)) (not (not (< _let_11 _let_10)))))))) (and (and (not (= (>= _let_1 _let_42) (or (>= _let_10 _let_51) (not (and (or (distinct _let_5 _let_34) (< _let_29 _let_55)) (ite (< _let_8 _let_4) (not (>= _let_48 _let_28)) (or (> (ite _let_22 _let_1 (- (- v0 v0))) (+ (- (- v0 v0)) v0)) (< _let_25 _let_26)))))))) (or (=> (or _let_61 (=> (<= _let_3 _let_25) (> _let_6 _let_12))) (ite (and (xor (xor (> _let_8 _let_43) (= _let_27 _let_27)) (< _let_11 (- v0 v0))) (> _let_38 _let_54)) (>= (- (- v0 v0)) v0) (or (<= (+ (- (- v0 v0)) v0) _let_28) (or (= (- (- (- v0 v0))) _let_1) (and (< _let_9 _let_11) (distinct _let_29 _let_36)))))) (ite (or (=> (>= _let_32 _let_6) (>= (- v0 v0) _let_28)) (ite (= (distinct _let_35 _let_56) (< _let_11 (+ (- (- v0 v0)) v0))) (not (< _let_7 _let_53)) (or (<= _let_35 _let_56) (<= (- (- v0 v0)) _let_1)))) (= (not (= _let_53 _let_50)) (or (>= _let_56 _let_52) (distinct _let_50 _let_58))) (or (distinct (- v0 v0) v0) (=> (not (< _let_1 _let_4)) (= (ite (distinct _let_54 _let_6) (= (< (+ (- (- v0 v0)) v0) _let_29) (distinct _let_38 _let_27)) (<= _let_44 _let_42)) (not (not (< (- (- (- v0 v0))) _let_3))))))))) (or (= _let_8 _let_7) (=> (ite (xor (< _let_35 _let_50) (<= _let_25 _let_6)) (> (+ (- (- v0 v0)) v0) _let_28) (or (=> (<= _let_31 _let_9) (< _let_41 _let_4)) (> _let_49 _let_10))) (and (= (ite (= (ite _let_21 (ite (and (> _let_46 _let_41) (< _let_37 _let_10)) (<= _let_50 (- (- (- v0 v0)))) (and _let_23 _let_24)) (< _let_30 _let_53)) _let_18) (not (not (or (<= _let_45 _let_5) (<= _let_47 _let_52)))) (and (and (>= _let_4 _let_12) (>= _let_36 _let_40)) (>= (- (- v0 v0)) _let_47))) (xor _let_14 (xor (<= _let_11 v0) _let_19))) _let_22)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))